Declarative Logic Programming with Primitive Recursive Relations on Lists

In a previous paper we introduced a system of recursion operators for formulating pure logic programs, dispensing with explicit recursions. The recursion operators, some of which are similar to higher-order functions known from functional programming, take the form of quasi-higher order predicates. In this paper we identify a comprehensive class of logic programs called primitive recursive relations over lists (including primitive recursive functions) using the so called fold recursion operators. We formulate and prove a duality theorem connecting our relational fold operators. We show how correct well-moded procedural interpretations using any fixed computation rule can be obtained from a declarative logic program. This is accomplished in a principled manner by a simplified data flow analysis enabled by the recursion operator formulation and the duality theorem. The recursion operators are handled in ordinary clauses by means of established metalogic programming techniques.