id : name_type. cid : name_type. exp : type. var : id -> exp. lam : id\exp -> exp. app : exp -> exp -> exp. mu : cid\exp -> exp. pass : cid -> exp -> exp. pred member A [A]. member X (X::L). member X (Y::L) :- member X L. pred subst exp exp id exp. subst (var X) E X E. subst (var Y) E X (var Y) :- not(X = Y). subst (app E1 E2) E X (app E1' E2') :- subst E1 E X E1', subst E2 E X E2'. subst (lam (y\E1)) E X (lam (y\E1')) :- y # E, y # X, subst E1 E X E1'. subst (mu (a\E1)) E X (mu (a\E1')) :- a # E, subst E1 E X E1'. subst (pass A E1) E X (pass A E1') :- subst E1 E X E1'. pred napp exp exp cid exp. napp (var Y) E A (var Y). napp (app E1 E2) E A (app E1' E2') :- napp E1 E A E1', napp E2 E A E2'. napp (lam (y\E1)) E A (lam (y\E1')) :- y # E, napp E1 E A E1'. napp (mu (a\C)) E A (mu (a\C')) :- a # E, napp C E A C'. napp (pass A E1) E A (pass A (app E1' E)) :- napp E1 E A E1'. napp (pass B E1) E A (pass B E1) :- not(A = B). ty : type. ==> : ty -> ty -> ty. infixr ==> 3. bot : ty. type ctx A = [(A,ty)]. pred tc (ctx id) exp ty (ctx cid). tc G (var X) T D :- member (X,T) G. tc G (lam (x\E)) (T1 ==> T2) D :- x # G, tc ((x,T1)::G) E T2 D. tc G (app E1 E2) T2 D :- tc G E1 (T1 ==> T2) D, tc G E2 T1 D. tc G (mu (x\E)) T D :- x # D, tc G E bot ((x,T)::D). tc G (pass A E) bot D :- member (A,T) D, tc G E T D. ?tc [] (lam (x\ (lam (y\ app (var y) (var x))))) T []. ?tc [] (mu (a\ (pass a (lam (x\ lam (y\ app (var x) (var y))))))) T []. ?tc [] (lam (x\ mu (a\ pass a (var x)))) T []. (*? tc [] (app (mu (a\ pass a (lam (x\ pass a (lam (z.var z)))))) (lam (z.var z))) T [].*) ?tc [] (lam (y\ mu (b\ pass b (app (var y) (lam (x\ mu (a\ pass b (var x)))))))) T []. ?tc [] (lam (x\ mu (a\ app (var x) (lam (y\ pass a (var y)))))) T [].