Language.DefinitionTree

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).

Documentation

type VStack = [Int]

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 LogicVar term = (Int, VStack)

type Subst term = Map (LogicVar term) term

A finite map from vars to terms (parameterized over the domain of terms)

data Formula term

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

Constructors

Fail

(Clause term) :+: (Formula term)

data Clause term

A clause is a guarded body; the latter is an AND-sequence of formulas

Constructors

G (Subst term) (Body term)

data Body term

Constructors

Fact

(Formula term) :*: (Body term)

prune :: Unifiable term => Formula term -> Subst term -> Formula term

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

prunec :: Unifiable term => Clause term -> Subst term -> Maybe (Clause term)

eval :: Unifiable term => Formula term -> Subst term -> [Subst term]

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]

Same as above, using the SLD-interleaving strategy. See Definition 3.1 of the LogicT paper (ICFP05)

class Unifiable term where

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

Methods

classify :: term -> Either (LogicVar term) (Int, [term])

build :: (Int, [term]) -> term

Instances

Unifiable UN

Constructor UZ is represented by 0, and US is represented by 1

bv :: LogicVar term -> term -> Subst term

building substitutions

ins :: Subst term -> (LogicVar term, term) -> Subst term

sapp :: Unifiable term => Subst term -> term -> term

Apply a substitution to a term

unify :: Unifiable term => Subst term -> Subst term -> Maybe (Subst term)

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)

Solve the equations using the naive realization of the Martelli and Montanari process

data UN

Unary numerals

Constructors

UNv (LogicVar UN)

UZ

US UN

Instances

Eq UN

Show UN

Unifiable UN

Constructor UZ is represented by 0, and US is represented by 1

genu :: Formula UN

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.

add :: VStack -> Formula UN

mul :: VStack -> Formula UN