Logic Programming

Elpi computes by reducing a query to smaller goals. What follows is when a rule applies to a goal, and what a rule means on its own. The surface syntax it refers to is the Syntax part of the manual, linked as it comes up. Elpi’s model is Prolog’s, rules and backtracking search, with λProlog’s treatment of syntax that contains binders layered on top.

Elpi vs Prolog

Elpi keeps Prolog’s core. Data is built from constructors, which in Elpi are declared and typed (Type declarations) rather than used freely as in Prolog. A program is a set of rules, each one a self-contained unit of meaning. And the search is backtracking: rules are tried in order, and when a goal fails the search retreats to the most recent still-open choice and takes its next alternative.

Where Elpi departs is in how a rule’s head meets the goal. Prolog unifies the two. Elpi unifies only a predicate’s output arguments and one-way matches the input ones: the head may inspect the goal but not instantiate a variable the goal left unbound. Which arguments are which is fixed by the signature (Type declarations); what the split is for is Constraints. This is the matching clauses idea of B-Prolog, marked per argument rather than per clause.

A head need not be linear: a variable may occur in it more than once, which forces the two positions to hold the same term:

pred symmetric tree.
symmetric leaf.
symmetric (node _ T T).

symmetric succeeds on a tree that is a leaf, or a node whose two children are the very same term; the repeated T in the second head is what ties them together. (It does not recurse, so it does not check that the children are themselves symmetric.)

Several rules may apply to one goal. Elpi tries them top to bottom and backtracks into the next on failure. The only control over this search is the cut, ! (Inference rules and queries), and Elpi’s is a hard cut: besides discarding the current rule’s untried alternatives, it also discards any alternative solutions still available for the premises already solved earlier in the same rule.

A rule is meaningful in isolation: adding one to a program, or taking one away, is a well-defined change, unlike an assignment or a function definition, which only mean something in a larger context. It is closer to adding or removing an axiom in a proof system. This is why the order in which rules are accumulated matters, why their relative order matters too once cut is in play, and why File structure and attributes gives a rule a name and a place among its siblings.

Elpi vs λProlog

λProlog adds binders. An object-language variable is represented directly by a bound variable of the programming language, a technique called Higher-Order Abstract Syntax, or λ-tree syntax. A simply-typed λ-calculus term is declared as

data tm.
symb app tm -> tm -> tm.
symb lam (tm -> tm) -> tm.

lam takes an Elpi function of type tm -> tm: the identity λx.x is written lam x\ x, and applying that function to a term substitutes the term for the bound x, with no substitution code to write. A bound variable like x is not a unification variable: it can never be assigned, only substituted for, and it is fresh, distinct from every other name in scope.

Type-checking this calculus needs one ingredient a Prolog rule cannot express on its own: a rule that holds only for the lifetime of one bound variable’s scope. pi introduces a fresh constant for the duration of a goal, and ==> adds a rule for the duration of a goal; together they give a bound variable exactly the context it needs. Types are declared like terms, with a constructor arr for the function space:

data ty.
symb arr ty -> ty -> ty.

pred of tm -> ty.
of (app H A) T :- of H (arr S T), of A S.
of (lam F) (arr S T) :- pi c\ of c S ==> of (F c) T.

To type-check lam F, the second rule introduces a fresh constant c for the bound variable, adds of c S for the rest of that goal only, and checks the body F c. The application rule is an ordinary Horn clause; the abstraction rule needs the ∀ and nested ⇒ of a Hereditary Harrop formula, the richer logic that λProlog, and so Elpi, is built on. A rule added by ==> is hypothetical: unlike Prolog’s assert / retract its scope is exactly the goal that added it, never the rest of the program (Inference rules and queries). The full checker, with weak-head reduction, is worked through in Simply-typed λ-calculus.

Run on a closed term, the checker infers a type without committing to what the bound variables stand for:

goal> Fst = (lam x\ lam y\ x), of Fst Ty.
Success:
  Fst = lam c0 \ lam c1 \ c0
  Ty = arr X0 (arr X1 X0)

This is as far as λProlog alone goes. Elpi is meant to type-check incomplete terms as well, the terms an interactive prover’s elaborator manipulates, still full of holes to be filled in. Ask the checker above for of X T with X an unknown hole and nothing useful happens: because the first argument of of is an input, no rule head matches a bare variable, and the goal simply fails. Made an output instead, the way plain λProlog with no modes would have it, the goal does worse: the first rule matches X against app H1 A1 for fresh H1, A1, then against app H2 A2 inside that, and so on without end. Neither outcome is what an elaborator needs. The way out is to suspend the goal on the hole until its shape is known instead of guessing, which is covered in Constraints.