Open7
ラムダ計算の基本
りんすなんとなく読めてしまうがために今まで何となくやり過ごしてきたラムダ計算を、一度きちんと学んでおく
りんすラムダ計算の構成要素
ラムダ計算は、次の3つの要素からなる：
- 変数:
x y - 抽象記号:
\lambda. - 括弧:
( )
りんすラムダ式の定義
ラムダ式の集合
-
x x \in \Lambda -
x M \in \Lambda \lambda x. M \in \Lambda -
M \in \Lambda N \in \Lambda (M N) \in \Lambda
りんすラムダ式の文法
ラムダ式の文法には、次のルールがある：
- 最外側の括弧は、これを無条件に外すことができる
(M N) = M N
- 適用は左結合
M N P = ((M N) P)
- 抽象は右結合
\lambda x. \lambda y. M = \lambda x. (\lambda y. M)
- 適用の結合は、抽象記号のそれよりも優先される
\lambda x. M N = \lambda x. (M N)
- 抽象記号の連続は、略記できる
\lambda x. \lambda y. \lambda z. M = \lambda x y z. M
りんす自由変数と束縛変数
抽象の本体のうち、抽象によって導入される変数を束縛変数(bound variables)という。適用によって抽象の変数（引数）に値を結びつけることを束縛と呼び、同じことだが、値が変数に束縛されるなどという。束縛変数以外の変数を自由変数(free variables)と呼ぶ。
次のラムダ式のうち
ラムダ式
-
\mathrm{FV}(x) = x - ただし
x
- ただし
-
\mathrm{FV}(\lambda x. M) = \mathrm{FV}(M) \backslash x - ただし
\lambda x. M
- ただし
-
\mathrm{FV}(M N) = \mathrm{FV}(M) \cup \mathrm{FV}(N) - ただし
(M N)
- ただし
自由変数を持たないラムダ式を閉じている(closed)などという。
ある抽象の自由変数は、より外側の抽象の束縛変数でありうる。ラムダ式
りんす簡約
ラムダ式の意味は、どのようにラムダ式を簡約(reduction)できるかによって定義される。簡約には次の３つがある：
-
\alpha - 変数名の変更
- E.g.
\lambda x. f x \rightarrow \lambda y. f y
-
\beta - 抽象に変数を適用する
- E.g.
(\lambda x. M x x)N \rightarrow M N N
-
\eta - 外延的等価（任意の引数について同じ結果を返す等価関係）
- E.g.
\lambda x. f x \rightarrow f
簡約によって同じ形に変換できることによって定義されるラムダ式の同値関係を、それぞれの名前を冠して次のように呼ぶ：
-
\alpha -
\beta -
\eta
りんすラムダ式の例
- 関数
id :: a -> a\lambda x. x
- 関数
const :: a -> b -> a\lambda xy. x
- チャーチ数
- 0:
\lambda xy. y - 1:
\lambda xy. x y - 2:
\lambda xy. x (x y)
- 0:
- ブール値
- true:
\lambda xyz. x y - false:
\lambda xyz. x z
- true:
-
if a then b else c-
\lambda abc. abc - ただし変数
a -
\eta \lambda a. a idと\eta
- ただし変数
-