The Semantics of Metapropramming in Prolog

TL;DR

This paper develops a formal semantics for pure Prolog programs with negation, including metaprograms and variable-headed clauses, using propositional models and ground instantiations to provide intuitive meaning.

Contribution

It introduces a novel semantics for Prolog that encompasses metaprogramming constructs and variable-headed clauses, extending traditional interpretations.

Findings

Provides a semantics for metaprograms in Prolog

Includes clauses with variables in heads, previously unsupported

Simplifies proofs of properties of metaprograms

Abstract

This paper describes a semantics for pure Prolog programs with negation that provides meaning to metaprograms. Metaprograms are programs that construct and use data structures as programs. In Prolog a primary mataprogramming construct is the use of a variable as a literal in the body of a clause. The traditional Prolog 3-line metainterpreter is another example of a metaprogram. The account given here also supplies a meaning for clauses that have a variable as head, even though most Prolog systems do not support such clauses. This semantics naturally includes such programs, giving them their intuitive meaning. Ideas from M. Denecker and his colleagues form the basis of this approach. The key idea is to notice that if we give meanings to all propositional programs and treat Prolog rules with variables as the set of their ground instances, then we can give meanings to all programs. We must treat Prolog rules (which may be metarules) as templates for generating ground propositional rules, and not as first-order formulas, which they may not be. We use parameterized inductive definitions to give propositional models to Prolog programs, in which the propositions are expressions. Then the set of expressions of a propositional model determine a first-order Herbrand Model, providing a first-order logical semantics for all (pure) Prolog programs, including metaprograms. We give examples to show the applicability of this theory. We also demonstrate how this theory makes proofs of some important properties of metaprograms very straightforward.