有限ラムダ多項式によるクロージャーの定義
クロージャーの定義
ラムダ式は以下のものから構成されます。
- 定数
- 変数
- let
=
in
- subst
=
in
- def
(
) =
in
- fun (
) =
- if
then
else
集合 の元は変数
、式
、
の元
の組
とします。この元は再帰的定義にはなっていないとします。この元を
と書くことにします。集合
を「時代」、
の元を「環境」と呼びます。
ある環境 で変数
に対応する式
を以下のように帰納的に定義します。
のとき
のとき
のとき
ある環境 に対して、変数
に対応する式を
で置き換えた環境
を以下のように帰納的に定義します。
のとき
のとき
のとき
ある時代 と環境
での式
の値
を考えます。
定数
の値
定数 の値は
です。
変数
の値
変数 の値は
です。
let
=
in
の値
は変数、
と
は式です。
の「次の時代」
を
とし、
で
とします。
subst
=
in
の値
は変数、
と
は式です。
の「次の時代」
を
とし、
で
とします。このような が存在しないときは
とします。
fun (
) =
の値
無名関数を表します。 は変数、
は式です。
です。
if
then
else
の値
、
、
は式です。
は
が
(「真」を表す定数)のとき
、
が
ではないとき
となります。
if
then
else
の値
上記の if を拡張したものも考えます。 は演算子、
は
の項数、
は変数、
、
、
は式です。
は
が
に一致するときは、
となります。
が
に一致しないときは、
となります。