Embedding Prolog in Haskell
Silvija Seres and Michael Spivey
The distinctive merit of the declarative reading of logic
programs is the validity of all the laws of reasoning
supplied by the predicate calculus with
equality. Surprisingly many of these laws are still valid
for the procedural reading; they can therefore be used
safely for algebraic manipulation, program transformation
and optimisation of executable logic programs.
This paper lists a number of common laws, and proves their
validity for the standard (depth-first search) procedural
reading of Prolog. They also hold for alternative
search strategies, e.g.~breadth-first search. Our proofs
of the laws are based on the standard algebra of
functional programming, after the strategies have been
given a rather simple implementation in Haskell.