# Lambda-calculus: Beta-equivalent terms have the same type

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...

• 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
Commented Feb 21, 2023 at 9:23
• For claim of principality, see macs.hw.ac.uk/~jbw/papers/… Theorem 1, and maybe try following the trail of references for a proof.
– Ilk
Commented Feb 21, 2023 at 9:36
• @Nift I think you should write these comments as an answer. Commented Feb 21, 2023 at 12:08
• @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
Commented Feb 21, 2023 at 12:59

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$$).

• 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
Commented Feb 22, 2023 at 15:56
• 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? Commented Feb 23, 2023 at 6:20
• 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
Commented Feb 23, 2023 at 11:18
• 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. Commented Feb 23, 2023 at 11:40
• 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. Commented Feb 23, 2023 at 11:45

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.