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

クロージャーの定義

wikipedia:クロージャなどを見ると(できることは同じようですが)クロージャーの定義にはいろいろあるようです。ここでも定義しておいた方が良いと思われるので、ここで使うものを定義しておきます。

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

定数
変数
算術演算子、比較演算子を使った $x \triangle y$ 、 $\triangle x$ という式
通常の関数適用
クロージャー
クロージャー適用
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$

変数と式を対応させたものを環境と呼ぶことにします。環境はポインターを使わないとうまく定義できないので、ポインターを使って定義します。ポインターを使わない方法は後で検討します。ポインターを Haskell のリストのような形で表します。

集合 $P$ によってインデックスが付けられた集合 $A = \{a_p\}_{p \in P}$ で $A$ の元は変数 $v$ 、式 $x$ 、ポインター( $P$ の元または $\bot$ をポインターと呼ぶことにします) $p'$ の組 $a_p = \langle v, x, p' \rangle$ であるものを考えます。 $a_p$ をポインター $p$ が参照する内容と呼ぶことにします。 $v$ と $x$ の組を $(v \mapsto x)$ と書いて、 $a_p = \langle (v \mapsto x), p' \rangle$ と書くことにします。これをリストのような形で書きます。 $p' = \bot$ のとき $a_p = (v \mapsto x) : \bot$ 、 $p' \ne \bot$ のとき $a_p = (v \mapsto x) : a_{p'}$ と書くことにします。

環境を(ポインターとして)

$\bot$ または
$(v \mapsto x) : e$ ( $v$ は変数、 $x$ は式、 $e$ は環境)

と帰納的に定義します。

ある環境 $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$ をポインター $p$ と見たときに、上に書いたポインターの集合 $P$ でインデックスが付けられた $A$ の元 $a_p$ を同じ $p$ に対応する別の $a'_p$ で置き換えた $A' = A - \{a_p\} + \{a'_p\}$ を、これ以降(後述のブロックでこれより後の部分)は $A$ の代わりに使うということを表します。

ある環境 $e$ での式 $x$ の値(数値または真理値) $\mathrm{val}(e, x)$ を考えます。

定数 $a$ の値

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

変数 $v$ の値

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

算術演算子、比較演算子を使った $x \triangle y$ 、 $\triangle x$ という式の値

$x \triangle y$ の値は $\mathrm{val}(e, x \triangle y) = \mathrm{val}(e, x) \nabla \mathrm{val}(e, y)$ となります。 $\nabla$ は $\triangle$ に対応する数値の演算で $\mathrm{val}(e, \triangle x)$ または $\mathrm{val}(e, \triangle y)$ が $\bot$ のときは値は $\bot$ とします。 $\triangle x$ の値は $\mathrm{val}(e, \triangle x) = \nabla \mathrm{val}(e, x)$ となります。 $\nabla$ は $\triangle$ に対応する数値の演算で $\mathrm{val}(e, \triangle x)$ が $\bot$ のときは値は $\bot$ とします。

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

$v$ は変数、 $x$ と $y$ は式です。
$\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$ は式です。
$\mathrm{val}(e, \operatorname{subst} v = x \operatorname{in} y) = \mathrm{val}(e(v \gets x), y)$
です。 $y$ は置き換えられた環境で評価されます。

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 c( (v_1, v_2, \cdots , v_n) . x, e')) : e$ です。再帰的定義のために $f$ の定義が追加されています。 $c( (v_1, v_2, \cdots , v_n) . x, e')$ はクロージャーです。
$\mathrm{val}(e'', c( (v_1, v_2, \cdots , v_n) . x, e')(x_1, x_2, \cdots , x_n)) \\ = \mathrm{val}( (v_1 \mapsto x_1) : (v_2 \mapsto x_2) : \cdots : (v_n \mapsto x_n) : e', x)$
となります。このときクロージャーが持っている環境 $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, c( (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)$ が真のとき $\mathrm{val}(e, y)$ 、 $\mathrm{val}(e, x)$ が偽のとき $\mathrm{val}(e, z)$ となります。

ブロックの記法

let $v$ = $x$ in $y$
subst $v$ = $x$ in $y$
def $f$ ( $v_1, v_2, \cdots , v_n$ ) = $x$ in $y$

が連続するとき

let v = x;
subst v' = x'
def f ( w1, w2, w_3 ) = x''
y

のようにブロックとして表すことができます。このブログの例のコードでは、C# のコードとして書きやすいためブロックで表しています。

変数の変更が不可能なクロージャーとポインターの調査

サーバーのプログラムを変数の変更が可能なクロージャーを使って書くと、サーバーのプログラムを更新することはブラウザーのプログラムを更新することと同様にできるという例を見てきました。これによってブラウザーのプログラムが複数あるときにも「同じことを二度書かない」ことを実現することができます。

これを変数の変更が不可能なクロージャーで書くとどうなるかということを考えていきます。これは、サーバーのプログラムを変更するとそれを使っているプログラムが使えなくなるので、それを避けることができるのかどうか調べるためです。

サーバーのプログラムが無限に続くものだ考えると、それを変数の変更が不可能なクロージャーで書くことはできないということになりますが、考え方を変えることによってできるのかどうかを調べてみます。サーバーのプログラムが有限の回数で終わるとすれば、変数の変更が不可能なクロージャーで書くことはできます。そのプログラムの無限に続く「バージョンアップ」のような考え方でできるかどうか調べてみます。

そのためにポインターを使っていたところをポインターを使わない形に書き直すことはできるかどうかを考えていきます。