Automath Type Inclusion in Barendregt’s Cube

Abstract

The introduction of a general definition of function was key to Frege’s formalisation of logic. Self-application of functions was at the heart of Russell’s paradox. Russell introduced type theory to control the application of functions and avoid the paradox. Since, different type systems have been introduced, each allowing different functional power. Most of these systems use the two binders $\lambda$ and $\varPi$ to distinguish between functions and types, and allow $\beta$-reduction but not $\varPi$-reduction. That is, $(\pi _{x:A}.B)C \rightarrow B[x: =C]$ is only allowed when $\pi$ is $\lambda$ but not when it is $\varPi$. Since $\varPi$-reduction is not allowed, these systems cannot allow unreduced typing. Hence types do not have the same instantiation right as functions. In particular, when b has type B, the type of $(\lambda _{x:A}.b)C$ is immediately given as $B[x: =C]$ instead of keeping it as $(\varPi _{x:A}.B)C$ to be $\varPi$-reduced to $B[x: =C]$ later. Extensions of modern type systems with both $\beta$- and $\varPi$-reduction and unreduced typing have appeared in [11, 12] and lead naturally to unifying the $\lambda$ and $\varPi$ abstractions [9, 10]. The Automath system combined the unification of binders $\lambda$ and $\varPi$ with $\beta$- and $\varPi$-reduction together with a type inclusion rule that allows the different expressions that define the same term to share the same type. In this paper we extend the cube of 8 influential type systems [3] with the Automath notion of type inclusion [5] and study its properties.

A Proofs

This appendix gives the proofs for Lemmas 12, 14, 15, 22, 27, as well as the unicity of types Lemma 21 for the ${\beta _a}$- and $\pi _{ai}$-cubes.

Proof

(Thinning Lemma 12 ).

• 1. First show by induction on $\varGamma \Vdash A =_rB$ that if $\varGamma$ and $\varDelta$ are $\vdash$-legal then:

  • If $\varGamma \equiv \varGamma _1, \varGamma _2 \subseteq ' \varGamma _1, d, \varGamma _2 \equiv \varDelta$ and $\varGamma \Vdash A =_rB$ then $\varDelta \Vdash A =_rB$.

  • If $\varGamma \equiv \varGamma _1, x: A, \varGamma _2 \subseteq ' \varGamma _1, x = B : A, \varGamma _2 \equiv \varDelta$ and $\varGamma \Vdash A =_rB$ then $\varDelta \Vdash A =_rB$.

  Then, show the statement by induction on $\varGamma \subseteq ' \varDelta$.

• 2. First show by induction on $\varGamma \vdash A : B$ that if $\varGamma$ and $\varDelta$ are $\vdash$-legal then:

  • If $\varGamma \equiv \varGamma _1, \varGamma _2 \subseteq ' \varGamma _1, d, \varGamma _2 \equiv \varDelta$ and $\varGamma \vdash A : B$ then $\varDelta \vdash A : B$.

  • If $\varGamma \equiv \varGamma _1, x: A, \varGamma _2 \subseteq ' \varGamma _1, x = B : A, \varGamma _2 \equiv \varDelta$ and $\varGamma \vdash A : B$ then $\varDelta \vdash A : B$.

  Then, show the statement by induction on $\varGamma \subseteq ' \varDelta$.

$\square$

Proof

(Lemma  14 ).

• 1. By induction on the derivation $\varGamma \vdash A:B$.

• 2. This is a corollary of 1. above.

• 3. By induction on the derivation $\varGamma \vdash AB: \Box$.

• 4. Since $y : *, x = y : *\vdash *: \Box$, then $y : *\vdash (\lambda _{x:*}.*)y:y$.

• 5. By induction on the derivation $\varGamma \vdash A:\Box$ using Start/Context Lemma 10 to show that the start and start-a rules do not apply, 1. above to show that conv$_r$ and app$_\backslash$ do not apply, and Substitution Lemma 13.

• 6. By induction on the derivation $\varGamma \vdash \pi ^1_{x_1:A_1}\pi ^2_{x_2:A_2}\dots \pi ^l_{x_l:A_l}.*:A$ using 1. above. Then, use 2. to deduce $A \equiv \Box$.

• 7. By induction on the derivation $\varGamma \vdash \varPi ^{i:1..l}_{x_i{:}A_i}.*:\Box$. Conv$_r$ and Q$_{\beta }$ don’t apply.

• 8. By induction on the derivation $\varGamma \vdash \lambda _{x:A}.B : C$.

• 9. By induction on the derivation $\varGamma \vdash A : \Box$.

• 10. Assume $\varGamma \vdash A:s$ and $\varGamma ,x{:}A\vdash B:*$. Then:

  

 $\square$

Proof

(Generation Lemma  15 ).

• 1. By induction on the derivation $\varGamma \vdash s:C$. The Q-rule does not apply.

• 2. By induction on the derivation $\varGamma \vdash x:C$. We only do the Q-rule. Assume $\varGamma \vdash x:*$ comes from $\varGamma \vdash x:\varPi ^{i:1..n}_{x_i{:}A_i}.*$. By IH, there is d in $\varGamma$ such that $x \equiv \mathtt{var}(d)$, $\varGamma \vdash \varPi ^{i:1..n}_{x_i{:}A_i}.*:s$, $\varGamma \vdash \mathtt{type}(d):s$ for some sort s and $\mathtt{type}(d)\le _{\beta }\varPi ^{i:1..n}_{x_i{:}A_i}.*$. Since $\varPi ^{i:1..n}_{x_i{:}A_i}.*\le _{\beta }*$, by Corollary 5.1, $\mathtt{type}(d)\le _{\beta }*$. By Lemma 14, $s \equiv \Box$ and $\varGamma \vdash *: \Box$.

• 3.,4.,5. By induction on the generation $\varGamma \vdash M:C$. We only do the new cases: the Q-rule and the difficult case of $\vdash _{\pi _a}$. First the Q-rule in $\vdash _{\beta _{Q}}$.

  Assume $M\equiv \lambda ^{i:1..m}_{x_i{:}A_i}.\varPi ^{i:m+1..k}_{x_i{:}A_i}.M'$, $M'$ is not of the form $\lambda _{x{:}N_1}.N_2$, $C\equiv \varPi ^{i:1..m}_{x_i{:}A_i}.*$, $m\le n$ and $\varGamma \vdash M:C$ because $\varGamma \vdash \lambda ^{i:1..k}_{x_i{:}A_i}.M' : \varPi ^{i:1..n}_{x_i{:}A_i}.*$. Write $U\equiv \lambda ^{i:1..k}_{x_i{:}A_i}.M'$ and $W\equiv \varPi ^{i:1..n}_{x_i{:}A_i}.*$.

  • i. $M\equiv \varPi _{x_1{:}A_1}.B$. Then $m=0$, $k>0$, and we used Rule (Q) to derive:

    $$\frac{\displaystyle \varGamma \vdash \lambda ^{i:1..k}_{x_i{:}A_i}.M' : \varPi ^{i:1..n}_{x_i{:}A_i}.*}{\displaystyle \varGamma \vdash \varPi ^{i:1..k}_{x_i{:}A_i}.M' : *}$$

    By IH, there are s, B such that $\varGamma ,x_1{:}A_1\vdash \lambda ^{i:2..k}_{x_i{:}A_i}.M':B$, $\varGamma \vdash \varPi _{x_1:A_1} . B:s$, and $\varPi _{x_1{:}A_1}.B \le _{\beta }\varPi ^{i:1..n}_{x_i{:}A_i}.*$ and if $\varPi _{x_1:A_1} . B\not \equiv \varPi ^{i:1..n}_{x_i{:}A_i}.*$ then $\varGamma \vdash \varPi ^{i:1..n}_{x_i{:}A_i}.*: \Box$ (note Lemma 14). By Lemma 14, $\varGamma , x_1:A_1 \vdash \varPi ^{i:2..n}_{x_i{:}A_i}.*: \Box$ and there is $s_1$ such that $\varGamma \vdash A_1:s_1$ and $(s_1, \Box ) \in \varvec{R}$, hence also, $(s_1, *) \in \varvec{R}$. By Corollary 5.2, $B \le _{\beta }\varPi ^{i:2..n}_{x_i{:}A_i}.*$. Determine $B' =_{\beta }B$ where $B' \le \varPi ^{i:2..n}_{x_i{:}A_i}.*$, say $B'\equiv \varPi ^{i:2..\ell }_{x_i{:}A_i}.*$ where $l \ge n$ and $\varGamma , x_1:A_1 \vdash \varPi ^{i:2..\ell }_{x_i{:}A_i}.*:\Box$. By conversion, $\varGamma ,x_1{:}A_1\vdash \lambda ^{i:2..k}_{x_i{:}A_i}.M':\varPi ^{i:2..\ell }_{x_i{:}A_i}.*$, and as $M'$ is not of the form $\lambda _{x{:}N_1}.N_2$, we can use (Q) and obtain $\varGamma ,x_1{:}A_1\vdash \varPi ^{i:2..k}_{x_i{:}A_i}.M':*$. Since $\varGamma \vdash A_1:s_1$ and $(s_1, *) \in \varvec{R}$ we are done.

  • ii. $M\equiv \lambda _{x_1{:}A_1}.b$. Then $k>0$ and $b \equiv \lambda ^{i:2..m}_{x_i{:}A_i}. \varPi ^{i:m+1..k}_{x_i{:}A_i}.M'$. By the induction hypothesis there are s, B such that $\varGamma \vdash \varPi _{x_1{:}A_1}.B:s$, $\varGamma ,x_1{:}A_1\vdash \lambda ^{i:2..k}_{x_i{:}A_i}.M':B$ and $\varPi _{x_1{:}A_1}.B\le _{\beta }\varPi ^{i:1..n}_{x_i{:}A_i}.*$ and if $\varPi ^{i:1..n}_{x_i{:}A_i}.*\not \equiv \varPi _{x_1{:}A_1}.B$ then $\varGamma \vdash \varPi ^{i:1..n}_{x_i{:}A_i}.*:\Box$ (note Lemma 14). Note that $\varPi _{x_1{:}A_1}.B\le _{\beta }\varPi ^{i:1..n}_{x_i{:}A_i}.*\le _{\beta }\varPi ^{i:1..m}_{x_i{:}A_i}.*$, so by Corollary 5.1, $\varPi _{x_1{:}A_1}.B\le _{\beta }\varPi ^{i:1..m}_{x_i{:}A_i}.*$. Determine $B'=_{\beta }\varPi _{x_1{:}A_1}.B$ such that $B'\le \varPi ^{i:1..n}_{x_i{:}A_i}.*$ and $\varGamma \vdash B' : \Box$. We can write $B'\equiv \varPi ^{i:1..\ell }_{x_i{:}A_i}.*$ for an $\ell$ such that $m\le n\le \ell$. Distinguish two cases:

    • * $k\le m$. Then $M\equiv \lambda ^{i:1..k}_{x_i{:}A_i}.M'$, $b \equiv \lambda ^{i:2..k}_{x_i{:}A_i}.M'$ and hence $\varGamma ,x_1{:}A_1\vdash b : B$.

    • * $k>m$. Then $M\equiv \lambda ^{i:1..m}_{x_i{:}A_i}.\varPi ^{i:m+1..k}_{x_i{:}A_i}.M'$. By conversion, $\varGamma ,x_1{:}A_1\vdash \lambda ^{i:2..k}_{x_i{:}A_i}.M' :B'$, and as $M'$ is not of the form $\lambda _{x{:}N_1}.N_2$, and $m\le n\le \ell$, we get by (Q) that $\varGamma ,x_1{:}A_1\vdash \lambda ^{i:2..m}_{x_i{:}A_i}. \varPi ^{i:m+1..k}_{x_i{:}A_i}.M' : \varPi ^{i:2..m}_{x_i{:}A_i}.*$.

  • iii. $M\equiv AB$. Then $k=m=0$, so $U\equiv AB$. By induction there are x, P, Q such that $\varGamma \vdash A: \varPi _{x{:}P}.Q$, $\varGamma \vdash B:P$ and $Q[x{: =}B]\le _{\beta }W$. Notice that $W\le _{\beta }C\equiv *$, so by Corollary 5.1, $B\le _{\beta }C$.

  Next we do the case 5(b)ii. of $\vdash _{\pi _a}$. By induction on the derivation rules we first prove that if $\varGamma \vdash (\pi _{y:D}.E)a :C$ then one of the following holds:

  • $\varGamma , y = a : D \vdash E: H$ and $\varGamma \Vdash H[y: =a] =_{\beta \varPi }C$ and if $H[y: =a]\not \equiv C$ then $\varGamma \vdash C:s$ for some s.

  • $\varGamma \vdash a:F$, $\varGamma \vdash \lambda _{y:D}.E : \varPi _{z:F}.G$, $\varGamma \Vdash C =_{\beta \varPi }G[z: =a]$ and if $G[z: =a] \not \equiv C$ then $\varGamma \vdash C:s$ for some s.

  If the first case holds, then by substitution and thinning, $\varGamma , y = a : D \Vdash H[y: =a]=_{\beta \varPi }H$ and $\varGamma , y = a : D \Vdash H[y: =a]=_{\beta \varPi }C$. Hence, $\varGamma , y = a : D \Vdash H =_{\beta \varPi }C$ and we use conv$_{\beta \varPi }$ to get $\varGamma , y = a : D \vdash E: C$.

  In the second case, by generation case 3. on $\varGamma \vdash \lambda _{y:D}.E : \varPi _{z:F}.G$ we get $\varGamma , y:D \vdash E : L$, $\varGamma \Vdash \varPi _{y:D}.L =_{\beta \varPi }\varPi _{z:F}.G$ and if $\varPi _{y:D}.L \not \equiv \varPi _{z:F}.G$ then $\varGamma \vdash \varPi _{z:F}.G : s'$ for some $s'$. Hence $y = z$ and $\varGamma \Vdash D =_{\beta \varPi }F$ and $\varGamma \Vdash L =_{\beta \varPi }G$. Now, using generation case 4. we prove that $\varGamma , y = a : D \vdash E:L$. Since $\varGamma \Vdash C =_{\beta \varPi }G[y: =a]$ we get $\varGamma , y = a : D \Vdash C =_{\beta \varPi }G$. Since $\varGamma \Vdash L =_{\beta \varPi }G$ we get $\varGamma , y = a : D \Vdash L =_{\beta \varPi }G$. Hence, $\varGamma , y = a : D \Vdash L =_{\beta \varPi }C$. We show that $\varGamma , y = a : D \vdash C:s''$ for some sort $s''$. Hence using $\varGamma , y = a : D \vdash E:L$ and conv$_{\beta \varPi }$, we get $\varGamma , y = a : D \vdash E:C$.

 $\square$

Proof

(Connecting cubes Lemma  22 ).

• 1. If $\varGamma \vdash _c (\varPi _{x:A}.B)a : C$, then by Lemma 15, $\exists A', B'$ such that $\varGamma \vdash _c \varPi _{x:A}.B : \varPi _{y:A'}.B'$. Again by Lemma 15, $\varGamma \Vdash \varPi _{y:A'}.B' =_r s_2$ for sort $s_2$, contradicting Church Rosser.

  As for the second statement, first show by induction on the derivation $\varGamma , x:C, \varDelta \vdash _c A : B$ that if both A and a are free of $\varPi$-redexes, $\varGamma , x:C, \varDelta \vdash _c A : B$ and $\varGamma \vdash _c a:C$, then $A[x: =a]$ is free of $\varPi$-redexes. Then show the statement by induction on $\varGamma \vdash _c A : B$.

• 2. Take for example $z : *, x: z \vdash _{\pi _i} (\lambda _{y:z}.y)x : (\varPi _{y:z}.z)x$ and hence terms of the form $(\varPi _{x:A}.B)a$ can be $\vdash _{\pi _i}$-legal. It is the new legal terms that led to the loss of correctness of types of the $\pi _i$-cube and hence of subject reduction because they can not be typable.

• 3. By induction on $\varGamma \vdash _{\pi _i} A : B$.

• 4. $z :*, x:z \vdash _{c} (\varPi _{y:z}.z)x : *$ and $z :*\vdash _{c} (\lambda _{y:*}.*)z : \Box$ provide examples.

• 5. $y : *\vdash _{\beta _a} (\lambda _{x:*}.*)y : \Box$.

• 6. Note that $=_\beta \subseteq =_{\beta \varPi }$.

  Also, note that $z :*, x:z \vdash _{c} (\varPi _{y:z}.z)x : *$ and $z : *, x: z \vdash _{c} x: (\varPi _{y:z}.z)x$.

  Note also that $z : *, x: z, y = (\varPi _{y:z}.z)x : *\vdash _{c} y:*$.

• 7. By correctness (resp. restricted correctness) of types, it is enough to show that if $\varGamma \vdash _c \varPi _{x:A}.B :C$ then $\varGamma \vdash _c \varPi _{x:A}.B :s$. We do this by induction on the derivation $\varGamma \vdash _c \varPi _{x:A}.B :C$.

• 8. (a) By induction on the derivation $\varGamma \vdash _\beta A:B$ using the substitution lemma for the $\pi _i$-cube and 7 above. (b) By induction on the derivation $\varGamma \vdash _{\pi _i} A:B$.

  (c) By (b) $\varGamma \vdash _\beta A:[B]_\varPi$. Since B is free of $\varPi$-redexes, $B = [B]_\varPi$ and $\varGamma \vdash _\beta A:B$.

  (d) Using (a), it is enough to find $\varGamma , A, B$ such that $\varGamma \vdash _{\pi i} A:B$ but $\varGamma \not \vdash _\beta A:B$. We know that $z : *, x: z \vdash _{\pi _i} (\lambda _{y:z}.y)x : (\varPi _{y:z}.z)x$ but by 3 above, $z : *, x: z \not \vdash _{\beta } (\lambda _{y:z}.y)x : (\varPi _{y:z}.z)x$.

• 9. (a) holds since the rules of $\vdash _\beta$ are a subset of the rules of $\vdash _{\beta _a}$.

  (b) is by induction on $\varGamma \vdash _{\beta _a} A:B$.

  (c) holds because the rules of $\vdash _{\pi _{i}}$ are a subset of the rules of $\vdash _{\pi _{ai}}$. As for strict inclusion, note that $\alpha : *\vdash _{\pi _{ai}} (\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y)\alpha : \varPi _{y: \alpha }.\alpha$ but $\alpha : *\not \vdash _{\pi _i} (\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y)\alpha : \varPi _{y: \alpha }.\alpha$ since we don’t have $y:\alpha$.

  (d) by induction on $\varGamma \vdash _{\pi _{ai}} A:B$. We only do the i-app rule. Let $\varGamma \vdash _{\pi _{ai}} Fa: (\varPi _{x:A}.B)a$ come from $\varGamma \vdash _{\pi _{ai}} F: \varPi _{x:A}.B$ and $\varGamma \vdash _{\pi _{ai}} a: A$. By IH, $\widetilde{\varGamma } \vdash _{\beta _a} \widetilde{F}:\widetilde{\varPi _{x:A}.B} \equiv \varPi _{x:\widetilde{A}}.\widetilde{B}$ and $\widetilde{\varGamma } \vdash _{\beta _a} \widetilde{a}:\widetilde{A}$. Hence by app, $\widetilde{\varGamma } \vdash _{\beta _a} \widetilde{F}\widetilde{a}:\widetilde{B}[x: =\widetilde{A}]$. Since $\varPi _{x:\widetilde{A}}.\widetilde{B}$ is $\widetilde{\varGamma }^{\vdash _{\beta _a}}$-term, by correctness of types, $\exists s$ such that $\widetilde{\varGamma } \vdash _{\beta _a}\varPi _{x:\widetilde{A}}.\widetilde{B} :s$. Hence by generation, $\widetilde{\varGamma }, x:\widetilde{A} \vdash _{\beta _a}\widetilde{B} :s$. Hence by thinning, $\widetilde{\varGamma }, x = \widetilde{a}:\widetilde{A} \vdash _{\beta _a}\widetilde{B} :s$. By let$_{\lambda }$, $\widetilde{\varGamma }\vdash _{\beta _a} (\lambda _{x :\widetilde{A}}.\widetilde{B})\widetilde{a} :s$. By conv$_{\beta \varPi }$, $\widetilde{\varGamma } \vdash _{\beta _a} \widetilde{F}\widetilde{a}:(\lambda _{x :\widetilde{A}}.\widetilde{B})\widetilde{a}$. If $\widetilde{F}$ was a $\varPi$-term, then by generation, $\widetilde{\varGamma } \Vdash \varPi _{x:\widetilde{A}}.\widetilde{B} =_\beta s_2$ for some $s_2$ absurd. Hence, $\widetilde{F}\widetilde{a} \equiv \widetilde{Fa}$.

• 10. $\alpha : *\vdash _{\beta _a} (\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y)\alpha : \varPi _{y: \alpha }.\alpha$ (see Example 28). However,

  $\alpha : *\not \vdash _{\beta } (\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y)\alpha : \varPi _{y: \alpha }.\alpha$ since we don’t have $y:\alpha$.

  Another way to prove this is to assume $\alpha : *\vdash _{\beta } (\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y)\alpha : \varPi _{y: \alpha }.\alpha$. Hence, by correctness of types, $\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y$ is $(\alpha : *)^{\vdash _{\beta }}$-term and by 9 (a) above it is $(\alpha : *)^{\vdash _{\beta _a}}$-legal, contradicting Example 28.

• 11. For ${\vdash _{\beta }} \subset {\vdash _{\beta _a}}$, use 9.(a) and 10. above. For ${\vdash _{\beta _a}} \subset {\vdash _{\pi _{ai}}}$, use 9.(b) above and this example: $z : *, x: z \vdash _{\pi _{ai}} (\lambda _{y:z}.y)x : (\varPi _{y:z}.z)x$ but by 1 above, $z : *, x: z \not \vdash _{\beta _a} (\lambda _{y:z}.y)x : (\varPi _{y:z}.z)x$.

• 12. (a) By induction on the derivation $\varGamma \vdash _{\beta _a} A:B$ using 6 above.

  (b) By induction on the derivation $\varGamma \vdash _{\pi _{a}} A:B$. we only do the (app) case. Assume $\varGamma \vdash _{\pi _{a}} Fa: B[x: =a]$ comes from $\varGamma \vdash _{\pi _{a}} F: \varPi _{x:A}.B$ and $\varGamma \vdash _{\pi _{a}} a: A$. By IH, $\varGamma \vdash _{\pi _{ai}} F: \varPi _{x:A}.B$ and $\varGamma \vdash _{\pi _{ai}} a: A$ and hence $\varGamma \vdash _{\pi _{ai}} Fa: (\varPi _{x:A}. B)a$ by (i-app). By correctness of types, $\varGamma \vdash _{\pi _{ai}} \varPi _{x:A}.B: s$ for some s and hence by generation, $\varGamma , x:A \vdash _{\pi _{ai}} B:s'$. Since $\varGamma \vdash _{\pi _{ai}} a: A$ then by substitution lemma, $\varGamma \vdash _{\pi _{ai}} B[x: =a] : s'$. Now, since $\varGamma \Vdash B[x: =a] =_{\beta \varPi }(\varPi _{x:A}. B)a$ we use (conv$_{\beta \varPi }$) to get $\varGamma \vdash _{\pi _{a}} Fa: B[x: =a]$.

  (c) Note that $z :*, x:z \vdash _{\pi _{a}} (\varPi _{y:z}.z)x : *$ but by 4 above, if $\varGamma \vdash _{\beta _{a}} A:B$ then all of $\varGamma , A$ and B are free of $\varPi$-redexes.

• 13. (a) By 1 above, A is free of $\varPi$-redexes.

  (b) By induction on $A \rightarrow \!\!\!\!\rightarrow _{\beta \varPi }A'$. Assume $A \rightarrow \!\!\!\!\rightarrow ^n_{\beta \varPi }A''\rightarrow _{\beta \varPi }A'$. By subject reduction, $\varGamma \vdash _\pi A'':B$ and hence by IH, $A \rightarrow \!\!\!\!\rightarrow ^n_{\beta }A''$ and $A''\rightarrow _{\beta }A'$. Hence, $A\rightarrow \!\!\!\!\rightarrow _{\beta }A'$.

• 14. One direction is trivial because every $\vdash _\beta$-rule is also a $\vdash _\pi$-rule (for (conv$_r$), note that $=_\beta \subseteq =_{\beta \varPi }$). For the other direction, use induction on $\varGamma \vdash _\pi A:B$. We only show the (conv$_r$) case. Let $\varGamma \vdash _\pi A:B$ come from $\varGamma \vdash _\pi A:B'$, $\varGamma \vdash _\pi B': s$ and $B =_{\beta \varPi } B'$. By Church-Rosser, $\exists B''$ such that $B'\rightarrow \!\!\!\!\rightarrow ^n_{\beta \varPi } B'' \leftarrow \!\!\!\! \leftarrow _{\beta \varPi } B$. By Correctness of types, $B \equiv \Box$ or $\exists s'$ such that $\varGamma \vdash _\pi B:s'$. If $B \equiv \Box$ then $B'' \equiv \Box$ and $B' \rightarrow \!\!\!\!\rightarrow ^n_{\beta \varPi } \Box$, hence by subject reduction and $\varGamma \vdash _\pi B': s$ we get $\varGamma \vdash _\pi \Box : s$ contradicting 1 above. Hence $\varGamma \vdash _\pi B:s'$ and by 13 above, $B \rightarrow \!\!\!\!\rightarrow _\beta B''$. Also, by 13, $B' \rightarrow \!\!\!\!\rightarrow _\beta B''$. Hence, $B =_\beta B'$. Hence, by IH and (conv$_r$), $\varGamma \vdash _\beta A:B$.

• 15. This is a corollary of item 12 above.

• 16. a. One direction holds by 12 above. The other direction is by induction on $\varGamma \vdash _{\pi _{ai}} A: B$. Since every $\vdash _{\pi _{ai}}$-rule (except the (i-app) rule) is also a rule of $\vdash _{\pi _{a}}$, we only deal with the (i-app) case. Assume $\varGamma \vdash _{\pi _{ai}} Fa: (\varPi _{x:A}.B)a$ comes from $\varGamma \vdash _{\pi _{ai}} F: \varPi _{x:A}.B$ and $\varGamma \vdash _{\pi _{ai}} a: A$. By IH, $\varGamma \vdash _{\pi _{a}} F: \varPi _{x:A}.B$ and $\varGamma \vdash _{\pi _{a}} a: A$ and hence by (app), $\varGamma \vdash _{\pi _{a}} Fa: B[x: =a]$. Since $\varGamma \Vdash (\varPi _{x:A}.B)a =_{\beta \varPi }B[x: =a]$, to derive $\varGamma \vdash _{\pi _{a}} Fa: (\varPi _{x:A}.B)a$, it is enough to show that $\varGamma \vdash _{\pi _{a}}(\varPi _{x:A}.B)a:s$ for some s. Since $\varGamma \vdash _{\pi _{a}} F: \varPi _{x:A}.B$, by correctness of types, $\varGamma \vdash _{\pi _{a}} \varPi _{x:A}.B : s$ and by generation, $\varGamma , x: A \vdash _{\pi _{a}} B : s'$ and $\varGamma \vdash _{\pi _{a}} A : s''$. It is easy to show that $\varGamma , x=a: A$ is legal. Hence, since $\varGamma , x: A \subseteq ' \varGamma , x=a: A$, we can use thinning to get $\varGamma , x=a: A\vdash _{\pi _{a}} B : s'$. And so, by (let), $\varGamma \vdash _{\pi _{a}} (\varPi _{x:A}.B)a:s'$.

  b. ${\vdash _{\pi }} = {\vdash _{\beta }}$ by 14 above. ${\vdash _{\beta }} \subset {\vdash _{\beta _a}} \subset {\vdash _{\pi _{ai}}}$ by 9 above. ${\vdash _{\pi _{ai}}} = {\vdash _{\pi _{a}}}$ by a. above. ${\vdash _{\beta }} \subset {\vdash _{\pi _i}}$ by 8 above. ${\vdash _{\pi _i}} \subset {\vdash _{\pi _{ai}}}$ by 9 above.

  c. $z : *, x: z \vdash _{\pi _i} (\lambda _{y:z}.y)x : (\varPi _{y:z}.z)x$ but $z : *, x: z \not \vdash _{\beta _a} (\lambda _{y:z}.y)x : (\varPi _{y:z}.z)x$ by 1 above.

  Also, $\alpha : *\vdash _{\beta _a} (\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y)\alpha : \varPi _{y: \alpha }.\alpha$ but

  $\alpha : *\not \vdash _{\pi _i} (\lambda _{\beta : *}.\lambda _{y: \beta }.(\lambda _{z:\alpha }.z)y)\alpha : \varPi _{y: \alpha }.\alpha$ since we don’t have $y:\alpha$.

 $\square$

Proof

(Restricted typability of subterms Lemma  27 for ${\vdash _{\beta _a}} + {\rightarrow _{be}}$ and ${\vdash _{\pi _{ai}}} + {\rightarrow _{\beta \varPi }}$ ). We will prove that:

• 1. If A is ${\vdash }$-legal and B is a subterm of A such that every bachelor $\lambda _{x:D}$ in B is also bachelor in A, then B is ${\vdash }$-legal.

• 2. If A is ${\vdash _{\pi _{ai}}}$-legal and B is a subterm of A such that every bachelor $\pi _{x:D}$ in B is also bachelor in A, then B is ${\vdash _{\pi _{ai}}}$-legal.

Let $c \in \{\beta _a,\pi _{ai}\}$. If $\varGamma \vdash _c C :A$, then by correctness of types, $A \equiv \Box$ (and there is nothing to prove) or $\varGamma \vdash _c A: s$. Hence, it is enough to prove the lemma for $\varGamma \vdash _c A: C$. For 1, we prove this by induction on the derivation that if $\varGamma \vdash _{\beta _a} A: C$ and B is a subterm of A resp. $\varGamma$ such that every bachelor $\lambda _{x:D}$ in B is also bachelor in A resp. $\varGamma$, then B is $\vdash _{\beta _a}$-legal. For 2, we prove this by induction on the derivation that if $\varGamma \vdash _{\pi _{ai}} A: C$ and B is a subterm of A resp. $\varGamma$ such that every bachelor $\pi _{x:D}$ in B is also bachelor in A resp. $\varGamma$, then B is $\vdash _{\pi _{ai}}$-legal.  $\square$

Proof

(Unicity of Types for ${\vdash _{\beta _a}} + {\rightarrow _\beta }$ and for ${\vdash _{\pi _{ai}}} + {\rightarrow _{\beta \varPi }}$ ).

• 1. By induction on the structure of A using the generation lemma.

• 2. First, show by Church-Rosser and subject reduction using 1 that:

  $$\begin{aligned} \text{ If } \varGamma \vdash _c A_1 : B_1 \text{ and } \varGamma \vdash _c A_2: B_2 \text{ and } A_1 =_{\overline{c}} A_2, \text{ then } \varGamma \Vdash B_1 =_{\overline{c}}B_2. \end{aligned}$$

  (*)

  Then, define

  • $[A]_{\langle \rangle } \equiv A$, $[A]_{\varGamma , x:C} \equiv [A]_\varGamma$ and $[A]_{\varGamma , x=B :C} \equiv [A[x: =B]]_\varGamma$.

  • $[x:A]_\varGamma$ as $x : [A]_\varGamma$ and $[x=B:A]_\varGamma$ as $x = [B]_\varGamma : [A]_\varGamma$.

  • $\varGamma ^0$ as $\varGamma$ and $\varGamma ^n$ as $\varGamma$ where n elements $d_1, \dots , d_n$ of $\varGamma$ have been replaced by $[d_1]_\varGamma , \dots , [d_n]_\varGamma$.

  Note that $[A]_{\varGamma ,\varGamma '} \equiv [[A]_{\varGamma '}]_{\varGamma }$, $\varGamma \Vdash A =_{\overline{c}}[A]_{\varGamma }$, and if $\varGamma \Vdash A_1 =_{\overline{c}}A_2$ then $[A_1]_\varGamma =_{\overline{c}} [A_2]_\varGamma$. Now prove by induction on $\varGamma \vdash _c A:B$ that:

  $$\begin{aligned} \text{ If } \varGamma \vdash _c A:B \text{ then } \varGamma ^n&\vdash _c [A]_\varGamma : [B]_\varGamma \text{ and } \varGamma ^n \vdash _c A:B\\&\text{ for } n \le \text{ the } \text{ number } \text{ of } \text{ elements } \text{ in } \varGamma . \end{aligned}$$

  Finally, assume $\varGamma \vdash _c A_1 : B_1$ and $\varGamma \vdash _c A_2: B_2$ and $\varGamma \Vdash A_1 =_{\overline{c}}A_2$. Then, $\varGamma \vdash _c [A_1]_\varGamma : [B_1]_\varGamma$, $\varGamma \vdash _c [A_2]_\varGamma : [B_2]_\varGamma$ and $[A_1]_\varGamma =_{\overline{c}} [A_2]_\varGamma$. Hence, by (*), $\varGamma \Vdash [B_1]_\varGamma =_{\overline{c}}[B_2]_\varGamma$. But, $\varGamma \Vdash B_1 =_{\overline{c}}[B_1]_{\varGamma }$ and $\varGamma \Vdash B_2 =_{\overline{c}}[B_2]_{\varGamma }$. Hence, $\varGamma \Vdash _c B_1 =_{\overline{c}}B_2$.

• 3. As $\varGamma \vdash _c A:B_2$, by correctness of types $B_2 \equiv \Box$ or $\varGamma \vdash _c B_2:s'$ for some $s'$.

  • If $\varGamma \vdash _c B_2:s'$ then by 2 above, $\varGamma \Vdash s =_{\overline{c}}s'$. By the proof of 2 above, $s \equiv [s]_\varGamma =_{\overline{c}}[s']_\varGamma \equiv s'$. Hence, $s \equiv s'$ and so, $\varGamma \vdash _c B_2:s$.

  • If $B_2 \equiv \Box$, we prove that if $\varGamma \Vdash A =_{\overline{c}}\Box$ then $\varGamma \not \vdash _c A: B$. If $\varGamma \Vdash A =_{\overline{c}}\Box$ and $\varGamma \vdash _c A: B$ then by the proof of 2 above, $[A]_\varGamma =_{\overline{c}}[\Box ]_\varGamma$ and $\varGamma ^n \vdash _c [A]_\varGamma : [B]_\varGamma$ for $n \le$ the number of elements in $\varGamma$. Hence $[A]_\varGamma \rightarrow \!\!\!\!\rightarrow _{\overline{c}} \Box$ and by SR, $\varGamma ^n \vdash _c \Box : [B]_\varGamma$ contradicting Lemma 22.

 $\square$