%%% Simple calculator for Church numerals in the simply typed lambda-calculus.
%%% Author: Frank Pfenning
%%% 
%%% #load church.
%%% #query church.

module church.
  
  %%% ``church_defs Z S P T'' unifies Z with the Church's zero, S with
  %%% Church's successor, P with plus, and T with times.
  church_defs
   (f \ x \ x)		          % zero.
   (n \ f \ x \ (f (n f x)))        % succ
   (n \ m \ f \ x \ (n f (m f x)))  % plus.
   (n \ m \ f \ x \ (n ((m f)) x))  % times. 
   .
  
  %%% ``ch G'' solves the result of applying G to Church's definition of
  %%% Zero, Succ, Plus, and Times, in that order.
  ch G :- church_defs Z S P T, G Z S P T.
  
  %%% "``chleq G'' solves the result of applying G to Church's definition
  %%% of Zero, Succ, Plus, and Times and the lambda prolog
  %%% definition of Less-or-equal on Church numerals.
  chleq G :- ch z \ s \ p \ t \ (G z s p t (m \ n \ (sigma C \ (p m C = n)))).