ラムダ計算と無限ラムダ多項式(13) - エレファント・ビジュアライザー調査記録

有限ラムダ多項式によるクロージャーの定義

有限ラムダ多項式

有限ラムダ多項式は以下のものから構成されます。

定数
変数
- $f$ は演算子、 $x_1, x_2, \cdots , x_n$ は有限ラムダ多項式

演算子 $f$ に対して演算子の項数 $n$ が決まっているとします。定数は項数 $0$ の演算子とします。

クロージャーの定義

ラムダ式は以下のものから構成されます。

定数
変数
$f(x_1, x_2, \cdots , x_n)$
$λ( (v_1, v_2, \cdots , v_n) . x, e)$
let $v$ = $x$ in $y$
subst $v$ = $x$ in $y$
def $f$ ( $v_1, v_2, \cdots , v_n$ ) = $x$ in $y$
fun ( $v_1, v_2, \cdots , v_n$ ) = $x$
if $x$ then $y$ else $z$

集合 $E$ の元は変数 $v$ 、式 $x$ 、 $E \cup \bot$ の元 $e$ の組 $\langle v, x, e \rangle$ とします。この元は再帰的定義にはなっていないとします。この元を $v \mapsto x : e$ と書くことにします。集合 $E$ を「時代」、 $E \cup \bot$ の元を「環境」と呼びます。

ある環境 $e$ で変数 $v$ に対応する式 $e(v)$ を以下のように帰納的に定義します。

$e = \bot$ のとき $e(v) = \bot$
$e = v \mapsto x : e'$ のとき $e(v) = x$
$e = v' \mapsto x : e' \ (v \ne v')$ のとき $e(v) = e'(v)$

ある環境 $e$ に対して、変数 $v$ に対応する式を $x$ で置き換えた環境 $e(v \gets x)$ を以下のように帰納的に定義します。

$e = \bot$ のとき $e(v \gets x) = \bot$
$e = v \mapsto y : e'$ のとき $e(v \gets x) = v \mapsto x : e'$
$e = v' \mapsto y : e' \ (v \ne v')$ のとき $e(v \gets x) = v' \mapsto y : e'(v \gets x)$

ある時代 $E$ と環境 $e \in E$ での式 $x$ の値 $\mathrm{val}(e, x)$ を考えます。

定数 $a$ の値

定数 $a$ の値は $\mathrm{val}(e, a) = a$ です。

変数 $v$ の値

変数 $v$ の値は $\mathrm{val}(e, v) = e(v)$ です。

$f(x_1, x_2, \cdots , x_n)$ の値

$f(x_1, x_2, \cdots , x_n)$ の値は、 $\mathrm{val}(e, f) = λ( (v_1, v_2, \cdots , v_n) . y, e')$ (クロージャー)のときは
$\mathrm{val}(e, λ( (v_1, v_2, \cdots , v_n) . y, e')(x_1, x_2, \cdots , x_n)) \\ = \mathrm{val}( e', \operatorname{let} v_1 = \mathrm{val}(e, x_1) \operatorname{in} \operatorname{let} v_2 = \mathrm{val}(e, x_2) \operatorname{in} \cdots \operatorname{let} v_n = \mathrm{val}(e, x_n) \operatorname{in} y)$
となります。このときクロージャーが持っている環境 $e'$ を使います。

$\mathrm{val}(e, f)$ がクロージャーではないときは、
$\mathrm{val}(e, f(x_1, x_2, \cdots , x_n)) = \mathrm{val}(e, f) ( \mathrm{val}(e, x_1), \mathrm{val}(e, x_2), \cdots , \mathrm{val}(e, x_n) )$
とします。 $\mathrm{val}(e, f)$ の部分は定数ではなくても良いものとします。

let $v$ = $x$ in $y$ の値

$v$ は変数、 $x$ と $y$ は式です。

$E$ の「次の時代」 $E'$ を $E' = E \cup \{v \mapsto x : e\}$ とし、 $E'$ で
$\mathrm{val}(e, \operatorname{let} v = x \operatorname{in} y) = \mathrm{val}(v \mapsto x : e, y)$
とします。

subst $v$ = $x$ in $y$ の値

$v$ は変数、 $x$ と $y$ は式です。

$E$ の「次の時代」 $E'$ を $E' = (E \setminus \{v \mapsto x' : e\}) \cup \{v \mapsto x : e\}$ とし、 $E'$ で
$\mathrm{val}(e, \operatorname{subst} v = x \operatorname{in} y) = \mathrm{val}(e(v \gets x), y)$
とします。このような $v \mapsto x' : e$ が存在しないときは
$\mathrm{val}(e, \operatorname{subst} v = x \operatorname{in} y) = \bot$
とします。

def $f$ ( $v_1, v_2, \cdots , v_n$ ) = $x$ in $y$ の値

関数定義を表します。 $f$ は変数(関数名)、 $v_1, v_2, \cdots , v_n$ は変数、 $x$ と $y$ は式です。
$\mathrm{val}(e, \operatorname{def} f (v_1, v_2, \cdots , v_n) = x \operatorname{in} y) = \mathrm{val}( e', y)$
とします。

ここで $e' = (f \mapsto λ( (v_1, v_2, \cdots , v_n) . x, e)) : e$ です(再帰的定義はしません)。 $E$ の「次の時代」 $E'$ を $E' = E \cup \{e'\}$ とします。

fun ( $v_1, v_2, \cdots , v_n$ ) = $x$ の値

無名関数を表します。 $v_1, v_2, \cdots , v_n$ は変数、 $x$ は式です。
$\mathrm{val}(e, \operatorname{fun} (v_1, v_2, \cdots , v_n) = x) = \mathrm{val}(e, λ( (v_1, v_2, \cdots , v_n) . x, e))$
です。

if $x$ then $y$ else $z$ の値

$x$ 、 $y$ 、 $z$ は式です。 $\mathrm{val}(e, \operatorname{if} x \operatorname{then} y \operatorname{else} z)$ は $\mathrm{val}(e, x)$ が $T$ (「真」を表す定数)のとき $\mathrm{val}(e, y)$ 、 $\mathrm{val}(e, x)$ が $T$ ではないとき $\mathrm{val}(e, z)$ となります。

if $f (v_1, v_2, \cdots , v_n) = x$ then $y$ else $z$ の値

上記の if を拡張したものも考えます。 $f$ は演算子、 $n$ は $f$ の項数、 $v_1, v_2, \cdots , v_n$ は変数、 $x$ 、 $y$ 、 $z$ は式です。

$\mathrm{val}(e, \operatorname{if} f (v_1, v_2, \cdots , v_n) = x \operatorname{then} y \operatorname{else} z)$ は $\mathrm{val}(e, x)$ が $f(x_1, x_2, \cdots , x_n)$ に一致するときは、
$\mathrm{val}(e, \operatorname{if} f (v_1, v_2, \cdots , v_n) = x \operatorname{then} y \operatorname{else} z) \\ = \mathrm{val}( e, \operatorname{let} v_1 = \mathrm{val}(e, x_1) \operatorname{in} \operatorname{let} v_2 = \mathrm{val}(e, x_2) \operatorname{in} \cdots \operatorname{let} v_n = \mathrm{val}(e, x_n) \operatorname{in} y)$
となります。

$\mathrm{val}(e, x)$ が $f(x_1, x_2, \cdots , x_n)$ に一致しないときは、
$\mathrm{val}(e, \operatorname{if} f (v_1, v_2, \cdots , v_n) = x \operatorname{then} y \operatorname{else} z) = \mathrm{val}(e, z)$
となります。