Inference rules and queries

A program is a sequence of rules and directives (data, symb, pred, accumulate, namespace { … }, …). What follows is the syntax of a rule, of the goals that make up a rule’s body, and of the queries run against a program. The rules here are the program’s inference rules: they are what the proof search chains together. The constraint handling rules that act on suspended goals are a separate construct with a syntax of their own (Constraint handling rules).

Rules

A rule is either a bare atom, called a fact, or an atom followed by :- and a body, called a conditional rule. Either way it ends with a full stop:

age alice 20.                              % a fact
older P Q :- age P N, age Q M, N > M.      % a conditional rule

The head is an application p t1 … tn (or just p). A conditional rule reads “the head holds if the body holds”. A rule’s variables are universally quantified over the whole rule, and every use of the rule gets a fresh set of them, so the fact same-two [T, T]. holds for any T, a different T on each call.

Several rules for the same predicate are alternatives. The search tries them in source order and backtracks into the next one whenever a later goal fails. That order can be adjusted with attributes (see below).

Goals

The body of a rule, and a query, are goals. A goal is one of:

• an atom, p t1 … tn: a call;

• g1, g2: conjunction (& is an accepted synonym, and a list [g1, g2, g3] also means g1, g2, g3);

• g1 ; g2: disjunction;

• H ==> g: solve g with the extra rule H added to the program for the duration of g; [H1, H2] ==> g adds several, and is read H2 ==> (H1 ==> g) so that H1 is the one tried first. =!=> is ==> with a cut automatically appended to H’s body (Committing a hypothetical rule, below);

• pi x\ g: solve g with a fresh constant standing for x; sigma X\ g uses a fresh unification variable instead (Binders and HOAS);

• !: cut (Control and cut).

=> is the traditional λProlog spelling of the same implication as ==>. The two differ only in precedence. ==> binds looser than ,, so a, b ==> c, d reads a, (b ==> (c, d)); => binds tighter, so a, b => c, d reads a, (b => c), d, which makes b available to c but not to d. That is usually a mistake, and Elpi prints a warning when a => appears as a non-final conjunct like this. This manual writes ==> throughout.

Because \ extends its body as far right as possible, a pi or sigma inside a conjunction swallows the goals after it: a, pi x\ b, c means a, (pi x\ (b, c)). Parenthesise the binder to keep a later goal out of the fresh constant’s scope.

../code/pi-scope.elpi:

% `pi x\ …` extends its body as far right as possible, so inside a conjunction
% it swallows the goals that follow it. Parenthesise the binder to keep a later
% goal out of the fresh constant's scope.

pred count-names string.
count-names Where :- names Ns, std.length Ns N, print Where "sees" N "name(s)".

main :-
  ( pi x\ count-names "inside" ) ,   % without the ( ) the next line is inside too
  count-names "after".

inside sees 1 name(s)
after sees 0 name(s)

Committing a hypothetical rule

H =!=> G adds H for the duration of G with a cut appended to its body: a rule head :- body becomes head :- body, !, and a bare fact head becomes head :- !. Once H yields its first solution the cut fires, so G finds no choice point to backtrack into and no later rule of the same predicate is tried. When H is a term the compiler can see it appends the cut up front; when H is only known at run time (a variable bound to a rule computed on the fly) the cut is appended dynamically, as the rule is added.

The use for it is a func predicate handed an extra rule at run time. The static rule copy X X alone lets copy a Z answer Z = a; adding copy a b beside it creates a second solution, and the determinacy checker (Determinacy checking) rejects the func for that choice point. =!=> removes it, so the program compiles and copy a Z has the single solution copy a b:

../code/tail-cut.elpi:

% =!=> adds a hard cut to the tail of a hypothetical rule. Here `copy a b` is
% added while the rest of main runs; the cut means a later `copy a Z` commits
% to Z = b and does not also backtrack into the static rule `copy X X` (which
% would give Z = a). std.findall collects every solution and finds just one.
%
% With plain ==> this program would not compile: `copy` is a func, and adding
% `copy a b` next to the static rule is flagged as "mutual exclusion
% violated" -- exactly the choice point =!=> removes.

data tm.
symb a tm.
symb b tm.

func copy tm -> tm.
copy X X.

main :-
  copy a b =!=> std.findall (copy a Z_) Sols,
  print "solutions of copy a:" Sols.

solutions of copy a: [copy a b]

Naming a subterm of the head

A rule head can name a subterm with (t as N) (Terms), so the body refers to it without spelling it out again. In a head, as may wrap an argument or a piece of one, but not the head as a whole:

whd (lam F as T) T. % a lambda is already in weak head normal form

Attributes

An attribute is written :-prefixed before the rule and may sit on its own line:

:name "step" :if "DEBUG"
step X :- ...

:name, :before, :after, :replace and :remove graft the rule among its predicate’s alternatives; :if keeps it only when a compiler variable is defined; :untyped exempts it from the type checker. All of them are described in Rule attributes. Attributes that describe the predicate instead (:index, :functional and the like) go on the pred / func signature (Type declarations).

Queries

A query is a goal run against a program:

• elpi prog.elpi -test runs the goal main;

• elpi prog.elpi -exec p -- a b c runs p ["a", "b", "c"] (the predicate receives a single list string);

• elpi prog.elpi with a goal typed or piped on standard input opens a goal> prompt, reads one goal, prints the value bound to each of its unification variables in the first solution, then asks whether to look for another;

• from a host application, through the OCaml API (Embedding and extending Elpi).

?- is not a query prefix in Elpi, as it is in some Prolog systems; it is the sequent separator used in constraint blocks and CHR rules (Constraint handling rules).

Facts, conditional rules and a query together:

../code/rules.elpi:

% Rules and queries — a small sample.

data person.
symb alice, bob, carol person.

pred parent -> person, person.        % two facts
parent alice bob.
parent bob carol.

pred ancestor -> person, person.      % two rules
ancestor X Y :- parent X Y.
ancestor X Y :- parent X Z, ancestor Z Y.

main :-
  std.findall (ancestor alice _) All,   % the query: every Y with `ancestor alice Y`
  std.length All N,
  print "alice has" N "descendants".

alice has 2 descendants