ALF Programming is Algebraic Logic Functional Programming. ALF programming language is used to combine the functional and logical techniques of programming. The ALF system was designed to be an efficient implementation of the combination of resolution, narrowing, rewriting, and rejection. An ALF Program consist of number of modules contained in a one modules which contains a sequence of goals to be proved.
module nats. export 0, s, +, < . datatype nat = f 0 ; s(nat) g. func + : nat, nat -> nat infixleft 500. pred < : nat, nat infix. rules. N + 0 = N. N + s(M) = s(N + M). 0 < s(M). s(N) < s(M) :- N < M. end nats
Syntax of ALF is defined in the two parts.
Context free component: Context free component of the syntax is defined by programmer in EBNF style.
Well Formed Program: In the second part various restrictions on the syntax are introduced in order to obtain well-formed programs satisfying the theoretical conditions for the completeness of the operational semantic