2.3 ラムダ項を用いたデータ型の定義の例 (Natタイプ)

2.3 ラムダ項を用いたデータ型の定義の例 (N at タイプ)
自然数を表わすデータ型 (タイプ)N at を次のように定義する．
N at :≡ (P → P ) → (P → P )
データ型 (タイプ)N at を持つ対象を次のように定義する．
0 :≡ λf P →P λxP x
1 :≡ λf P →P λxP (f x)
2 :≡ λf P →P λxP (f (f x))
..
.
n :≡ λf P →P λxP (f (· · · (f x) · · ·))
| {z }
n個
0 に対するタイプチェックの例 (0 が N at の証明になっていることのチェック)．
[P ]x
→−Ix
P →P
N at(≡ (P → P ) → (P → P ))
→−If
2 に対するタイプチェックの例 (2 が N at の証明になっていることのチェック)．
[P → P ]
f
[P → P ]f
P
[P ]x
→E
→−E
P
→−Ix
P →P
N at(≡ (P → P ) → (P → P ))
→−If
次にタイプ N at に関する簡単なプログラムを書いてみることにする．まず，自然数 n を入力して n + 1(n
の次の数) を出力する Suc という関数のプログラム (アルゴリズム) をラムダ項で与える．
定義 2.3.1 (Suc)
Suc := λnN at λf P →P λxP (f ((nf )x))
計算の例： たとえば Suc に 3 を入力した場合の β− 簡約による計算の過程は次のようになる．
(Suc 3) ≡ (λnN at f P →P λxP (f ((nf )x))λf P →P λxP (f (f (f x))))
¤ λf P →P λxP (f ((λf P →P λxP (f (f (f x)))f )x))
¤ λf P →P λxP (f (λxP (f (f (f x)))x))
¤ λf P →P λxP (f (f (f (f x))))
≡ 4
練習問題 2.3.1 (Suc 4) を計算せよ．
20
Suc に対する自然演繹証明
[P → P ]f
[N at(≡ ((P → P ) → (P → P )))]n
P →P
P
→−Ix
P →P
N at(≡ (P → P ) → (P → P ))
N at → N at
[P → P ]f
P
→−E
[P ]x
→−E
→−E
→−If
→−In
次に自然数 2 つを引数とする加法のプログラムを与える．
定義 2.3.2 (+)
+ := λmN at λnN at λf P →P λxP ((mf )((nf )x))
計算の例：
3 + 2 ¤ ((+3)2)
¤ λf P →P λxP ((3f )((2f )x))
≡ λf P →P λxP (λxP (f (f (f x)))(f (f x)))
¤ λf P →P λxP (f (f (f (f (f x)))))
≡ 5
練習問題 2.3.2 対応する証明を作り，3 + 2 のタイプが N at となっていることを確かめよ．
乗法演算子 (かけ算) はこの言語で次のようにプログラムできる．
T imes := λmN at λnN at λf P →P (m(nf ))
このプログラム (T imes) のタイプが確かに N at → (N at → N at) となっていることを対応する (自然演
繹の) 証明を与えて確かめよ．
かけ算のプログラム T imes に 3 と 2 をインプットとして与えてプログラムを走らせた例
3 T imes 2
¤ ¤λf P →P (3(2f ))
¤ ¤λf P →P (3λxP (f (f x)))
≡ λf P →P (λf P →P λxP (f (f (f x))) λxP (f (f x)))
|
{z
}
≡F
¤ λf P →P λxP (F (F (F x)))
¤ λf P →P λxP (F (F (f (f x))))
¤ λf P →P λxP (F (f (f (f (f x)))))
¤ λf P →P λxP (f (f (f (f (f (f x))))))
≡ 6
21
練習問題 2.3.3 次の計算過程を示せ．
1. (3 + 4) + 2
2. (2 × 3) + 2
定義 2.3.3
Bool
T
F
def
≡
N at → (N at → N at)
≡
λaN at λbN at a
def
def
≡
λaN at λbN at b
定義 2.3.4 (タイプ A のプログラム x と y に対する if − then − else)
If − then − else := λpBool λxN at λy N at ((px)y)
即ち，If p then x:Nat else y:Nat を ((pxN at )y N at ) と定義していることとなる．
計算の例：
λpBool λxN at λy N at ((px)y)T st
¤¤ If T then s else t
≡
((λaN at λbN at a)s)t
¤
(λbN at s)t
¤
s
(なぜなら，変項が新たに束縛されることはないから．)
練習問題 2.3.4 s : N at 及び t : N at として If − then − else F st が t となることを計算せよ．
定義 2.3.5 (AN D，OR)
AN D
OR
def
≡
λaBool λbBool λmN at λnN at ((a((bm)n))((bn)m))
def
≡
λaBool λbBool λmN at λnN at ((a((bm)m))((bm)n))
(e.g.)
T OR F
¤¤ λmN at λnN at ((T ((F m)m))((F m)n))
≡
λmN at λnN at (((λcN at λdN at c)((F m)m))((F m)n))
¤
λmN at λnN at ((λdN at ((F m)m))((F m)n))
¤
λmN at λnN at ((F m)m)
≡
λmN at λnN at (((λcN at dN at d)m)n)
≡
T
¤¤ λmN at λnN at m
F OR F
¤¤ ((λmN at λnN at ((F ((F m)m))((F m)n))
¤¤ λmN at λN at ((F m)n)
¤¤ λmN at λN at n
≡
F
22
練習問題 2.3.5
T AN D T が
T AN D F
が
F AN D T
F AN D F
T OR T
が
が
が
T
F
F
F
T
F OR F
が F
となることを計算して確かめよ．
23