あまり厳密ではないけど、ざっくり書いてみる。
計算理論
- 「計算」を数学的に厳密に定義することで、「計算」に何ができて何ができないのかを解き明かす理論。
ラムダ計算
- 計算理論で使われる1つのモデル。
- ラムダ式（≒1引数無名高階関数の定義）と簡約（≒関数が返す値の評価）ですべての計算を表現できるというもの。
- 複数の引数を持つ関数はカリー化によって1引数関数として扱われる。
- ラムダ式がラムダ式を受け取ったりラムダ式を返したりできないと、理論が成立しない。
- 型のないラムダ計算と、型付きラムダ計算の両方が研究されている。
関数型言語
- ラムダ計算を理論的基盤としたプログラミング言語。
- ラムダ式という名前の無名関数を記述できる。たいてい複数の引数を持つラムダ式を定義できるが、常にカリー化されるかどうかは言語による。
- すべてをラムダ式で扱うのは冗長だし効率も悪いので、関数や変数やリテラルなど、ラムダ式以外の要素も使うことができる。
- とはいえ、ラムダ式に限らず、ほとんどあらゆるものが式である。
- あらゆるものが式なので、returnが不要。
- 式を組み合わせることで計算手順を記述する。gotoが不要。
- 高階関数（引数や戻り値として関数を扱う関数）を使ってプログラムを書くのが普通。
- プログラムの実行は式の評価とほぼ同義。
