Alpha-conversion for lambda terms with explicit weakenings
George Cherevichenko
Abstract
Using explicit weakenings, we can define alpha-conversion by simple equations without any mention of free variables.
1 Terms and alpha-conversion
The set of terms Λ ↑ \Lambda\!\uparrow\! Λ ↑ 1 . A term of the form ↑ M \uparrow\!M ↑ M M [ ↑ ] M[\uparrow\!\,] M [ ↑ ] λ x ↑ M \lambda\mathsf{x}\!\uparrow\!M λ x ↑ M λ x ( M [ ↑ ] ) \lambda\mathsf{x}(M[\uparrow\!\,]) λ x ( M [ ↑ ]) ↑ λ x M \uparrow\!\lambda\mathsf{x}M ↑ λ x M ( λ x M ) [ ↑ ] (\lambda\mathsf{x}M)[\uparrow\!\,] ( λ x M ) [ ↑ ] F : Λ ↑ → Λ ↑ F\colon\Lambda\!\uparrow\!\,\,\to\Lambda\!\uparrow\! F : Λ ↑ → Λ ↑ F F F { y x } \{\mathsf{y}\mathsf{x}\} { yx } { y x } z 1 … z n \{\mathsf{y}\mathsf{x}\}_{\mathsf{z}_{1}\ldots\mathsf{z}_{n}} { yx } z 1 … z n { y x } \{\mathsf{y}\mathsf{x}\} { yx } [ y / x ] [\mathsf{y}/\mathsf{x}] [ y / x ] [ 1 ⋅ ↑ ] [1\cdot\!\uparrow\!\,] [ 1 ⋅ ↑ ] ⟨ F s t , S n d ⟩ \langle Fst,Snd\rangle ⟨ F s t , S n d ⟩ F x F_{\mathsf{x}} F x [ ⇑ F ] [\Uparrow\!F] [ ⇑ F ] F M FM F M F ( M ) F(M) F ( M ) { y x } λ z x \{yx\}\lambda zx { y x } λ z x { y x } ( λ z x ) \{yx\}(\lambda zx) { y x } ( λ z x )
Alpha-conversion is the smallest compatible equivalence relation such that λ x M = α λ y { y x } M \lambda\mathsf{x}M=_{\alpha}\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}M λ x M = α λ y { yx } M x , y , M \mathsf{x},\mathsf{y},M x , y , M 2 .
Example 1.1 **.**λ x z = α λ y z = α λ z ↑ z = α λ x ↑ z = α λ y ↑ z \lambda xz=_{\alpha}\lambda yz=_{\alpha}\lambda z\!\uparrow\!z=_{\alpha}\lambda x\!\uparrow\!z=_{\alpha}\lambda y\!\uparrow\!z λ x z = α λ y z = α λ z ↑ z = α λ x ↑ z = α λ y ↑ z
λ x z = α λ z { z x } z = λ z ↑ z \lambda xz=_{\alpha}\lambda z\{zx\}z=\lambda z\!\uparrow\!z λ x z = α λ z { z x } z = λ z ↑ z
λ y z = α λ z { z y } z = λ z ↑ z \lambda yz=_{\alpha}\lambda z\{zy\}z=\lambda z\!\uparrow\!z λ y z = α λ z { z y } z = λ z ↑ z
λ x z = α λ x { x x } z = λ x ↑ z \lambda xz=_{\alpha}\lambda x\{xx\}z=\lambda x\!\uparrow\!z λ x z = α λ x { xx } z = λ x ↑ z
Example 1.2 **.**λ x λ z x = α λ y λ z y \lambda x\lambda z\,x=_{\alpha}\lambda y\lambda z\,y λ x λ z x = α λ y λ z y
λ x λ z x = α λ y { y x } λ z x = λ y λ z { y x } z x = λ y λ z ↑ { y x } x = λ y λ z ↑ y \lambda x\lambda z\,x=_{\alpha}\lambda y\{yx\}\lambda z\,x=\lambda y\lambda z\{yx\}_{z}\,x=\lambda y\lambda z\uparrow\!\{yx\}\,x=\lambda y\lambda z\uparrow\!y λ x λ z x = α λ y { y x } λ z x = λ y λ z { y x } z x = λ y λ z ↑ { y x } x = λ y λ z ↑ y
λ y λ z y = α λ y { y y } λ z y = λ y λ z { y y } z y = λ y λ z ↑ { y y } y = λ y λ z ↑ y \lambda y\lambda z\,y=_{\alpha}\lambda y\{yy\}\lambda z\,y=\lambda y\lambda z\{yy\}_{z}\,y=\lambda y\lambda z\uparrow\!\{yy\}\,y=\lambda y\lambda z\uparrow\!y λ y λ z y = α λ y { y y } λ z y = λ y λ z { y y } z y = λ y λ z ↑ { y y } y = λ y λ z ↑ y
Definition 1.3 **.**Context is a finite list of variables, may be with repetitions. n i l nil ni l Γ = x , x , y , z \Gamma=x,x,y,z Γ = x , x , y , z Γ , Δ \Gamma,\Delta Γ , Δ Γ \Gamma Γ Δ \Delta Δ
Definition 1.4 **.**{ x 1 x 2 } Γ \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma} { x 1 x 2 } Γ { x 1 x 2 } y 1 … y n \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\mathsf{y}_{1}\ldots\mathsf{y}_{n}} { x 1 x 2 } y 1 … y n Γ = y 1 … y n \Gamma=\mathsf{y}_{1}\ldots\mathsf{y}_{n} Γ = y 1 … y n
{ x 1 x 2 } n i l \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{nil} { x 1 x 2 } ni l { x 1 x 2 } \{\mathsf{x}_{1}\mathsf{x}_{2}\} { x 1 x 2 }
Note that
{ x 1 x 2 } Γ , y ↑ M = ↑ { x 1 x 2 } Γ M \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma,\mathsf{y}}\!\uparrow\!M=\,\uparrow\!\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma}M { x 1 x 2 } Γ , y ↑ M = ↑ { x 1 x 2 } Γ M
{ x 1 x 2 } Γ , y y = y \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma,\mathsf{y}}\,\mathsf{y}=\mathsf{y} { x 1 x 2 } Γ , y y = y
{ x 1 x 2 } Γ , y z = ↑ { x 1 x 2 } Γ z \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma,\mathsf{y}}\,\mathsf{z}=\,\uparrow\!\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma}\,\mathsf{z} { x 1 x 2 } Γ , y z = ↑ { x 1 x 2 } Γ z z ≠ y \mathsf{z}\neq\mathsf{y} z = y
Lemma 1.5 **.**{ x 1 x 2 } { x 2 x 3 } M = { x 1 x 3 } M \{\mathsf{x}_{1}\mathsf{x}_{2}\}\{\mathsf{x}_{2}\mathsf{x}_{3}\}M=\{\mathsf{x}_{1}\mathsf{x}_{3}\}M { x 1 x 2 } { x 2 x 3 } M = { x 1 x 3 } M
Proof.
We shall prove the stronger statement
{ x 1 x 2 } Γ { x 2 x 3 } Γ M = { x 1 x 3 } Γ M \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Gamma}\,M=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Gamma}\,M { x 1 x 2 } Γ { x 2 x 3 } Γ M = { x 1 x 3 } Γ M
(Γ \Gamma Γ M M M
Case 1. M = λ y N M=\lambda\mathsf{y}N M = λ y N
Prove the induction step
tensy
\penalty 1 { x 1 x 2 } Γ , y { x 2 x 3 } Γ , y N = { x 1 x 3 } Γ , y N \displaystyle\penalty 1\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma,\mathsf{y}}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Gamma,\mathsf{y}}\,N=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Gamma,\mathsf{y}}\,N \penalty 1 { x 1 x 2 } Γ , y { x 2 x 3 } Γ , y N = { x 1 x 3 } Γ , y N
{ x 1 x 2 } Γ { x 2 x 3 } Γ λ y N = { x 1 x 3 } Γ λ y N \displaystyle\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Gamma}\,\lambda\mathsf{y}N=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Gamma}\,\lambda\mathsf{y}N { x 1 x 2 } Γ { x 2 x 3 } Γ λ y N = { x 1 x 3 } Γ λ y N
This is true because
{ x 1 x 2 } Γ { x 2 x 3 } Γ λ y N = λ y { x 1 x 2 } Γ , y { x 2 x 3 } Γ , y N \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Gamma}\,\lambda\mathsf{y}N=\lambda\mathsf{y}\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Gamma,\mathsf{y}}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Gamma,\mathsf{y}}\,N { x 1 x 2 } Γ { x 2 x 3 } Γ λ y N = λ y { x 1 x 2 } Γ , y { x 2 x 3 } Γ , y N
{ x 1 x 3 } Γ λ y N = λ y { x 1 x 3 } Γ , y N \{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Gamma}\,\lambda\mathsf{y}N=\lambda\mathsf{y}\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Gamma,\mathsf{y}}\,N { x 1 x 3 } Γ λ y N = λ y { x 1 x 3 } Γ , y N
Case 2. M M M z \mathsf{z} z Γ \Gamma Γ
Suppose Γ = n i l \Gamma=nil Γ = ni l
{ x 1 x 2 } { x 2 x 3 } z = { x 1 x 3 } z \{\mathsf{x}_{1}\mathsf{x}_{2}\}\{\mathsf{x}_{2}\mathsf{x}_{3}\}\mathsf{z}=\{\mathsf{x}_{1}\mathsf{x}_{3}\}\mathsf{z} { x 1 x 2 } { x 2 x 3 } z = { x 1 x 3 } z
If z = x 3 \mathsf{z}=\mathsf{x}_{3} z = x 3
{ x 1 x 2 } { x 2 x 3 } x 3 = x 1 = { x 1 x 3 } x 3 \{\mathsf{x}_{1}\mathsf{x}_{2}\}\{\mathsf{x}_{2}\mathsf{x}_{3}\}\mathsf{x}_{3}=\mathsf{x}_{1}=\{\mathsf{x}_{1}\mathsf{x}_{3}\}\mathsf{x}_{3} { x 1 x 2 } { x 2 x 3 } x 3 = x 1 = { x 1 x 3 } x 3
If z ≠ x 3 \mathsf{z}\neq\mathsf{x}_{3} z = x 3
{ x 1 x 2 } { x 2 x 3 } z = ↑ z = { x 1 x 3 } z \{\mathsf{x}_{1}\mathsf{x}_{2}\}\{\mathsf{x}_{2}\mathsf{x}_{3}\}\mathsf{z}=\,\uparrow\!\mathsf{z}=\{\mathsf{x}_{1}\mathsf{x}_{3}\}\mathsf{z} { x 1 x 2 } { x 2 x 3 } z = ↑ z = { x 1 x 3 } z
Suppose Γ = Δ , y \Gamma=\Delta,\mathsf{y} Γ = Δ , y
tensy
\penalty 1 { x 1 x 2 } Δ { x 2 x 3 } Δ z = { x 1 x 3 } Δ z \displaystyle\penalty 1\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta}\,\mathsf{z}=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta}\,\mathsf{z} \penalty 1 { x 1 x 2 } Δ { x 2 x 3 } Δ z = { x 1 x 3 } Δ z
{ x 1 x 2 } Δ , y { x 2 x 3 } Δ , y z = { x 1 x 3 } Δ , y z \displaystyle\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta,\mathsf{y}}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\,\mathsf{z}=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\,\mathsf{z} { x 1 x 2 } Δ , y { x 2 x 3 } Δ , y z = { x 1 x 3 } Δ , y z
If z = y \mathsf{z}=\mathsf{y} z = y
{ x 1 x 2 } Δ , y { x 2 x 3 } Δ , y y = y = { x 1 x 3 } Δ , y y \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta,\mathsf{y}}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\,\mathsf{y}=\mathsf{y}=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\,\mathsf{y} { x 1 x 2 } Δ , y { x 2 x 3 } Δ , y y = y = { x 1 x 3 } Δ , y y
If z ≠ y \mathsf{z}\neq\mathsf{y} z = y
{ x 1 x 2 } Δ , y { x 2 x 3 } Δ , y z = ↑ { x 1 x 2 } Δ { x 2 x 3 } Δ z \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta,\mathsf{y}}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\,\mathsf{z}=\,\uparrow\!\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta}\,\mathsf{z} { x 1 x 2 } Δ , y { x 2 x 3 } Δ , y z = ↑ { x 1 x 2 } Δ { x 2 x 3 } Δ z
{ x 1 x 3 } Δ , y z = ↑ { x 1 x 3 } Δ z \{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\,\mathsf{z}=\,\uparrow\!\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta}\,\mathsf{z} { x 1 x 3 } Δ , y z = ↑ { x 1 x 3 } Δ z
Case 3. M = ↑ N M=\,\uparrow\!N M = ↑ N
If Γ = n i l \Gamma=nil Γ = ni l
{ x 1 x 2 } { x 2 x 3 } ↑ N = ↑ N = { x 1 x 3 } ↑ N \{\mathsf{x}_{1}\mathsf{x}_{2}\}\{\mathsf{x}_{2}\mathsf{x}_{3}\}\uparrow\!N=\,\uparrow\!N=\{\mathsf{x}_{1}\mathsf{x}_{3}\}\uparrow\!N { x 1 x 2 } { x 2 x 3 } ↑ N = ↑ N = { x 1 x 3 } ↑ N
If Γ = Δ , y \Gamma=\Delta,\mathsf{y} Γ = Δ , y M M M
tensy
\penalty 1 { x 1 x 2 } Δ { x 2 x 3 } Δ N = { x 1 x 3 } Δ N \displaystyle\penalty 1\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta}\,N=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta}\,N \penalty 1 { x 1 x 2 } Δ { x 2 x 3 } Δ N = { x 1 x 3 } Δ N
{ x 1 x 2 } Δ , y { x 2 x 3 } Δ , y ↑ N = { x 1 x 3 } Δ , y ↑ N \displaystyle\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta,\mathsf{y}}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\uparrow\!N=\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\uparrow\!N { x 1 x 2 } Δ , y { x 2 x 3 } Δ , y ↑ N = { x 1 x 3 } Δ , y ↑ N
because
{ x 1 x 2 } Δ , y { x 2 x 3 } Δ , y ↑ N = ↑ { x 1 x 2 } Δ { x 2 x 3 } Δ N \{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta,\mathsf{y}}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\uparrow\!N=\,\uparrow\!\{\mathsf{x}_{1}\mathsf{x}_{2}\}_{\Delta}\{\mathsf{x}_{2}\mathsf{x}_{3}\}_{\Delta}\,N { x 1 x 2 } Δ , y { x 2 x 3 } Δ , y ↑ N = ↑ { x 1 x 2 } Δ { x 2 x 3 } Δ N
{ x 1 x 3 } Δ , y ↑ N = ↑ { x 1 x 3 } Δ N \{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta,\mathsf{y}}\uparrow\!N=\,\uparrow\!\{\mathsf{x}_{1}\mathsf{x}_{3}\}_{\Delta}\,N { x 1 x 3 } Δ , y ↑ N = ↑ { x 1 x 3 } Δ N
Case 4. M = N 1 N 2 M=N_{1}N_{2} M = N 1 N 2
Straightforward, because F ( N 1 N 2 ) = F ( N 1 ) F ( N 2 ) F(N_{1}N_{2})=F(N_{1})F(N_{2}) F ( N 1 N 2 ) = F ( N 1 ) F ( N 2 )
Lemma 1.6 **.**{ y x } F x M = F y { y x } M \{\mathsf{y}\mathsf{x}\}F_{\mathsf{x}}M=F_{\mathsf{y}}\{\mathsf{y}\mathsf{x}\}M { yx } F x M = F y { yx } M
Proof.
We shall prove the stronger statement
{ y x } Γ F x , Γ M = F y , Γ { y x } Γ M \{\mathsf{y}\mathsf{x}\}_{\Gamma}\,F_{\mathsf{x},\Gamma}\,M=F_{\mathsf{y},\Gamma}\,\{\mathsf{y}\mathsf{x}\}_{\Gamma}\,M { yx } Γ F x , Γ M = F y , Γ { yx } Γ M
(Γ \Gamma Γ M M M
Case 1. M = λ z N M=\lambda\mathsf{z}N M = λ z N
Prove the induction step
tensy
\penalty 1 { y x } Γ , z F x , Γ , z N = F y , Γ , z { y x } Γ , z N \displaystyle\penalty 1\{\mathsf{y}\mathsf{x}\}_{\Gamma,\mathsf{z}}\,F_{\mathsf{x},\Gamma,\mathsf{z}}\,N=F_{\mathsf{y},\Gamma,\mathsf{z}}\,\{\mathsf{y}\mathsf{x}\}_{\Gamma,\mathsf{z}}\,N \penalty 1 { yx } Γ , z F x , Γ , z N = F y , Γ , z { yx } Γ , z N
{ y x } Γ F x , Γ λ z N = F y , Γ { y x } Γ λ z N \displaystyle\{\mathsf{y}\mathsf{x}\}_{\Gamma}\,F_{\mathsf{x},\Gamma}\,\lambda\mathsf{z}N=F_{\mathsf{y},\Gamma}\,\{\mathsf{y}\mathsf{x}\}_{\Gamma}\,\lambda\mathsf{z}N { yx } Γ F x , Γ λ z N = F y , Γ { yx } Γ λ z N
This is true because
{ y x } Γ F x , Γ λ z N = λ z { y x } Γ , z F x , Γ , z N \{\mathsf{y}\mathsf{x}\}_{\Gamma}\,F_{\mathsf{x},\Gamma}\,\lambda\mathsf{z}N=\lambda\mathsf{z}\,\{\mathsf{y}\mathsf{x}\}_{\Gamma,\mathsf{z}}\,F_{\mathsf{x},\Gamma,\mathsf{z}}\,N { yx } Γ F x , Γ λ z N = λ z { yx } Γ , z F x , Γ , z N
F y , Γ { y x } Γ λ z N = λ z F y , Γ , z { y x } Γ , z N F_{\mathsf{y},\Gamma}\,\{\mathsf{y}\mathsf{x}\}_{\Gamma}\,\lambda\mathsf{z}N=\lambda\mathsf{z}\,F_{\mathsf{y},\Gamma,\mathsf{z}}\,\{\mathsf{y}\mathsf{x}\}_{\Gamma,\mathsf{z}}\,N F y , Γ { yx } Γ λ z N = λ z F y , Γ , z { yx } Γ , z N
Case 2. M M M z \mathsf{z} z Δ \Delta Δ
Suppose Γ = n i l \Gamma=nil Γ = ni l
{ y x } F x z = F y { y x } z \{\mathsf{y}\mathsf{x}\}F_{\mathsf{x}}\,\mathsf{z}=F_{\mathsf{y}}\{\mathsf{y}\mathsf{x}\}\mathsf{z} { yx } F x z = F y { yx } z
If z = x \mathsf{z}=\mathsf{x} z = x
{ y x } F x x = y = F y { y x } x \{\mathsf{y}\mathsf{x}\}F_{\mathsf{x}}\,\mathsf{x}=\mathsf{y}=F_{\mathsf{y}}\{\mathsf{y}\mathsf{x}\}\mathsf{x} { yx } F x x = y = F y { yx } x
If z ≠ x \mathsf{z}\neq\mathsf{x} z = x
{ y x } F x z = ↑ F z = F y { y x } z \{\mathsf{y}\mathsf{x}\}F_{\mathsf{x}}\,\mathsf{z}=\,\uparrow\!F\mathsf{z}=F_{\mathsf{y}}\{\mathsf{y}\mathsf{x}\}\mathsf{z} { yx } F x z = ↑ F z = F y { yx } z
Suppose Γ = Δ , w \Gamma=\Delta,\mathsf{w} Γ = Δ , w
tensy
\penalty 1 { y x } Δ F x , Δ z = F y , Δ { y x } Δ z \displaystyle\penalty 1\{\mathsf{y}\mathsf{x}\}_{\Delta}F_{\mathsf{x},\Delta}\,\mathsf{z}=F_{\mathsf{y},\Delta}\{\mathsf{y}\mathsf{x}\}_{\Delta}\,\mathsf{z} \penalty 1 { yx } Δ F x , Δ z = F y , Δ { yx } Δ z
{ y x } Δ , w F x , Δ , w z = F y , Δ , w { y x } Δ , w z \displaystyle\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}F_{\mathsf{x},\Delta,\mathsf{w}}\,\mathsf{z}=F_{\mathsf{y},\Delta,\mathsf{w}}\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}\,\mathsf{z} { yx } Δ , w F x , Δ , w z = F y , Δ , w { yx } Δ , w z
If z = w \mathsf{z}=\mathsf{w} z = w
{ y x } Δ , w F x , Δ , w w = w = F y , Δ , w { y x } Δ , w w \{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}F_{\mathsf{x},\Delta,\mathsf{w}}\,\mathsf{w}=\mathsf{w}=F_{\mathsf{y},\Delta,\mathsf{w}}\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}\,\mathsf{w} { yx } Δ , w F x , Δ , w w = w = F y , Δ , w { yx } Δ , w w
If z ≠ w \mathsf{z}\neq\mathsf{w} z = w
{ y x } Δ , w F x , Δ , w z = ↑ { y x } Δ F x , Δ z \{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}F_{\mathsf{x},\Delta,\mathsf{w}}\,\mathsf{z}=\,\uparrow\!\{\mathsf{y}\mathsf{x}\}_{\Delta}F_{\mathsf{x},\Delta}\,\mathsf{z} { yx } Δ , w F x , Δ , w z = ↑ { yx } Δ F x , Δ z
F y , Δ , w { y x } Δ , w z = ↑ F y , Δ { y x } Δ z F_{\mathsf{y},\Delta,\mathsf{w}}\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}\,\mathsf{z}=\,\uparrow\!F_{\mathsf{y},\Delta}\{\mathsf{y}\mathsf{x}\}_{\Delta}\,\mathsf{z} F y , Δ , w { yx } Δ , w z = ↑ F y , Δ { yx } Δ z
Case 3. M = ↑ N M=\,\uparrow\!N M = ↑ N
If Γ = n i l \Gamma=nil Γ = ni l
{ y x } F x ↑ N = ↑ F N = F y { y x } ↑ N \{\mathsf{y}\mathsf{x}\}F_{\mathsf{x}}\!\uparrow\!N=\,\uparrow\!FN=F_{\mathsf{y}}\{\mathsf{y}\mathsf{x}\}\!\uparrow\!N { yx } F x ↑ N = ↑ F N = F y { yx } ↑ N
If Γ = Δ , w \Gamma=\Delta,\mathsf{w} Γ = Δ , w M M M
tensy
\penalty 1 { y x } Δ F x , Δ N = F y , Δ { y x } Δ N \displaystyle\penalty 1\{\mathsf{y}\mathsf{x}\}_{\Delta}F_{\mathsf{x},\Delta}\,N=F_{\mathsf{y},\Delta}\{\mathsf{y}\mathsf{x}\}_{\Delta}\,N \penalty 1 { yx } Δ F x , Δ N = F y , Δ { yx } Δ N
{ y x } Δ , w F x , Δ , w ↑ N = F y , Δ , w { y x } Δ , w ↑ N \displaystyle\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}F_{\mathsf{x},\Delta,\mathsf{w}}\uparrow\!N=F_{\mathsf{y},\Delta,\mathsf{w}}\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}\uparrow\!N { yx } Δ , w F x , Δ , w ↑ N = F y , Δ , w { yx } Δ , w ↑ N
because
{ y x } Δ , w F x , Δ , w ↑ N = ↑ { y x } Δ F x , Δ N \{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}F_{\mathsf{x},\Delta,\mathsf{w}}\uparrow\!N=\,\uparrow\!\{\mathsf{y}\mathsf{x}\}_{\Delta}F_{\mathsf{x},\Delta}\,N { yx } Δ , w F x , Δ , w ↑ N = ↑ { yx } Δ F x , Δ N
F y , Δ , w { y x } Δ , w ↑ N = ↑ F y , Δ { y x } Δ N F_{\mathsf{y},\Delta,\mathsf{w}}\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{w}}\uparrow\!N=\,\uparrow\!F_{\mathsf{y},\Delta}\{\mathsf{y}\mathsf{x}\}_{\Delta}\,N F y , Δ , w { yx } Δ , w ↑ N = ↑ F y , Δ { yx } Δ N
Case 4. M = N 1 N 2 M=N_{1}N_{2} M = N 1 N 2
Straightforward, because F ( N 1 N 2 ) = F ( N 1 ) F ( N 2 ) F(N_{1}N_{2})=F(N_{1})F(N_{2}) F ( N 1 N 2 ) = F ( N 1 ) F ( N 2 )
Theorem 1.7 **.**If M = α N M=_{\alpha}N M = α N F ( M ) = α F ( N ) F(M)=_{\alpha}F(N) F ( M ) = α F ( N )
Proof.
We need to prove F λ x M = α F λ y { y x } M F\lambda\mathsf{x}M=_{\alpha}F\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}M F λ x M = α F λ y { yx } M
F λ x M = λ x F x M = α λ y { y x } F x M = λ y F y { y x } M = F λ y { y x } M F\lambda\mathsf{x}M=\lambda\mathsf{x}F_{\mathsf{x}}M=_{\alpha}\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}F_{\mathsf{x}}M=\lambda\mathsf{y}F_{\mathsf{y}}\{\mathsf{y}\mathsf{x}\}M=F\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}M F λ x M = λ x F x M = α λ y { yx } F x M = λ y F y { yx } M = F λ y { yx } M
(the third equality by the previous lemma).
∎
2 de Bruijn’s terms
For each variable z \mathsf{z} z M M M d b z ( M ) db_{\mathsf{z}}(M) d b z ( M ) M = α N M=_{\alpha}N M = α N d b z ( M ) = d b z ( N ) db_{\mathsf{z}}(M)=db_{\mathsf{z}}(N) d b z ( M ) = d b z ( N )
Definition 2.1 **.**d b z ( x ) = x db_{\mathsf{z}}(\mathsf{x})=\mathsf{x} d b z ( x ) = x
d b z ( ↑ M ) = ↑ d b z ( M ) db_{\mathsf{z}}(\uparrow\!M)=\,\uparrow\!db_{\mathsf{z}}(M) d b z ( ↑ M ) = ↑ d b z ( M )
d b z ( M N ) = d b z ( M ) d b z ( N ) db_{\mathsf{z}}(MN)=db_{\mathsf{z}}(M)db_{\mathsf{z}}(N) d b z ( M N ) = d b z ( M ) d b z ( N )
d b z ( λ x M ) = λ z { z x } d b z ( M ) db_{\mathsf{z}}(\lambda\mathsf{x}M)=\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(M) d b z ( λ x M ) = λ z { zx } d b z ( M )
Example 2.2 **.**d b z ( λ x λ y y ) = λ z λ z z db_{z}(\lambda x\lambda y\,y)=\lambda z\lambda z\,z d b z ( λ x λ y y ) = λ z λ z z
d b z ( λ x λ y x ) = λ z λ z ↑ z db_{z}(\lambda x\lambda y\,x)=\lambda z\lambda z\uparrow\!z d b z ( λ x λ y x ) = λ z λ z ↑ z d b db d b
d b z ( λ y x ) = λ z ↑ x db_{z}(\lambda y\,x)=\lambda z\uparrow\!x d b z ( λ y x ) = λ z ↑ x
Lemma 2.3 **.**d b z ( M ) = α M db_{\mathsf{z}}(M)=_{\alpha}M d b z ( M ) = α M
Proof.
Induction on the structure of M M M
If M = λ x N M=\lambda\mathsf{x}N M = λ x N d b z ( N ) = α N db_{\mathsf{z}}(N)=_{\alpha}N d b z ( N ) = α N
d b z ( λ x N ) = λ z { z x } d b z ( N ) = α λ x d b z ( N ) = α λ x N db_{\mathsf{z}}(\lambda\mathsf{x}N)=\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(N)=_{\alpha}\lambda\mathsf{x}\,db_{\mathsf{z}}(N)=_{\alpha}\lambda\mathsf{x}N d b z ( λ x N ) = λ z { zx } d b z ( N ) = α λ x d b z ( N ) = α λ x N
∎
Theorem 2.4 **.**If d b z ( M ) = d b z ( N ) db_{\mathsf{z}}(M)=db_{\mathsf{z}}(N) d b z ( M ) = d b z ( N ) M = α N M=_{\alpha}N M = α N
Proof.
M = α d b z ( M ) = d b z ( N ) = α N M=_{\alpha}db_{\mathsf{z}}(M)=db_{\mathsf{z}}(N)=_{\alpha}N M = α d b z ( M ) = d b z ( N ) = α N
Lemma 2.5 **.**F ( d b z M ) = d b z ( F M ) F(db_{\mathsf{z}}M)=db_{\mathsf{z}}(FM) F ( d b z M ) = d b z ( F M )
Proof.
Induction on the structure of M M M
Case 1. If M = λ x N M=\lambda\mathsf{x}N M = λ x N
F ( d b z ( λ x N ) ) = F λ z { z x } d b z ( N ) = λ z F z { z x } d b z ( N ) = λ z { z x } F x d b z ( N ) F(db_{\mathsf{z}}(\lambda\mathsf{x}N))=F\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(N)=\lambda\mathsf{z}F_{\mathsf{z}}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(N)=\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}F_{\mathsf{x}}\,db_{\mathsf{z}}(N) F ( d b z ( λ x N )) = F λ z { zx } d b z ( N ) = λ z F z { zx } d b z ( N ) = λ z { zx } F x d b z ( N )
the last equality by Lemma 1.6
d b z ( F λ x N ) = d b z ( λ x F x N ) = λ z { z x } d b z ( F x N ) db_{\mathsf{z}}(F\lambda\mathsf{x}N)=db_{\mathsf{z}}(\lambda\mathsf{x}F_{\mathsf{x}}N)=\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(F_{\mathsf{x}}N) d b z ( F λ x N ) = d b z ( λ x F x N ) = λ z { zx } d b z ( F x N )
but F x d b z ( N ) = d b z ( F x N ) F_{\mathsf{x}}\,db_{\mathsf{z}}(N)=db_{\mathsf{z}}(F_{\mathsf{x}}N) F x d b z ( N ) = d b z ( F x N )
Case 2. If M M M y \mathsf{y} y
F ( d b z y ) = F y F(db_{\mathsf{z}}\mathsf{y})=F\mathsf{y} F ( d b z y ) = F y
d b z ( F y ) = F y db_{\mathsf{z}}(F\mathsf{y})=F\mathsf{y} d b z ( F y ) = F y F y F\mathsf{y} F y ↑ … ↑ ⏟ n \underbrace{\uparrow\!\ldots\uparrow\!}_{n} n ↑ … ↑
More rigorously, use induction on the structure of F F F 1 ).
Suppose F F F { x 1 x 2 } \{\mathsf{x}_{1}\mathsf{x}_{2}\} { x 1 x 2 }
d b z ( { x 1 x 2 } y ) = { x 1 x 2 } y db_{\mathsf{z}}(\{\mathsf{x}_{1}\mathsf{x}_{2}\}\mathsf{y})=\{\mathsf{x}_{1}\mathsf{x}_{2}\}\mathsf{y} d b z ({ x 1 x 2 } y ) = { x 1 x 2 } y
If y = x 2 \mathsf{y}=\mathsf{x}_{2} y = x 2
d b z ( { x 1 x 2 } x 2 ) = d b z ( x 1 ) = x 1 = { x 1 x 2 } x 2 db_{\mathsf{z}}(\{\mathsf{x}_{1}\mathsf{x}_{2}\}\mathsf{x}_{2})=db_{\mathsf{z}}(\mathsf{x}_{1})=\mathsf{x}_{1}=\{\mathsf{x}_{1}\mathsf{x}_{2}\}\mathsf{x}_{2} d b z ({ x 1 x 2 } x 2 ) = d b z ( x 1 ) = x 1 = { x 1 x 2 } x 2
If y ≠ x 2 \mathsf{y}\neq\mathsf{x}_{2} y = x 2
d b z ( { x 1 x 2 } y ) = d b z ( ↑ y ) = ↑ d b z ( y ) = ↑ y = { x 1 x 2 } y db_{\mathsf{z}}(\{\mathsf{x}_{1}\mathsf{x}_{2}\}\mathsf{y})=db_{\mathsf{z}}(\uparrow\!\mathsf{y})=\,\uparrow\!db_{\mathsf{z}}(\mathsf{y})=\,\uparrow\!\mathsf{y}=\{\mathsf{x}_{1}\mathsf{x}_{2}\}\mathsf{y} d b z ({ x 1 x 2 } y ) = d b z ( ↑ y ) = ↑ d b z ( y ) = ↑ y = { x 1 x 2 } y
Now prove the induction step
tensy
\penalty 1 d b z ( F y ) = F y \displaystyle\penalty 1db_{\mathsf{z}}(F\mathsf{y})=F\mathsf{y} \penalty 1 d b z ( F y ) = F y
d b z ( F x y ) = F x y \displaystyle db_{\mathsf{z}}(F_{\mathsf{x}}\mathsf{y})=F_{\mathsf{x}}\mathsf{y} d b z ( F x y ) = F x y
If y = x \mathsf{y}=\mathsf{x} y = x
d b z ( F x x ) = d b z ( x ) = x = F x x db_{\mathsf{z}}(F_{\mathsf{x}}\,\mathsf{x})=db_{\mathsf{z}}(\mathsf{x})=\mathsf{x}=F_{\mathsf{x}}\,\mathsf{x} d b z ( F x x ) = d b z ( x ) = x = F x x
If y ≠ x \mathsf{y}\neq\mathsf{x} y = x
d b z ( F x y ) = d b z ( ↑ F y ) = ↑ d b z ( F y ) db_{\mathsf{z}}(F_{\mathsf{x}}\,\mathsf{y})=db_{\mathsf{z}}(\uparrow\!F\mathsf{y})=\,\uparrow\!db_{\mathsf{z}}(F\mathsf{y}) d b z ( F x y ) = d b z ( ↑ F y ) = ↑ d b z ( F y )
F x y = ↑ F y F_{\mathsf{x}}\,\mathsf{y}=\,\uparrow\!F\mathsf{y} F x y = ↑ F y
Case 3. Suppose M = ↑ N M=\,\uparrow\!N M = ↑ N
If F F F { x 2 , x 1 } \{\mathsf{x}_{2},\mathsf{x}_{1}\} { x 2 , x 1 }
{ x 1 , x 2 } d b z ( ↑ N ) = { x 1 , x 2 } ↑ d b z ( N ) = ↑ d b z ( N ) \{\mathsf{x}_{1},\mathsf{x}_{2}\}\,db_{\mathsf{z}}(\uparrow\!N)=\{\mathsf{x}_{1},\mathsf{x}_{2}\}\!\uparrow\!db_{\mathsf{z}}(N)=\,\uparrow\!db_{\mathsf{z}}(N) { x 1 , x 2 } d b z ( ↑ N ) = { x 1 , x 2 } ↑ d b z ( N ) = ↑ d b z ( N )
d b z ( { x 1 , x 2 } ↑ N ) = d b z ( ↑ N ) = ↑ d b z ( N ) db_{\mathsf{z}}(\{\mathsf{x}_{1},\mathsf{x}_{2}\}\!\uparrow\!N)=db_{\mathsf{z}}(\uparrow\!N)=\,\uparrow\!db_{\mathsf{z}}(N) d b z ({ x 1 , x 2 } ↑ N ) = d b z ( ↑ N ) = ↑ d b z ( N )
If function has the form F x F_{\mathsf{x}} F x M M M
tensy
\penalty 1 d b z ( F N ) = F N \displaystyle\penalty 1db_{\mathsf{z}}(FN)=FN \penalty 1 d b z ( F N ) = F N
d b z ( F x ↑ N ) = F x ↑ N \displaystyle db_{\mathsf{z}}(F_{\mathsf{x}}\!\uparrow\!N)=F_{\mathsf{x}}\!\uparrow\!N d b z ( F x ↑ N ) = F x ↑ N
because
d b z ( F x ↑ N ) = d b z ( ↑ F N ) = ↑ d b z ( F N ) db_{\mathsf{z}}(F_{\mathsf{x}}\!\uparrow\!N)=db_{\mathsf{z}}(\uparrow\!FN)=\,\uparrow\!db_{\mathsf{z}}(FN) d b z ( F x ↑ N ) = d b z ( ↑ F N ) = ↑ d b z ( F N )
F x ↑ N = ↑ F N F_{\mathsf{x}}\!\uparrow\!N=\,\uparrow\!FN F x ↑ N = ↑ F N
Case 4. M = N 1 N 2 M=N_{1}N_{2} M = N 1 N 2
Straighforward.
∎
Theorem 2.6 **.**If M = α N M=_{\alpha}N M = α N d b z ( M ) = d b z ( N ) db_{\mathsf{z}}(M)=db_{\mathsf{z}}(N) d b z ( M ) = d b z ( N )
Proof.
We need to prove d b z ( λ x M ) = d b z ( λ y { y x } M ) db_{\mathsf{z}}(\lambda\mathsf{x}M)=db_{\mathsf{z}}(\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}M) d b z ( λ x M ) = d b z ( λ y { yx } M )
d b z ( λ x M ) = λ z { z x } d b z ( M ) db_{\mathsf{z}}(\lambda\mathsf{x}M)=\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(M) d b z ( λ x M ) = λ z { zx } d b z ( M )
d b z ( λ y { y x } M ) = db_{\mathsf{z}}(\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}M)= d b z ( λ y { yx } M ) =
= λ z { z y } d b z ( { y x } M ) =\lambda\mathsf{z}\{\mathsf{z}\mathsf{y}\}db_{\mathsf{z}}(\{\mathsf{y}\mathsf{x}\}M) = λ z { zy } d b z ({ yx } M )
= λ z { z y } { y x } d b z ( M ) =\lambda\mathsf{z}\{\mathsf{z}\mathsf{y}\}\{\mathsf{y}\mathsf{x}\}db_{\mathsf{z}}(M) = λ z { zy } { yx } d b z ( M )
= λ z { z x } d b z ( M ) =\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(M) = λ z { zx } d b z ( M ) 1.5 )
∎
Theorem 2.7 **.**λ x M = α λ y N \lambda\mathsf{x}M=_{\alpha}\lambda\mathsf{y}N λ x M = α λ y N { z x } M = α { z y } N \{\mathsf{z}\mathsf{x}\}M=_{\alpha}\{\mathsf{z}\mathsf{y}\}N { zx } M = α { zy } N
Proof.
Suppose { z x } M = α { z y } N \{\mathsf{z}\mathsf{x}\}M=_{\alpha}\{\mathsf{z}\mathsf{y}\}N { zx } M = α { zy } N
λ z { z x } M = α λ z { z y } N \lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}M=_{\alpha}\lambda\mathsf{z}\{\mathsf{z}\mathsf{y}\}N λ z { zx } M = α λ z { zy } N
and
λ x M = α λ z { z x } M = α λ z { z y } N = α λ y N \lambda\mathsf{x}M=_{\alpha}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}M=_{\alpha}\lambda\mathsf{z}\{\mathsf{z}\mathsf{y}\}N=_{\alpha}\lambda\mathsf{y}N λ x M = α λ z { zx } M = α λ z { zy } N = α λ y N
Suppose λ x M = α λ y N \lambda\mathsf{x}M=_{\alpha}\lambda\mathsf{y}N λ x M = α λ y N
d b z ( λ x M ) = d b z ( λ y N ) db_{\mathsf{z}}(\lambda\mathsf{x}M)=db_{\mathsf{z}}(\lambda\mathsf{y}N) d b z ( λ x M ) = d b z ( λ y N )
λ z { z x } d b z ( M ) = λ z { z y } d b z ( N ) \lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(M)=\lambda\mathsf{z}\{\mathsf{z}\mathsf{y}\}db_{\mathsf{z}}(N) λ z { zx } d b z ( M ) = λ z { zy } d b z ( N )
{ z x } d b z ( M ) = { z y } d b z ( N ) \{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(M)=\{\mathsf{z}\mathsf{y}\}db_{\mathsf{z}}(N) { zx } d b z ( M ) = { zy } d b z ( N )
and { z x } M = α { z y } N \{\mathsf{z}\mathsf{x}\}M=_{\alpha}\{\mathsf{z}\mathsf{y}\}N { zx } M = α { zy } N
M = α d b z ( M ) M=_{\alpha}db_{\mathsf{z}}(M) M = α d b z ( M )
N = α d b z ( N ) N=_{\alpha}db_{\mathsf{z}}(N) N = α d b z ( N )
∎
3 de Bruijn’s terms 2
The set of inference rules is shown in Tab. 3 . Note that for each Γ , M \Gamma,M Γ , M Γ ⊢ M \Gamma\vdash M Γ ⊢ M
Lemma 3.1 **.**For each Γ , M \Gamma,M Γ , M Γ ⊢ M \Gamma\vdash M Γ ⊢ M
Proof.
Induction on the structure of M M M
Case 1. M M M x \mathsf{x} x Γ \Gamma Γ
If Γ = n i l \Gamma=nil Γ = ni l n i l ⊢ x nil\vdash\mathsf{x} ni l ⊢ x
If Γ = Δ , z \Gamma=\Delta,\mathsf{z} Γ = Δ , z
Δ , x ⊢ x \Delta,\mathsf{x}\vdash\mathsf{x} Δ , x ⊢ x z = x \mathsf{z}=\mathsf{x} z = x
tensy
\penalty 1 Δ ⊢ x \displaystyle\penalty 1\Delta\vdash\mathsf{x} \penalty 1Δ ⊢ x
Δ , z ⊢ x \displaystyle\Delta,\mathsf{z}\vdash\mathsf{x} Δ , z ⊢ x
if z ≠ x \mathsf{z}\neq\mathsf{x} z = x
Case 2. And so on (nothing more to prove).
∎
Example 3.2 **.**The (unique) inference of n i l ⊢ λ x λ y x y z nil\vdash\lambda x\lambda y\,xyz ni l ⊢ λ x λ y x y z
tensy
\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{ \displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 4.853pt\hbox{ \displaystyle\penalty 1x\vdash x}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=32.80307pt\hbox{}}}\hbox{\kern 0.0pt\hbox{ \displaystyle x,y\vdash x}}}}\hskip 5.0pt plus 1.0fil\penalty 2\quad x,y\vdash y }\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=109.37134pt\hbox{}}}\hbox{\kern 35.65334pt\hbox{x , y ⊢ x y \displaystyle x,y\vdash xy x , y ⊢ x y \penalty 1 n i l ⊢ z \displaystyle\penalty 1nil\vdash z \penalty 1 ni l ⊢ z \displaystyle\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 4.853pt\hbox{ \displaystyle\penalty 1x\vdash z}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=32.1781pt\hbox{}}}\hbox{\kern 0.0pt\hbox{ \displaystyle x,y\vdash z}}}}\hskip 5.0pt plus 1.0fil\penalty 2 }}}}\hskip 5.0pt plus 1.0fil\penalty 2}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=254.20595pt\hbox{}}}\hbox{\kern 105.52548pt\hbox{ \displaystyle x,y\vdash xyz}}}}\hskip 5.0pt plus 1.0fil\penalty 2
\displaystyle\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 9.23071pt\hbox{ \displaystyle\penalty 1x\vdash\lambda y,xyz}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=64.67198pt\hbox{}}}\hbox{\kern 0.0pt\hbox{ \displaystyle nil\vdash\lambda x\lambda y,xyz}}}}\hskip 5.0pt plus 1.0fil\penalty 2
Definition 3.3 **.**The set of generalized de Bruin’s terms is shown in Tab. 4 . For each Γ , M \Gamma,M Γ , M ∥ Γ ⊢ M ∥ \|\Gamma\vdash M\| ∥Γ ⊢ M ∥ 4 . Note that we can write these rules shorter:
[TABLE]
Example 3.4 **.**∥ n i l ⊢ λ x λ y x y z ∥ = λ λ ( ↑ 1 ‾ ) 1 ‾ ↑ ↑ z \|nil\vdash\lambda x\lambda y\,xyz\|=\lambda\lambda(\uparrow\!\underline{1})\underline{1}\uparrow\!\,\uparrow\!z ∥ ni l ⊢ λ x λ y x y z ∥ = λλ ( ↑ 1 ) 1 ↑ ↑ z
because
tensy
\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{ \displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 12.63066pt\hbox{ \displaystyle\penalty 1|x\vdash x|=\underline{1}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=75.58058pt\hbox{}}}\hbox{\kern 0.0pt\hbox{ \displaystyle|x,y\vdash x|=,\uparrow!\underline{1}}}}}\hskip 5.0pt plus 1.0fil\penalty 2\quad\|x,y\vdash y\|=\underline{1} }\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=181.59319pt\hbox{}}}\hbox{\kern 46.20876pt\hbox{∥ x , y ⊢ x y ∥ = ( ↑ 1 ‾ ) 1 ‾ \displaystyle\|x,y\vdash xy\|=(\uparrow\!\underline{1})\underline{1} ∥ x , y ⊢ x y ∥ = ( ↑ 1 ) 1 \penalty 1 ∥ n i l ⊢ z ∥ = z \displaystyle\penalty 1\|nil\vdash z\|=z \penalty 1∥ ni l ⊢ z ∥ = z \displaystyle\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 10.13072pt\hbox{ \displaystyle\penalty 1|x\vdash z|=,\uparrow!z}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=85.60133pt\hbox{}}}\hbox{\kern 0.0pt\hbox{ \displaystyle|x,y\vdash z|=,\uparrow!,\uparrow!z}}}}\hskip 5.0pt plus 1.0fil\penalty 2 }}}}\hskip 5.0pt plus 1.0fil\penalty 2}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=379.85101pt\hbox{}}}\hbox{\kern 131.91411pt\hbox{ \displaystyle|x,y\vdash xyz|=(\uparrow!\underline{1})\underline{1}\uparrow!,\uparrow!z}}}}\hskip 5.0pt plus 1.0fil\penalty 2
\displaystyle\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 12.14738pt\hbox{ \displaystyle\penalty 1|x\vdash\lambda y,xyz|=\lambda(\uparrow!\underline{1})\underline{1}\uparrow!,\uparrow!z}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=149.2065pt\hbox{}}}\hbox{\kern 0.0pt\hbox{ \displaystyle|nil\vdash\lambda x\lambda y,xyz|=\lambda\lambda(\uparrow!\underline{1})\underline{1}\uparrow!,\uparrow!z}}}}\hskip 5.0pt plus 1.0fil\penalty 2
Theorem 3.5 **.**If M = α N M=_{\alpha}N M = α N ∥ Γ ⊢ M ∥ = ∥ Γ ⊢ N ∥ \|\Gamma\vdash M\|=\|\Gamma\vdash N\| ∥Γ ⊢ M ∥ = ∥Γ ⊢ N ∥ Γ \Gamma Γ
Proof.
We have to prove
∥ Γ ⊢ λ x M ∥ = ∥ Γ ⊢ λ y { y x } M ∥ \|\Gamma\vdash\lambda\mathsf{x}M\|=\|\Gamma\vdash\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}M\| ∥Γ ⊢ λ x M ∥ = ∥Γ ⊢ λ y { yx } M ∥
It is enough to prove
∥ Γ , x ⊢ M ∥ = ∥ Γ , y ⊢ { y x } M ∥ \|\Gamma,\mathsf{x}\vdash M\|=\|\Gamma,\mathsf{y}\vdash\{\mathsf{y}\mathsf{x}\}M\| ∥Γ , x ⊢ M ∥ = ∥Γ , y ⊢ { yx } M ∥
because
∥ Γ ⊢ λ x M ∥ = λ ∥ Γ , x ⊢ M ∥ \|\Gamma\vdash\lambda\mathsf{x}M\|=\lambda\|\Gamma,\mathsf{x}\vdash M\| ∥Γ ⊢ λ x M ∥ = λ ∥Γ , x ⊢ M ∥
∥ Γ ⊢ λ y { y x } M ∥ = λ ∥ Γ , y ⊢ { y x } M ∥ \|\Gamma\vdash\lambda\mathsf{y}\{\mathsf{y}\mathsf{x}\}M\|=\lambda\|\Gamma,\mathsf{y}\vdash\{\mathsf{y}\mathsf{x}\}M\| ∥Γ ⊢ λ y { yx } M ∥ = λ ∥Γ , y ⊢ { yx } M ∥
We shall prove the stronger statement
∥ Γ , x , Δ ⊢ M ∥ = ∥ Γ , y , Δ ⊢ { y x } Δ M ∥ \|\Gamma,\mathsf{x},\Delta\vdash M\|=\|\Gamma,\mathsf{y},\Delta\vdash\{\mathsf{y}\mathsf{x}\}_{\Delta}\,M\| ∥Γ , x , Δ ⊢ M ∥ = ∥Γ , y , Δ ⊢ { yx } Δ M ∥
for arbitrary Δ \Delta Δ M M M
Case 1. M = λ z N M=\lambda\mathsf{z}N M = λ z N
tensy
\penalty 1 ∥ Γ , x , Δ , z ⊢ N ∥ = ∥ Γ , y , Δ , z ⊢ { y x } Δ , z N ∥ \displaystyle\penalty 1\|\Gamma,\mathsf{x},\Delta,\mathsf{z}\vdash N\|=\|\Gamma,\mathsf{y},\Delta,\mathsf{z}\vdash\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{z}}\,N\| \penalty 1∥Γ , x , Δ , z ⊢ N ∥ = ∥Γ , y , Δ , z ⊢ { yx } Δ , z N ∥
∥ Γ , x , Δ ⊢ λ z N ∥ = ∥ Γ , y , Δ ⊢ { y x } Δ λ z N ∥ \displaystyle\|\Gamma,\mathsf{x},\Delta\vdash\lambda\mathsf{z}N\|=\|\Gamma,\mathsf{y},\Delta\vdash\{\mathsf{y}\mathsf{x}\}_{\Delta}\,\lambda\mathsf{z}N\| ∥Γ , x , Δ ⊢ λ z N ∥ = ∥Γ , y , Δ ⊢ { yx } Δ λ z N ∥
This is true because
∥ Γ , x , Δ ⊢ λ z N ∥ = λ ∥ Γ , x , Δ , z ⊢ N ∥ \|\Gamma,\mathsf{x},\Delta\vdash\lambda\mathsf{z}N\|=\lambda\|\Gamma,\mathsf{x},\Delta,\mathsf{z}\vdash N\| ∥Γ , x , Δ ⊢ λ z N ∥ = λ ∥Γ , x , Δ , z ⊢ N ∥
∥ Γ , y , Δ ⊢ { y x } Δ λ z N ∥ = ∥ Γ , y , Δ ⊢ λ z { y x } Δ , z N ∥ = λ ∥ Γ , y , Δ , z ⊢ { y x } Δ , z N ∥ \|\Gamma,\mathsf{y},\Delta\vdash\{\mathsf{y}\mathsf{x}\}_{\Delta}\,\lambda\mathsf{z}N\|=\|\Gamma,\mathsf{y},\Delta\vdash\lambda\mathsf{z}\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{z}}\,N\|=\lambda\|\Gamma,\mathsf{y},\Delta,\mathsf{z}\vdash\{\mathsf{y}\mathsf{x}\}_{\Delta,\mathsf{z}}\,N\| ∥Γ , y , Δ ⊢ { yx } Δ λ z N ∥ = ∥Γ , y , Δ ⊢ λ z { yx } Δ , z N ∥ = λ ∥Γ , y , Δ , z ⊢ { yx } Δ , z N ∥
Case 2. M M M z \mathsf{z} z
∥ Γ , x , Δ ⊢ z ∥ = ∥ Γ , y , Δ ⊢ { y x } Δ z ∥ \|\Gamma,\mathsf{x},\Delta\vdash\mathsf{z}\|=\|\Gamma,\mathsf{y},\Delta\vdash\{\mathsf{y}\mathsf{x}\}_{\Delta}\,\mathsf{z}\| ∥Γ , x , Δ ⊢ z ∥ = ∥Γ , y , Δ ⊢ { yx } Δ z ∥
Induction over the length of Δ \Delta Δ
Suppose Δ = n i l \Delta=nil Δ = ni l
∥ Γ , x ⊢ z ∥ = ∥ Γ , y ⊢ { y x } z ∥ \|\Gamma,\mathsf{x}\vdash\mathsf{z}\|=\|\Gamma,\mathsf{y}\vdash\{\mathsf{y}\mathsf{x}\}\mathsf{z}\| ∥Γ , x ⊢ z ∥ = ∥Γ , y ⊢ { yx } z ∥
If z = x \mathsf{z}=\mathsf{x} z = x
∥ Γ , x ⊢ x ∥ = 1 ‾ \|\Gamma,\mathsf{x}\vdash\mathsf{x}\|=\underline{1} ∥Γ , x ⊢ x ∥ = 1
∥ Γ , y ⊢ { y x } x ∥ = ∥ Γ , y ⊢ y ∥ = 1 ‾ \|\Gamma,\mathsf{y}\vdash\{\mathsf{y}\mathsf{x}\}\mathsf{x}\|=\|\Gamma,\mathsf{y}\vdash\mathsf{y}\|=\underline{1} ∥Γ , y ⊢ { yx } x ∥ = ∥Γ , y ⊢ y ∥ = 1
If z ≠ x \mathsf{z}\neq\mathsf{x} z = x
∥ Γ , x ⊢ z ∥ = ↑ ∥ Γ ⊢ z ∥ \|\Gamma,\mathsf{x}\vdash\mathsf{z}\|=\,\uparrow\!\|\Gamma\vdash\mathsf{z}\| ∥Γ , x ⊢ z ∥ = ↑ ∥Γ ⊢ z ∥
∥ Γ , y ⊢ { y x } z ∥ = ∥ Γ , y ⊢ ↑ z ∥ = ↑ ∥ Γ ⊢ z ∥ \|\Gamma,\mathsf{y}\vdash\{\mathsf{y}\mathsf{x}\}\mathsf{z}\|=\|\Gamma,\mathsf{y}\vdash\,\uparrow\!\mathsf{z}\|=\,\uparrow\!\|\Gamma\vdash\mathsf{z}\| ∥Γ , y ⊢ { yx } z ∥ = ∥Γ , y ⊢ ↑ z ∥ = ↑ ∥Γ ⊢ z ∥
Suppose Δ = Σ , w \Delta=\Sigma,\mathsf{w} Δ = Σ , w
tensy
\penalty 1 ∥ Γ , x , Σ ⊢ z ∥ = ∥ Γ , y , Σ ⊢ { y x } Σ z ∥ \displaystyle\penalty 1\|\Gamma,\mathsf{x},\Sigma\vdash\mathsf{z}\|=\|\Gamma,\mathsf{y},\Sigma\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma}\,\mathsf{z}\| \penalty 1∥Γ , x , Σ ⊢ z ∥ = ∥Γ , y , Σ ⊢ { yx } Σ z ∥
∥ Γ , x , Σ , w ⊢ z ∥ = ∥ Γ , y , Σ , w ⊢ { y x } Σ , w z ∥ \displaystyle\|\Gamma,\mathsf{x},\Sigma,\mathsf{w}\vdash\mathsf{z}\|=\|\Gamma,\mathsf{y},\Sigma,\mathsf{w}\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma,\mathsf{w}}\,\mathsf{z}\| ∥Γ , x , Σ , w ⊢ z ∥ = ∥Γ , y , Σ , w ⊢ { yx } Σ , w z ∥
If z = w \mathsf{z}=\mathsf{w} z = w
∥ Γ , x , Σ , w ⊢ w ∥ = 1 ‾ \|\Gamma,\mathsf{x},\Sigma,\mathsf{w}\vdash\mathsf{w}\|=\underline{1} ∥Γ , x , Σ , w ⊢ w ∥ = 1
∥ Γ , y , Σ , w ⊢ { y x } Σ , w w ∥ = ∥ Γ , x , Σ , w ⊢ w ∥ = 1 ‾ \|\Gamma,\mathsf{y},\Sigma,\mathsf{w}\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma,\mathsf{w}}\,\mathsf{w}\|=\|\Gamma,\mathsf{x},\Sigma,\mathsf{w}\vdash\mathsf{w}\|=\underline{1} ∥Γ , y , Σ , w ⊢ { yx } Σ , w w ∥ = ∥Γ , x , Σ , w ⊢ w ∥ = 1
If z ≠ w \mathsf{z}\neq\mathsf{w} z = w
∥ Γ , x , Σ , w ⊢ z ∥ = ↑ ∥ Γ , x , Σ ⊢ z ∥ \|\Gamma,\mathsf{x},\Sigma,\mathsf{w}\vdash\mathsf{z}\|=\,\uparrow\!\|\Gamma,\mathsf{x},\Sigma\vdash\mathsf{z}\| ∥Γ , x , Σ , w ⊢ z ∥ = ↑ ∥Γ , x , Σ ⊢ z ∥
∥ Γ , y , Σ , w ⊢ { y x } Σ , w z ∥ = ∥ Γ , y , Σ , w ⊢ ↑ { y x } Σ z ∥ = ↑ ∥ Γ , y , Σ ⊢ { y x } Σ z ∥ \|\Gamma,\mathsf{y},\Sigma,\mathsf{w}\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma,\mathsf{w}}\,\mathsf{z}\|=\|\Gamma,\mathsf{y},\Sigma,\mathsf{w}\vdash\,\uparrow\!\{\mathsf{y}\mathsf{x}\}_{\Sigma}\,\mathsf{z}\|=\,\uparrow\!\|\Gamma,\mathsf{y},\Sigma\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma}\,\mathsf{z}\| ∥Γ , y , Σ , w ⊢ { yx } Σ , w z ∥ = ∥Γ , y , Σ , w ⊢ ↑ { yx } Σ z ∥ = ↑ ∥Γ , y , Σ ⊢ { yx } Σ z ∥
Case 3. M = ↑ N M=\,\uparrow\!N M = ↑ N
Suppose Δ = n i l \Delta=nil Δ = ni l
∥ Γ , x ⊢ ↑ N ∥ = ∥ Γ , y ⊢ { y x } ↑ N ∥ \|\Gamma,\mathsf{x}\vdash\,\uparrow\!N\|=\|\Gamma,\mathsf{y}\vdash\{\mathsf{y}\mathsf{x}\}\!\uparrow\!N\| ∥Γ , x ⊢ ↑ N ∥ = ∥Γ , y ⊢ { yx } ↑ N ∥
because
∥ Γ , x ⊢ ↑ N ∥ = ↑ ∥ Γ ⊢ N ∥ \|\Gamma,\mathsf{x}\vdash\,\uparrow\!N\|=\,\uparrow\!\|\Gamma\vdash N\| ∥Γ , x ⊢ ↑ N ∥ = ↑ ∥Γ ⊢ N ∥
∥ Γ , y ⊢ { y x } ↑ N ∥ = ∥ Γ , y ⊢ ↑ N ∥ = ↑ ∥ Γ ⊢ N ∥ \|\Gamma,\mathsf{y}\vdash\{\mathsf{y}\mathsf{x}\}\!\uparrow\!N\|=\|\Gamma,\mathsf{y}\vdash\,\uparrow\!N\|=\,\uparrow\!\|\Gamma\vdash N\| ∥Γ , y ⊢ { yx } ↑ N ∥ = ∥Γ , y ⊢ ↑ N ∥ = ↑ ∥Γ ⊢ N ∥
Suppose Δ = Σ , w \Delta=\Sigma,\mathsf{w} Δ = Σ , w M M M
tensy
\penalty 1 ∥ Γ , x , Σ ⊢ N ∥ = ∥ Γ , y , Σ ⊢ { y x } Σ N ∥ \displaystyle\penalty 1\|\Gamma,\mathsf{x},\Sigma\vdash N\|=\|\Gamma,\mathsf{y},\Sigma\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma}\,N\| \penalty 1∥Γ , x , Σ ⊢ N ∥ = ∥Γ , y , Σ ⊢ { yx } Σ N ∥
∥ Γ , x , Σ , w ⊢ ↑ N ∥ = ∥ Γ , y , Σ , w ⊢ { y x } Σ , x ↑ N ∥ \displaystyle\|\Gamma,\mathsf{x},\Sigma,\mathsf{w}\vdash\,\uparrow\!N\|=\|\Gamma,\mathsf{y},\Sigma,\mathsf{w}\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma,\mathsf{x}}\!\uparrow\!N\| ∥Γ , x , Σ , w ⊢ ↑ N ∥ = ∥Γ , y , Σ , w ⊢ { yx } Σ , x ↑ N ∥
This is true because
∥ Γ , x , Σ , w ⊢ ↑ N ∥ = ↑ ∥ Γ , x , Σ ⊢ N ∥ \|\Gamma,\mathsf{x},\Sigma,\mathsf{w}\vdash\,\uparrow\!N\|=\,\uparrow\!\|\Gamma,\mathsf{x},\Sigma\vdash N\| ∥Γ , x , Σ , w ⊢ ↑ N ∥ = ↑ ∥Γ , x , Σ ⊢ N ∥
∥ Γ , y , Σ , w ⊢ { y x } Σ , x ↑ N ∥ = ∥ Γ , y , Σ , w ⊢ ↑ { y x } Σ N ∥ = ↑ ∥ Γ , y , Σ ⊢ { y x } Σ N ∥ \|\Gamma,\mathsf{y},\Sigma,\mathsf{w}\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma,\mathsf{x}}\!\uparrow\!N\|=\|\Gamma,\mathsf{y},\Sigma,\mathsf{w}\vdash\,\uparrow\!\{\mathsf{y}\mathsf{x}\}_{\Sigma}\,N\|=\,\uparrow\!\|\Gamma,\mathsf{y},\Sigma\vdash\{\mathsf{y}\mathsf{x}\}_{\Sigma}\,N\| ∥Γ , y , Σ , w ⊢ { yx } Σ , x ↑ N ∥ = ∥Γ , y , Σ , w ⊢ ↑ { yx } Σ N ∥ = ↑ ∥Γ , y , Σ ⊢ { yx } Σ N ∥
Case 4. M = N 1 N 2 M=N_{1}N_{2} M = N 1 N 2
Straightforward.
∎
Now we shall prove that ∥ n i l ⊢ M ∥ = ∥ n i l ⊢ N ∥ \|nil\vdash M\|=\|nil\vdash N\| ∥ ni l ⊢ M ∥ = ∥ ni l ⊢ N ∥ M = α N M=_{\alpha}N M = α N
Definition 3.6 **.**For each z \mathsf{z} z Γ \Gamma Γ { z / Γ } \{\mathsf{z}/\Gamma\} { z /Γ }
{ z / n i l } M = M \{\mathsf{z}/nil\}M=M { z / ni l } M = M
{ z / x , Δ } M = { z / Δ } { z x } Δ M \{\mathsf{z}/\mathsf{x},\Delta\}M=\{\mathsf{z}/\Delta\}\{\mathsf{z}\mathsf{x}\}_{\Delta}M { z / x , Δ } M = { z /Δ } { zx } Δ M
For example
{ z / x } M = { z x } M \{\mathsf{z}/\mathsf{x}\}M=\{\mathsf{z}\mathsf{x}\}M { z / x } M = { zx } M
{ z / x 1 , x 2 } M = { z x 2 } { z x 1 } x 2 M \{\mathsf{z}/\mathsf{x}_{1},\mathsf{x}_{2}\}M=\{\mathsf{z}\mathsf{x}_{2}\}\{\mathsf{z}\mathsf{x}_{1}\}_{\mathsf{x}_{2}}M { z / x 1 , x 2 } M = { z x 2 } { z x 1 } x 2 M
{ z / x 1 , x 2 , x 3 } = { z x 3 } { z x 2 } x 3 { z x 1 } x 2 , x 3 M \{\mathsf{z}/\mathsf{x}_{1},\mathsf{x}_{2},\mathsf{x}_{3}\}=\{\mathsf{z}\mathsf{x}_{3}\}\{\mathsf{z}\mathsf{x}_{2}\}_{\mathsf{x}_{3}}\{\mathsf{z}\mathsf{x}_{1}\}_{\mathsf{x}_{2},\mathsf{x}_{3}}M { z / x 1 , x 2 , x 3 } = { z x 3 } { z x 2 } x 3 { z x 1 } x 2 , x 3 M
Note that
{ z / Δ , x } ↑ N = ↑ { z / Δ } N \{\mathsf{z}/\Delta,\mathsf{x}\}\!\uparrow\!N=\,\uparrow\!\{\mathsf{z}/\Delta\}N { z /Δ , x } ↑ N = ↑ { z /Δ } N
{ z / Δ , x } x = z \{\mathsf{z}/\Delta,\mathsf{x}\}\mathsf{x}=\mathsf{z} { z /Δ , x } x = z
{ z / Δ , x } y = ↑ { z / Δ } y \{\mathsf{z}/\Delta,\mathsf{x}\}\mathsf{y}=\,\uparrow\!\{\mathsf{z}/\Delta\}\mathsf{y} { z /Δ , x } y = ↑ { z /Δ } y y ≠ x \mathsf{y}\neq\mathsf{x} y = x
(easy induction)
Example 3.7 **.**λ x 1 λ x 2 M = α λ z λ z { z / x 1 , x 2 } M \lambda\mathsf{x}_{1}\lambda\mathsf{x}_{2}M=_{\alpha}\lambda\mathsf{z}\lambda\mathsf{z}\{\mathsf{z}/\mathsf{x}_{1},\mathsf{x}_{2}\}M λ x 1 λ x 2 M = α λ z λ z { z / x 1 , x 2 } M
λ x 1 λ x 2 M = α λ z { z x 1 } λ x 2 M = λ z λ x 2 { z x 1 } x 2 M = α λ z λ z { z x 2 } { z x 1 } x 2 M \lambda\mathsf{x}_{1}\lambda\mathsf{x}_{2}M\\
=_{\alpha}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}_{1}\}\lambda\mathsf{x}_{2}M\\
=\lambda\mathsf{z}\lambda\mathsf{x}_{2}\{\mathsf{z}\mathsf{x}_{1}\}_{\mathsf{x}_{2}}M\\
=_{\alpha}\lambda\mathsf{z}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}_{2}\}\{\mathsf{z}\mathsf{x}_{1}\}_{\mathsf{x}_{2}}M λ x 1 λ x 2 M = α λ z { z x 1 } λ x 2 M = λ z λ x 2 { z x 1 } x 2 M = α λ z λ z { z x 2 } { z x 1 } x 2 M
Lemma 3.8 **.**{ z / Γ } λ z { z x } M = λ z { z / Γ , x } M \{\mathsf{z}/\Gamma\}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}M=\lambda\mathsf{z}\,\{\mathsf{z}/\Gamma,\mathsf{x}\}M { z /Γ } λ z { zx } M = λ z { z /Γ , x } M
Proof.
Induction over the length of Γ \Gamma Γ
Suppose Γ = y , Δ \Gamma=\mathsf{y},\Delta Γ = y , Δ
tensy
\penalty 1 { z / Δ } λ z { z x } N = λ z { z / Δ , x } N \displaystyle\penalty 1\{\mathsf{z}/\Delta\}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}N=\lambda\mathsf{z}\{\mathsf{z}/\Delta,\mathsf{x}\}N \penalty 1 { z /Δ } λ z { zx } N = λ z { z /Δ , x } N
{ z / y , Δ } λ z { z x } M = λ z { z / y , Δ , x } M \displaystyle\{\mathsf{z}/\mathsf{y},\Delta\}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}M=\lambda\mathsf{z}\,\{\mathsf{z}/\mathsf{y},\Delta,\mathsf{x}\}M { z / y , Δ } λ z { zx } M = λ z { z / y , Δ , x } M
where N = { z y } Δ , x M N=\{\mathsf{z}\mathsf{y}\}_{\Delta,\mathsf{x}}M N = { zy } Δ , x M
{ z / y , Δ } λ z { z x } M = = { z / Δ } { z y } Δ λ z { z x } M = { z / Δ } λ z { z y } Δ , z { z x } M = { z / Δ } λ z { z x } { z y } Δ , x M \{\mathsf{z}/\mathsf{y},\Delta\}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}M=\\
=\{\mathsf{z}/\Delta\}\{\mathsf{z}\mathsf{y}\}_{\Delta}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}M\\
=\{\mathsf{z}/\Delta\}\lambda\mathsf{z}\{\mathsf{z}\mathsf{y}\}_{\Delta,\mathsf{z}}\{\mathsf{z}\mathsf{x}\}M\\
=\{\mathsf{z}/\Delta\}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}\{\mathsf{z}\mathsf{y}\}_{\Delta,\mathsf{x}}M { z / y , Δ } λ z { zx } M = = { z /Δ } { zy } Δ λ z { zx } M = { z /Δ } λ z { zy } Δ , z { zx } M = { z /Δ } λ z { zx } { zy } Δ , x M 1.6
= λ z { z / Δ , x } { z y } Δ , x M =\lambda\mathsf{z}\{\mathsf{z}/\Delta,\mathsf{x}\}\{\mathsf{z}\mathsf{y}\}_{\Delta,\mathsf{x}}M = λ z { z /Δ , x } { zy } Δ , x M
= λ z { z / y , Δ , x } M =\lambda\mathsf{z}\{\mathsf{z}/\mathsf{y},\Delta,\mathsf{x}\}M = λ z { z / y , Δ , x } M
∎
Definition 3.9 **.**For each generalized de Bruijn’s term A A A z \mathsf{z} z d b z ( A ) db_{\mathsf{z}}(A) d b z ( A ) d b z ( A ) ∈ Λ ↑ db_{\mathsf{z}}(A)\in\Lambda\!\uparrow\! d b z ( A ) ∈ Λ ↑
d b z ( x ) = x db_{\mathsf{z}}(\mathsf{x})=\mathsf{x} d b z ( x ) = x
d b z ( 1 ‾ ) = z db_{\mathsf{z}}(\underline{1})=\mathsf{z} d b z ( 1 ) = z
d b z ( λ A ) = λ z d b z ( A ) db_{\mathsf{z}}(\lambda A)=\lambda\mathsf{z}\,db_{\mathsf{z}}(A) d b z ( λ A ) = λ z d b z ( A )
d b z ( A B ) = d b z ( A ) d b z ( B ) db_{\mathsf{z}}(AB)=db_{\mathsf{z}}(A)db_{\mathsf{z}}(B) d b z ( A B ) = d b z ( A ) d b z ( B )
d b z ( ↑ A ) = ↑ d b z ( A ) db_{\mathsf{z}}(\uparrow\!A)=\,\uparrow\!db_{\mathsf{z}}(A) d b z ( ↑ A ) = ↑ d b z ( A )
Example 3.10 **.**d b z ( λ λ ( ↑ 1 ‾ ) 1 ‾ ↑ ↑ z ) = λ z λ z ( ↑ z ) z ↑ ↑ z db_{z}(\lambda\lambda(\uparrow\!\underline{1})\underline{1}\uparrow\!\,\uparrow\!z)=\lambda z\lambda z(\uparrow\!z)z\uparrow\!\,\uparrow\!z d b z ( λλ ( ↑ 1 ) 1 ↑ ↑ z ) = λ z λ z ( ↑ z ) z ↑ ↑ z
d b x ( λ λ ( ↑ 1 ‾ ) 1 ‾ ↑ ↑ z ) = λ x λ x ( ↑ x ) x ↑ ↑ z db_{x}(\lambda\lambda(\uparrow\!\underline{1})\underline{1}\uparrow\!\,\uparrow\!z)=\lambda x\lambda x(\uparrow\!x)x\uparrow\!\,\uparrow\!z d b x ( λλ ( ↑ 1 ) 1 ↑ ↑ z ) = λ x λ x ( ↑ x ) x ↑ ↑ z
Theorem 3.11 **.**d b z ∥ n i l ⊢ M ∥ = d b z ( M ) db_{\mathsf{z}}\|nil\vdash M\|=db_{\mathsf{z}}(M) d b z ∥ ni l ⊢ M ∥ = d b z ( M )
Proof.
We shall prove the stronger statement: for each Γ \Gamma Γ
d b z ∥ Γ ⊢ M ∥ = { z / Γ } d b z ( M ) db_{\mathsf{z}}\|\Gamma\vdash M\|=\{\mathsf{z}/\Gamma\}db_{\mathsf{z}}(M) d b z ∥Γ ⊢ M ∥ = { z /Γ } d b z ( M )
Induction on the structure of M M M
Case 1. M = λ x N M=\lambda\mathsf{x}N M = λ x N
Prove the induction step
tensy
\penalty 1 d b z ∥ Γ , x ⊢ N ∥ = { z / Γ , x } d b z ( N ) \displaystyle\penalty 1db_{\mathsf{z}}\|\Gamma,\mathsf{x}\vdash N\|=\{\mathsf{z}/\Gamma,\mathsf{x}\}db_{\mathsf{z}}(N) \penalty 1 d b z ∥Γ , x ⊢ N ∥ = { z /Γ , x } d b z ( N )
d b z ∥ Γ ⊢ λ x N ∥ = { z / Γ } d b z ( λ x N ) \displaystyle db_{\mathsf{z}}\|\Gamma\vdash\lambda\mathsf{x}N\|=\{\mathsf{z}/\Gamma\}db_{\mathsf{z}}(\lambda\mathsf{x}N) d b z ∥Γ ⊢ λ x N ∥ = { z /Γ } d b z ( λ x N )
Note that
∥ Γ ⊢ λ x N ∥ = λ ∥ Γ , x ⊢ N ∥ \|\Gamma\vdash\lambda\mathsf{x}N\|=\lambda\|\Gamma,\mathsf{x}\vdash N\| ∥Γ ⊢ λ x N ∥ = λ ∥Γ , x ⊢ N ∥
hence
d b z ∥ Γ ⊢ λ x N ∥ = = λ z d b z ∥ Γ , x ⊢ N ∥ = λ z { z / Γ , x } d b z ( N ) db_{\mathsf{z}}\|\Gamma\vdash\lambda\mathsf{x}N\|=\\
=\lambda\mathsf{z}\,db_{\mathsf{z}}\|\Gamma,\mathsf{x}\vdash N\|\\
=\lambda\mathsf{z}\,\{\mathsf{z}/\Gamma,\mathsf{x}\}db_{\mathsf{z}}(N) d b z ∥Γ ⊢ λ x N ∥ = = λ z d b z ∥Γ , x ⊢ N ∥ = λ z { z /Γ , x } d b z ( N )
But
d b z ( λ x N ) = λ z { z x } d b z ( N ) db_{\mathsf{z}}(\lambda\mathsf{x}N)=\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(N) d b z ( λ x N ) = λ z { zx } d b z ( N )
hence
{ z / Γ } d b z ( λ x N ) = = { z / Γ } λ z { z x } d b z ( N ) = λ z { z / Γ , x } d b z ( N ) \{\mathsf{z}/\Gamma\}db_{\mathsf{z}}(\lambda\mathsf{x}N)=\\
=\{\mathsf{z}/\Gamma\}\lambda\mathsf{z}\{\mathsf{z}\mathsf{x}\}db_{\mathsf{z}}(N)\\
=\lambda\mathsf{z}\,\{\mathsf{z}/\Gamma,\mathsf{x}\}db_{\mathsf{z}}(N) { z /Γ } d b z ( λ x N ) = = { z /Γ } λ z { zx } d b z ( N ) = λ z { z /Γ , x } d b z ( N ) 3.8
Case 2. M M M x \mathsf{x} x
d b z ∥ Γ ⊢ x ∥ = { z / Γ } d b z ( x ) db_{\mathsf{z}}\|\Gamma\vdash\mathsf{x}\|=\{\mathsf{z}/\Gamma\}db_{\mathsf{z}}(\mathsf{x}) d b z ∥Γ ⊢ x ∥ = { z /Γ } d b z ( x )
Induction on the length of Γ \Gamma Γ
Suppose Γ = n i l \Gamma=nil Γ = ni l
d b z ∥ n i l ⊢ x ∥ = x = d b z ( x ) db_{\mathsf{z}}\|nil\vdash\mathsf{x}\|=\mathsf{x}=db_{\mathsf{z}}(\mathsf{x}) d b z ∥ ni l ⊢ x ∥ = x = d b z ( x )
Suppose Γ = Δ , y \Gamma=\Delta,\mathsf{y} Γ = Δ , y
tensy
\penalty 1 d b z ∥ Δ ⊢ x ∥ = { z / Δ } d b z ( x ) \displaystyle\penalty 1db_{\mathsf{z}}\|\Delta\vdash\mathsf{x}\|=\{\mathsf{z}/\Delta\}db_{\mathsf{z}}(\mathsf{x}) \penalty 1 d b z ∥Δ ⊢ x ∥ = { z /Δ } d b z ( x )
d b z ∥ Δ , y ⊢ x ∥ = { z / Δ , y } d b z ( x ) \displaystyle db_{\mathsf{z}}\|\Delta,\mathsf{y}\vdash\mathsf{x}\|=\{\mathsf{z}/\Delta,\mathsf{y}\}db_{\mathsf{z}}(\mathsf{x}) d b z ∥Δ , y ⊢ x ∥ = { z /Δ , y } d b z ( x )
If y = x \mathsf{y}=\mathsf{x} y = x
d b z ∥ Δ , x ⊢ x ∥ = d b z ( 1 ‾ ) = z db_{\mathsf{z}}\|\Delta,\mathsf{x}\vdash\mathsf{x}\|=db_{\mathsf{z}}(\underline{1})=\mathsf{z} d b z ∥Δ , x ⊢ x ∥ = d b z ( 1 ) = z
{ z / Δ , x } d b z ( x ) = { z / Δ , x } x = z \{\mathsf{z}/\Delta,\mathsf{x}\}db_{\mathsf{z}}(\mathsf{x})=\{\mathsf{z}/\Delta,\mathsf{x}\}\mathsf{x}=\mathsf{z} { z /Δ , x } d b z ( x ) = { z /Δ , x } x = z
If y ≠ x \mathsf{y}\neq\mathsf{x} y = x
d b z ∥ Δ , y ⊢ x ∥ = d b z ( ↑ ∥ Δ ⊢ x ∥ ) = ↑ d b z ( ∥ Δ ⊢ x ∥ ) db_{\mathsf{z}}\|\Delta,\mathsf{y}\vdash\mathsf{x}\|=db_{\mathsf{z}}(\uparrow\!\|\Delta\vdash\mathsf{x}\|)=\,\uparrow\!db_{\mathsf{z}}(\|\Delta\vdash\mathsf{x}\|) d b z ∥Δ , y ⊢ x ∥ = d b z ( ↑ ∥Δ ⊢ x ∥ ) = ↑ d b z ( ∥Δ ⊢ x ∥ )
{ z / Δ , y } d b z ( x ) = { z / Δ , y } x = ↑ { z / Δ } x \{\mathsf{z}/\Delta,\mathsf{y}\}db_{\mathsf{z}}(\mathsf{x})=\{\mathsf{z}/\Delta,\mathsf{y}\}\mathsf{x}=\,\uparrow\!\{\mathsf{z}/\Delta\}\mathsf{x} { z /Δ , y } d b z ( x ) = { z /Δ , y } x = ↑ { z /Δ } x
Case 3. M = ↑ N M=\,\uparrow\!N M = ↑ N
Suppose Γ = n i l \Gamma=nil Γ = ni l
tensy
\penalty 1 d b z ∥ n i l ⊢ N ∥ = d b z ( N ) \displaystyle\penalty 1db_{\mathsf{z}}\|nil\vdash N\|=db_{\mathsf{z}}(N) \penalty 1 d b z ∥ ni l ⊢ N ∥ = d b z ( N )
d b z ∥ n i l ⊢ ↑ N ∥ = d b z ( ↑ N ) \displaystyle db_{\mathsf{z}}\|nil\vdash\,\uparrow\!N\|=db_{\mathsf{z}}(\uparrow\!N) d b z ∥ ni l ⊢ ↑ N ∥ = d b z ( ↑ N )
This is true because
d b z ∥ n i l ⊢ ↑ N ∥ = d b z ( ↑ ∥ n i l ⊢ N ∥ ) = ↑ d b z ∥ n i l ⊢ N ∥ db_{\mathsf{z}}\|nil\vdash\,\uparrow\!N\|=db_{\mathsf{z}}(\uparrow\!\|nil\vdash N\|)=\,\uparrow\!db_{\mathsf{z}}\|nil\vdash N\| d b z ∥ ni l ⊢ ↑ N ∥ = d b z ( ↑ ∥ ni l ⊢ N ∥ ) = ↑ d b z ∥ ni l ⊢ N ∥
d b z ( ↑ N ) = ↑ d b z ( N ) db_{\mathsf{z}}(\uparrow\!N)=\,\uparrow\!db_{\mathsf{z}}(N) d b z ( ↑ N ) = ↑ d b z ( N )
Suppose Γ = Δ , y \Gamma=\Delta,\mathsf{y} Γ = Δ , y M M M
tensy
\penalty 1 d b z ∥ Δ ⊢ N ∥ = { z / Δ } d b z ( N ) \displaystyle\penalty 1db_{\mathsf{z}}\|\Delta\vdash N\|=\{\mathsf{z}/\Delta\}db_{\mathsf{z}}(N) \penalty 1 d b z ∥Δ ⊢ N ∥ = { z /Δ } d b z ( N )
d b z ∥ Δ , y ⊢ ↑ N ∥ = { z / Δ , y } d b z ( ↑ N ) \displaystyle db_{\mathsf{z}}\|\Delta,\mathsf{y}\vdash\,\uparrow\!N\|=\{\mathsf{z}/\Delta,\mathsf{y}\}db_{\mathsf{z}}(\uparrow\!N) d b z ∥Δ , y ⊢ ↑ N ∥ = { z /Δ , y } d b z ( ↑ N )
This is true because
d b z ∥ Δ , y ⊢ ↑ N ∥ = d b z ( ↑ ∥ Δ ⊢ N ∥ ) = ↑ d b z ∥ Δ ⊢ N ∥ db_{\mathsf{z}}\|\Delta,\mathsf{y}\vdash\,\uparrow\!N\|=db_{\mathsf{z}}(\uparrow\!\|\Delta\vdash N\|)=\,\uparrow\!db_{\mathsf{z}}\|\Delta\vdash N\| d b z ∥Δ , y ⊢ ↑ N ∥ = d b z ( ↑ ∥Δ ⊢ N ∥ ) = ↑ d b z ∥Δ ⊢ N ∥
{ z / Δ , y } d b z ( ↑ N ) = { z / Δ , y } ↑ d b z ( N ) = ↑ { z / Δ } d b z ( N ) \{\mathsf{z}/\Delta,\mathsf{y}\}db_{\mathsf{z}}(\uparrow\!N)=\{\mathsf{z}/\Delta,\mathsf{y}\}\!\uparrow\!db_{\mathsf{z}}(N)=\,\uparrow\!\{\mathsf{z}/\Delta\}db_{\mathsf{z}}(N) { z /Δ , y } d b z ( ↑ N ) = { z /Δ , y } ↑ d b z ( N ) = ↑ { z /Δ } d b z ( N )
Case 4. M = N 1 N 2 M=N_{1}N_{2} M = N 1 N 2
Straightforward.
∎
