A model of the evaluation of logic programs (i.e., resolving Horn clauses)
The point is not to re-implement Prolog with all the conveniences but to formalize evaluation strategies such as SLD, SLD-interleaving, and others. The formalization is aimed at reasoning about termination and solution sequences. See App A and B of the full FLOPS 2008 paper (the file arithm.pdf in this directory).
- type VStack = [Int]
- type LogicVar term = (Int, VStack)
- type Subst term = Map (LogicVar term) term
- data Formula term
- data Clause term = G (Subst term) (Body term)
- data Body term
- prune :: Unifiable term => Formula term -> Subst term -> Formula term
- prunec :: Unifiable term => Clause term -> Subst term -> Maybe (Clause term)
- eval :: Unifiable term => Formula term -> Subst term -> [Subst term]
- evali :: Unifiable term => Formula term -> Subst term -> [Subst term]
- class Unifiable term where
- bv :: LogicVar term -> term -> Subst term
- ins :: Subst term -> (LogicVar term, term) -> Subst term
- sapp :: Unifiable term => Subst term -> term -> term
- unify :: Unifiable term => Subst term -> Subst term -> Maybe (Subst term)
- solve :: Unifiable term => Subst term -> [(Either (LogicVar term) term, term)] -> Maybe (Subst term)
- data UN
- genu :: Formula UN
- add :: VStack -> Formula UN
- mul :: VStack -> Formula UN
Documentation
A logic var is represented by a pair of an integer
and a list of `predicate marks' (which are themselves
integers). Such an odd representation is needed to
ensure the standardization apart: different instances
of a clause must have distinctly renamed variables.
Unlike Claessen, we get by without the state monad
to generate unique variable names (labels). See the
discussion and examples in the tests
section below.
Our main advantage is that we separate the naming of
variables from the evaluation strategy. Evaluation
no longer cares about generating fresh names, which
notably simplifies the analysis of the strategies.
Logic vars are typed, albeit phantomly.
type Subst term = Map (LogicVar term) termSource
A finite map from vars to terms (parameterized over the domain of terms)
Formulas
A formula describes a finite or _infinite_ AND-OR tree that encodes the logic-program clauses that may be needed to evaluate a particular goal. We represent a goal g(t1,...,tn) by a combination of the goal g(X1,...,Xn), whose arguments are distinct fresh logic variables, and a substitution {Xi=ti}. For a goal g(X1,...,Xn), a |Formula| encodes all the clauses of the logic program that could possibly prove g, in their order. Each clause
g(t1,...,tn) :- b1(t11,...,t1m), ...
is represented by the (guarding) substitution {Xi=ti, Ykj=tkj} and the sequence of the goals bk(Yk1,...,Ykm) in the body. Each of these goals is again encoded as a |Formula|. All variables in the clauses are renamed to ensure the standardization apart.
Our trees are similar to Antoy's definitional trees, used to encode rewriting rules and represent control strategies in term-rewriting systems and _functional logic_ programming. However, in definitional trees, function calls can be nested, and patterns are linear.
The translation from Prolog is straightforward; the first step is to re-write clauses so that the arguments of each goal are logic variables: A fact
g(term).
is converted to
g(X) :- X = term.
A clause
g(term) :- g1(term1), g2(term2).
is converted to
g(X) :- X = term, _V1 = term1, g1(_V1), _V2=term2, g2(_V2).
See the real examples at the end
A formula (parameterized by the domain of terms) is an OR-sequence of clauses
A clause is a guarded body; the latter is an AND-sequence of formulas
prune :: Unifiable term => Formula term -> Subst term -> Formula termSource
The evaluation process starts with a formula and the initial
substitution, which together represent a goal. The
guarding substitution of the clause conjoins with the current
substitution to yield the substitution for the evaluation of the body.
The conjunction of substitutions may lead to a contradiction,
in which case the clause is skipped (pruned
).
Evaluation as pruning: we traverse a tree and prune away failed branches
eval :: Unifiable term => Formula term -> Subst term -> [Subst term]Source
A different evaluator: Evaluate a tree to a stream (lazy list) given the initial substitution s. Here we use the SLD strategy.
evali :: Unifiable term => Formula term -> Subst term -> [Subst term]Source
Same as above, using the SLD-interleaving strategy. See Definition 3.1 of the LogicT paper (ICFP05)
class Unifiable term whereSource
Evaluation, substitutions and unification are parametric over terms (term algebra), provided the following two operations are defined. We should be able to examine a term and determine if it is a variable or a constructor (represented by an integer) applied to a sequence of zero or more terms. Conversely, given a constructor (represented by an integer) and a list of terms-children we should be able to build a term. The two operations must satisfy the laws:
either id build . classify === id classify . build === Right
unify :: Unifiable term => Subst term -> Subst term -> Maybe (Subst term)Source
Conjoin two substitutions (see Defn 1 of the FLOPS 2008 paper). We merge two substitutions and solve the resulting set of equations, returning Nothing if the two original substitutions are contradictory.
solve :: Unifiable term => Subst term -> [(Either (LogicVar term) term, term)] -> Maybe (Subst term)Source
Solve the equations using the naive realization of the Martelli and Montanari process
Unary numerals
Encoding of variable names to ensure standardization apart.
A clause such as genu(X) or add(X,Y,Z) may appear in the tree
(infinitely) many times. We must ensure that each instance uses distinct
logic variables. To this end, we name variables by a pair (Int, VStack)
whose first component is the local label of a variable within a clause.
VStack is a path from the root of the tree to the current occurrence
of the clause in the tree. Each predicate along the path is represented
by an integer label (0 for genu, 1 for add, 2 for mul, etc).
To pass
arguments to a clause, we add to the current substitution
the bindings for the variables of that clause. See the genu' example
below: whereas (0,h) is the label of the variable X in the current
instance of genu, (0,genu_mark:h) is X in the callee.
A logic program
genu([]). genu([u|X]) :- genu(X).
and the goal genu(X) are encoded as follows. The argument of genu' is the path of the current instance of genu' from the top of the AND-OR tree.