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

ラムダ計算における2進数計算

平成 17 年 3 月

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

大家幸敏目次

1 はじめに 2 2 基本的なラムダ項 2 3 数の定義 3 4 基本的な算術の定義 5 5 加算の定義 7 6 減算の定義 8 7 乗算の定義 9 8 除算の定義 9 9 計算可能性 10 10 付録 11 11 おわりに 11 12 謝辞 13

1 はじめに

ラムダ計算における数の表現としては例えば次のようなものが知られている。

• (チャーチ数)

自然数 n (n ≥ 0) に対してラムダ項 n̄ を以下のように定める。

n̄ =^{def} λfx.f^{n}x

ただし M^{n}N は以下の通り。

\begin{aligned}X^{n}Y & ≡ & \underbrace{X(X(… (X}_{n 個の X}Y) …)) \\ X^{0}Y & ≡ & Y \end{aligned}

• 自然数 n (n ≥ 0) に対してラムダ項^{⌈}n^{⌉} を以下のように定める。

T =^{def} λxy.x
F =^{def} λxy.y
M.N =^{def} λx.xMN
[M_{1}, …, M_{n}] =^{def} \begin{cases}I & n = 0 \\ M_{1}.[M_{2}, …, M_{n}] & n > 0 \end{cases}
⌈n^{⌉} =^{def} [\underbrace{F, …, F}_{n 個の F}]

これらはいずれも自然数 n に対して、 1 つめの場合は n 個の f、 2 つめの場合は n 個の F というように、自然数をラムダ計算上では 1 進数とみなして計算を行うものである。しかし 1 進数とみなす場合、表記が直感的でなかったり演算のコストが高いなど、様々な場面において効率を上げることができない。そこで本論文では、自然数をラムダ計算上で 2 進数とみなして数の定義や四則演算の定義を行い、自然数上の任意の関数が数を 2 進数とみなしたラムダ計算上で定義可能であることを示した。

なおこの論文は古森雄一先生より詳細な方針を与えられ、それらの検討・検証を大家が行った。

2 基本的なラムダ項

定義 2.1. ラムダ項 K, I を次のように定義する。

\begin{aligned}K & ≡ & λxy.x \\ I & ≡ & λx.x \end{aligned}

定義 2.2. ラムダ項 P air を次のように定める。

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

このとき M, N は対であるといい、以下では状況に応じて簡単のために

< M, N >

と書く。

定義 2.3. i, j が自然数かつ i ≥ 1 かつ 1 ≤ j ≤ i のとき、ラムダ項 K_{j}^{i} を次のように定める。

K_{j}^{i} ≡ λx_{1} … x_{i}.x_{j} i, j : 自然数かつ i ≥ 1 かつ 1 ≤ j ≤ i

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

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

T, F をこのように定めることで、ラムダ項 LMN に対して、 L が T の場合は M、 L が F の場合は N とすることができる。

3 数の定義

定義 3.1. (1 桁の数) 整数 1, 0, −1 に対応するラムダ項 ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} を次のように定める。

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

定義 3.2. (数の表現) 整数 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 が同時には現れないこととする。

例 3.3. 整数 5 に対応するラムダ項 ˜5 を考える。

5 = 2^{2} ∗ 1 + 2^{1} ∗ 0 + 2^{0} ∗ 1

であるので、 ˜5 は

˜5 =<<< ˜0^{∗}, ˜1^{∗} >, ˜0^{∗} >, ˜1^{∗} >

と表すことができる。また

5 = 2^{4} ∗ 0 + 2^{3} ∗ 0 + 2^{2} ∗ 1 + 2^{1} ∗ 0 + 2^{0} ∗ 1

であるが、

˜5 =<<<<< ˜0^{∗}, ˜0^{∗} >, ˜0^{∗} >, ˜1^{∗} >, ˜0^{∗} >, ˜1^{∗} >

と表すことはできない。 (連続した ˜0)

同様に、

5 = 2^{3} ∗ 1 + 2^{2} ∗ (−1) + 2^{1} ∗ 0 + 2^{0} ∗ 1

であるが、

˜5 =<<<< ˜0^{∗}, ˜1^{∗} >, ˜−1^{∗} >, ˜0^{∗} >, ˜1^{∗} >

と表すことはできない。 (˜1 と ˜0 が同時に現れる)

数の表現として、上の方法とは別にリストを使った方法も考えることができる。しかしリストを使う場合、 nil 定数をリストの終点とみなすわけだが、例えば nil =^{def} F としても、一般のラムダ項が nil と等しいかどうかをいうことは非常に困難であるため、ここではリストを使った方法を選択しなかった。

なお、以降のラムダ項においては、入力されるラムダ項に一定の制限を課しており、この制限内での入力に対しては期待する変換が行われるものとする。制限をはずれた入力に対しては、いくらかの変換は進むものの、期待される変換が行われる保証はない。この期待しない結果が返ることを未定義と言う。

以下では明示されない入力に対する変換は未定義とする。ただし文脈から入力が容易に推測される場合においても入力は明示しないこととする。

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

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

Proof. 次のラムダ項 M を考える。

M = λx.xα_{1}α_{2}α_{3}α_{4}α_{5}α_{6} α_{i}(1 ≤ i ≤ 6) はラムダ項

このラムダ項 M に対して次のようになる α_{i}(1 ≤ i ≤ 6) を定めたい。

M˜1^{∗} =_{β} T  (1)
M˜0^{∗} =_{β} T  (2)
M ˜−1^{∗} =_{β} T  (3)
M < U, V > =_{β} F  U, V はラムダ項  (4)

(1) から (4) の左辺をベータ変換すると次のようになる。

M˜1^{∗} =_{β} α_{1}α_{4}α_{5}α_{6}  (5)
M˜0^{∗} =_{β} α_{2}α_{4}α_{5}α_{6}  (6)
M ˜−1^{∗} =_{β} α_{3}α_{4}α_{5}α_{6}  (7)
M < U, V > =_{β} α_{1}UV α_{2}α_{3}α_{4}α_{5}α_{6}  (8)

(8) より

α_{1} = K_{3}^{3}  (9)

とすることで、 U, V に依存しない形にできる。また、 (5) および (9) より

M˜1^{∗} =_{β} α_{6}  (10)

であるから

α_{6} = T  (11)

が定まる。なお (8) は (9) により

M < U, V > =_{β} α_{2}α_{3}α_{4}α_{5}α_{6}  (12)

とベータ変換できる。ここで α_{2} = I とすると、 (12) より M˜0 =_{β} α_{3}α_{4}α_{5}α_{6} となるが、 (12) より M ˜−1 =_{β} M < U, V > となり不適当。そこで

α_{2} = K  (13)

とすると、 (6) (7) (12) は (9) (11) (13) よりそれぞれ

M˜0^{∗} =_{β} α_{4}T  (14)
M ˜−1^{∗} =_{β} α_{3}α_{4}α_{5}T  (15)
M < U, V > =_{β} α_{3}α_{5}T  (16)

となる。

(16) より

α_{3} = K  (17)
α_{5} = F  (18)

また (14) (15) より

α_{4} = I  (19)

と定めればよいことがわかる。以上 (9) (11) (13) (17) (18) (19) より

Isn = λx.xK_{3}^{3}KKIF T

とすれば題意を満たす。

4 基本的な算術の定義

定義 4.1. ˜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))

定義 4.2. ラムダ項 ñ

\begin{matrix}ñ ≡< ⋯ << x̃_{i}, x̃_{i−1} >, ⋯ >, x̃_{j} >, ⋯ >, x̃_{0} > i ≥ 0 0 ≤ j ≤ i \\ x̃_{k} = ˜0 (j ≤ k ≤ i) \end{matrix}

に対して

< ⋯ << x̃_{j−1}, x̃_{j−2} >, ⋯ >, x̃_{0} >

を返すラムダ項 T r を次のように定める。

T r =^{def} λx. (Isn (Hdr x))

((Hdr x) x (F tr x) x)

((Iz (T r (Hdr x)))
(F tr x)
(P air (T r (Hdr x)) (F tr x)))

x には ñ を入力。

ここでラムダ項 Iz は、あるラムダ項が ˜0^{∗} の場合に T、そうでなければ F を返すもので、次のように定める。

Iz =^{def} λx. (Isn x) (x F T F) F

x には任意のラムダ項を入力。

定義 4.3. ラムダ項 ñ

\begin{matrix}ñ ≡< ⋯ << x̃_{i}, x̃_{i−1} >, ⋯ >, x̃_{0} > i ≥ 0 \\ x̃_{i} = ˜1^{∗} x̃_{j} (0 ≤ j ≤ i) は˜1^{∗}, ˜0^{∗}, ˜−1^{∗}のいずれか \end{matrix}

に対して、

\begin{matrix}< ⋯ << x̃_{k}, { \atop x_{k−1}} >, ⋯ >, k̃_{0} > k ≥ 0 \\ x̃_{k} = ˜1^{∗} x̃_{l} (0 ≤ l ≤ i) は˜1^{∗}, ˜0^{∗}のいずれか \end{matrix}

と変換するラムダ項 Std を次のように定める。

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

Std^{∗} =^{def} λxy. (Isn y)

((Iz x) y ˜0^{∗})

((Iz x)
((F tr y)

(P air (Std^{∗} ˜0^{∗} (Hdr y)) (F tr y)) (P air (Std^{∗} ˜0^{∗} (Hdr y)) (F tr y)) (P air (Std^{∗} ˜−1^{∗} (Hdr y)) ˜1^{∗}))

((F tr y)

(P air (Std^{∗} ˜0^{∗} (Hdr y)) ˜0^{∗})
(P air (Std^{∗} ˜−1^{∗} (Hdr y)) ˜1^{∗})
((F tr (Hdr y))
(P air (Std^{∗} ˜0^{∗} (Hdr y)) ˜1^{∗})
(P air (Std^{∗} ˜−1^{∗} (Hdr y)) ˜0^{∗})
(P air (Std^{∗} ˜−1^{∗} (Hdr y)) ˜1^{∗}))))

x は ˜−1^{∗} を変換するための桁借りで、 y に変換対象のラムダ項 ñ を入力。

定義 4.4. 自然数 n が m より大きいとき、ラムダ項 ñ は m̃ より大きいという。ラムダ項 ñ が ˜0 より大きい場合は T そうでなければ F を返すラムダ項 Gt を次のように定める。

Gt =^{def} λx. (Isn (Hdr x)) ((F tr x) T F F) T

x にはラムダ項 ñ を入力。

5 加算の定義

定義 5.1. 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} を加算するラムダ項を再帰的に定義する。

定義 5.2. 繰り上がりおよび 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}。

このように再帰的定義可能であることは、次の定理より示される。定理 5.3. (再帰定理)

任意のラムダ項 M と変数 x に対して fx =_{β} Mfx となるラムダ項 f が定められる。 Proof. 以下のラムダ項

Y =_{β} λf.(λx.f(xx))(λx.f(xx))

に対して f = Y M とすると

Y Mx ≡ (λf.(λx.f(xx))(λx.f(xx)))Mx
→_{β} (λx.M(xx))(λx.M(xx)))x
→_{β} M((λx.M(xx))(λx.M(xx)))x
M(Y M)x ≡ M((λf.(λx.f(xx))(λx.f(xx)))M)x
→_{β} M((λx.M(xx))(λx.M(xx)))x

より Y Mx =_{β} M(Y M)x

以上より、 2 つのラムダ項 ñ_{1}, ñ_{2} を加算するラムダ項を定義することができる。定義 5.4. 2 つのラムダ項 ñ_{1}, ñ_{2} を加算するラムダ項 Add を次のように定める。

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

6 減算の定義

減算は加算する 2 つのラムダ項のうち、片方のラムダ項 ñ =< ⋯ << x̃_{i}, x̃_{i−1} >, ⋯ >, x̃_{0} > (i ≥ 1) の各 x̃_{j} (1 ≤ j ≤ i) を正負逆転させたものとの加算として定義できる。定義 6.1. ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} をそれぞれ ˜−1^{∗}, ˜0^{∗}, ˜1^{∗} に変換するラムダ項 Inv^{∗} を次のように定める。

Inv^{∗} =^{def} λx.x ˜−1^{∗} ˜0^{∗} ˜1^{∗}

定義 6.2. ñ の正負を逆転させるラムダ項 Inv を次のように定める。

Inv =^{def} λx. (Isn x)

(Inv^{∗} x)
(P air (Inv (Hdr x)) (Inv (F tr x)))

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

Sub =^{def} λxy.Add x (Inv y)

7 乗算の定義

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

Mul =^{def} λxy. (Isn y)

(y x ˜0^{∗} (Inv x))

(Add (Mul x (F tr y)) (P air (Mul x (Hdr y)) ˜0^{∗})

8 除算の定義

定義 8.1. ラムダ項 ñ

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

に対して、

< x̃_{i}, < x̃_{i−1}, ⋯ < x̃_{1}, x̃_{0} > ⋯ >

を返すラムダ項 Rev_{a} を次のように定める。

Rev_{a} x =^{def} λ x . (Isn (Hdr x)) x (Con (Rev_{a} (Hdr x)) (F tr x))

ここでラムダ項 Con は、ラムダ項 x̃ が ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} のいずれかであるとき、

\begin{matrix}Con < x̃_{k}, < { \atop x_{k−1}}, ⋯ < x̃_{1}, x̃_{0} > ⋯ > x̃ (k ≥ 0) \\ =_{β}< x̃_{k}, < { \atop x_{k−1}}, ⋯ < x̃_{1}, < x̃_{0}, x̃ > ⋯ > \end{matrix}

と変換するラムダ項で、次のように定める。

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

(P air (Hdr x) (P air (F tr x) y))

(P air (Hdr x) (Con (F tr x) y))

x には ñ を入力、 y には ˜1^{∗}, ˜0^{∗}, ˜−1^{∗} のいずれかを入力。また逆に

< x̃_{i}, < x̃_{i−1}, ⋯ < x̃_{1}, x̃_{0} > ⋯ >

に対して

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

と変換するラムダ項 Rev_{d} を次のように定める。

Rev_{d} =^{def} λx. (Isn x) x (P air (Hdr x) (Rev_{d} (F tr x)))

x には Rev_{a} で変換されたラムダ項を入力。定義 8.2. ラムダ項 ñ_{1}, ñ_{2} から商と余りの対を返すようなラムダ項 Div を次のように定める。

Div =^{def} λxy. P air (Rev_{d} ((Div^{∗} ˜0^{∗} x y) K)) (Rev_{d} ((Div^{∗} ˜0^{∗} x y) (KI))))

x, y はそれぞれラムダ項 ñ_{1}, ñ_{2} を入力。

Div^{∗} =^{def} λxyz. (Isn z)

((Gt (Sub (Rev_{d} (P air x z)) y))

(P air ˜1 (Sub (Rev_{d} (P air x z)) y))
(P air ˜0 (P air x z)))
((Gt (Sub (Rev_{d} (P air x (z K))) y))
(P air (P air ˜1 (A K)) (A (K I)))
(P air (P air ˜0 (B K)) (B (K I))))

x, y はそれぞれ Rev_{a} で変換済みの ñ_{1}, ñ_{2}、 z には計算途中の余りを入力。出力は対であり、また Rev_{a} で変換された形になることに注意。

なお A, B は以下。

A ≡ (Div^{∗} (Std (Sub (Rev_{d} (P air x (z K))) y)) y (z (K I)) )

B ≡ (Div^{∗} (Std (Rev_{d} (P air x (z K)))) y (z (K I)) )

9 計算可能性

定理 9.1. 自然数上の計算可能な関数が、任意の自然数 n (n ≥ 0) に対してラムダ項 ñ を考えることにより定義可能である。

Proof. 自然数上の計算可能な関数が、本論文の冒頭で紹介したチャーチ数によって定義可能であることは既に知られている。そこで、任意の自然数 n に対するチャーチ数\overline{n} とラムダ項 ñ との相互変換を与えることによって自然数上の計算可能な関数が定義可能であることを示す。今、\overline{n} から ñ への変換を行うラムダ項を T_{12}、逆に ñ から\overline{n} への変換を行うラムダ項を T_{21} とする。これら T_{12} および T_{21} は次のように定められる。

T_{12} = λx. (x (T F) T) ˜0^{∗} (Add ˜1^{∗} (T_{12} (P red x))

T_{21} = λx. (Isn x)

(x ˜1^{∗} ˜0^{∗} ˜1^{∗})
(+_{1} (∗_{1} (T_{21} (Hdr x)) \overline{2}) (T_{21} (F tr x)))

ここで、 +_{1}, ∗_{1}, P red はそれぞれチャーチ数に対する演算で、 +_{1} は 2 つのチャーチ数の加算、 ∗_{1} は 2 つのチャーチ数の乗算、 P red はチャーチ数\overline{n} に対して\overline{n − 1} を返すラムダ項である。これらのラムダ項によりチャーチ数との相互変換を行うことで、自然数上の任意の関数が定義可能であることを示すことができる。

10 付録

チャーチ数

• 数の表現自然数 n(n ≥ 0) に対してラムダ項\overline{n} を\overline{n} =^{def} λfx.f^{n}(x) と定める。ただし M^{n}(N) は

\underbrace{M(M(… (M}_{n 個}N) …)) の略。

• 演算 \overline{n} に対して\overline{n + 1} を返すラムダ項 Succ、 2 つのチャーチ数の加算を行うラムダ項 +_{1}、 2 つのチャーチ数の乗算を行うラムダ項 ∗_{1}、 2 つのチャーチ数の積算を行うラムダ項 P ow をそれぞれ次のように定める

Succ =^{def} λyfx.f(yfx)
+_{1} =^{def} λyzfx.yf(zfx)
∗_{1} =^{def} λyzf.y(zf)
P ow =^{def} λyz.zy

2 つのチャーチ数\overline{m}, \overline{n} に対して、 < \overline{m}, \overline{n} >⟶^{f}< \overline{n}, \overline{n + 1} > と変換するラムダ項 f を次のように定める。

\begin{matrix}f & =^{def} & λp. < (π_{2}^{2} p), (Succ (π_{2}^{2} p)) > \\ π_{2}^{2} & =^{def} & λp.p(λab.b) \end{matrix}

なお π_{2}^{2} はラムダ項 A, B に対して次のような変換を行うラムダ項である。

π_{2}^{2} < A, B >=_{β} B

チャーチ数\overline{n} に対して、 n が 0 より大きいときは\overline{n − 1}、 n が 0 のときは\overline{0} を返すラムダ項 P red を上の f を用いて次のように定める。

P red =^{def} λn.(π_{1}^{2}(nf < \overline{0}, \overline{0} >))

なお π_{2}^{2} はラムダ項 A, B に対して次のような変換を行うラムダ項である。

π_{2}^{2} < A, B >=_{β} B

11 おわりに

今回、以上の定義を検証するために Lamal^{1} を使用した。しかし Lamal では次のようなラムダ項に対する変換の出力が崩れるという現象^{2} を発見した。

1古森雄一作 2作者曰く、仕様とのこと。

T HIS IS NLAMGAR2 ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗∗  (20)
SIZE OF node = 16 ∗ ∗ ∗ P LEASE W AIT A MOMENT.  (21)
F reeNodes = 6006  (22)
K = lambda x y x;  (23)
K = lambda x y x;  (24)
A = lambda x(x K K);  (25)
A = lambda x(x K K);  (26)
A K;  (27)
A K;  (28)
A K  (29)
( lambda x ( x ( co880 : lambda x y x) co880 ) ) co880  (30)
sub ( co880 : lambda x y x) ( cons x co880 0 )  (31)
newnodes = 10  (32)

(23) (25) (27) が入力で、それ以外は Lamal による出力である。ここで期待する出力は K すなわち lambda x y x であるが、このとおり出力が崩れてしまって

いる。これは lamal がベータ変換を行わないことに起因することをつきとめたが、改良が困難であったため、本論文では Lamal によるコードを省略した。ただし Lamal による検証コードは以下のページで公開する予定である。

http://www.math.s.chiba-u.ac.jp/˜ 03um0302/

12 謝辞

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

参考文献

[1] J.R.Hindley and J.P.Seldin: Introduction to combinators and lambda-calculus (Cambridge University Press, 1986)

[2] 千葉大学理学部 2000 年度後期計算理論配布資料

[3] Mayer Goldberg: One-Point Bases For λ-Calculi With Constants http://www.cs.bgu.ac.il/˜ gmayer/talks/files/one-point-bases.pdf