Just $ A sandbox

プログラミングと計算機科学とかわいさ

de Bruijn Indexとβ変換

$ KMN \equiv (\lambda xy. x)MN \longrightarrow_{\beta} M $を示したいとする.

α変換

$y \notin \text{FV}(M)$ならば, $ (\lambda xy. x)MN \to (\lambda y. M) N \to M[y:=N] \equiv M $となる.
問題は$y \notin \text{FV}(M)$ならば$ M[y:=N] \equiv M $の部分で, これを示すにはMについての帰納法を使う.

$M \equiv x$(変数)の時は$x=y, x \neq y$で場合分けして明らか. $M \equiv (\lambda x. M_0)$の時は, α変換によって$x \neq y$としてよく, このとき$M[y:=N] \equiv (\lambda x. M_0)[y:=N] \equiv (\lambda x. M_0[y:=N])$となり, あとは帰納法の仮定よりOK. $M \equiv (M M')$のときは帰納法の仮定と代入の性質から明らか.

さてこれをIsabelle(proof assistant)で証明しようとすると, α変換によって$x \neq y$としてとれるというところを示すのが難しい.
α変換の煩わしさを軽減するためにλ式の定義を少し変えて, de Bruijn Indexによる定義をする.

de Bruijn Index

<λ-expr> ::= <var :: nat> | λ. <λ-expr> | (<λ-expr> <λ-expr>)

によって定義する. 変数の代わりに自然数を使い, さらに函数抽象をするときに束縛変数を指定しない.
<var :: nat>は, その変数のいくつ前にあるλによって束縛されているかを表す(この変数の添字の割り振り方をde Bruijn Indexと呼ぶらしい).

例として, $\lambda. \lambda. 1 \equiv \lambda xy. x$, $\lambda. \lambda. 0 (\lambda. 0 1) \equiv \lambda xy. y (\lambda z. z y)$である.

de Bruijn Indexのλ式のβ変換をどのように定義するかを考える.
λ式Mの中で, Mの中の変数nがあったとき, nに対応するλがMに含まれていることとnがMの束縛変数であることは等しい.

このとき, $(\lambda. M) N$のβ変換は, Mの中の自由変数の値を一つ減らし(λがはずれるため), Nの中の自由変数の値はλに対応するMの中の変数の深さだけ増やす.
例: $(\lambda. \lambda. \lambda. 5 2) (\lambda. 0 1) \to (\lambda. \lambda. (5-1) (\lambda. 0 (1+2))) \equiv (\lambda. \lambda. 4 (\lambda. 0 3)) $

de Bruijn Indexによるλ式の表現は, 束縛変数の添字の振り方に自由度がないのでα変換を考える必要がない.

元の問題へ

結局元の問題に戻ると, $ KMN \longrightarrow M $を示すのが目的だった.
de Bruijn Indexでは, $ (\lambda. \lambda. 1) M N \to (\lambda M) N \to M $ となることを示せばよい.
けれど, これもあまり上手くいかなかったので結局どうすればいいのだろう.

K,M,Nが変数条件を満たす時, unshift 1 (λ shift 1 (shift 1 M)) $ N ⟶ Mが示せればいいと思うけれど.