この記事はProlog Advent Calendar 2016の２日目の記事です。
ほとんど、一人アドベントカレンダーになりそうなのですけど、せっかくなので全部埋めてみたいと思いつつ、Prolog関連のネタを小出しに書いていってみようと思います。
今日は、線形論理型言語について書いてみようと思います。
Rust基礎勉強会とかもあるそうなので、調べていたことをちょっと書いてみます。いろいろと調べていたことは調べていたのですけど、能力不足です。すいません。
ググると、いくつか出てきます。
Lolli
これが元になって、LLPやTLLPが作られたようです。
LLP
Lolliを発展させて、非決定的な要素をなくしたもののようです。
神戸大学で開発されていたようです。
TLLP
LLPを更に発展させて時相な要素を追加したもののようです。
TLLP interpreter in Prolog
これらの言語は結局どんな言語なのか？
どうも、Prologを高速化するためにリソース管理をし用みたいな感じのように思えました。
RustがGCレスで高速に実装したいというのに近いのかなと。
論理型言語ですので、あたりまえですけど、線形型ではありません。
論理をリソースのように扱って1回使ったら消費されてなくなる論理を作って使ったり、リターン値を返すのに、一時的なリソースを作っておいてそこに値を入れて返すことに用いたりする目的で使うようでした。
Lolli言語ではリソースはまとめて一気に消す述語があって消すことができます。ただし、消す述語を書いたあとでも使われるリソースはいい感じに取り扱ってくれます。失敗したらトラックバックをするから推論可能なのです。というものでした。
Lolliのリソースを一気にまとめて消す機能は便利なのですが、非決定的な計算になるので遅くなるし、標準出力などをしていた場合は、何度も出力されると行った問題が出ます。
そこで、LLPでは、決定的な言語にして、リソースを一気にまとめて消す述語を使うと完全にリソースを全て消してしまいます。こうすれば、決定的な論理として扱えるのでよいだろうということだったようです。
現在我々が想像するATSやRustの線形型やAffine型は、リソース1つ1つに対して作成したら消費するという考えがありますが、初期の論理型言語はいいかんじに、まとめて消したり、全部消したりするだけなので、手動でGCをするようなものとして扱われていたようです。
ソースもそれなりに読み込んでいたのですけど、うまく説明できなくてすいませんです。
% A Prolog implementation of Lolli
:- style_check(-singleton).
% The logic begin interpreted contains the following logical connectives:
% true/0 a constant (empty tensor, written as 1 in the logic)
% erase/0 a constant (erasure, written as Top in the logic)
% bang/1 the modal, written as {} in the paper.
% 解釈されるロジックの開始には、次の論理接続が含まれます。
% true/0 定数（空のテンソル、論理で1と書かれている）
% erase/0 定数（消去、論理のトップとして書かれている）
% bang/1 論文で{}と書かれた様式
:- op(145,xfy,->). % linear implication, written as -o in the paper
:- op(145,xfy,=>). % intuitionistic implication
:- op(145,xfy,x). % multiplicative conjunction (tensor)
:- op(145,xfy,&). % additive conjunction
:- op(145,xfy,::). % non-empty list constructor
interp(G) :- prove(nil,nil, G),!.
isG(true).
isG(erase).
isG(B) :- isA(B).
isG(B -> B2) :- isR(B1), isG(B2).
isG(B => B2) :- isR(B1), isG(B2).
isG(B & B2) :- isG(B1), isG(B2).
isG(B x B2) :- isG(B1), isG(B2).
isG(bang(B)) :- isG(B).
isR(erase).
isR(B) :- isA(B).
isR(B1 & B2) :- isR(B1), isR(B2).
isR(B1 -> B2) :- isG(B1), isR(B2).
isR(B1 => B2) :- isG(B1), isR(B2).
bc(I,I,A, A).
bc(I,O,A, G -> R) :- bc(I,M,A,R), prove(M,O,G).
bc(I,O,A, G => R) :- bc(I,O,A,R), prove(O,O,G).
bc(I,O,A, R1 & R2) :- bc(I,O,A,R1); bc(I,O,A,R2).
pickR(bang(R)::I, bang(R)::I, R).
pickR(R::I, del::I, R) :- isR(R).
pickR(S::I, S::O, R) :- pickR(I,O,R).
subcontext(del::O, R ::I) :- isR(R), subcontext(O,I).
subcontext(S::O, S::I) :- subcontext(O,I).
subcontext(nil, nil).
prove(I,I, true).
prove(I,O, erase) :- subcontext(O,I).
prove(I,O, G1 & G2) :- prove(I,O,G1), prove(I,O,G2).
prove(I,O, R -> G) :- prove(R :: I, del :: O,G).
prove(I,O, R => G) :- prove(bang(R) :: I, bang(R) :: O,G).
prove(I,O, G1 x G2) :- prove(I,M,G1), prove(M,O,G2).
prove(I,I, bang(G)) :- prove(I,I,G).
prove(I,O, A) :- isA(A), pickR(I,M,R), bc(M,O,A,R).
% The following code provides the hooks into application programs.
:- op(150,yfx,<-). % the converse of the linear implication
% Applications using this interpreter are specified using the <-/2 functor (denoting the converse
% of linear implication). We shall assume that clauses so specified are implicitly banged (belong
% to the unbounded part of the initial context) and that the first argument to -> is atomic. The
% following clause is the hook to clauses specified using <-.
prove(I,O, A) :- isA(A), A <- G, prove(I,O,G).
% A few input/output non-logicals.
prove(I,I, write(X)) :- write(X).
prove(I,I, read(X)) :- read(X).
prove(I,I, nl) :- nl.
% The following is a flexible specification of isA/1
notA(write(_)). notA(read(_)).
notA(nl). notA(erase). notA(true). notA(del).
notA(_ & _). notA(_ x _). notA(_ -> _). notA(_ => _). notA(bang(_)).
isA(A) :- \+(notA(A)).
(_ <- _) :- fail.
formula(1 ,true, (a -> a)).
formula(2 ,true, (a -> (b -> (a x b)))).
formula(3 ,true, (a => bang(a))).
formula(4 ,true, ((a & b) -> (a & b))).
formula(5 ,true, (a => (a & a))).
formula(6 ,true, (a => (a x a))).
formula(7 ,true, ((a & b) -> a)).
formula(8 ,true, (a -> (a & a))).
formula(9 ,true, (a => b => bang(a & b))).
formula(10,true, ((a & b) => (bang(a)x bang(b)))).
formula(11,true, ((a -> b -> c) -> (a => b => c))).
formula(12,true, (((a x b) -> c) -> (a -> b -> c))).
formula(13,true, (a -> b -> (a x erase))).
formula(14,true, (a -> b -> (erase x a))).
formula(15,true, (a -> b -> (b x erase x a))).
formula(16,true, (a -> b => (b x erase x a))).
formula(17,true, ((a & b) -> (a & b) -> ((a x a) & (a x b) & (b x b)))).
formula(18,true, (a => b -> (b x bang(a)))).
formula(19,true, (a => b -> (bang(a) x b))).
formula(20,fail, (a -> (a x a))).
formula(21,fail, (a -> a -> a)).
formula(22,fail, (a -> b -> (a & b))).
formula(23,fail, ((a & b) -> (a x b))).
formula(24,fail, ((a -> b -> c) -> (a -> b) -> a -> c)).
formula(25,true, ((a -> b -> c) -> (a -> b) -> (a -> a -> c))).
formula(26,true, (a -> b -> c -> erase)).
formula(27,true, (a -> a -> a -> (a x erase))).
formula(28,true, (a -> b -> c -> (erase x erase))).
examples :- formula(X, R, F), write(X), (interp(F), R=true,write(" solved ok"); R=fail,write(" failed ok")), nl, fail.
examples.
:- examples.
:- interp(true).
:- interp(a->a).
:- \+ interp(a->(a x a)).
:- interp(a->(a & a)).
:- interp(a=>(a x a x a)).
:- interp(a->(a x write(a) x nl)).
:- halt.
なかんじで、テストが動いたりします。
LLPだとformulaのうちeraseしたあとに、使っているリソースは消えてなくなるようです。
例がどこにあるのかもよくわからなかったのですけど、例がそれなりにあったので拾ってきてくっつけただけという、いい加減なお話になってます。すいません。