%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Interpreter for focused linear logic (LLF) %
% %
% Specific for Linear Nested systems %
% %
% Author: Elaine Pimentel (2015) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This prover is for a fragment of LLF, used for specifying and
%% verifying properties of linear nested systems. The grammar we use is:
%% Object level formulas
%% F := A | F cand F | F cor F | F cimp F | cfalse | box F | hearts F.
%% Labelled formulas
%% L := r X F, l X F.
%% Linear logic formulas
%% M := A | M @ M | M , M | M & M | pi M | sigma M | top.
%% Observe that we don't use all the connectives.
% Unfocused sequents have the form C H R TH PC G, where C and H control
% the limit of the height of the proof; TH is the classical context containing
% the theory; R is linear and has the relation singleton; contains only positive
% formulas or the classical atomic ones. The context is the same mixting linear
% and classical formulas, but for our encodings, this is not a problem; finally,
% G is the normal linear context.
% Focused sequents have the form C H R TH PC P, where P is a positiv formula.
module llf.
%%%% Inference rules for LLF
llf C T G :- (((theory4 T TH),(prove_a C 0 (relB z x) TH nil (G::nil))) ; ((theory T TH), prove_a C 0 (rel z x) TH nil (G::nil))).
%%% Negative Phase
prove_a C H R TH PC (top::G) :-
printf [nl, pc " Top rule.", nl, fl].
prove_a C H R TH PC ((A & B)::G) :-
printf [nl, pc " With right ", nl, fl],
prove_a C H R TH PC (A::G),
prove_a C H R TH PC (B::G).
prove_a C H R TH PC ((A @ B)::G) :-
printf [nl, pc " Par right ", nl, fl],
prove_a C H R TH PC (A::B::G).
prove_a C H R TH PC ((pi A)::G) :-
printf [nl, pc " Forall right ", nl, fl],
pi X\ prove_a C H R TH PC ((A X)::G).
%% Collecting positive or atomic formulas
prove_a C H R TH PC (P::G):-
(pos P; atomic P),
printf [nl, pc" storing positive and atomic formulas ", pc P, pc "' to G.", nl, fl],
prove_a C H R TH (P::PC) G.
%% Changing relational formulas
prove_a C H R TH PC (R1::G):-
(R1 = (rel X Y); R1 = (relH X Y); R1 = (relH X Y) ; R1 = (relE X Y Z)),
printf [nl, pc" storing relational formula ", nl, fl],
prove_a C H R1 TH PC G.
%%% Synchronous Phase
%% Not a very efficient way of implementing this
prove_s C H R TH PC (A , B):-
printf [nl, pc " Tensor right ", nl, fl],
split PC PC1 PC2,
prove_s C H R TH PC1 A,
prove_s C H R TH PC2 B.
prove_s C H R TH PC (sigma A) :-
printf [nl, pc " Exists right ", nl, fl],
sigma X\ prove_s C H R TH PC (A X).
%%% Identity and Decide rules
%% Unfocusing
prove_s C H R TH PC A :-
neg A,
printf [nl, pc " Unfocusing ", nl, fl],
prove_a C H R TH PC (A::nil).
%% Focusing on PC
prove_a C H R TH (PC) nil :-
memb P PC,
% pos P, we will only focus on negated atoms
P = perp A,
H1 is H + 1,
H1 <= C,
printf [nl, pc " DRL rule: choosing '", pc P, pc "' positive . H = ", pc H1, nl, fl],
prove_s C H1 R TH PC P.
% actually here we could finish the proof...
%% Focusing on the theory
prove_a C H R TH PC nil :-
memb F TH,
H1 is H + 1,
H1 <= C,
printf [nl, pc " DRC, choosing '", pc F, pc "' from theory. ", nl, fl],
prove_s C H1 R TH PC F.
%% I -- observe that atoms are classical...
prove_s C H R TH PC (perp A) :-
memb A PC,
printf [nl, pc " Initial rule: proving '", pc A, pc "' H = ", pc H, nl, fl],
flush std_out.
%% Initial relational
prove_s C H R TH PC (perp A) :-
((A = (rel X Y),R = (rel X Y)); (A = (relB X Y),R = (relB X Y)); (A = (relH X Y),R = (relH X Y)) ; (A = (relE X Y Z),R = (relE X Y Z))),
printf [nl, pc " Initial rule on relations", nl, fl],
flush std_out.
%%%% Positive and negative formulas
pos (A , B).
pos (sigma A).
pos (perp A).
neg (A & B).
neg (pi A).
neg (A @ B).
neg top.
neg (rel X Y).
neg (relB X Y).
neg (relH X Y).
neg (relE X Y Z).
neg A :- atomic A.
%%%% Definition of atomic
non_atomic (A , B).
non_atomic (sigma A).
non_atomic (A & B).
non_atomic (pi A).
non_atomic top.
non_atomic (A @ B).
non_atomic (perp A).
%% R relations cannot be treated as logical atomic formulas.
non_atomic (rel X Y).
non_atomic (relB X Y).
non_atomic (relH X Y).
non_atomic (relE X Y Z).
atomic (l X A).
atomic (r X A).
atomic A :- not (non_atomic A).
%%%% Prints
printf nil.
printf (pc (Item : string) :: L) :- !, print Item, printf L.
printf (pc Item :: L) :- term_to_string Item Str, print Str, printf L.
printf (nl :: L) :- print "\n", printf L.
printf (fl :: L) :- flush std_out, printf L.
%%%% Auxiliary functions
% (memb X L) succeeds if X is a member of L. In contrast to ``member'',
% this will succeed as often as X unifies with members of L.
memb X (X :: L).
memb X (Y :: L) :- memb X L.
% (memb_and_rest X L M) succeeds for every occurrence of X in L,
% where M is the result of removing that occurrence from L.
memb_and_rest A (A :: Rest) Rest.
memb_and_rest A (B :: Tail) (B :: Rest) :- memb_and_rest A Tail Rest.
% (split L K M) succeeds if L is split into K and M (implements
% multiset splitting).
split nil nil nil.
split (X::L) (X::K) M :- split L K M.
split (X::L) K (X::M) :- split L K M.
%%%% Tests G3cp
%llf 100 g3cp (r x (a cimp a)).
%llf 100 g3cp (r x ((a cand b) cimp (a cand b))).
%llf 100 g3cp (r x ((a cand b) cimp a)).
%llf 100 g3cp (r x ((a cand b) cimp (a cor b))).
%llf 100 g3cp (r x ((a cor b) cimp (a cand b))).
%llf 100 g3cp (r x ((a cand (a cimp b)) cimp b)).
%%%% Tests K
%llf 100 k (r x ((box a) cimp (box a))).
%llf 100 k (r x (a cimp (box a))).
%llf 100 k (r x ((box a) cimp a)).
%llf 100 k (r x ((box (a cimp b)) cimp ((box a) cimp (box b)))).
%%%% Tests KTS4
%llf4 100 kts4 (r x ((box a) cimp (box a))).
%llf4 100 kts4 (r x ((hearts a) cimp (hearts a))).
%llf4 100 kts4 (r x ((hearts a) cimp (box a))).
%llf4 100 kts4 (r x ((box a) cimp (hearts a))).
%%%% Systems
theory g3cp
(
(sigma A\ sigma B\ sigma X\ (perp (l X (A cimp B))) , ((r X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cimp B))) , ((l X A) @ (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cand B))) , ((l X A) @ (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cand B))) , ((r X A) & (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cor B))) , ((l X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cor B))) , ((r X A) @ (l X B))) ::
(sigma A\ sigma X\ (perp (r X A)) , (perp (l X A))) ::
( perp (l X cfalse) , top) :: nil
).
theory k
(
(sigma A\ sigma B\ sigma X\ (perp (l X (A cimp B))) , ((r X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cimp B))) , ((l X A) @ (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cand B))) , ((l X A) @ (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cand B))) , ((r X A) & (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cor B))) , ((l X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cor B))) , ((r X A) @ (l X B))) ::
(sigma A\ sigma X\ sigma Z\ (perp (r X (box A))),(perp (rel Z X)),pi Y\ (r Y A) @ (rel X Y)) ::
(sigma A\ sigma X\ sigma Y\ (perp (l X (box A))),(perp (rel X Y)), ((l Y A) @ (rel X Y))) ::
(sigma A\ sigma X\ (perp (r X A)) , (perp (l X A))) ::
( perp (l X cfalse) , top) :: nil
).
theory4 kts4
(
(sigma A\ sigma B\ sigma X\ (perp (l X (A cimp B))) , ((r X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cimp B))) , ((l X A) @ (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cand B))) , ((l X A) @ (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cand B))) , ((r X A) & (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cor B))) , ((l X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cor B))) , ((r X A) @ (l X B))) ::
(sigma A\ sigma X\ (perp (r X A)) , (perp (l X A))) ::
(sigma A\ sigma X\ sigma Z\ (perp (r X (box A))),(perp (relB Z X)),pi Y\ (r Y A) @ (relH X Y)) ::
(sigma A\ sigma X\ sigma Z\ (perp (r X (box A))),(perp (relH Z X)),pi Y\ (r Y A) @ (relH X Y)) ::
(sigma A\ sigma X\ sigma Y\ (perp (l X (box A))),(perp (relH X Y)), ((l Y A) @ (relH X Y))) ::
(sigma A\ sigma X\ sigma Y\ (perp (l X (hearts A))),(perp (relH X Y)), ((l Y A) @ (relH X Y))) ::
(sigma A\ sigma X\ sigma Y\ (perp (l X (hearts A))),(perp (relH X Y)), ((l Y (hearts A)) @ (relH X Y))) ::
(sigma A\ sigma X\ sigma Z\ (perp (r X (hearts A))),(perp (relB Z X)),pi Y\ (r Y A) @ (relH X Y)) ::
(sigma A\ sigma X\ sigma Z\ (perp (r X (hearts A))),(perp (relH Z X)),pi Y\ (r Y A) @ (relH X Y)) ::
(sigma A\ sigma X\ sigma Y\ (perp (l X (hearts A))),(perp (relH X Y)), ((l Y (hearts A)) @ (relH X Y))) ::
% (sigma A\ sigma X\ (perp (l X (box A))) , (l X A)) ::
% (sigma A\ sigma X\ (perp (l X (hearts A))) , (l X A)) ::
( perp (l X cfalse) , top) :: nil
).
theory ec
(
(sigma A\ sigma B\ sigma X\ (perp (l X (A cimp B))) , ((r X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cimp B))) , ((l X A) @ (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cand B))) , ((l X A) @ (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cand B))) , ((r X A) & (r X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (l X (A cor B))) , ((l X A) & (l X B))) ::
(sigma A\ sigma B\ sigma X\ (perp (r X (A cor B))) , ((r X A) @ (l X B))) ::
(sigma A\ sigma X\ (perp (r X A)) , (perp (l X A))) ::
(sigma A\ sigma X\ sigma Z\ (perp (r X (box A))),(perp (rel Z X)),pi Y\ pi W\ (r Y A) @ (l W A) @ (relE X Y W)) ::
(sigma A\ sigma X\ sigma Y\ sigma Z\ (perp (l X (box A))),(perp (relE X Y Z)), ((l Y (box A)) @ (rel X Y)) , ((r Z (box A)) @ (rel X Z))) ::
(sigma A\ sigma X\ sigma Y\ sigma Z\ (perp (l X (box A))),(perp (relE X Y Z)), ((l Y (box A)) @ (relE X Y Z)) , ((r Z (box A)) @ (rel X Z))) ::
( perp (l X cfalse) , top) :: nil
).
%%%% Commands
%tjcc llf && tjlink llf && tjsim llf
%open.