Abstract: 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 (depthfirst search) procedural reading of Prolog. They also hold for alternative search strategies, e.g. breadthfirst 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.
This one of those fun things, where you conenct two different languages together (see the SILK paper below for another example).
This time you also win an example of functional programming in Haskell, as well as some proofs about logic programming.
Posted to theory by Ehud Lamm on 2/9/01; 4:29:43 AM
