フラクタル代数言語 Fractal (2) - エレファント・ビジュアライザー調査記録

フラクタル代数言語 Fractal の構文

フラクタル代数言語 Fractal の構文は Prolog と同様(サブセット)とします。以下 Wikipedia の Prolog の項から必要な部分を引用します。

項

Prolog のデータを項と呼びます。項は定数、変数、複合項のいずれかとなります。

定数
- アトム：小文字で始まる文字列。
- 数値：数字で始まる文字列。
変数
- 通常の変数：大文字か下線「_」で始まる文字列で無名変数でないもの。
- 無名変数：下線「_」のみからなるもの。
複合項
- 通常の複合項：アトムの後に1個以上の項をカンマ「,」で区切ってかっこ「(」と「)」囲んでだものを付け加えたもの。
- リスト：1個以上の項をカンマ「,」で区切って角かっこ「[」と「]」囲んでだもの、または「[]」だけのもの(これは要素のないリストを表す)。

プログラム

プログラムはホーン節を並べたものとなります。
ホーン節は以下のどれかとなります。

頭部.
頭部 :- 本体部.

本体部は

副目標1,副目標2, ... 副目標n

という形となります(目標と呼びます)。
頭部と各副目標は通常の複合項となります(述語項と呼びます)。

Prolog プログラムの実行

「?- 本体部.」の形(質問)が入力されることによって Prolog のプログラムが実行されます。

Prolog のプログラムは論理式を表しています。ホーン節
$\hspace{5em} h \operatorname{:-} q_1, q_2, \cdots , q_n .$
は
$\hspace{5em} q_1 \land q_2 \land \cdots \land q_n \implies h$
という論理式を表しています。

本体部がない
$\hspace{5em} h .$
という形は $n=0$ の場合で
$\hspace{5em} h$
という論理式を表しています。

$\hspace{5em} \operatorname{?-} q_1, q_2, \cdots , q_n .$
は、ホーン節の頭部がない場合で、頭部が「偽」の場合を表し
$\hspace{5em} \lnot ( q_1 \land q_2 \land \cdots \land q_n )$
または
$\hspace{5em} q_1 \land q_2 \land \cdots \land q_n \implies \bot$
という論理式を表します( $\bot$ は「偽」を表します)。

Prolog のプログラムの実行を説明するために、論理式のプログラムによる1回の変換を考えます。

述語項 $p$ のプログラム
$\hspace{5em} \begin{eqnarray*} h_1 & \operatorname{:-} & q_{11}, q_{12}, \cdots , q_{1m_1}. \\ h_2 & \operatorname{:-} & q_{21}, q_{22}, \cdots , q_{2m_2}. \\ & \vdots \\ h_n & \operatorname{:-} & q_{2n}, q_{n2}, \cdots , q_{nm_n}. \\ \end{eqnarray*}$
による1回の変換 $\lambda$ は $p$ を
$\hspace{5em} \begin{array}{c} ( (p = h_1) \land q_{11} \land q_{12} \land \cdots \land q_{1m_1}) \\ \lor \\ ( (p = h_2) \land q_{21} \land q_{22} \land \cdots \land q_{2m_2}) \\ \lor \\ \vdots \\ \lor \\ ( (p = h_n) \land q_{2n} \land q_{n2} \land \cdots \land q_{nm_n}) \\ \end{array}$
に変換するものとします。 $p = h_i$ は $p$ と $h_i$ が一致することを表すもので、述語項とプログラムの変数は重複しないようにあらかじめ変数を置き換えておくものとします。 $p$ を $\lambda$ で変換したものを $\lambda(p)$ と書きます。

述語項から $\land$ と $\lor$ を繰り返してできる論理式 $e$ は
$\hspace{5em} \begin{array}{c} (p_{11} \land p_{12} \land \cdots \land p_{1m_1}) \\ \lor \\ (p_{21} \land p_{22} \land \cdots \land p_{2m_2}) \\ \lor \\ \vdots \\ \lor \\ (p_{2n} \land p_{n2} \land \cdots \land p_{nm_n}) \\ \end{array}$
という形に書くことができます。この形を選言標準形と呼びます。

$e$ を $\lambda$ で変換した $\lambda(e)$ を
$\hspace{5em} \begin{array}{c} (\lambda(p_{11}) \land \lambda(p_{12}) \land \cdots \land \lambda(p_{1m_1})) \\ \lor \\ (\lambda(p_{21}) \land \lambda(p_{22}) \land \cdots \land \lambda(p_{2m_2})) \\ \lor \\ \vdots \\ \lor \\ (\lambda(p_{2n}) \land \lambda(p_{n2}) \land \cdots \land \lambda(p_{nm_n})) \\ \end{array}$
とします。すべての述語項とプログラムの変数は重複しないようにあらかじめ変数を置き換えておくものとします。 $\lambda(e)$ も選言標準形に変形することができるので、 $\lambda$ による変換を繰り返すことができます。 $e$ を $\lambda$ で $n$ 回変換したものを $\lambda^n(e)$ と書きます。

$\lambda$ の本体部をすべて「真」に変えたものを $\lambda_T$ とします。 $\lambda$ の本体部をすべて「偽」に変えたものを $\lambda_F$ とします。これを使ってプログラムの実行を有限回で止めたものを考えます。
$\hspace{5em} \operatorname{?-} q_1, q_2, \cdots , q_n .$
が入力されたとき、 $e = q_1 \land q_2 \land \cdots \land q_n$ に対して $\lambda_T(\lambda^n(e))$ と $\lambda_F(\lambda^n(e))$ を考えます。

項全体の集合を $T$ とします。変数を含まない項全体の集合を $T_C$ とします。 $t \in T$ の定数化 $\sigma : T \to T_C$ を $t$ に含まれる各変数 $v \in T$ を変数を含まない項 $\sigma(v) \in T_C$ に変換する写像とします。

ある $n \in \mathbb{N}$ に対して、ある定数化 $\sigma : T \to T_C$ に対して $\sigma(\lambda_F(\lambda^n(e)))$ が真であるとき、 $e$ の $\lambda$ による $n$ 回の変換は成功ということにします。このような $n \in \mathbb{N}$ が存在するとき、 $e$ の $\lambda$ による(無限回の)変換は成功ということにします。

ある $n \in \mathbb{N}$ に対して、任意の定数化 $\sigma : T \to T_C$ に対して $\sigma(\lambda_T(\lambda^n(e)))$ が偽であるとき、 $e$ の $\lambda$ による $n$ 回の変換は失敗ということにします。このような $n \in \mathbb{N}$ が存在するとき、 $e$ の $\lambda$ による(無限回の)変換は失敗ということにします。