1 ラムダ項による数学的対象の表現

コンピュータ・サイエンス入門 ラムダ計算第 3 回目資料

勝股 審也 2009 年 5 月 21 日

1 ラムダ項による数学的対象の表現

ラムダ項で種々の数学的対象を表現することができる。

1.1 真偽値

定義1.1 次のラムダ項を定義する。

T=λxy.x(=K), F=λxy.y,

また、ifLthenMelseNをLMNというラムダ項の略記とする。

T,Fはそれぞれ真、偽を表現するラムダ項であり、ifMthenLelseNはMがTにβ簡約されたな らばLを、Fに簡約されたならばNを返すラムダ項である。プログラミング言語のCやJavaで言 えば丁度e1?e2 :e3という式に相当する。

補題1.2 次が成立する。

ifTthenMelseN→^∗_β M, ifFthenMelseN→^∗_βN 問題1.3 以下を満たすラムダ項を与えよ。

1. TとFに対して否定として振る舞うラムダ項Not:

Not T→^∗_βF, Not F→^∗_β T

2. TとFに対して論理積として振る舞うラムダ項And:

And T T→^∗_βT And F T→^∗_βF And T F→^∗_βF And F F→^∗_βF

3. TとFに対して論理和として振る舞うラムダ項Or:

Or T T→^∗_βT Or F T→^∗_βT Or T F→^∗_βT Or F F→^∗_β F

1.2 組

定義1.4 2つのラムダ項M,Nに対しhM,Niをλx.x M Nというラムダ項の略記とする。また、ラ ムダ項Fst,Sndを以下で定義する。

Fst=λx.xT, Snd=λx.xF

これらは組と射影のラムダ項による表現を与える。

補題1.5 以下が成立する。

FsthM,Ni=(λx.xT) (λx.x M N)→^∗_β M SndhM,Ni=(λx.xF) (λx.x M N)→^∗_β N

一般にn個のラムダ項M1,· · ·,Mnの組をλx.x M1· · ·Mnと定義し、hM1,· · ·,Mniと書くことにする。

問題1.6 n個の組から第i成分(1≤i≤n)を取り出すラムダ項Projⁿ_i を定義せよ。つまり Projⁿ_i hM1,· · ·,Mni →^∗_β Mi

を満たすProjⁿ_i を定義せよ。

1.3 自然数

定義1.7 自然数nに対しラムダ項dneを再帰的に定義する。

1. d0e=I

2. dn+1e=hF,dnei

補題1.8 以下を満たすラムダ項Succ,Pred,Zero?が存在する。

Succdne →^∗_β dn+1e, Preddn+1e →^∗_βdne, Zero?d0e →^∗_βT, Zero?dn+1e →^∗_β F 証明 以下の通りにすればよい。

Succ=λx.hF,xi, Pred=Snd, Zero?=Fst

組を使った自然数の表現の他、以下の直接的な自然数の表現も存在する。

定義1.9 (チャーチ数) 自然数nに対してラムダ項cnを以下で定義する。

c_n=λsz. z }| {n

s(· · ·(s z)· · ·) 補題1.10 以下を満たすラムダ項Succ⁰,Zero⁰?が存在する。

Succ⁰cn→^∗_β cn+1, Zero⁰?cn+1 →^∗_βF, Zero⁰?c0→^∗_β T, 証明 以下の通りにすればよい。

Succ⁰=λnsz.s(n s z), Zero⁰?=λn.n(λx.F)T

問題1.11 ラムダ項Add⁰,Mul⁰,Exp⁰を以下で定義する。

Add⁰=λnm.mSucc⁰n, Mul⁰=λnm.m(Add⁰n)c0, Exp⁰=λnm.m(Mul⁰n)c1

これらが以下を満たすことを示せ。

Add⁰c_nc_m→^∗_βc_n+m, Mul⁰c_nc_m→^∗_β c_n×m, Exp⁰c_nc_m→^∗_βc_nm

問題1.12 以下を満たすラムダ項Pred⁰を定義せよ。

Pred⁰c0→^∗_βc0, Pred⁰cn+1→^∗_βcn

(ヒント:自然数上の関数 f ∈N²→N²をf(n,m)=(n+1,n)と定義して z }| {k

f(· · ·f(0,0))を計算すると、

結果の第二成分はどうなるか?)

2 帰納的関数のラムダ定義可能性

定義2.1 自然数上の全域関数 f ∈Nⁿ →Nとラムダ項Fに対して以下が成立する時、Fは f をラ ムダ定義すると言う。

∀x₁,· · ·,x_n∈N.Fdx₁e · · · dx_ne →^∗_βdf(x₁,· · · ,x_n)e. (1) また、自然数上の全域関数 f ∈Nⁿ→Nに対しあるラムダ項Fが存在してFが f をラムダ定義す る時、f はラムダ定義可能であると言う。

ラムダ定義可能な自然数上の全域関数はどれぐらいあるのだろうか？この講義では全域帰納的関数 に限定した結果を紹介したい。

帰納的関数の定義を簡単におさらいしよう。まず以下の4つの規則を考える:

1. 初期関数Pⁿ_i ∈Nⁿ →N,Kⁿ_m∈Nⁿ→N,S ∈N→Nは帰納的関数である。

2. 帰納的関数 f ∈N^m*N,g1,· · ·,gm∈Nⁿ*Nの合成関数

h(x₁,· · ·,x_n)=f(g₁(x₁,· · ·,x_n),· · ·,g_m(x₁,· · · ,x_n)) は帰納的関数である。

3. 帰納的関数φ∈Nⁿ*N, ψ∈Nⁿ⁺²*Nにより帰納的に定義された関数 f ∈Nⁿ⁺¹*Nは帰納 的関数である(原始帰納法)。

f(~x,0) = φ(~x)

f(~x,k+1) = ψ(~x,k,f(~x,k))

4. 帰納的関数φ∈Nⁿ⁺¹ *Nの最小解関数µ(φ)∈Nⁿ*Nは帰納的関数である。

これらのみを有限回用いて「帰納的関数である」と結論された関数こそが帰納的関数であった。こ こで規則4を制限した規則5を考える。

5. φ∈Nⁿ⁺¹*Nが帰納的関数であり、さらに

∀x1,· · ·,xn∈Nⁿ.∃y∈N. φ(x1,· · · ,xn,y)=0 が成立するとき、µ(φ)∈Nⁿ*Nは帰納的関数である。

命題2.2 規則1,2,3,5のみを有限回用いて構成された関数は全域帰納的関数である。また、全域帰

納的関数は規則1,2,3,5のみを有限回用いて構成できる。

定理2.3 任意のn引数全域帰納的関数はラムダ定義可能である。

証明 この証明の中では「全域帰納的関数」を単に「帰納的関数」と言うことにする。また、ベク トル記法~xは適切な長さの変数の列x1,· · ·,xnの略記とする(コンマは文脈に応じて無視せよ)。

証明ではラムダ項Θ=(λx f.f(xx f))(λx f.f(xx f))に関する以下の性質を用いる(第1回目の資料 の問題5.6を参照)。

ΘM→^∗_β M(ΘM)

さて、命題2.2よりf は規則1,2,3,5のみを有限回用いて構成されたと仮定してよい。従って f の構成手順に関する帰納法で証明する。

1. f が初期関数の場合。練習問題とする。

2. f が帰納的関数同士の合成の場合。練習問題とする。

3. f がφ∈Nⁿ→N, ψ∈Nⁿ⁺²→Nという帰納的関数に以下の原始帰納法を施して得られた関数 の場合。

f(~x,0) = φ(~x)

f(~x,k+1) = ψ(~x,k,f(~x,k))

帰納法の仮定はφ, ψはラムダ定義可能という主張である。よってそれらをラムダ定義するラ ムダ項Φ,Ψを取り、ラムダ項Fを以下で定義する。

F =λ~x.Θ(λhy.ifZero?ythenΦ~xelseΨ~x(Predy) (h(Predy))) ここでΦ~xは(· · ·(Φx1)· · · xn)の略記とする(Ψ~xについても同様)。

以下ではFが f をラムダ定義していることをn=1の場合で見てみる。証明するべき事柄は

∀x,y∈N.Fdxe dye →^∗_β df(x,y)eであるので、これをyに関する帰納法で証明する。

(a) y=0の場合。x∈Nを一つ取る。最初に以下の1ステップβ簡約を行い、得られたラ ムダ項で下線の引いてある部分をWxと略記することにする。

Fdxe d0e →_βΘ(λhy.ifZero?ythenΦdxeelseΨdxe(Predy) (h(Predy)))d0e 以下、β簡約を進める。

ΘWxd0e →^∗_β Wx(ΘWx)d0e

→^∗_β ifZero?d0ethenΦdxeelseΨdxe(Predd0e) (ΘWx(Predd0e))

→^∗_β Φdxe

→^∗_β dφ(x)e=df(x,0)e.

(b) y=k+1の場合。x∈Nを一つ取る。帰納法の仮定としてFdxe dke →^∗_βdf(x,k)eを仮定 する。このこととChurch-Rosserの定理からΘWxdke →^∗_βdf(x,k)eが導かれる。よって

Fdxe dk+1e →^∗_β W_x(ΘW_x)dk+1e

→^∗_β ifZero?dk+1ethenΦdxe

elseΨdxe(Preddk+1e) (ΘWx(Preddk+1e))

→^∗_β Ψdxe(Preddk+1e) (ΘWx(Preddk+1e))

→^∗_β Ψdxe dke(ΘWxdke)

→^∗_β Ψdxe dke df(x,k)e

→^∗_β dψ(x,k,f(x,k))e=df(x,k+1)e

よって帰納法よりFは f をラムダ定義している。

4. f が∀~x∈Nⁿ⁺¹.∃y∈N. φ(~x,y)=0を満たす帰納的関数φの最小解関数µ(φ)として定義され た場合。帰納法の仮定はφがラムダ定義可能という主張である。よってφをラムダ定義する ラムダ項Φを取り、ラムダ項Fを以下で定義する。

F=λ~x.Θ(λhy.ifZero? (Φ~x y) thenyelseh(Succy))d0e ここでΦ~xは(· · ·(Φx1)· · · xn)の略記とする。

以下ではFが f をラムダ定義していることをn=1の場合で見てみる。y0 = f(x)とおくと、

φ(x,y0) =0であり、かつ任意の0 ≤k <y0に対してφ(x,k) >0が成立する。まず以下の1 ステップβ簡約を行い、得られたラムダ項の下線の引いてある部分をZxと略記することに する。

Fdxe →_βΘ(λhy.ifZero? (Φdxey) thenyelseh(Succy))d0e (2) すると

ΘZ_xdy₀e →^∗_βdy₀e (3) が成立し、また任意の0≤k<y₀において

ΘZxdke →^∗_βΘZxdk+1e (4)

が成立する(証明せよ)。従って(2,3,4)から

Fdxe →_βΘZxd0e →^∗_βΘZxd1e →^∗_β· · · →^∗_βΘZxdy0e →^∗_βdy0e=df(x)e よってFは f をラムダ定義している。

1-4.から帰納法より(全域)帰納的関数はラムダ定義可能であることが示された。

実は全域帰納的関数に限らず、帰納的関数全てはラムダ定義可能である。

定理2.4 (Kleene) (部分関数のラムダ定義可能性の適切な定義のもとで)帰納的関数はラムダ定義 可能である。

証明のあらすじは定理2.3と同じであるが、証明中で与えたラムダ項を「未定義」の概念を正確に 扱えるようにやや変更しなければならない。詳細はBarendregtの本の8.4節を参照のこと。