千葉大学大学院 自然科学研究科修士論文

ラムダ項のβ 正規形を結合子を用いて求める方法

平成 18 年 3 月

数学・情報数理学専攻情報数理学講座

内藤昭宏目次

1 はじめに 2 2 CLt-項 2 3 ラムダ項 3 4 ラムダ項から CLt-項への変換 4 5 CLt-項からラムダ項への変換 5 6 =_{α} であることの証明 5 7 β 正規形の求まる速度 10 8 終わりに 13 9 謝辞 14

1 はじめに

与えられたラムダ項 M に対して、その正規形 M^{∗} を手動で求めるというのは結構面倒なことである。計算機を使って求める際にも代入を行う時の α 変換などに時間を要するために効率を上げることが難しい。そこで本論分では、 β 正規形を早く求めることを目標に以下の方法についての検証を行ってみた。

1. ラムダ項を一度結合子を用いてラムダを消去した項に変換する。

2. さらにそれについて変換規則を用いてそれ以上変形できない形にする。

3. これを再びラムダ項に変換してから β リダクションを行い、 β 正規形を求める。

この方法は結合子の変換規則を用いることによって、 β リダクションの回数を減らすことにより速度を早める事を目的としている。またこの方法を用いて求まったものが M^{∗} と =_{α} になっていることの証明も行ってみた。

なおこの論文は [1] を参考に古森雄一先生より詳細な方針を与えられ、それらの検討・検証を内藤が行った。

2 CLt-項

CLt-項というものを以下のように帰納的に定義する。定数記号には I, K′, B′, C′, S′ が含まれているものとする。

定義 2.1 (CLt-項).

1. 変数と定数記号は CLt-項である (この形の CLt-項を原子という).

2. M と N が CLt-項ならば, (MN) は CLt-項である (この形の CLt-項を適用という).

定義通りに書くと括弧が多くなって読みづらくなってしまうので適当に省略する事とする。そして、足りない括弧は左から補うことにする。例えば S′xyC′K′ は ((((S′x)y)C′)K′) を表している。

ここでは I, K′, B′, C′, S′ を基本的な結合子とし CLt-項の変換規則を以下のように定義する。

定義 2.2 (変換規則).

(I) IM ⊳_{1wt} M, (K′) K′MNRU ⊳_{1wt} MNR, (B′) B′MNRU ⊳_{1wt} MN(RU),
(C′) C′MNRU ⊳_{1wt} M(NU)R, (S′) S′MNRU ⊳_{1wt} M(NU)(RU) .

CLt-項 M に対して上の変換規則を用いて有限回の変形を行い、それ以上変形できなくなったその最終結果を M の正規形と呼び\overline{M} と表すこととする。

3 ラムダ項

ラムダ項を以下のように再帰的に定義する。定義 3.1 (ラムダ項).

1. 変数はラムダ項である (この形のラムダ項を原子という).

2. M と N がラムダ項ならば, (MN) はラムダ項である (この形のラムダ項を適用という).

3. x が変数 M がラムダ項の時 (λx.M) はラムダ項である (この形のラムダ項を抽象という).

CLt-項の時と同様に括弧を省略し、足りない括弧は左から補うこととする。ただし抽象については一番外側の括弧となっているときだけ省略する。すなわち (λx.M) は λx.M と省略するが,((λx.M)N) を λx.MN とはしない λx.MN は (λx.(MN)) の省略形である. また (λx.(λy.(λz.M))) などは λxyz.M と省略する.

ラムダ項 M に含まれる自由変数の集合を F V (M) とする。定義 3.2 (代入 (substitution)). M, N をラムダ項, x を変数とする. M の中の (自由に現れる) x に N を代入した結果 [N/x]M を次のように帰納的に定義する.

1. [N/x]x ≡ N ,

2. [N/x]M ≡ M (x ∉ F V (M) のとき),

3. [N/x](QR) ≡ ([N/x]Q [N/x]R) (x ∈ F V (QR) のとき),

4. [N/x](λy.Q) ≡ λy.[N/x]Q (x ∈ F V (Q) かつ y ∉ F V (N) のとき),

5. [N/x](λy.Q) ≡ λz.[N/x][z/y]Q (x ∈ F V (Q) かつ y ∈ F V (N) のとき). ここで y ≢ x は仮定されている. また, z は今までに現れていない変数である

定義 3.3 (β 変換).

ラムダ項の β 変換 ⊳_{1β} を以下のように再帰的に定義する。

1. (λx.M)N ⊳_{1β} [N/x]M

2. M⊳_{1β} N ならば、 λx.M ⊳_{1β} λx.N, MP ⊳_{1β} NP, P M ⊳_{1β} P N.

β 変換の基になる (λx.M)N の形のラムダ項を β -redex とよぶ.

β 変換を有限回繰り返し実行して P から Q が得られるとき P ⊳_{β} Q とかく. また β 変換可能なラムダ項同士を同一視することによって得られるラムダ項間の等号関係を =_{β} で表す. すなわちラムダ項 P, Q に対して

P ≡ P_{1} ↔_{β} P_{2} ↔_{β} ⋯ ↔_{β} P_{n} ≡ Q

(ただし M ↔_{β} N ⟺_{def} (M ⊳_{1β} N またはN ⊳_{1β} M))
を満たす n ≥ 1 と P_{1}, P_{2}, ⋯, P_{n} がある時、 P =_{β} Q とかく

ラムダ項 M が β-redex を含まないとき M は β 正規形であるという. また M ⊳_{β} N を満たす β 正規形 N がある時 M は β 正規形 N をもつ、あるいは N は M の β 正規形であるという.

定理 3.4 (Church-Rosser の定理). M ⊳_{β} N かつ M ⊳_{β} R ならば次のような項 T が存在する. N ⊳_{β} T かつ R ⊳_{β} T.

4 ラムダ項から CLt-項への変換

定義 4.1 (変換^{∘}). M をラムダ項とする。このとき CLt-項への変換 M^{∘} を以下のように帰納的に定義する。

1. x^{∘} ≡ x

2. (MN)^{∘} ≡ M^{∘}N^{∘}

3. (λx.M)^{∘} ≡ λx^{t}.M^{∘}

また λx^{t}.M を以下のように帰納的に定義する。定義 4.2 (変換 t). M を CLt-項, x を変数とする. 変数 x を含まない項 (λ^{t}x.M) を以下のように帰納的に定義する.

1. (λ^{t}x.x) ≡ I,

2. (λ^{t}x.MUV) ≡ K′MUV (M が閉項かつ x ∉ F V (UV) のとき),

3. (λ^{t}x.MUV) ≡ B′MU(λ^{t}x.V) (M が閉項かつ x ∉ F V (U) のとき),

4. (λ^{t}.MUV) ≡ C′M(λ^{t}x.U)V) (M が閉項かつ x ∉ F V (V) のとき),

5. (λ^{t}x.MUV) ≡ S′M(λ^{t}x.U)(λ^{t}x.V) (M_{1} が閉項かつ x ∈ F V (U) かつx ∈ F V (V)) の時),

6. (λ^{t}x.MN) ≡ (λ^{t}x.IMN),

7. (λ^{t}x.M) ≡ (λ^{t}x.IIM) .

この変換 t は David Turner によって発見された変換を少し変更したものである（[2] 参照）ほかの変換方法では λx_{1}, …, x_{n}.M を変換したときの変換後の項の大きさが最悪の場合 n^{2} に比例した大きさになってしまうのに対し、この変換は最悪の場合でも n に比例した大きさで抑えることができる。例 4.3 (変換例). 実際に λxyz.xz(yz) を CL-t 項に変換してみる。

λ^{t}z.xz(yz) ≡ λ^{t}z.I(xz)(yz)
≡ S′I(λ^{t}z.xz)(λ^{t}z.yz)
≡ S′I(λ^{t}z.Ixz)(λ^{t}z.Iyz)
≡ S′I(B′Ix(λ^{t}z.z))(B′Iy(λ^{t}z.z))
≡ S′I(B′IxI)(B′IyI)
λ^{t}yz.xz(yz) ≡ λ^{t}y.S′I(B′IxI)(B′IyI)
≡ B′(S′I)(B′IxI)(λ^{t}y.B′IyI)
≡ B′(S′I)(B′IxI)(C′(B′I)II)
λ^{t}xyz.xz(yz) ≡ λ^{t}x.B′(S′I)(B′IxI)(C′(B′I)II)
≡ C′(B′(S′I))(λ^{t}x.B′IxI)(C′(B′I)II)
≡ C′(B′(S′I))(C′(B′I)(C′(B′I)))

よって (λxyz.xz(yz))^{∘} ≡ C′(B′(S′I))(C′(B′I)(C′(B′I))) となる。

5 CLt-項からラムダ項への変換

定義 5.1 (CLt-項からラムダ項への変換). CLt-項からラムダ項への変換^{♯} を以下のように帰納的に定義する。 x^{♯} ≡ x I^{♯} ≡ λx.x K′^{♯} ≡ λxyzu.xyz B′^{♯} ≡ λxyzu.xy(zu) C′^{♯} ≡ λxyzu.x(yu)z S′^{♯} ≡ λxyzu.x(yu)(zu) (MN)^{♯} ≡ M^{♯}N^{♯}

6 =_{α} であることの証明

ここではラムダ項 M に対し、この方法を用いて求まったものが、その正規形 M^{∗} と β 同値であることの証明を行う。まずは準備として以下の補題を示す。注意として、これ以降の証明では S′ 等の基本結合子をラムダ項に変換した際に現れる変数（例えば S′ を変換した λxyzu.x(yu)(zu) の xyzu）はすべて今までに現れてない変数 (new-variable) であるとする。補題 6.1. 任意の CLt-項 M に対し

(λ^{t}x.M)^{♯}x =_{β} M^{♯}

が成り立つ。 Proof. M に関する帰納法で示す。

■ M ≡ x の時

(λ^{t}x.x)^{♯}x ≡ I^{♯}x
≡ (λx.x)x
⊳_{1β} x

■ M ≡ M_{1}M_{2}M_{3} (M_{1} が閉項かつ x ∉ F V (M_{2}M_{3})) の時

(λ^{t}x.M_{1}M_{2}M_{3})^{♯}x ≡ (K′M_{1}M_{2}M_{3})^{♯}x
≡ (λxyzu.xyz)M_{1}^{♯}M_{2}^{♯}M_{3}^{♯}x
⊳_{1β} M_{1}^{♯}M_{2}^{♯}M_{3}^{♯}
≡ (M_{1}M_{2}M_{3})^{♯}

■ M ≡ M_{1}M_{2}M_{3} (M_{1} が閉項かつ x ∉ F V (M_{2})) の時

(λ^{t}x.M_{1}M_{2}M_{3})^{♯}x ≡ (B′M_{1}M_{2}(λ^{t}x.M_{3}))^{♯}x
≡ (λxyzu.xy(zu))M_{1}^{♯}M_{2}^{♯}(λ^{t}x.M_{3})^{♯}x
⊳_{1β} M_{1}^{♯}M_{2}^{♯}((λ^{t}x.M_{3})^{♯}x)

帰納法の仮定から (λ^{t}x.M_{3})^{♯}x =_{β} M_{3}^{♯} 、よって

\begin{matrix}=_{β} & M_{1}^{♯}M_{2}^{♯}M_{3}^{♯} \\ ≡ & (M_{1}M_{2}M_{3})^{♯} \end{matrix}

■ M ≡ M_{1}M_{2}M_{3} (M_{1} が閉項かつ x ∉ F V (M_{3})) の時上と同様に

(λ^{t}x.M_{1}M_{2}M_{3})^{♯}x ≡ (C′M_{1}(λ^{t}x.M_{2})M_{3})^{♯}x
≡ (λxyzu.x(yu)z)M_{1}^{♯}(λ^{t}x.M_{2})M_{2}^{♯}M_{3}^{♯}x
⊳_{1β} M_{1}^{♯}((λ^{t}x.M_{2})^{♯}x)M_{3}^{♯}
=_{β} M_{1}^{♯}M_{2}^{♯}M_{3}^{♯}
≡ (M_{1}M_{2}M_{3})^{♯}

■ M ≡ M_{1}M_{2}M_{3} (M_{1} が閉項かつ x ∈ F V (M_{2}) かつx ∈ F V (M_{3})) の時上と同様に

(λ^{t}x.M_{1}M_{2}M_{3})^{♯}x ≡ (S′M_{1}(λ^{t}x.M_{2})(λ^{t}x.M_{3}))^{♯}x
≡ (λxyzu.x(yu)(zu))M_{1}^{♯}(λ^{t}x.M_{2})^{♯}(λ^{t}x.M_{3})^{♯}x
⊳_{1β} M_{1}^{♯}((λ^{t}x.M_{2})^{♯}x)((λ^{t}x.M_{3})^{♯}x)
=_{β} M_{1}^{♯}M_{2}^{♯}M_{3}^{♯}
≡ (M_{1}M_{2}M_{3})^{♯}

■ M ≡ M_{1}M_{2} の時

(λ^{t}x.M_{1}M_{2})^{♯}x ≡ (λ^{t}x.IM_{1}M_{2})^{♯}x

I は閉項なので、上のいずれかと同じ議論をすればよい。

■ M ≡ M_{1} の時

(λ^{t}x.M_{1})^{♯}x ≡ (λ^{t}x.IIM_{1})^{♯}x

I は閉項なので、上のいずれかと同じ議論をすればよい。

定理 6.2. 任意のラムダ項 M に対し

(M^{∘})^{♯} =_{β} M

が成り立つ。

Proof. M に関する帰納法で示す。 ■ M ≡ x の時

\begin{aligned}(x^{∘})^{♯} & ≡ & x^{♯} \\ & ≡ & x \end{aligned}

■ M ≡ M_{1}M_{2}の時帰納法の仮定から

\begin{aligned}(M_{1}^{∘})^{♯} & ≡ & M_{1} \\ (M_{2}^{∘})^{♯} & ≡ & M_{2} \end{aligned}

よって

((M_{1}M_{2})^{∘})^{♯} ≡ (M_{1}^{∘}M_{2}^{∘})^{♯}
≡ (M_{1}^{∘})^{♯}(M_{2}^{∘})^{♯}
≡ M_{1}M_{2}

■ M ≡ λx.N の時

\begin{aligned}M^{∘} & ≡ & (λx.N)^{∘} \\ & ≡ & λ^{t}x.N^{∘} \end{aligned}

□ N^{∘} ≡ x の時

\begin{aligned}(λ^{t}x.x)^{♯} & ≡ & I^{♯} \\ & ≡ & λx.x \end{aligned}

□ N^{∘} ≡ N_{1}N_{2}N_{3} (N_{1} が閉項かつ x ∉ F V (M_{2}M_{3})) の時

(λ^{t}x.N_{1}N_{2}N_{3})^{♯} ≡ (K′N_{1}N_{2}N_{3})^{♯}
≡ (λxyzu.xyz)N_{1}^{♯}N_{2}^{♯}N_{3}^{♯}
⊳_{1β} λu.N_{1}^{♯}N_{2}^{♯}N_{3}^{♯}
=_{α} λx.N_{1}^{♯}N_{2}^{♯}N_{3}^{♯} (u は new-variable なので N_{1},N_{2},N_{3} には出現しない)
≡ λx.(N_{1}N_{2}N_{3})^{♯}
≡ λx.(N^{∘})^{♯}
=_{β} λx.N (帰納法の仮定より)

□ N^{∘} ≡ N_{1}N_{2}N_{3} (N_{1} が閉項かつ x ∉ F V (N_{2})) の時

(λ^{t}x.N_{1}N_{2}N_{3})^{♯} ≡ (B′N_{1}N_{2}(λ^{t}x.N_{3}))^{♯}
≡ (λxyzu.xy(zu))N_{1}^{♯}N_{2}^{♯}(λ^{t}x.N_{3})^{♯}
⊳_{1β} λu.N_{1}^{♯}N_{2}^{♯}((λ^{t}x.N_{3})^{♯}u)
=_{α} λx.N_{1}^{♯}N_{2}^{♯}((λ^{t}x.N_{3})^{♯}x)
=_{β} λx.N_{1}^{♯}N_{2}^{♯}N_{3}^{♯} (補題 6.1 より)
≡ λx.(N_{1}N_{2}N_{3})^{♯}
≡ λx.(N^{∘})^{♯}
=_{β} λx.N (帰納法の仮定より)

□ N^{∘} ≡ N_{1}N_{2}N_{3} (N_{1} が閉項かつ x ∉ F V (N_{3})) の時上と同様に

(λ^{t}x.N_{1}N_{2}N_{3})^{♯} ≡ (C′N_{1}(λ^{t}x.N_{2})N_{3})^{♯}
≡ (λxyzu.x(yu)z)N_{1}^{♯}(λ^{t}x.N_{2})^{♯}N_{3}^{♯}
⊳_{1β} λu.N_{1}^{♯}((λ^{t}x.N_{2})^{♯}u)N_{3}^{♯}
=_{α} λx.N_{1}^{♯}((λ^{t}x.N_{2})^{♯}x)N_{3}^{♯}
=_{β} λx.N_{1}^{♯}N_{2}^{♯}N_{3}^{♯}
≡ λx.(N_{1}N_{2}N_{3})^{♯}
≡ λx.(N^{∘})^{♯}
=_{β} λx.N

□ N^{∘} ≡ N_{1}N_{2}N_{3} (M_{1} が閉項かつ x ∈ F V (N_{2}) かつx ∈ F V (N_{3})) の時上と同様に

(λ^{t}x.N_{1}N_{2}N_{3})^{♯} ≡ (S′N_{1}(λ^{t}x.N_{2})(λ^{t}x.N_{3})^{♯}
≡ (λxyzu.x(yu)(zu))N_{1}^{♯}(λ^{t}x.N_{2})^{♯}(λ^{t}x.N_{3})^{♯}
⊳_{1β} λu.N_{1}^{♯}((λ^{t}x.N_{2})^{♯}u)((λ^{t}x.N_{3})^{♯}u)
=_{α} λx.N_{1}^{♯}((λ^{t}x.N_{2})^{♯}x)((λ^{t}x.N_{3})^{♯}x)
=_{β} λx.N_{1}^{♯}N_{2}^{♯}N_{3}^{♯}
≡ λx.(N_{1}N_{2}N_{3})^{♯}
≡ λx.(N^{∘})^{♯}
=_{β} λx.N

□ N^{∘} ≡ N_{1}N_{2} の時

(λ^{t}x.N_{1}N_{2})^{♯} ≡ (λ^{t}x.IN_{1}N_{2})^{♯}

I は閉項なので上のいずれかと同じ議論をすればよい。

□ N^{∘} ≡ N_{1} の時

(λ^{t}x.N_{1})^{♯} ≡ (λ^{t}x.IIN_{1})^{♯}

I は閉項なので上のいずれかと同じ議論をすればよい。

定理 6.3. CLt-項 M,N に対し M ⊳_{1wt} N ⇒ M^{♯} ⊳_{β} N^{♯}

Proof. (略証)

M ⊳_{1wt} N について使われた規則が (S′) の時を考える. このとき M は S′M_{1}M_{2}M_{3}M_{4} を含んでいる. つまり

M ≡ ⋯ (⋯ (S′M_{1}M_{2}M_{3}M_{4} ⋯) ⋯) ⋯

とあらわせる. よって N はこれを変換したもの、つまり

N ≡ ⋯ (⋯ (M_{1}(M_{2}M_{4})(M_{3}M_{4}) ⋯) ⋯) ⋯

とあらわせる. よって

M^{♯} ≡ ⋯^{♯} (⋯^{♯} ((S′)^{♯}M_{1}^{♯}M_{2}^{♯}M_{3}^{♯}M_{4}^{♯} ⋯^{♯}) ⋯^{♯}) ⋯^{♯}
≡ ⋯^{♯} (⋯^{♯} ((λxyzu.x(yu)(zu))M_{1}^{♯}M_{2}^{♯}M_{3}^{♯}M_{4}^{♯} ⋯^{♯}) ⋯^{♯}) ⋯^{♯}
⊳_{β} ⋯^{♯} (⋯^{♯} (M_{1}^{♯}(M_{2}^{♯}M_{4}^{♯})(M_{3}^{♯}M_{4}^{♯}) ⋯^{♯}) ⋯^{♯}) ⋯^{♯}
≡ N^{♯}

使われた変換規則がほかの場合も同様である.

定理 6.2, 定理 6.3 とラムダ項のチャーチ · ロッサー性から以下のことが成り立つ。

定理 6.4. ラムダ項 M に対し

M^{∗} =_{α} ((\overline{M^{∘}})^{♯})^{∗}

が成り立つ。

7 β 正規形の求まる速度

上記の方法を用いて β 正規形を求めるとき、実際に普通に求めるのと比較してどれくらい差があるのか、上記の方法を行う C プログラムを作成して検証してみた. そのプログラム及びマニュアルは以下のページにのせておく予定である.

http://www.math.s.chiba-u.ac.jp/˜ 04um0304/

このプログラムではラムダ項及び CLt-項を tree 型のグラフとして扱っている. また CLT-項に変換して求める場合の最後の β-リダクションについては、直接求める場合と同じ関数を用いて計算している. また代入の時は必ず α 変換を行うように作っており、代入を後回しにしたりせずに最後まで行ってから次に進むようにしてある.

例 7.1 (実行例 1). (λxyz.xz(yz))(λxy.y)(uu) の β 正規形を求めてみる以下プログラムの入出力である. > (lambda x y z . x z (y z))(lambda x y . y)(u u);

——————-kekka———————- (lambda x . u u x) 0 SEC chokusetu:(lambda x . u u x) 0 SEC ———————————————-

—kekka— 以降がプログラムの出力である。また SEC は β 正規形を求めるまでにかかった時間であり、 CLt-項になおして求める方法は CLt 項に変換を行うところから β 正規形を求めるまでにかかった時間である. また小数点以下は切り捨ててある. 確かに直接求める方法と =_{α} となっていることがわかる. またこのラムダ項には η -redex が含まれているが η リダクションは行われていないこともわかる. なお η リダクションとは以下のようなものであり余分な抽象を消し去る意味を持つ

(λx.Mx) ⊳_{η} M(x ∉ F V (M))

例 7.2 (ラムダ項における２進計算の足し算). 次の検証に使用するものは 2004 年度の修士論文「ラムダ計算における２進計算」 ([3] 参照) より、加算を行うラムダ項を、このラムダ項が正しい入力に対し正しく動くかどうかという確認も込めて、使用させていただきました. 以下に簡単にその定義を紹介します

基本的なラムダ項と整数 n の２進表記をラムダ項で表したものは以下のように定義する.

定義 7.3 (真偽値). ラムダ項 T, F を次のように定める。

\begin{aligned}T & ≡ & λxy.x \\ F & ≡ & λxy.y \end{aligned}

T, F をこのように定めることで、ラムダ項 LMN に対して、 L が T の場合は M、 L が F の場合は N とすることができる。定義 7.4 (1 桁の数). 整数 1, 0, −1 に対応するラムダ項 ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} を次のように定める。

\begin{aligned}˜1^{∗} & ≡ & λxyz.x \\ ˜0^{∗} & ≡ & λxyz.y \\ ˜−1^{∗} & ≡ & λxyz.z \end{aligned}

定義 7.5 (数の表現). 整数 n が次のように表せるとする。

n = 2^{i} ∗ x_{i} + 2^{i−1} ∗ x_{i−1} + 2^{i−2} ∗ x_{i−2} + … + 2^{0} ∗ x_{0} i ≥ 0
x_{j} (0 ≤ j ≤ i) は 1 または 0 または −1

この整数 n に対応するラムダ項 ñ を次のように定める。

ñ ≡ < ⋯ <<< ˜0, x̃_{i} >, x̃_{i−1} >, x̃_{i−2} >, ⋯ >, x̃_{0} >

ただし、 x_{k} (0 ≤ k ≤ i) から x_{i} には連続して ˜0 が現れないこと、また x_{k} には ˜1 と ˜−1 が同時には現れないこととする。また < M, N > は対を表しており以下のものの省略表現として用いている.

P air =^{def} λx.xMN M, N はラムダ項

定義 7.6. ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} の場合は ˜0^{∗}、 ñ =< M, N > の場合は M を返すようなラムダ項 Hdr を次のように定める。

Hdr =^{def} λx.(Isn x) ˜0^{∗} (xK)

また、 ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} の場合はそのまま、 ñ =< M, N > の場合は N を返すようなラムダ項 F tr を次のように定める。

F tr =^{def} λx.(Isn x) x (x(KI))

定理 7.7. ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} の場合には T 、対の場合には F を返すようなラムダ項 Isn は次のように定められる。

\begin{matrix}Isn = λx.xK_{3}^{3}KKIF T \\ x には任意のラムダ項を入力。 \end{matrix}

ただし K_{3}^{3} ≡ λxyz.z である.

定義 7.8. 1 桁の数同士を加算した結果、繰り上がりの値を返すラムダ項 Add_{1} と、繰り上がりを切り捨てた値を返すラムダ項 Add_{2} を以下のように定める。

Add_{1} =^{def} λxyz.x (y (z ˜1^{∗} ˜1^{∗} ˜0^{∗}) (z ˜1^{∗} ˜0^{∗} ˜0^{∗})  ˜0^{∗})
(y (z ˜1^{∗} ˜0^{∗} ˜0^{∗})  ˜0^{∗}  (z ˜0^{∗} ˜0^{∗} ˜−1^{∗}))
(y  ˜0^{∗}  (z ˜0^{∗} ˜0^{∗} ˜−1^{∗}) (z ˜0^{∗} ˜−1^{∗} ˜−1^{∗}))
Add_{2} =^{def} λxyz.x (y (z ˜1^{∗} ˜0^{∗} ˜1^{∗}) (z ˜0^{∗} ˜1^{∗} ˜0^{∗})  z)
(y (z ˜0^{∗} ˜1^{∗} ˜0^{∗})  z  (z ˜0^{∗} ˜−1^{∗} ˜0^{∗}))
(y  z  (z ˜0^{∗} ˜−1^{∗} ˜0^{∗}) (z ˜−1^{∗} ˜0^{∗} ˜−1^{∗}))

なお上において、 x は繰り上がり、 y, z は加算する数をあらわし、それぞれ ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} を入力。

これらの定義を用いて、ラムダ項 ñ_{1}, ñ_{2} を加算するラムダ項を再帰的に定義する。

定義 7.9. 繰り上がりおよび 2 つのラムダ項 ñ_{1}, ñ_{2} を加算した結果を返すラムダ項 Add^{∗} を次のように定める。

Add^{∗} = λxyz.

(Isn y)

((Isn z)

(P air (Add_{1} x y z) (Add_{2} x y z))
(P air (Add^{∗} (Add_{1} x (F tr y) (F tr z)) (Hdr y) (Hdr z))
(Add_{2} x (F tr y) (F tr z))))

(P air (Add^{∗} (Add_{1} x (F tr y) (F tr z)) (Hdr y) (Hdr z))

(Add_{2} x (F tr y) (F tr z)))

x は繰り上がりを表すラムダ項 ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} で、 y, z はラムダ項 ñ_{1}, ñ_{2}。

定義 7.10. 2 つのラムダ項 ñ_{1}, ñ_{2} を加算するラムダ項 Add を次のように定める。

Add =^{def} Add^{∗} ˜0^{∗}

例 7.11. 以上のラムダ項を用いて

1. ˜1^{∗} + ˜1^{∗},

2. < ˜1^{∗}, ˜1^{∗} > + << ˜1^{∗}, ˜0^{∗} >, ˜0^{∗} >,

3. <<<<<<< ˜1^{∗}, ˜0^{∗} >, ˜−1^{∗} >, ˜1^{∗} >, ˜0^{∗} >, ˜0^{∗} >, ˜−1^{∗} >, ˜1^{∗} > + <<<<<<<<<< ˜1^{∗}, ˜−1^{∗} >, ˜0^{∗} >, ˜−1^{∗} >, ˜1^{∗} >, ˜1^{∗} >, ˜1^{∗} >, ˜0^{∗} >, ˜−1^{∗} >, ˜−1^{∗} >, ˜0^{∗} >

の計算を行ってみた. ただし 3 に関しては直接求める方法では計算にかなりの時間がかかると思われるので行っていない. 以下がその出力である. ただし入力における N1, N0, Nm1 はそれぞれ ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} をあらわす

1. > Add N1 N1; ⋯ 入力 ——————-kekka———————- (lambda x . x (lambda x y z . x) (lambda x y z . y)) 0 SEC chokusetu:(lambda x . x (lambda x y z . x) (lambda x y z . y)) 27 SEC ———————————————- > 2. > Add (lambda x . x N1 N1)(lambda x . x (lambda x . x N1 N0)N0); ⋯ 入力

——————-kekka———————- (lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . x)) 0 SEC chokusetu:(lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . x)) 536 SEC ———————————————- >

3. > Add (lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x N1 N0)Nm1)N1)N0)N0)Nm1)N1) (lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x N1 Nm1)N0)Nm1)N1)N1)N1)N0)Nm1)Nm1)N0); ⋯ 入力 ——————-kekka———————- (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . z)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . y)) (lambda x y z . z)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x)) 3 SEC ———————————————- >

計算自体は正しく行われているので足し算に関しては正しく定義されているようである. また 1,2 からわかるように直接求めるよりも明らかに早く求まっていることがわかる. このように再帰を使っていたりするラムダ項に関しては, 直接求めるよりもかなり早く求めることができそうである.

8 終わりに

今回の結果については、正規形を求める速度についてかなりの差がでてしまっているが、なぜここまで差がでるかが理論的に解明する事がまだできていない、よって今後の課題としては、この差が生まれることを理論的に解明する事があげられる。

また、ラムダ計算において再帰を定義するために必要なラムダ項として Y コンビネータというものがある. 実際に今回検証に利用した２進数の足し算を行うラムダ項も再帰があるので, この Y コンビネータを使っている. この論文では Y コンビネータに関する変換規則を定義していないのだが, Y コンビネータに関する規則を CLt 項の変換規則に加えてやればさらに効率よく求めることができそうである.

9 謝辞

本論文作成にあたり、指導教官の古森雄一先生、ならびに古森研究室の皆様に多大なご協力を頂きましたことを心から感謝いたします。

参考文献

[1] S.C.Kleene, 「Proof by Cases in Formal Logic」 , The Annals of Mathematics, 2nd Ser., Vol.35,No3(Jul,1934)529-544, P537 の定理 6V

[2] 千葉大学理学部 2005 年度 前期情報数学 1 配布資料古森雄一著

[3] 千葉大学自然科学研究科 2004 年度修士論文, 大家幸敏, 「ラムダ計算における２進計算」 http://www.math.s.chiba-u.ac.jp/˜ komori/masters thesis/2004

[4] 高橋正子, 「計算論 -計算可能性とラムダ計算-」近代科学社 1991