2/13 夜会話
隣の人からラムダ式の定義とかモロモロについて語ってもらった。
内容のまとめなので、間違い多々ある気がする。
記号の加算無限集合identifier*1を定義する。
この時、次のラムダ式eは次のように定義される。
1. e∈identifier ならば、eはラムダ式である。
2. eをラムダ式とする時、(λx -> e)はラムダ式である。(ただし、x∈identifier)
3. a,bをラムダ式とするとき、(a b)はラムダ式である。
注：本来は.(ドット)を利用してλx.eのように書くべきだが、慣れないため、この記事では->として記述する。
やっぱり、手続き型言語とかやってる私みたいな人はドットを書かれるととにかく高い優先順位と見做してしまいがちな気がする。
ラムダ式で使用されるその他の定義
α変換(名前の変更)
(λx -> e) をα変換すると、(λy -> (e|x=>y))が得られる。
すなわち、(λx ->)を除去して、(λy -> e')を得る。
ここでe'は、e中のxをyに置き換えたものである。
ただし、α変換を行う場合、置き換え元のeはyに依存してはならない。*3
コンビネータ
よくつかわれるラムダ式として、次の３つがある。
コンビネータは、関数集合の部分集合。
I = λx -> x
K = λx -> (λy -> x)
F = λx -> (λy -> y)
Iコンビネータ
ID関数。 受け取った引数をそのまま返す関数。
コンビネータの適用
(K I) = ( (λx -> (λy -> x)) (λx -> x) )
(α変換) => ( (λa -> (λy -> a)) (λx -> x) )
(β簡約) => (λy -> (λx -> x)) = F
∴ (K I) = F
(F I) = ( (λx -> (λy -> y)) (λx -> x) )
(α変換) => ( (λa -> (λy -> y)) (λx -> x) )
(β簡約) => (λy -> y) = I
∴ (F I) = I
宿題
S = λxyz -> x z (y z) = (λx -> (λy -> (λz -> x z (y z)) ) ) とする。
この時、(S K K)を計算せよ。
この時、S = (λx -> (λy -> (λz -> x) z ) (y z) )とした間違えた展開をしないのは、変数の束縛の問題（らしい）。
与える解釈によっては、簡約がとまってそれ以上の展開ができなくなる（のかな？）
プログラミング言語の場合は式を与えると、先に型推論を行い、適用可能な型を見つけ出し、
実行時にそれ以外の型が来る場合、コンパイルエラーとなる。
一方で、ラムダ式で間違えた展開をした場合は、途中で束縛が止まるだけとなり、何も得られない。
このようなルールを定めるのは「便利」だからだそうだが、
正直、便利なのはいいとして、「何が不便」であって、こう解釈すると「何が便利か」が数式を見るだけだと見えてこないことが多い。
私が数学が苦手なのは、きっとこれが見つけられない分野なのだろうなあ。
集合論系統は実用とつながっていて、利点・表現できないと不便が見分けやすかったから。
