## Saturday, 21 June 2008

### Pure Type Systems type checker in Prolog

They ( http://people.cs.uu.nl/andres/LambdaPi/index.html http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html ) said it was easy but actually it's very hard, of course these posts are very helpful though. My other reference is the book Lectures on the Curry-Howard Isomorphism (Studies in Logic and Foundations of Mathematics - Vol 149).

Assuming this doesn't have any bugs, does it..?
`:- op(1200, xfx, :=).:- op(150, xfx, ⊢).:- op(140, xfx, :).:- op(100, yfx, \$).sort(★).sort(▢).axiom(★,▢).rule(★,★,★). % λ→rule(★,▢,▢). % λPrule(▢,★,★). % λ2rule(▢,▢,▢). % λωunfold(Term, TermU) :- unfold([],Term,TermU).unfold(_, Sort, Sort) :- sort(Sort).unfold(Γ, Ident, Value) :- member(Ident, Γ) -> Ident = Value ; ( Ident := ValueD ), unfold(ValueD, Value).unfold(Γ, λ(Var:Type,Body), λ(Var:TypeU,BodyU)) :- unfold(Γ, Type, TypeU), unfold([Var|Γ], Body, BodyU).unfold(Γ, π(Var:Type,Body), π(Var:TypeU,BodyU)) :- unfold(Γ, Type, TypeU), unfold([Var|Γ], Body, BodyU).unfold(Γ, U \$ V, P \$ Q) :- unfold(Γ, U, P), unfold(Γ, V, Q).alpha(X,Y) :- alpha([],X,Y).alpha(_,Id,Id) :- !.alpha(Γ,Var1,Var2) :- member(Var1=Var2,Γ).alpha(Γ,λ(Var1:Type1,Body1), λ(Var2:Type2,Body2)) :- alpha(Γ,Type1,Type2), alpha([Var1=Var2|Γ],Body1,Body2).alpha(Γ,π(Var1:Type1,Body1), π(Var2:Type2,Body2)) :- alpha(Γ,Type1,Type2), alpha([Var1=Var2|Γ],Body1,Body2).alpha(Γ,U \$ V,P \$ Q) :- alpha(Γ,U,P), alpha(Γ,V,Q).subst(X->Y,X,Y) :- !.subst(_->_,Var,Var) :- atomic(Var).subst(X->Y,λ(X:Type1,Body),λ(X:Type2,Body)) :- !, subst(X->Y,Type1,Type2).subst(X->Y,λ(Z:Type1,Body1),λ(Z:Type2,Body2)) :- subst(X->Y,Type1,Type2), subst(X->Y,Body1,Body2).subst(X->Y,π(X:Type1,Body),π(X:Type2,Body)) :- !, subst(X->Y,Type1,Type2).subst(X->Y,π(Z:Type1,Body1),π(Z:Type2,Body2)) :- subst(X->Y,Type1,Type2), subst(X->Y,Body1,Body2).subst(X->Y,U \$ V,P \$ Q) :- subst(X->Y,U,P), subst(X->Y,V,Q).eval(λ(U:_,B) \$ V, BetaVal) :- !, subst(U->V,B,Beta), eval(Beta,BetaVal).eval(X \$ Y, XY) :- !, eval(X,Xv), eval(Xv \$ Y,XY).eval(Value, Value).type(Term, Type) :- unfold(Term,TermU), [] ⊢ TermU : Type.hasType(Term, Type) :- type(Term, Type1), unfold(Type,TypeU), eval(TypeU, Type2), alpha(Type1,Type2)._ ⊢ S1 : S2 :- axiom(S1,S2).Γ ⊢ I : T :- once(member(I:T, Γ)).Γ ⊢ λ(A:T,B) : π(A:Tv,C) :- Γ ⊢ T : S1, sort(S1), eval(T,Tv), [A:Tv|Γ] ⊢ B : C. %%, /* sanity checks: */ Γ ⊢ π(A:Tv,C) : S2, sort(S2).Γ ⊢ π(A:T,B) : S :- Γ ⊢ T : S1, [A:T|Γ] ⊢ B : S2, rule(S1,S2,S).Γ ⊢ P \$ Q : T :- Γ ⊢ P : π(X:U,B), Γ ⊢ Q : V, alpha(U,V), eval(λ(X:U,B) \$ Q,T).id := λ(t:★, λ(x:t, x)).idTy := π(x:★, π(e:x, x)).const := λ(s:★, λ(t:★, λ(u:s, λ(v:t, u)))).constTy := π(u:★, π(v:★, π(g0:u, π(g1:v, u)))).%%bool := π(a:★, a -> a -> a).bool := π(a:★, π(g1:a, π(g2:a, a))).true := λ(a:★, λ(x:a, λ(y:a, x))).false := λ(a:★, λ(x:a, λ(y:a, y))).%%nat := π(u:★, u -> (u -> u) -> u).nat := π(u:★, π(g1:u, π(g2:π(g3:u, u), u))).zero := λ(a:★, λ(x:a, λ(f:π(g:a, a), x))).%%succ := λ(n:nat, λ(a:★, λ(x:a, λ(f:(a -> a), f \$ (n \$ a \$ x \$ f))))).succ := λ(n:nat, λ(a:★, λ(x:a, λ(f:π(g:a, a), f \$ (n \$ a \$ x \$ f))))).add := λ(m:nat, λ(n:nat, m \$ nat \$ n \$ succ)).eq := λ(a:★, λ(x:a, λ(y:a,       λ(p:π(x:a, ★), π(g:p\$x, p\$y))))).%%eq(a:★, x:a, y:a) := λ(p:π(x:a, ★), π(g:p\$x, p\$y)).`