関数プログラミング(1) - エレファント・コンピューティング調査報告

関数プログラミングと論理プログラミングを対応させることによって、入出力が無限に実行されるプログラムをどのように書けば良いのかを考えていきます。関数プログラミングで無限に続く入出力を書く方法を考える必要はあるのですが、それを記述する言葉がない(わからない)ので、いったん論理プログラミングに変換して無限に続く入出力を書くにはどうするかを考えることが目的です。

簡単な関数プログラミングのシステムから考えていきます。関数プログラミングのプログラミングは式であって、ある式 $e$ に現れる変数 $x$ を他の式で置き換えるという関数を表す

$\displaystyle \lambda x . e$

と、ある関数 $f$ に式 $e$ を引数として渡した結果を表す

$\displaystyle f e$

と、ある式 $a$ に現れる変数 $x$ を他の式 $e$ で置き換えた式を表す

$\displaystyle \mathop{let} x = e \mathop{in} a$

と、ある式 $a$ に現れる変数 $f$ を他の式 $e$ で置き換えた式を表す

$\displaystyle \mathop{let} \mathop{rec} f = e \mathop{in} a$

( $f$ は関数を表し $e$ にあらわれても良いとします)からなるものとします。これだけではたいしたことはできないとは思いますが、無限に続く入出力を記述する方法を考えることが目的ですので、とりあえずこれだけでやってみることにします。細かいところは後で説明する予定です。

これらをそれぞれ

$\displaystyle \lambda(x, e)$

$\displaystyle \alpha(f, e)$

$\displaystyle \pi(x, e, a)$

$\displaystyle \rho(f, e, a)$

と書くことにします。 $\alpha(\lambda(x, a), e) = \pi(x, e, a)$ が成り立つので $\pi$ は $\lambda$ と $\alpha$ で表すことができます。

これらを PLP の項として表すことにして、関数プログラミングの式を PLP の項として表した $t$ を評価する PLP のプログラムを考えます。PLP の微分 $d$ と PLP の述語式 $d$ と PLP の代入 $\sigma$ が $\sigma(d^n(r))$ が真となるものとします。 $r$ が $p(t, v)$ という形の述語式( $v$ は変数)のとき、 $\sigma(v)$ が $t$ を評価したものになるような $d$ を求める問題を考えます。