5
$\begingroup$

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

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

2 Answers 2

6
$\begingroup$

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

$\endgroup$
8
  • $\begingroup$ 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. $\endgroup$
    – Bob
    Feb 22, 2023 at 15:56
  • 1
    $\begingroup$ 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? $\endgroup$ Feb 23, 2023 at 6:20
  • 1
    $\begingroup$ 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). $\endgroup$
    – Bob
    Feb 23, 2023 at 11:18
  • $\begingroup$ 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. $\endgroup$ Feb 23, 2023 at 11:40
  • $\begingroup$ 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. $\endgroup$ Feb 23, 2023 at 11:45
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.