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

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

フラクタル代数言語 Fractal (2)

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

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

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 による(無限回の)変換は失敗ということにします。

このようにして  n 回で変換を止めたものの列によって無限の回数実行されるプログラムを表すプログラミング言語を作るということが目的ですが、変換を途中で止める方法がこれでは不十分ではないかと思われますので、今後検討していくことにします。

Prolog のプログラムの実行順序は、基本的にはこの考え方で説明できると考えられます。 x \land y x の後に  y x \lor y x の後に  y、のように非可換と考えて順に調べていけば良いということになるのですが、これも今後検討していきます。