λProlog の copy-clauses 技法

2023/03/09

はじめに

λProlog ([1]) 固有のプログラムテクニックに copy-clauses があります([2])。HOAS (Higher-order abstract syntax) のような、データ構造としての高階な項を扱うために重要な手法です（注）。しかし、いかにも初見殺しなところがあるので、実例を動かしながら調べてみましょう。

（注）例えば、自然数からなる任意のリストが与えられた時、値が「2」である要素をλ抽象するプログラム（[1,2,3,2,3] が入力されたら、λx.[1,x,3,x,3] を出力するプログラム）を作ることを考えてください。大抵のプログラミング言語では、xが具体化された後に、その値で2を置き換える関数は定義できますが、ラムダ項そのものを出力ことはできないはずです。

λPrologの処理系としてはELPIを使いますが、Coq-ELPIの機能は使いません。Coq-ELPIの場合については最後に触れます。
このコードは以下にあります。
https://github.com/suharahiromichi/prolog/blob/master/elpi/copy_clauses.elpi

HOASの例

具体的な問題として、CoqのGallina項の内部構造([4])を単純化したような、HOASを定義します。
最初に断っておきますが、今回はこのGallina項の簡約系を作るわけではありません。このあと、適用(apply)や、抽象(abstruct)という言葉を使いますが、これらは、λPrologのデータ構造に対する操作であり、Gallina項に対するものではありません。
型tmが項を表します。

a、b、c、dを定項とします。
関数適用は、appコンストラクタで表現します。appの後ろにtm型のリストをとります。
関数(いわゆるλ式)は、funコンストラクタで表現します。funの後ろにλPrologのλ項（例：x\F）を書きます。
Coqでの表記 fun x => a b x は、fun x\ app [a, b, x] となります。（引数の数やカリー化は、ここでは気にしないことにします。）


kind tm type.

type a, b, c, d tm.
type app list tm -> tm.
type fun (tm -> tm) -> tm.

copy 述語

tm上のcopy述語を次のように定義します。
app Lのcopyはmap述語を使います。ただし、ELPIのmap述語は双方向性がないので、定義しなおしています。
判じ物なのは、fun Mのcopyです。
fun MのMはλPrologの関数なので、M単体で述語に渡すことはできません。なので、x というローカルな変数を用意してMに適用したかたちで、M xをM1 xにcopyします。
ただし、xをxにcopyするために、これもローカルな述語定義（ルール）copy x xを用意します。これは、copy述語の一連の定義の先頭に追加されます。ISO Prolog のassertaに似ていますが、
pi x\ copy x x => copy (M x) (M1 x) の終了時に無効になります。
また、pi x\ copy x x => copy (M x) (M1 x) は、
pi (x\ (copy x x => copy (M x) (M1 x))) の意味です。
pi x\ (copy (M x) (M1 x) :- copy x x) と書いても同じですが、習慣として=>を使うようです。括弧も少なくて済みます。
copy述語は、双方向に使いたいので、引数はすべてo:としておきます。


pred map o:list A, i:(A -> B -> prop), o:list B.
map [] _ [].
map [X|XS] F [Y|YS] :- F X Y, map XS F YS.

pred copy o:tm, o:tm.
%copy M M1 :- print "M=" M ", M1=" M1, fail.
copy a a.
copy b b.
copy c c.
copy d d.
copy (app L) (app L1) :- map L copy L1.
copy (fun M) (fun M1) :- pi x\ copy x x => copy (M x) (M1 x).

Copy の例

このcopyの例を見てみます。test1 は、SをTにcopyする、ただし、bはdにcopyするルールを優先する、と読みます。これは、copy S Tの実行先立って、テンポラリにdをbにコピーする
copy b dのルールが追加されることにより実現されます。


pred sample_term_0 o:tm.
sample_term_0 (app [a, b, c, b, c]).

pred test0.
test0 :-
      sample_term_0 S,
      copy b d => copy S T,
      print T.

subst 述語

copyを使って、λPrologの関数Mに、項Tを適用してSを得る述語を定義します。substというよりapplyですが、文献([2])に準じてsubstとします。
すなわち、x というローカルな変数を用意してMに適用したかたち M xで、それをSにcopyします。ただし、copyに先立って、xをTにcopyするルールを追加します。
subst述語は、双方向に使いたいので、引数はすべてo:としておきます。


pred subst o:(tm -> tm), o:tm, o:tm.
subst M T S :- pi x\ copy x T => copy (M x) S.

適用という意味では、S = M T と同じですが、これがλ変数のユニフィケーションだけで済ませる「浅い」適用であるのに対して、これから定義するのは、項のcopyを伴う「深い」適用といえるものです。深い適用のことは、"object-level substitution" というようです([7])。
適用だけではつまらないお思う方は、次の実行例を見てください。これを逆向きに使ってλ抽象が実現できます。これを "object-level generalization" と言います。
また、全解を求めることは、部分項とそれが出現する文脈を求めることもできます。

実行例

subst述語は、項Tへの関数Mの適用の結果がSとして定義されていますが、これを逆方向に使って、SをTで抽象して関数Mを得ることもできます。
また、Sに対してとり得るTとMの組み合わせの全解を求めることで、部分項とそれが出現する文脈を列挙することができるわけです。

単純な例

substitution の例 (object-level substitution)
逆向きに使った、抽象化の例 (object-level generalization)
全解を出力すると、抽象する・しないの複数の組み合わせが得られます。
それでも、抽象するほうが先に出力されるのは、substの定義のcopy x Tが、
copyの定義の前(assertaのように)追加されているためです。
部分項と文脈を求める例


pred sample_term_1 o:(tm -> tm).
sample_term_1 (x\ app [a, x, c, x, c]).

pred sample_term_2 o:tm.
sample_term_2 (app [a, b, c, b, c]).

pred test1.
test1 :-
      sample_term_1 M,
      subst M d S,
      print S.

pred test2.
test2 :-
       sample_term_2 S,
       subst M b S,
       print M.

pred test21.
test21 :-
       sample_term_2 S,
       subst M T S,
       print "M=" M ", T=" T ", S=" S,
       M T = S.     % サブタームになっていることの確認

pred  test22.
test22 :-
       sample_term_2 S,
       std.findall (subst _ _ S) L,
       print L.

少し複雑な例

substの対象にfunが入っている例です。
ネストの深いところにある定数からなる項も取り出せるが、λ変数を含む項は、λ式全体でないと取り出せない。


pred sample_term_3 o:tm.
sample_term_3 (fun x\ app [a, x, (fun y\ app [b, y, c])]).

pred test31.
test31 :-
       sample_term_3 S,
       subst M T S,
       print "M=" M ", T=" T,
       M T = S.     % サブタームになっていることの確認

pred test32.
test32 :-
       sample_term_3 S,
       std.findall (subst _ _ S) L,
       print L.

Coq-ELPI のcopy述語

Coq-ELPIでは [3] に、CoqのHOASのためのcopy述語が定義されています。また、[5]と[6]で、使用例が説明されています。
ただし、[3]で定義されたcopy述語は、第一引数がin、第二引数がoutと固定されていて、cutオペレータが散りばめられているので、前節までのように、双方向に使うことはできません。必要に応じて定義することになります。また、copy-ctx-item、copy-arity、copy-indt-decl、
copy-fields、copy-constructorという述語は、その中からcopyを呼び出します。例えば、チュートリアル[5]では、

pi a\ copy P a => copy-indt-decl Decl (Decl' a))

のように、Coqのコンストラクタ（parameter、inductive、record）の定義の一部を抽象する例が掲載されています。
この例は、DeclをDecl' aにコピーする、ただし、Pはaにコピーする、と読めます。

文献

[1] λProlog (Lambda Prolog) の紹介

[2] PROGRAMMING WITH HIGHER-ORDER LOGIC

[3] coq-elpi/elpi/coq-lib.elpi

[4] Tutorial on the HOAS for Coq terms

[5] Tutorial Coq-ELPI Comamand

[6] Tutorial Coq-ELPI Tacitcs

[7] CHuck C. Liang, "Object-level Substitution, Unification and Generalization in Meta-logic"