エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

ラムダ計算と無限ラムダ多項式(13)

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

有限ラムダ多項式

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

演算子  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) となります。