HOAS based self interpreter for lambda calculus

Just copied this out of Self-applicable Partial Evaluation for Pure Lambda Calculus

(define-syntax Q ; quote a lambda term
  (syntax-rules (lambda)
    ((Q (lambda (x) M)) (lambda (a)
                          (lambda (b)
                            (lambda (c)
                              (a (lambda (x) (Q M)))))))
    ((Q (M N)) (lambda (a)
                 (lambda (b)
                   (lambda (c)
                     ((b (Q M)) (Q N))))))
    ((Q x) (lambda (a)
             (lambda (b)
               (lambda (c)
                 (c x)))))))

(define E ; evaluate a quoted lambda term
  ((lambda (m)
    ((lambda (f) (m (lambda (a) ((f f) a))))
     (lambda (f) (m (lambda (a) ((f f) a))))))
   (lambda (E)
     (lambda (t)
       (((t (lambda (M) (lambda (x) (E (M x)))))
         (lambda (M) (lambda (N) ((E M) (E N)))))
        (lambda (x) x))))))

(define test-1
  (E (Q (lambda (i) i))))

(define test-2
  (E (Q (((lambda (m)
            ((lambda (f) (m (lambda (a) ((f f) a))))
             (lambda (f) (m (lambda (a) ((f f) a))))))
          (lambda (E)
            (lambda (t)
              (((t (lambda (M) (lambda (x) (E (M x)))))
                (lambda (M) (lambda (N) ((E M) (E N)))))
               (lambda (x) x)))))
         (lambda (a) (lambda (b) (lambda (c) (a (lambda (i) (lambda (a) (lambda (b) (lambda (c) (c i)))))))))))))

; ((lambda (i) i) 'ok)
; ok 
; > (test-1 'ok)
; ok
; > (test-2 'ok)
; ok

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(★,▢,▢). % λP
rule(▢,★,★). % λ2
rule(▢,▢,▢). % λω


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)).

Type inference for The Simply Typed Lambda Calculus

%% Type inference for The Simply Typed Lambda Calculus

:- op(150, xfx, ⊢).
:- op(140, xfx, :).
:- op(100, xfy, ->).
:- op(100, yfx, $).

Γ ⊢    Term : Type          :- atom(Term), member(Term : Type, Γ).
Γ ⊢ λ(A, B) : Alpha -> Beta :- [A : Alpha|Γ] ⊢ B : Beta.
Γ ⊢   A $ B : Beta          :- Γ ⊢ A : Alpha -> Beta, Γ ⊢ B : Alpha.

/** Examples:

% Typing fix
?- Γ ⊢ y $ f : Y, Γ ⊢ f $ (y $ f) : Y.
Γ = [y: (Y->Y)->Y, f:Y->Y|_G330]

% Typing the Y combinator
?- Γ ⊢ λ(f, (λ(f,f $ f)) $ (λ(g,f $ (g $ g)))) : Y.
Y = (_G309 -> _G309) -> _G309 

% Typing flip id
?- Id = λ(i, i), Flip = λ(f, λ(y, λ(x, f $ x $ y))),
   Γ ⊢ Flip $ Id : T.
T = _G395 -> (_G395 -> _G411) -> _G411

**/