計算能力

計算能力についてのメモ。間違ってるかもしれないけど。

計算能力の高い順で並べてみた。

• 部分帰納的関数（partial recursive function） ＝ チューリング機械（Turing machine）
• 多相λ計算（polymorphic lambda calculus, System F）
• ゲーデルの体系（T）
• 原始帰納的関数（primitive recursive function）
• 単純型つきλ計算（simply typed lambda calculus）

計算複雑性と一緒に表にしたら面白そうなんだけど、私には荷が重い。

「Barendregt's Lambda Cube」ではλ-cubeについてまとめられている。でも分かりにくいので、以下に表にしてみた。

• λ項を項変数でλ抽象
• λ項を型変数でλ抽象(2)
• 型を項変数でλ抽象(ω)
• 型を型変数でλ抽象(P)

一番上の「λ項を項変数でλ抽象」は基本的なもので、それ以外の下の三つ(2, ω, P)のあるなしで以下のように分類される。

2	ω	P	名前
×	×	×	λ→（単純型つきλ計算, simply typed lambda calculus）
○	×	×	λ2（多相λ計算, polymorphic lambda calculus, System F）
×	○	×	λω_
×	×	○	λP（LF）
○	○	×	λω（System Fω）
○	×	○	λP2
×	○	○	λPω_
○	○	○	λPω（CC, The Calculus of Constructions）

なんかいろいろと間違っている気がするので、そのうち直す。