1.7.1 プログラムは公理の集まり

KL1 プログラムを構成する節は 述語名(引数, ...) :- ガード | ボディ.

という形式をしている. ここで縦棒 (``| '') を取り除いて, ガードと ボディの区別をなくしてしまうと, 節の形は 述語名(引数, ...) :- ゴール, ... .

という形式である.

前に述べたように, ガードにあるユニフィケーションを, ヘッド中に直接相手 を書くように略記してしまうことができた. ガードとボディの区別をなくし てしまったので, もとはボディにあったユニフィケーションにも, この規則を 適用することにする. たとえばストリームを結合するプログラム

append([], In2, Out) :- Out = In2.
append([Msg|In1], In2, Out) :-
    Out = [Msg|OutTail],
    append(In1, In2, OutTail).

a([], O, O).
a([M|I1], I2, [M|O]) :- a(I1, I2, O).

このような変換をした結果は, 一階述語論理の公理して解釈することができる. その意味づけは, `` :-'' の右辺が成り立つならば, 左辺が成り立つ (右辺が空なら, 左辺は無条件に成り立つ) ということで, 上の append の例 のふたつの節を論理式として書けば, それぞれ

ということになる. 日本語で書き下せば, (1.1) は「どんな についても, が成り立つ」, もうちょっと解釈を入れると 「空リストと何かを結合したものは, その何かである」という意味である. (1.2) は「どんな についても, が成り立てば が成り立つ」, 解釈を入れ て「 と を結合したものが になっているのなら, と を結合したものは になっている」という ことになる.