Elpi の組込述語 (stdlib編)

@suharahiromichi

2022/12/04

λProlog (lProlog、LambdaProlog) は、その名前の通り、Prolog本来の導出原理に加えて、ラムダ計算も計算原理に持つという、おもしろい言語です。
Embeddable Lambda Prolog Interpreter (ELPI) は、定理証明支援系 Coq の機能拡張のためのλPrologの処理系で、Coqと一緒に配布されていますが、単独でUNIX系OSのコマンドラインからインタプリタを起動して使うことも使用可能です。
しかし、ドキュメントが少なく、とくに組込述語（一般的なプログラミング言語の組込関数）は通常のProlog (以下、ISO Prologと呼びます)と異なる部分が多いため、一覧を作成してみました。
ここでは、ELPIのソースコード [1]

src/builtin_stdlib.elpi

の namespace std で定義された組込述語をできるだけ例を交えて説明します。
λPrologやELPIについての説明は [2] と、そこに書いた参考文献を参考にしてください。
この組込述語は、ドキュメントではstdlibと呼ばれますが、呼び出し時には、std.を付けます。stdlib ではないので、注意してください。なお、これ以外に特別な宣言は要りません。

この記事の元になるソースコードは以下にあります。

このファイルの例の使い方は、コマンドラインから、elpiコマンドの引数として呼び出してください。対話モードで goal> プロンプトの後にtest10.やtest11.などと入力してください。Enterの前に.が要ります。複数解がある場合は、More? (Y/n)と表示されるので、Enterを押すとバックトラックが行われ別解が出力されます。
一般的なPrologと異なり、一回毎にコマンドプロンプトに戻りますので、elpiコマンドから再度実行してください。

% elpi elpi_stdlib_note.elpi
goal> test10.<Enter>

% elpi elpi_stdlib_note.elpi
goal> test11.<Enter>

stdlib の使い方

述語名の前にstd.を付けて使います。λProlog の標準的な型として、命題を表すpropの他、以下の型が使われいます。

• int
• float
• string
• bool
• list X
• pair X Y
• option A
• diagnostic
  前4つは一般的な定義で、float は1.0と小数点をつけて、stringはダブルクォーテーションで囲んで表現します。boolは、真はtt、偽はffです。trueとfalseは、ISO Prologと同様に述語(よって、λPrologではpred型)なので注意してください。

list X

list は、次のように定義されています。ここでXは任意の型を示す型変数です。
::はcons、[]はnilを表します。ISO Prologの[ A | B ]という表記も使えます。

kind list type -> type.
type (::) X -> list X -> list X.
type ([]) list X.

pair A B

pair は直積型で、次のように定義されています。コンストラクタは pr で、1と"one"のpairはpr 1 "one"となります。カンマの記法は用意されていません。

kind pair type -> type -> type.
type pr A -> B -> pair A B.

option A

option A は、noneまたはsome Xを返すデータ型で、Xの型はAです。maybe型とも呼ばれます。次のように定義されています。

kind option type -> type.
type none option A.
type some A -> option A.

diagnostic

diagnostic は、okまたはerror 文字列を返すデータ型で、次のように定義されています。

kind diagnostic type.
type ok diagnostic.
type error string -> diagnostic.

規約

最初に builtin_stdlib.elpi の冒頭のコメントを訳しておきます。

• すべての述語は、いくつかの入力引数を使用してモードを宣言します...

• 名前が R で終わる述語はリレーションです（あらゆる方向に機能します。
  つまり、すべての引数が出力モードになります）。

• 名前が!で終わる述語 カットを含み、最初の結果のみを生成します。

• このライブラリによって与えられたすべてのエラーは、fatal-error[-w-data]
  を呼び出すことになり、別の方法で処理するためにはオーバーライドします。

• このライブラリによるすべてのデバッグ出力は最終的に debug-print を呼
  び出し、異なる方法で処理するためにはオーバーライドします。

stdlib の説明

pred fatal-error i:string.

pred fatal-error-w-data i:string, i:A.

pred debug-print i:string, i:A.

pred ignore-failure! i:prop.

ignore-failure! p の命題pが失敗しても成功しても、全体がは成功する。

pred test4.
pred test4_1.
test4 :-
      std.ignore-failure! true,
      print 1.
test4_1 :-
      std.ignore-failure! fail,
      print 2.

pred assert! i:prop, i:string.

assert! C Mで、Cが失敗したら、メッセージMを出力する。

pred test5.
test5 :-
      std.assert! fail "Fail!".

pred assert-ok! i:(diagnostic -> prop), i:string.

assert!と似ているが、対象の命題が診断結果として、
okまたはerror Sを返す述語を使用します。対象の命題が失敗した場合もerrorと見なされるが、no diagnostic returnedになる。

pred sample6 o:diagnostic.
sample6 (error "an error").
pred test6.
test6 :-
      std.assert-ok! sample6 "diag-result".

pred spy i:prop.

spy p で、述語pの呼出(enter)と結果(exit)を表示すると同時に、
More? (Y/n)で、nを選ぶとpを失敗させることができます。また、pに代替節がある場合は、Yで選択できます。

pred test7.
pred sample7 o:int.
sample7 1.
sample7 2.
test7 :-
      std.spy (sample7 X),
      print X.

pred spy! i:prop.

spyと同じですが、
More? (Y/n)で、Yを選んでもpの代替節は選ばれず、単に成功するだけです。

pred test8.
test8 :-
      std.spy! (sample7 X),
      print X.

pred unsafe-cast o:A, o:B.

ELPIの型チェックを回避する。次の例は、float (1.0) を int であるべき箇所 sample8 に代入している。

pred test8.
pred sample8 i:int.
sample8 X :-
        print X.
test8 :-
      std.unsafe-cast 1.0 X,
      sample8 X.

pred length i:list A, o:int.

最後の引数が出力となる。最初の引数が変数（未束縛）ならエラーになる。

pred test9.
test9 :-
      std.length [1, 2, 3] N,
      std.debug-print "length is" N.

pred rev i:list A, o:list A.

リストを反転します。最後の引数が出力となる。じつは、std.revの定義は良いものではなく、std.rev X [3,2,1]は無限ループになります。しかし、引数のi/oを守る限り問題はありません。

pred test10.
test10 :-
       std.rev [1, 2, 3] X,
       std.debug-print "rev is" X.

次のように、ホーン節の順番を入れ換えると大丈夫ですが、バックトラックで戻ってくると、また無限ループになります。

pred rev i:list A, o:list A.
rev L RL  :- rev.aux L []  RL.
rev.aux [] L L.
rev.aux [X|XS] ACC R :- std.spy (rev.aux XS [X|ACC] R).

pred test10_1.
test10_1 :-
       rev X [9, 8, 7],
       std.debug-print "new rev is" X.

pred last i:list A, o:A.

最後の要素が出力となる。空リストならfatal-errorになります。

pred test11.
test11 :-
       std.last [1, 2, 3] X,
       std.debug-print "last is" X.

pred append i:list A, i:list A, o:list A.

最後の引数が出力となる。

pred test12.
test12 :-
       std.append [1, 2, 3] [4, 5, 6] X,
       std.debug-print "append is" X.

pred appendR o:list A, o:list A, o:list A.

規約の2番目の例。非決定的な append である。第1と第2引数が「o」であることが異なる。以降では、述語が成功する条件のみならず、バックトラックしても成功するか、さらに、何回成功するか、も考えてみてください。

pred test13.
test13 :-
       std.appendR X Y [1, 2, 3, 4, 5, 6],
       print "append is" X "and" Y.

pred take i:int, i:list A, o:list A.

最後の引数が出力となる。先頭からN個とりだす。lengthより大きければ、fatal errorとなる。

pred test14.
test14 :-
       std.take 2 [1, 2, 3] X,
       print "take 2 is" X.

pred take-last i:int, i:list A, o:list A.

最後の引数が出力となる。末尾からN個とりだす。lengthより大きければ、fatal errorとなる。

pred test15.
test15 :-
       std.take-last 2 [1, 2, 3] X,
       print "take-last 2 is" X.

pred drop i:int, i:list A, o:list A.

最後の引数が出力となる。先頭からN個捨てる。lengthより大きければ、fatal errorとなる。

pred test16.
test16 :-
       std.drop 2 [1, 2, 3] X,
       print "drop 2 is" X.

pred drop-last i:int, i:list A, o:list A.

最後の引数が出力となる。末尾からN個捨てる。lengthより大きければ、fatal errorとなる。

pred test17.
test17 :-
       std.drop-last 2 [1, 2, 3] X,
       print "drop-last 2 is" X.

pred split-at i:int, i:list A, o:list A, o:list A.

最後の引数が出力となる。最初の要素の前を0として、N番目のところで分割する。

pred test18.
test18 :-
       std.split-at 2 [1, 2, 3, 4] X Y,
       print "split at" X Y.

pred fold i:list B, i:A, i:(B -> A -> A -> prop), o:A.

fold リスト 初期値 f 答えのとき、ISO Proloのfoldlと同じです。f に与えられる引数の順番はISO Prologとは同じですが、Coqなどの関数型言語のfold_left関数と異なることに注意してください。Coqでは以下が等価です。

foldl (fun x y => subn y x) 0 [:: 1; 2; 3]
または

foldl (fun x => subn ^~ x) 0 [:: 1; 2; 3]

pred test19.
test19 :-
       std.fold [1, 2, 3] 0 (x\ y\ z\ z is x - y) X,
%      (3 - (2 - (1 - 0))) = 2
       print "fold sub is" X.

その例を含めていませんが、f x y zが複数解あるときは、バックトラックで使われます。

pred fold2 i:list C, i:list B, i:A, i:(C -> B -> A -> A -> prop), o:A.

二つのリストに対してfoldをおこない、一つの値を求めます。二つのリストの長さが異なる場合は、fatal-error になります。

pred test20.
test20 :-
       std.fold2 [1, 2, 3] [4, 5, 6] 0 (x\y\z\u\ u is x + y + z) X,
       print "fold2 is" X.

pred map i:list A, i:(A -> B -> prop), o:list B.

map f リストに対して、f x yがfailすると全体がFailする。また、f x yが複数解あるときは、バックトラックで使われる。

pred test21.
pred sampl21 i:int o:int.
sampl21 X Y :-
      Y is ~ X.
sampl21 X Y :-
      Y is X + 1.
test21 :-
       std.map [1, 2, 3] sampl21 X,
       print "map sampl21 is" X.

pred map-i i:list A, i:(int -> A -> B -> prop), o:list B.

0から始まるindex付きのmap。案外便利かも。

pred test22.
test22 :-
       std.map-i ["a","b","c"] (i\ a\ b\ b = pr i a) X,
       print "map-i is" X.

pred map-filter i:list A, i:(A -> B -> prop), o:list B.

map-filter f リスト 結果 で、mapと同じだが f が失敗した場合は、結果から抜かれる。

pred test23.
pred even2 i:int o:int.
even2 N M :-
     M is (N div 2) * 2,
     N = M.
test23 :-
       std.map-filter [1, 2, 3, 4] even2 X,
       print "map even is" X.

pred map2 i:list A, i:list B, i:(A -> B -> C -> prop), o:list C.

2項演算を使ったふたつのリストからなるmapです。ふたつのリストの長さが異なるとfatal-errorとなります。

pred test24.
test24 :-
       std.map2 [1, 2, 3] [4, 5, 6] (x\ y\ z\ z is x + y) X,
       print X.

pred map2-filter i:list A, i:list B, i:(A -> B -> C -> prop), o:list C.

map2-filter f リスト1 リスト2 結果 で、map2と同じだが fが失敗した場合は、結果から抜かれる。

pred test25.
test25 :-
       std.map2-filter [9, 6, 2] [3, 2, 0]
                       (x\ y\ z\ not(y = 0), !, z is x div y) X,
       print X.

pred map-ok i:list A, i:(A -> B -> diagnostic -> prop), o:list A, o:diagnostic.

mapと同じですが、diagnostic でerror 文字列が返った場合は、そこで打ち切り、エラーにしてdiagnosticを返します。

pred test26.
pred diagtwo i:int o:int o:diagnostic.
diagtwo 1 2 ok.
diagtwo 3 4 ok.
diagtwo 0 0 (error "xxxx").
test26 :-
       std.map-ok [1, 0, 3] diagtwo X D,
       print X D.

pred fold-map i:list A, i:B, i:(A -> B -> C -> B -> prop), o:list C, o:B.

fold-map リスト 初期値 f Map結果 Fold結果 のとき、fは、
f x y z uで、xとyが入力、zがMapのための計算、uがFoldのための計算です。coq-libの同名の述語とは定義が違うようです。

pred test27.
test27 :-
       std.fold-map [1, 2, 3] 0 (x\y\z\u\ z is ~ x, u is x - y) Map Fold,
       print "fold-map is" Map Fold.
%      Fold = (3 - (2 - (1 - 0))) = 2

Mapのための計算は2引数でもよいため、foldの途中結果をMapに返すこともできます。

pred test27_1.
test27_1 :-
       std.fold-map [1, 2, 3] 0 (x\y\z\u\ z is x - y, u is x - y) Map Fold,
       print "fold-map is" Map Fold.

pred omap i:option A, i:(A -> B -> prop), o:option B.

option A 型の中身に対して処理をします。

pred test28.
pred test28_1.
pred minus i:int o:int.
minus N M :-
      M is ~ N.
test28 :-
       std.omap (some 1) minus X,
       print "omap (some 1) is" X.
test28_1 :-
       std.omap none minus X,
       print "omap none is" X.

pred nth i:int, i:list A, o:A.

先頭を0として、N番目の要素を取り出す。ISO Prologの nth0と同じ。

pred test29.
test29 :-
       std.nth 0 [1, 2, 3] X,
       print "nth is" X.

pred lookup i:list (pair A B), i:A, o:B.

連想配列。バックトラックで複数解が得られる。

pred test30.
test30 :-
       std.lookup [pr 1 11, pr 2 12, pr 1 13] 1 X,
       print "lookup 1 is" X.

pred lookup! i:list (pair A B), i:A, o:B.

連想配列。唯一解のみ。

pred test31.
test31 :-
       std.lookup! [pr 1 11, pr 2 12, pr 1 13] 1 X,
       print "lookup! 1 is" X.

pred mem! i:list A, o:A.

∈ メンバー述語です。

pred test32.
test32 :-
       std.mem! [1, 2, 1] 1,
       print "succ".

pred mem i:list A, o:A.

∈ メンバー述語ですが、非決定的に動作します。つまり、バックトラックで戻ってきても、要素の個数だけ成功します。

pred test33.
test33 :-
       std.mem [1, 2, 1] 1,
       print "succ".

pred exists i:list A, i:(A -> prop).

exists リスト pで、リストに引数の命題pを成功する要素 x がひとつでもあれば成功する。要素が複数あれば、バックトラックしてもその回数だけ成功する。
p xが複数回成功するなら、その分も成功する。

pred test34.
pred one i:int.
one 1.
test34 :-
       std.exists [1, 2, 1] one,
       print "ok".

pred exists2 i:list A, i:list B, i:(A -> B -> prop).

exists2 リスト1 リスト2 pで、
2つのリストの同じ場所にpを成功する要素 x と y があれば成功する。
p x yが複数回成功するなら、その分も成功する。

pred test35.
pred onetwo i:int i:int.
onetwo 1 2.
test35 :-
       std.exists2 [0, 1, 1] [1, 2, 2] onetwo,
       print "ok".

pred forall i:list A, i:(A -> prop).

forall リスト pで、リストの要素全てが引数の命題pを成功するなら成功する。

pred test36.
test36 :-
       std.forall [1, 1, 1] one,
       print "ok".

pred forall-ok i:list A, i:(A -> diagnostic -> prop), o:diagnostic.

forallと同じだが、diagnostic すなわちokまたはerror 文字列を返す述語を使用します。全体の結果として、最初にerrorになったときのdiagnosticを返します。

pred test37.
pred test37_1.
pred diagone i:int o:diagnostic.
diagone 1 ok.
diagone 2 (error "2 is ng").
diagone 3 (error "3 is ng").
test37 :-
       std.forall-ok [1, 1, 1] diagone Diag,
       print Diag.
test37_1 :-
       std.forall-ok [1, 2, 3] diagone Diag,
       print Diag.

pred forall2 i:list A, i:list B, i:(A -> B -> prop).

forall2 リスト1 リスト2 pで、
2つのリストの同じ場所の要素全てが引数の命題pを成功するなら成功する。

pred test38.
test38 :-
       std.forall2 [1, 1, 1] [2, 2, 2] onetwo,
       print "ok".

pred filter i:list A, i:(A -> prop), o:list A.

述語pが成功する要素だけをピックアップします。該当する要素がなければ[]を返して成功します。

pred test39.
pred sample39 i:int.
sample39 1.
test39 :-
       std.filter [1, 2, 3] sample39 X,
       print X.

pred zip i:list A, i:list B, o:list (pair A B).

ふたつのリストから、pairのリストを作ります。

pred test40.
test40 :-
       std.zip [1, 2, 3] ["one", "two", "three"] X,
       print X.

pred unzip i:list (pair A B), o:list A, o:list B.

zipの逆です。

pred test41.
test41 :-
       std.unzip [pr 1 "one", pr 2 "two", pr 3 "three"] X Y,
       print X Y.

pred flatten i:list (list A), o:list A.

リストの入れ子を除きます。ただしリストのリストだけで、ISO Prologのように任意の入れ子には対応していません。

pred test42.
test42 :-
       std.flatten [[1], [2, 3, 4, 5], [6, 7, 8], []] X,
       print X.

リストのリストのリストからはリストのリストになります。

pred test42_1.
test42_1 :-
       std.flatten [[[1, 2], [3, 4]], [[5, 6], [7, 8]]] X,
       print X.

pred null i:list A.

リストかnilなら成功します。

pred test43.
test43 :-
       not (std.null [_]),
       std.null [],
       std.null nil,
       print "[] is null".

pred iota i:int, o:list int.

0からN-1までのリストを返す。

pred test44.
test44 :-
       std.iota 3 X,
       print "iota is" X.

pred intersperse i:A, i:list A, o:list A.

リストの要素の間に要素を挿入します。

pred test45.
test45 :-
       std.intersperse 0 [1,2,3] X,
       print X.

pred flip i:(A -> B -> prop), i:B, i:A.

述語の第1引数と第2引数を交換します。

pred test46.
pred oneone i:int i:string.
oneone 1 "one".
test46 :-
       std.flip oneone "one" 1.

3個以上の引数の述語に適用することもできます。

pred test46_1.
pred oneonetwo i:int i:string i:int.
oneonetwo 1 "one" 2.
test46_1 :-
       std.flip (oneonetwo 1) 2 "one".

引数の順番を任意に入れ替えるには、λを使う方法もあります。

pred test46_2.
test46_2 :-
         P = (x\ z\ y\ oneonetwo x y z),
         print (P 1 2 "one"),
         P 1 2 "one".

pred time i:prop, o:float.

pred do! i:list prop.

pred do-ok! o:diagnostic, i:list (diagnostic -> prop).

pred lift-ok i:prop, i:string, o:diagnostic.

lift-ok p 文字列 Xで、成功ならok、失敗ならerror 文字列を返します。

pred test50.
test50 :-
       std.lift-ok true "xxx" X,
       print X.

pred test50_1.
test50_1 :-
       std.lift-ok false "xxx" Y,
       print Y.

lift-okの定義には問題があり、成功してokを返しても、バックトラックするとerror 文字列を返してしまいます。修正した定義を以下に示します。

pred lift-ok' i:prop, i:string, o:diagnostic.
lift-ok' P Msg R :- (P, !, R = ok; R = error Msg).
pred test50'.
test50' :-
       lift-ok' true "xxx" X,
       print X.

pred spy-do! i:list prop.

pred while-ok-do! i:diagnostic, i:list (diagnostic -> prop), o:diagnostic.

pred any->string i:A, o:string.

λPrologの項を文字列に変換します。型が付かない項でも変換されますが、ワーニングがでます。

pred test53.
test53 :-
       std.any->string (error "abc") X,
       print X.

pred max i:A, i:A, o:A.

>= を使って大きい方を求めます。2個の引数しか取れませんが、
{}を使って関数型言語風にネストできます。

pred test54.
pred test54_1.
pred test54_2.
test54 :-
       print {std.max {std.max {calc (0 + 1)} {calc (1 + 1)}}
                      {std.max {calc (1 + 2)} {calc (2 + 2)}}}.

これは、次の例と正確に一致し、calcの中身の計算は1回だけなので、(Cのマクロを展開した場合と違って)効率は悪くありません。

test54_1 :-
       X11 is 0 + 1,
       X12 is 1 + 1,
       std.max X11 X12 X1,
       X21 is 1 + 2,
       X22 is 2 + 2,
       std.max X21 X22 X2,
       std.max X1 X2 X,
       print X.

自分で定義した型についても、>=を定義することでmaxを適用できます。

kind windrose type.
type n, e, w, s windrose.
pred (>=) i:windrose i:windrose.
e >= n.
s >= n.
w >= n.
s >= e.
w >= e.
w >= s.
test54_2 :-
         print {std.max {std.max n e} {std.max w s}}.

pred findall i:prop, o:list prop.

バックトラックで得られる複数解をリストとして返します。第1引数のprop全体を返すのが、ISO Prologと異なります。この過程で、第1引数のpropが実行されるため、printなどのその副作用も実行されます。

pred test55.
pred sample55 o:int.
sample55 1.
sample55 2 :- print "this is 2".
sample55 3.
test55 :-
       std.findall (sample55 _) L,
       print "findall is " L.

namespace についての説明

namespace はネストできますが、その外からはその全てを指定する必要があります。

namespace space1 {
namespace space2 {
pred test99.
test99 :- std.rev [97, 98, 99] X, print X.
}
}
pred test99_1.
test99_1 :- space1.space2.test99.

参考文献

[1] ELPIソースコード
https://github.com/LPCIC/elpi/tree/master/

[2] λProlog (Lambda Prolog) の紹介
https://qiita.com/suharahiromichi/items/a046859da0c0883e7304