TaPL読書録 #4

前回:

hkdnet.hatenablog.com

今回は5章終わりまで、と思っていたが 5.2. の最後まででいい時間になってしまったので終わり。

今回は記憶がおぼろげなのでおぼろげに書きます。

ラムダ計算におけるリストの表現などについて Scott encoding, Church encoding と言われて何もわからなかったが、以下のブログに詳しい。

d.hatena.ne.jp

ラムダ計算ができる言語が欲しくなるが、arrow function があるJavaScriptがよろしいのではないかという話になった

github.com

power の話になったときに、回答例の power2 がこれは確かに power であるという確信がもてない。ここで power2' について考える。

power2  = \n. \m. m n;
power2' = \n. \m. \s. \z. m n s z; # イータ変換による

型のようなナニカを雰囲気で想像したときに(要は定義をせずに使う)。
まず Church数 は2引数関数であり、第一引数に a -> a な関数を、第二引数に a を取り、a を返します。

cn :: (a -> a) -> a -> a

ここで m n に注目すると m :: (a -> a) -> a -> an :: (a -> a) -> a -> a について、 A = (a -> a) とすると n :: A -> A と捉えることも可能で型が一致しているような雰囲気があって面白い。

m :: (A -> A) -> A -> A
m :: ((a->a) -> (a -> a)) -> (a -> a) -> (a -> a) # 展開した
m n :: (a -> a) -> (a -> a) # nを適用した
m n :: (a -> a) -> a -> a # カリー化を考えると括弧に意味がない気がするので消した

となり m n が Church 数の型と一致するのが確認できる。

さて、我々は plus を手に入れ times を手に入れ power を手に入れるに至った。そうすると Knuth の矢印表記についても考えたくなるのは必然であるという話になった。ので、軟弱な私は即座にググった。

mindsarentmagic.org

やっぱりあったね。相性いいね、という気持ちになって終わった。

equal について、回答例では再帰を使わなかったが以下のようにも書けるような気がする。

eq = \m. \n. test (iszro m) (iszro n) (eq (prd m) (prd n));
eq = \m. \n. test (or (iszro m) (iszro n)) (and (iszro n) (iszro m)) (eq (prd m) (prd n))
2引数をとる関数に対応するYコンビネータ G に関して
equal = G eq

ここで教えてもらったのが、不動点コンビネータを使わずに関数を引数にとる方法もある。 lambda計算においては、適用するときに同じ項をそこに平べったく書けば良いとのこと(未検証)

fact f c = if (iszro c) then (succ 0) else (f f (prd c))
showFact = fact (if (iszro c) then (succ 0) else (f f (prd c))) c4

次回は5.3 〜 6章全体まで。