ラムダ計算
ラムダ計算 (lambda calculus) は、1930年代にアロンゾ・チャーチが関数による数学の基礎づけを目的として導入した形式的体系である。
ほどなくしてラムダ計算で表現できる関数のクラスは再帰的関数のクラスと一致することが示され（チャーチ＝チューリングのテーゼ、ラムダ計算はチューリングマシンと等価な計算モデルである）、数学全体の基礎づけには表現力が不十分であることがわかったが、1960年代に入ってプログラミング言語の理論的基盤として脚光を浴びる。Lisp、Scheme、OCaml、ML、Haskellなどの関数型プログラミング言語はラムダ計算を実装している。
基本的な定義 編集
公理 編集
最初の概念は「抽象化」である。これは関数の定義に類似している。
- λx.M
は引数 x を受け取り項 M を返す関数を定義する。
ラムダ計算の関数は名前を持たない。
第二の概念は呼出し( invocation )である。これは本質的には関数呼出し( call)である。
- M N
これは引数Nを項Mに結合する
定義 編集
ラムダ計算における項とは、定義された関数のことであり、項には変数を含むことができる。
- 変数
- 変数は任意の項を表すことができる。項には自由変数と束縛変数を含むことができる。
- 束縛変数
- 束縛変数は、引数として渡された項と束縛される変数である。例えば、λx.xyでは、xは束縛される変数である。
- 自由変数(Free variables)
- 自由変数は、ある項の中で、他の項に束縛されていない変数のことである。例えば、λx.xyにおいて、yは自由変数である。
型なしラムダ計算 編集
β簡約 編集
単純型つきラムダ計算 編集
関連書籍 編集
