関数型プログラミング言語詳解

ラムダ計算という、頑張って全てを関数として表そうとする計算モデルがあるらしい。

ラムダ計算の式の変換

という変換だと理解した。

式は基本的に、外側＆左側から評価していくと、これ以上評価不可能な形に落ち着くらしい。

再帰関数の評価方法が面白い。
例えばFactorialを例にとる。

Factorialは処理中でFactorialが呼ばれるため、以下のように書ける

FAC = \n. (...FAC...) ← どこかでFACを使っている

β変換を使って切り出して書いてみる

FAC = \fac. (\n. (...fac...)) FAC

\fac. (\n. (...fac...)) の部分はFACとは独立している。

H = \fac. (\n. (...fac...))

として、

FAC = H FAC

上記式より、FACの内容はHにのみ依存して決まるため、Hを受け取ってFACを作る関数をYとする。つまり

FAC = Y H = H (Y H)

ここまでの法則を使って、FAC 1を評価してみる

ちなみに、Y H = H (Y H)を満たす実装の１つは以下である。

(* 3 4) = 12であるが、12というexpressionに「数値の12である」という意味づけをする必要がある。
評価する際に必要になるため、ラムダ計算で現れるexpressionにはそれぞれ意味づけをする必要がある。

例えば「✖️」は以下のような意味を持つ

このように意味づけをしておくことで、例えば「aが0の場合、bを評価しなくて良い」のようなことが可能になる。

E1 ⇔ E2ならばEval[[ E1 ]] = Eval[[ E2 ]]が言えるが、逆は言えない。

Enriched Lambda ExpressionのBNF

Bというexpressionにvという名前をつけてE中で使える

(let v = B in E) = ((\v.E) B)

letrec f  ...f ...g
          g = ...f....

のように、再起が使える版のret

(letrec v = B in E) = (let v = Y (\v.B) in E)