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

%%% #load "abstract_syntax.mod", "substitution.mod", "normal_form.mod".
%%% #query abstract_syntax, substitution, normal_form.

module normal_form.

import abstract_syntax, substitution.

type	normal_form		term -> o.
%%% ``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 I' M)) :-
	normal_form (lambda I' 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)).