<p>Actually I have deleted an answer to what I claimed in the comments and would like to provide a counterexample in Curry-style STLC, this is 5.12 in
<a href="https://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf" rel="nofollow noreferrer">https://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf</a>, which I reproduce here.
There are <span class="math-container">$M$</span>, <span class="math-container">$M'$</span> ∈ Λ and <span class="math-container">$σ$</span>, <span class="math-container">$σ'$</span> ∈ T such that <span class="math-container">$M' \twoheadrightarrow_{\beta} M$</span> and
<span class="math-container">$\vdash M : σ$</span>, <span class="math-container">$\vdash M' : σ'$</span>, but <span class="math-container">$\nvdash M' : σ$</span>.
Take <span class="math-container">$M \equiv \lambda xy.y$</span>, <span class="math-container">$M' \equiv SK$</span>. Take <span class="math-container">$\sigma \equiv \alpha \rightarrow (\beta \rightarrow \beta)$</span> and <span class="math-container">$\sigma' \equiv (\beta \rightarrow \alpha) \rightarrow (\beta \rightarrow \beta)$</span>.</p>
<p>Take these M' and M, given that <span class="math-container">$M' \twoheadrightarrow_{\beta} M$</span>, <span class="math-container">$M' \equiv_{\beta} M$</span>,, but by the above <span class="math-container">$M$</span> has a typing <span class="math-container">$\sigma$</span>, but <span class="math-container">$M'$</span> does not. To see why <span class="math-container">$M$</span> having a typing <span class="math-container">$\sigma$</span> is trivial.
For M' and M being equivalent see as follows,
M' =  SK <br/>
= (λxyz.xz(yz))(λxy.x) <br/>
= λyz.(λxy.x)z(yz) <br/>
= λyz.(λy.z)(yz) <br/>
= λyz. z
which is we can alpha rename to <span class="math-container">$M$</span>.
For <span class="math-container">$M'$</span> not having typing <span class="math-container">$\sigma$</span> see as follows, to type SK we need to know that the second argument of S is a function.</p>
<p>Thus we have 2 <span class="math-container">$\beta$</span>-equivalent terms, only one of which is typeable at <span class="math-container">$\sigma$</span>, but both are simply typeable.</p>

CC BY-SA 4.0
2023-02-22T09:35:05.053Z
2023-02-22T09:35:05.053Z
Ilk
<p>The answer depends on what you mean by &quot;simply-typed <span class="math-container">$\lambda$</span>-calculus&quot;.  There are two possibilities:</p>
<ul>
<li><p><strong>Church-style:</strong> in this formulation, terms explicitly carry their type and reduction/expansion preserve it by definition, that is, if <span class="math-container">$t\to u$</span>, then <span class="math-container">$t$</span> and <span class="math-container">$u$</span> necessarily have the same type.  Then the result you are mentioning is, as you say, a consequence of confluence: by confluence, <span class="math-container">$t$</span> is <span class="math-container">$\beta$</span>-equivalent to <span class="math-container">$u$</span> iff there exists <span class="math-container">$v$</span> such that <span class="math-container">$t\to^\ast v$</span> and <span class="math-container">$u\to^\ast v$</span>. By definition, <span class="math-container">$t$</span> has the same type as <span class="math-container">$v$</span>, which has the same type as <span class="math-container">$u$</span>. (In fact, you don't even need confluence: by definition, <span class="math-container">$t$</span> and <span class="math-container">$u$</span> are <span class="math-container">$\beta$</span>-equivalent if there is a finite chain of reductions and &quot;anti-reductions&quot; relating <span class="math-container">$t$</span> and <span class="math-container">$u$</span>, so their types must be the same because in the Church-style system reductions only relate terms with the same type).</p>
</li>
<li><p><strong>Curry-style:</strong> if you see simple types as a <em>type system</em> for the <span class="math-container">$\lambda$</span>-calculus, then the result you mention is false, because such a type system does not enjoy <em>subject expansion</em>.  For example, let <span class="math-container">$t:=(\lambda x.xx)I$</span> and <span class="math-container">$u:=II$</span>, where <span class="math-container">$I$</span> is the identity.  Then <span class="math-container">$t\to u$</span>, so <span class="math-container">$t$</span> and <span class="math-container">$u$</span> are <span class="math-container">$\beta$</span>-equivalent, and yet <span class="math-container">$u$</span> is simply-typable and <span class="math-container">$t$</span> is not.  As proved in Nift's answer below, there are even examples of this phenomenon in which <span class="math-container">$t$</span> too is typable (but has strictly less types than <span class="math-container">$u$</span>).</p>
</li>
</ul>

CC BY-SA 4.0
2023-02-22T15:56:40.060Z
When you claim that "if $t \to u$, then $t$ and $u$ necessarily have the same type", you do not only rely on subject reduction but also on subject expansion. Does subject expansion really hold for Church-style simply-typed lambda calculus? It is not obvious to me.
Bob
CC BY-SA 4.0
2023-02-23T06:20:10.793Z
Subject reduction and subject expansion only make sense for Curry-style type systems.  In the Church-style presentation, the types are written in the terms, you have no choice.  I have the feeling that maybe you are not familiar with the Church-style presentation?
Damiano Mazza
CC BY-SA 4.0
2023-02-23T11:18:23.067Z
Take the reduction $(\lambda x^\sigma . M) N \to M[N/x]$. if $(\lambda x^\sigma . M) N$ has type $\tau$, then obviously $M[N/x]$ too. But, in the other direction, if $M[N/x]$ has type $\tau$, it is not obvious that $(\lambda x^\sigma . M) N$ too has type $\tau$ because the $\sigma$ that occurs is arbitrary (it is not written in $M[N/x]$ as you say).
Bob
CC BY-SA 4.0
2023-02-23T11:40:06.160Z
It *is* written in $M[N/x]$: it is the type of $N$, which appears as subterm of $M[N/x]$, unless $x$ does not appear free in $M$, which is a trivial case.
Damiano Mazza
CC BY-SA 4.0
2023-02-23T11:45:56.490Z
Anyway, the point is that in the Church-style formulation you can't choose the type of terms. Terms come with a unique type which may be unambiguously inferred from the type annotations.  It so happens that, in a $\beta$-reduction $M\to N$, the type of $M$ and the type of $N$ are the same.  I say *the* type because you have no choice, you can't attribute a type to $M$ (or to $N$) and then check whether it is preserved by reduction (or expansion), it doesn't make sense.
Damiano Mazza
CC BY-SA 4.0
2023-02-23T11:51:28.883Z
I wrongly believed that Church-style meant type annotations on lambda abstractions only.
Bob
CC BY-SA 4.0
2023-02-23T12:44:25.450Z
Well, for a closed therm, Church style *is* type annotations on $\lambda$-abstractions only.
Damiano Mazza
CC BY-SA 4.0
2023-02-23T12:47:08.843Z
For general terms, Church style means type annotations on $\lambda$-abstractions *and* on free variables.  That's enough to recover the type of every subterm (in particular the term itself).
Damiano Mazza
CC BY-SA 4.0
2023-02-21T09:16:40.827Z
2023-02-23T10:48:37.977Z
2023-02-23T10:48:37.977Z
Damiano Mazza
<p>In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type?</p>
<p>My guess is that I should use the subject reduction, and maybe the confluence...</p>

CC BY-SA 4.0
2023-02-21T09:23:25.350Z
This is a suggestion in light of Damiano Mazza's answer. Perhaps a less ambiguous question might be: In curry-style stlc (which is what I think you meant originally), when 2 typeable terms are beta equivalent do they have the same type? The answer is yes by normalization and principality of typing in stlc.
Ilk
CC BY-SA 4.0
2023-02-21T09:36:07.937Z
For claim of principality, see http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:slightly-longer.pdf Theorem 1, and maybe try following the trail of references for a proof.
Ilk
CC BY-SA 4.0
2023-02-21T12:08:21.737Z
@Nift I think you should write these comments as an answer.
Damiano Mazza
CC BY-SA 4.0
2023-02-21T12:59:10.997Z
@Nift You say that the answer is yes for Curry-style simply-typed λ-calculus but Damiano Mazza wrote in his answer that it is no.
Bob
<type-theory><pl.programming-languages><lambda-calculus><typed-lambda-calculus><normalization>
Lambda-calculus: Beta-equivalent terms have the same type
Bob
# Lambda-calculus: Beta-equivalent terms have the same type

(Asked by: username_0 on 2023-02-20)

In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type?

My guess is that I should use the subject reduction, and maybe the confluence...

**Tags:** type-theory, pl.programming-languages, lambda-calculus, typed-lambda-calculus, normalization
> **Comments:**
> **username_1**: This is a suggestion in light of Damiano Mazza's answer. Perhaps a less ambiguous question might be: In curry-style stlc (which is what I think you meant originally), when 2 typeable terms are beta equivalent do they have the same type? The answer is yes by normalization and principality of typing in stlc.  
> **username_1**: For claim of principality, see http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:slightly-longer.pdf Theorem 1, and maybe try following the trail of references for a proof.  
> **username_2**: @Nift I think you should write these comments as an answer.  
> **username_0**: @Nift You say that the answer is yes for Curry-style simply-typed λ-calculus but Damiano Mazza wrote in his answer that it is no.  

---

## 2 answers

### Answer by username_2 on 2023-02-21. Score: 7 | Accepted answer

The answer depends on what you mean by "simply-typed $\lambda$-calculus". There are two possibilities:

* **Church-style:** in this formulation, terms explicitly carry their type and reduction/expansion preserve it by definition, that is, if $t\to u$, then $t$ and $u$ necessarily have the same type. Then the result you are mentioning is, as you say, a consequence of confluence: by confluence, $t$ is $\beta$-equivalent to $u$ iff there exists $v$ such that $t\to^\ast v$ and $u\to^\ast v$. By definition, $t$ has the same type as $v$, which has the same type as $u$. (In fact, you don't even need confluence: by definition, $t$ and $u$ are $\beta$-equivalent if there is a finite chain of reductions and "anti-reductions" relating $t$ and $u$, so their types must be the same because in the Church-style system reductions only relate terms with the same type).
* **Curry-style:** if you see simple types as a *type system* for the $\lambda$-calculus, then the result you mention is false, because such a type system does not enjoy *subject expansion*. For example, let $t:=(\lambda x.xx)I$ and $u:=II$, where $I$ is the identity. Then $t\to u$, so $t$ and $u$ are $\beta$-equivalent, and yet $u$ is simply-typable and $t$ is not. As proved in Nift's answer below, there are even examples of this phenomenon in which $t$ too is typable (but has strictly less types than $u$).

> **Comments:**
> **username_0**: When you claim that "if $t \to u$, then $t$ and $u$ necessarily have the same type", you do not only rely on subject reduction but also on subject expansion. Does subject expansion really hold for Church-style simply-typed lambda calculus? It is not obvious to me.  
> **username_2**: Subject reduction and subject expansion only make sense for Curry-style type systems.  In the Church-style presentation, the types are written in the terms, you have no choice.  I have the feeling that maybe you are not familiar with the Church-style presentation?  
> **username_0**: Take the reduction $(\lambda x^\sigma . M) N \to M[N/x]$. if $(\lambda x^\sigma . M) N$ has type $\tau$, then obviously $M[N/x]$ too. But, in the other direction, if $M[N/x]$ has type $\tau$, it is not obvious that $(\lambda x^\sigma . M) N$ too has type $\tau$ because the $\sigma$ that occurs is arbitrary (it is not written in $M[N/x]$ as you say).  
> **username_2**: It *is* written in $M[N/x]$: it is the type of $N$, which appears as subterm of $M[N/x]$, unless $x$ does not appear free in $M$, which is a trivial case.  
> **username_2**: Anyway, the point is that in the Church-style formulation you can't choose the type of terms. Terms come with a unique type which may be unambiguously inferred from the type annotations.  It so happens that, in a $\beta$-reduction $M\to N$, the type of $M$ and the type of $N$ are the same.  I say *the* type because you have no choice, you can't attribute a type to $M$ (or to $N$) and then check whether it is preserved by reduction (or expansion), it doesn't make sense.  
> **username_0**: I wrongly believed that Church-style meant type annotations on lambda abstractions only.  
> **username_2**: Well, for a closed therm, Church style *is* type annotations on $\lambda$-abstractions only.  
> **username_2**: For general terms, Church style means type annotations on $\lambda$-abstractions *and* on free variables.  That's enough to recover the type of every subterm (in particular the term itself).  

---

### Answer by username_1 on 2023-02-22. Score: 3

Actually I have deleted an answer to what I claimed in the comments and would like to provide a counterexample in Curry-style STLC, this is 5.12 in
<https://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf>, which I reproduce here.
There are $M$, $M'$ ∈ Λ and $σ$, $σ'$ ∈ T such that $M' \twoheadrightarrow\_{\beta} M$ and
$\vdash M : σ$, $\vdash M' : σ'$, but $\nvdash M' : σ$.
Take $M \equiv \lambda xy.y$, $M' \equiv SK$. Take $\sigma \equiv \alpha \rightarrow (\beta \rightarrow \beta)$ and $\sigma' \equiv (\beta \rightarrow \alpha) \rightarrow (\beta \rightarrow \beta)$.

Take these M' and M, given that $M' \twoheadrightarrow\_{\beta} M$, $M' \equiv\_{\beta} M$,, but by the above $M$ has a typing $\sigma$, but $M'$ does not. To see why $M$ having a typing $\sigma$ is trivial.
For M' and M being equivalent see as follows,
M' = SK   
= (λxyz.xz(yz))(λxy.x)   
= λyz.(λxy.x)z(yz)   
= λyz.(λy.z)(yz)   
= λyz. z
which is we can alpha rename to $M$.
For $M'$ not having typing $\sigma$ see as follows, to type SK we need to know that the second argument of S is a function.

Thus we have 2 $\beta$-equivalent terms, only one of which is typeable at $\sigma$, but both are simply typeable.


---

