% % An eager evaluator for lambda terms % ?- op(500, quant, lambda). % declare lambda as a quantifier ?- op(800, xfx, =>). % single reduction ?- op(800, xfx, =>*). % zero or more reductions ?- obvar_prefix(x). % lambda evaluation A =>* Result :- reduce(A, B, IsReduced), ( IsReduced == true -> simplify_term(B, Result) ; Result = B ). reduce(A(B), Result, IsReduced) :- reduce(A, C, IsReduced), reduce(B, D, BIsReduced), IsReduced = BIsReduced, reduce_application(C, D, Result, IsReduced), !. reduce(lambda x A, Result, IsReduced) :- reduce(A, B, IsReduced), IsReduced == true, !, Result = lambda x B. reduce(X, X, _). reduce_application(lambda x F, A, Result, true) :- !, ( quant(A) -> reduce([A/x]F, Result, _) % A is a lambda abstraction ; Result = [A/x]F ). reduce_application(F, A, Result, IsReduced) :- IsReduced == true, Result = F(A).