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...
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$– IlkFeb 21 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$– IlkFeb 21 at 9:36
-
$\begingroup$ @Nift I think you should write these comments as an answer. $\endgroup$– Damiano MazzaFeb 21 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$– BobFeb 21 at 12:59
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
8
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$).
answered Feb 21 at 9:16
-
$\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$– BobFeb 22 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 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$– BobFeb 23 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 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 at 11:45
$\begingroup$
$\endgroup$
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.
