|
127
|
1 --Lambda Calculusの簡約
|
|
|
2
|
|
|
3 ここでは、Haskell の式をそのまま使う。record と data は使わない
|
|
|
4
|
|
|
5 ---Types
|
|
|
6
|
|
|
7 1. a,b,c などは型である。Haskell の Integer や Char も型である。
|
|
|
8
|
|
|
9 2. U,V が型なら U -> V も型である。(関数)
|
|
|
10
|
|
|
11 3. U,V が型なら (U , V) も型である。(Pair、直積)
|
|
|
12
|
|
|
13 ここでは、これらによって作られる型のみを考える。
|
|
|
14
|
|
|
15 ---Term
|
|
|
16
|
|
|
17 Term は以下の規則によって型と一緒に構築される。
|
|
|
18
|
|
|
19 1. Haskell の変数 x,y,z は項。つまり let a = ... で宣言された小文字で始まる記号。対応する型(変数で指定された)を持つ。
|
|
|
20 1 や 'a' も対応する型を持つ項である。
|
|
|
21
|
|
|
22 2. u が型U、v が型V を持てば、(u,v) は型(U,V)を持つ項である。
|
|
|
23
|
|
|
24 3. 型(U,V)を持つ項 t に対して、fst t は型U を持つ項、snd t は型 V を持つ項である。
|
|
|
25
|
|
|
26 4. v が型V を持つ項で、x0,x1,...,xn が型Uを持てば、 \x0 x1 ..., xn -> v は項である。
|
|
|
27 Haskell によって変数の名前のスコープは適切に扱われるとする。
|
|
|
28
|
|
|
29 5. t が型 U->V を持ち、u が 型U を持てば、 t u は型V を持つ項である。
|
|
|
30
|
|
|
31 これら項は、Haskell によって評価される。これらは変換規則と提供する。
|
|
|
32
|
|
|
33 1. 変数は変数の値
|
|
|
34
|
|
|
35 2. (u,v) は pair
|
|
|
36
|
|
|
37 3. fst と snd は pair の最初と次を取ってくる関数
|
|
|
38
|
|
|
39 4. lambda 式は、与えられた引数により変数の置き換えを行う
|
|
|
40
|
|
|
41 5. 関数の適用を行う。
|
|
|
42
|
|
|
43 ---等式
|
|
|
44
|
|
|
45 fst (x,y) == x
|
|
|
46 snd (x,y) == y
|
|
|
47 (\x y -> v) u == v
|
|
|
48
|
|
|
49 さらに
|
|
|
50
|
|
|
51 ((fst v),(snd v))==v
|
|
|
52 (\x t x) = t
|
|
|
53
|
|
|
54 ---正則形 (Normal form)
|
|
|
55
|
|
|
56 Haskell の計算は、これらの項をなるべく簡単に変換していくもの。
|
|
|
57
|
|
|
58 fst (u,v)
|
|
|
59 snd (u,v)
|
|
|
60 (\x -> v) u
|
|
|
61
|
|
|
62 のような形が式に含まれていなければ、式はこれ以上計算できない。
|
|
|
63
|
|
|
64 逆に含まれていれば、次のように変換できる。
|
|
|
65
|
|
|
66 fst (u,v) -> u
|
|
|
67 snd (u,v) -> v
|
|
|
68 (\x -> v) u -> v[u/x] (v の中のxをuで置き換える)
|
|
|
69
|
|
|
70 置き換えによって、さらに計算が進む場合もある。
|
|
|
71
|
|
|
72 --問題
|
|
|
73
|
|
|
74 以下の式を計算せよ
|
|
|
75
|
|
|
76 (\x -> (snd x,fst x)) (1,2)
|
|
|
77
|
|
|
78 以下の式は Haskkel がエラーを出す。
|
|
|
79
|
|
|
80 (\x -> (snd x,fst x)) ((\x -> t 3 ),2)
|
|
|
81
|
|
|
82 適切に実行されるように t に関する修正を加えよ。
|
|
|
83
|
|
|
84
|
