%%% normal forms for the lambda calculus
%%%
%%% AUTHOR: Gary T. Leavens

module normal_form.
  
  accumulate substitution.
  
  %%% ``normal_form M'' succeeds if M is in beta-eta normal form.
  
  %%% variables are in normal form.
  normal_form (var X).
  
  
  %%% applications are in normal form if they aren't a beta redex and subterms
  %%% are in normal form.
  normal_form (ap (var X) N) :-
  	normal_form N.
  normal_form (ap (ap M1 M2) N) :-
  	normal_form (ap M1 M2),
  	normal_form N.
  
  
  %%% lambdas are in normal form if they aren't an eta redex and subterms are
  %%% in normal form.
  normal_form (lambda I (var X)).
  normal_form (lambda I (lambda I2 M)) :-
  	normal_form (lambda I2 M).
  
  normal_form (lambda I (ap M (var I))) :-
  	free_in I M,                     % violates side condition of eta
  	normal_form M.
  normal_form (lambda I (ap M (var X))) :-
  	not(I = X),
  	normal_form (ap M (var X)).
  normal_form (lambda I (ap M (ap N1 N2))) :-
  	normal_form (ap M (ap N1 N2)).
  normal_form (lambda I (ap M (lambda X Body))) :-
  	normal_form (ap M (lambda X Body)).