λProlog module pcf

sig pcf. kind tm, ty type. type zero, tt, ff tm. type succ, pred, is_zero tm -> tm. type if tm -> tm -> tm -> tm. type abs, rec ty -> (tm -> tm) -> tm. type app tm -> tm -> tm. type num, bool ty. type arr ty -> ty -> ty. type eval tm -> tm -> o. type of tm -> ty -> o.

module pcf. eval zero zero. eval tt tt. eval ff ff. eval (succ M) (succ V) :- eval M V. eval (pred M) zero :- eval M zero. eval (pred M) V :- eval M (succ V). eval (is_zero M) tt :- eval M zero. eval (is_zero M) ff :- eval M (succ V). eval (if M N1 N2) V :- eval M tt, eval N1 V. eval (if M N1 N2) V :- eval M ff, eval N2 V. eval (abs T R) (abs T R). eval (app M N) V :- eval M (abs T R), eval (R N) V. eval (rec T R) V :- eval (R (rec T R)) V. of zero num. of tt bool. of ff bool. of (succ M) num :- of M num. of (pred M) num :- of M num. of (is_zero M) bool :- of M num. of (if M N1 N2) T :- of M bool, of N1 T, of N2 T. of (abs T R) (arr T U) :- pi n\ (of n T => of (R n) U). of (app M N) T :- of M (arr U T), of N U. of (rec T R) T :- pi n\ (of n T => of (R n) T).