A version of λR implemented in Prolog

quant.pro

module(quant).

% Database (algebra)

%! type ann := zero | one | omega.

%! zero(+X:ann) is semidet.
%! add(-X:ann, -Y:ann, +Z:ann) is nondet.
%! one(+X:ann) is semidet.
%! mult(+X:ann, -Y:ann, +Z:ann) is nondet.
%! del(+X:ann) is semidet.
%! dup(+X:ann, -Y:ann, -Z:ann) is nondet.
zero(zero).
zero(omega).
add(zero,zero,zero).
add(one,zero,one).
add(zero,one,one).
add(omega,omega,omega).
one(one).
one(omega).
mult(zero,_,zero).
mult(one,Y,Y).
mult(omega,zero,zero).
mult(omega,omega,omega).
del(_).
dup(X,X,X).

% Lifting to vectors

%! zerov(+R:list(ann)) is semidet.
%! addv(-P:list(ann), -Q:list(ann), +R:list(ann)) is nondet.
%! delv(+R:list(ann)) is semidet.
%! dupv(+P:list(ann), -Q:list(ann), -R:list(ann)) is nondet.
%! basis(+R:list(ann), +I:nat) is semidet.
%! scale(+X:ann, -P:list(ann), +Q:list(ann)) is nondet.
zerov(nil).
zerov(snoc(R,X)) :- zero(X), zerov(R).
addv(nil,nil,nil).
addv(snoc(P,X),snoc(Q,Y),snoc(R,Z)) :- add(X,Y,Z), addv(P,Q,R).
delv(nil).
delv(snoc(R,X)) :- del(X), delv(R).
dupv(nil,nil,nil).
dupv(snoc(P,X),snoc(Q,Y),snoc(R,Z)) :- dup(X,Y,Z), dupv(P,Q,R).
basis(snoc(R,X),z) :- one(X), zerov(R).
basis(snoc(R,X),s(I)) :- zero(X), basis(R,I).
scale(_,nil,nil).
scale(X,snoc(P,Y),snoc(Q,Z)) :- mult(X,Y,Z), scale(X,P,Q).

% Context operations

%! type ctx := ctx(list(ann), list(ty)).

%! lookup(+G:list(a), +I:nat, -A:a) is semidet.
lookup(snoc(_,A),z,A).
lookup(snoc(G,_),s(I),A) :- lookup(G,I,A).

%! empty(-RG:ctx) is det.
empty(ctx(nil,nil)).
%! bind(+RG:ctx, +RhoA:(ann, ty), -RGx:ctx) is det.
bind(ctx(R,G),(Rho,A),ctx(snoc(R,Rho),snoc(G,A))).

% Type system
%
% v - variable (de Bruijn)
% a - type annotation/cut
% u - embedding (underline)
% c - constructor
% e - eliminator
%
% Types:
% A, B, C ::= fun((Rho,A),B) | unit | tensor((Pi,A),(Rho,B))
%           | top | with(A,B) | empty | plus((Pi,A),(Rho,B))
% fun ~ ⊸, unit ~ I, tensor ~ ⊗, top ~ ⊤, with ~ &, empty ~ 0, plus ~ ⊕
%
% Some rules:
%
%  I : RΓ ⊐ A       A ∋ S      S ∈ B  B ≤ A
% -------------   ----------   ------------
% RΓ ⊢ v(I) ∈ A   a(A,S) ∈ A     A ∋ u(S)
%
% Plus rules for each type former...

%! subty(+A:ty, +B:ty).
subty(A,A).

%! syn(+RG:ctx, +E:tm(syn), -A:ty).
%! chk(+RG:ctx, +A:ty, +S:tm(chk)).
:- discontiguous syn/3.
:- discontiguous chk/3.

% Variables
syn(ctx(R,G),v(I),A) :- basis(R,I), lookup(G,I,A).
% Change of direction
syn(RG,a(A,S),A) :- chk(RG,A,S).
chk(RG,A,u(S)) :- syn(RG,S,B), subty(B,A).
% Function
syn(ctx(R,G),e(F,S),B) :-
  addv(P,RhoQ,R), scale(Rho,Q,RhoQ),
  syn(ctx(P,G),F,fun((Rho,A),B)), chk(ctx(Q,G),A,S).
chk(RG,fun((Rho,A),B),c(T)) :- bind(RG,(Rho,A),RGx), chk(RGx,B,T).
% Empty tensor product
syn(ctx(R,G),e(E,C,S),C) :- addv(P,Q,R), syn(ctx(P,G),E,unit), chk(Q,C,S).
chk(ctx(R,_),unit,c()) :- zerov(R).
% Tensor product
syn(ctx(R,G),e(E,C,S),C) :-
  addv(P,Q,R), syn(ctx(P,G),E,tensor((Pi,A),(Rho,B))),
  bind(ctx(Q,G),(Pi,A),QGx), bind(QGx,(Rho,B),QGxy), chk(QGxy,C,S).
chk(ctx(R,G),tensor((Pi,A),(Rho,B)),c(S,T)) :-
  addv(PiP,RhoQ,R), scale(Pi,PiP,P), chk(ctx(P,G),A,S),
  scale(Rho,RhoQ,Q), chk(ctx(Q,G),B,T).
% Empty with product
chk(ctx(R,_),top,c()) :- delv(R).
% With product
syn(RG,e(E,l),A) :- syn(RG,E,with(A,_)).
syn(RG,e(E,r),B) :- syn(RG,E,with(_,B)).
chk(ctx(R,G),with(A,B),c(S,T)) :-
  dupv(R,P,Q), chk(ctx(P,G),A,S), chk(ctx(Q,G),B,T).
% Empty sum
syn(ctx(R,G),e(E,C),C) :- addv(P,Q,R), syn(ctx(P,G),E,empty), delv(Q).
% Sum
syn(ctx(R,G),e(E,C,S,T),C) :-
  addv(P,Q,R), syn(ctx(P,G),E,plus((Pi,A),(Rho,B))), dupv(Q,Qx,Qy),
  bind(ctx(Qx,G),(Pi,A),QGx), bind(ctx(Qy,G),(Rho,B),QGy),
  chk(QGx,C,S), chk(QGy,C,T).
chk(ctx(R,G),plus((Pi,A),_),c(l,S)) :- scale(Pi,P,R), chk(ctx(P,G),A,S).
chk(ctx(R,G),plus(_,(Rho,B)),c(r,T)) :- scale(Rho,Q,R), chk(ctx(Q,G),B,T).

% Examples:

%! chkclosed(+A:ty, +S:tm(chk)).
chkclosed(A,S) :- chk(ctx(nil,nil),A,S).

% swap⊗ : 1(1a ⊗ 1b) ⊸ 1b ⊗ 1a ∋ λx. let y, z = x in z, y
:- chkclosed(fun((one,tensor((one,a),(one,b))),tensor((one,b),(one,a))),
             c(u(e(v(z),_,c(u(v(z)),u(v(s(z)))))))).
% unitl⊕ : 1(10 ⊕ 1a) ⊸ a ∋ λx. case x of { inl y ↦ case y of {}, inr y ↦ y }
:- chkclosed(fun((one,plus((one,empty),(one,a))),a),
             c(u(e(v(z),_,u(e(v(z),_)),u(v(z)))))).
% dup& : 1a ⊸ a & a ∋ λx. x, x
:- chkclosed(fun((one,a),with(a,a)), c(c(u(v(z)),u(v(z))))).
% extract : ωa ⊸ a ∋ λx. x
:- chkclosed(fun((omega,a),a), c(u(v(z)))).
% duplicate : ωa ⊸ 0I ⊗ ω(0I ⊗ ωa) ∋ λx. (), (), x
:- chkclosed(fun((omega,a),
                 tensor((zero,unit),(omega,tensor((zero,unit),(omega,a))))),
             c(c(c(),c(c(),u(v(z)))))).
% expsplit : ω(a & b) ⊸ ωa ⊗ ωb ∋ λx. (x.fst, x.snd)
:- chkclosed(fun((omega,with(a,b)),tensor((omega,a),(omega,b))),
             c(c(u(e(v(z),l)),u(e(v(z),r))))).
% expjoin : 1(ωa ⊗ ωb) ⊸ 0I ⊗ ω(a & b) ∋ λxy. let x, y = xy in (), x, y
:- chkclosed(fun((one,tensor((omega,a),(omega,b))),
                 tensor((zero,unit),(omega,with(a,b)))),
             c(u(e(v(z),_,c(c(),c(u(v(s(z))),u(v(z)))))))).