演習 5.2.1 論理演算の or 関数、not 関数を実装せよ。
| tru | = | λt.λf. t |
| fls | = | λt.λf. f |
| and | = | λb.λc. b c fls |
<or演算>
A or B は、
- A が tru なら tru を返す
- A が fls なら B を返す
このことから、 or = λb.λc. b tru c
<not演算>
not 演算は tru, fls を入れ替える。
このことから、 not = λa. a fls tr
演習 5.2.2 後者関数を定義する別の方法をみつけよ。
| c0 | = | λs.λz. z |
| c1 | = | λs.λz. s z |
| succ | = | λn.λs.λz. s (n s z) |
| succ' | = | λn.λs.λz. n s (s z) |
演習 5.2.3 plus を用いずに Church 数の乗算を定義せよ。
| plus | = | λm.λn.λs.λz. m s (n s z) |
| times | = | λm.λn. m (plus n) c0 |
| times' | = | λm.λn.λs.λz. m (n s) z |
演習 5.2.4 ある数を他の数で累乗する項を定義せよ。
pow = λm.λn. n (times m) c1
plus/timesの定義と同じような感じで
(補足：ゼミにて、 λm.λn. n m という別解がある by asai 先生)
演習 5.2.5 prd と使って減算の関数を定義せよ。
sub = λm.λn. n pred m
m から n回 prdすればよい。
演習 5.2.6 prd cn を計算するために、おおよそ何ステップの計算が必要か。
| prd cn | = | (λm. fst (m ss zz)) cn |
| -> | fst (cn ss zz) |
| = | fst ((λs.λz. s (s ... z)) ss zz) |
| -> | fst ((λz. ss (ss ... z)) zz) |
| -> | fst (ss (ss ... zz)) |
| = | fst (ss (ss .. (pair c0 c0))) |
以降、ss (pair c_n1 c_n2) のような app の eval が n 回行われる。
ss (pair c_n1 c_n2) を eval するためのステップ数を考える。
pair の eval は既に終わっているものとする。
| ss (pair c_n1 c_n2) |
| = | (λp. pair (snd p) (plus c1 (snd p))) (pair c_n1 c_n2) |
| -> | pair (snd (pair c_n1 c_n2)) (plus c_n1 (snd (pair c_n1 c_n2))) |
| -> | (λs.λb. b (snd (pair c_n1 c_n2)) s) (plus c_n1 (snd (pair c_n1 c_n2))) |
| -> | λb. b (snd (pair c_n1 c_n2)) (plus c_n1 (snd (pair c_n1 c_n2))) |
| -> | λb. b ((pair c_n1 c_n2) fls) (plus c_n1 (snd (pair c_n1 c_n2))) |
| -> | λb. b (fls c_n1 c_n2) (plus c_n1 (snd (pair c_n1 c_n2))) |
| -> | λb. b ((λf. f) c_n2) (plus c_n1 (snd (pair c_n1 c_n2))) |
| -> | λb. b c_n2 (plus c_n1 (snd (pair c_n1 c_n2))) |
| ->* | λb. b c_n2 (c_n1+c_n2) |
| (ここでかかるステップ数をn'とする) |
| (c_n1+c_n2 は (plus ..) の eval が終わったもの) |
★ plus の定義から、plus の評価には、
2(引数うけとり) + 4(ボディ部 m s (n s z) の eval) = 6ステップ
★ (snd (pair c_n1 c_n2)) の評価には、
2(pair部が引数うけとってλb. b c_n1 c_n2) +
1(snd引数受け取り) + 3 (snd内部) = 6ステップ
よって、 n' = 12
ss (pair c_n1 c_n2) を正規形にするのに19回ステップ必要なので、合計 19n
演習 5.2.7 等価性をブール値で返す equal を定義せよ
| equal c3 c3 | = | λt.λf. t |
| equal c3 c2 | = | λt.λf. f |
iszero = λn. n (λa.λb. fls) tru
equal = λm.λn. ((iszero (sub m n)) and (iszero (sub n m)))
演習 5.2.8 リスト [x, y, z] は λc.λn. c (x (c y (c z n))) となる。nil の表現はどうなるか。要素 h とリスト t を受け取り、h を t の前につける関数 cons をかけ。isnil, head, tail も書いてみよ。
| nil | = | λc.λn. n |
| cons | = | λh.λt.λc.λn. c h (t c n) |
| isnil | = | λt. t (λa. fls) tru |
| head | = | λt. t true n |
| g | = | λh.λp. pair (snd p) (cons h (snd p)) |
| tail | = | λt. fst (t g (pair nil nil)) |
演習 5.2.9 なぜ g の定義の中で、Churchブール値に関する Church ブール関数ではなく、プリミティブな if を使ったか。if でなく test を使った factorial を定義せよ。
二つの異なる表現であるChurch ブール値と、プリミティブなブール値の使用を
区別しなくてはならないから。
(補足：上のは間違っている。この章では call-by-value を仮定しているため、test では発散してしまうから。上の理由はなんか勘違いをしている... むしろ上の理由だと、if 文を使っちゃいけないことになる。ので完全に勘違い)
演習 5.2.10 プリミティブな自然数を対応する Church 数に変換する関数 churchnat を定義せよ。
churchnat = fix g
g = λcnat.λn. if (iszero 0) then (λa. c0) else (λa. scc (cnat (pred n)))
演習 5.2.11 fix と 演習 5.2.8 のリストの表現を用いて Church数のリストの総和を計算する関数をかけ。
sumall = fix g
g = λsm.λt. if (isnil t) then (λa. c0) else (λa. (plus (head a) (sm (tail a))))
演習 5.3.3 任意の項 t について、|FV(t)| <= size(t) を示せ。
部分項に関する帰納法で示す。
(i) t = x
成立。
(ii) t = λx.t1
*1) t1 は t の部分項なので、帰納法の仮定より、|FV(t1)| <= size(t1)
ここで、
| FV(t) | = | FV(t1) \ {x} |
| size(t) | = | size(t1) + 1 |
である。
このことから、
|FV(t)| <= |FV(t1)| かつ size(t1) <= size(t)
*1 より、 |FV(t)| <= size(t)
(iii) t = t1 t2
*2) 帰納法の仮定より、 |FV(t1)| <= size(t1)、|FV(t2)| <= size(t2)
ここで、
| FV(t) | = | FV(t1) ∪ FV(t2) |
| size(t) | = | size(t1) + size(t2) + 1 |
である。
このことから、
|FV(t)| <= |FV(t1)| + |FV(t2)|
size(t1) + size(t2) = size(t) - 1
*2 より、|FV(t1)| + |FV(t2)| <= size(t1) + size(t2)
すなわち、 |FV(t)| <= size(t) - 1
size(t) - 1 <= size(t) なので、|FV(t)| <= size(t) が示せた。
演習 5.3.6 これらの規則を変更し、他の三種の評価戦略(完全β簡約・正規順序・遅延評価) を表現するようにせよ。
演習以外の部分まだよんでいないのであとで解く。
演習 5.3.7 演習3.5.16では行き詰まり状態の項が特別な変数 wrong へと評価されるものを定義した。この意味論を λNBへと拡張せよ。
同様
演習 5.3.8 「大ステップ」スタイルでλ項の評価規則を形式化するにはどうすればよいか。
[大ステップの評価]
| t1 ↓ λx.t | t2 ↓ v | B-App |
| t1 t2 ↓ [x -> v]t |