Go to the first, previous, next, last section, table of contents.

5 Logic Programming

Twelf gives an operational interpretation to signatures under the computation-as-proof-search paradigm. The fundamental idea is to fix a simple search strategy and then search for a derivation of a query according to this strategy. The result may be a substitution for the free variables in a query and a derivation, or explicit failure. It is also possible that the computation does not terminate.

A query can be posed in three different ways: as a %query declaration, as a %solve declaration, or interactively, using a top-level invoked from ML with Twelf.top which prompts with `?-' (see section 5.3 Interactive Queries). 

query ::= id : term   % X : A, X a free variable
        | term        % A

bound ::= nat         % number of solutions
        | *           % unbounded number

qdecl ::= bound bound query % expected solutions, try limit, query

decl ::= ...
       | %query qdecl.      % execute query
       | %solve id : term.  % solve and name proof term

In all of these cases, the free variables in a query are interpreted existentially, which is in contrast to constant declarations where free variables are interpreted universally. In particular, free variables might be instantiated during type reconstruction and during execution of the query.

5.1 Query Declaration

The query form 

%query expected try A.

will try to solve the query A and verify that it gives the expected number of solutions, but it will never try to find more than indicated by try. It succeeds and prints a message, whose precise form depends on the value of Twelf.chatter if A has the expected number of solutions; otherwise it either fails with an error message or does not terminate. `%query' has no other effect on the state of Twelf. Here are some examples. 

%query 1 * A.      % check that A has exactly one solution
%query 1 1 A.      % check that A has at least one solution
%query * 3 A.      % A has infinitely many solutions, check 3
%query * * A.      % fails if A has finitely many solutions
%query 1 0 A.      % skip this query

5.2 Solve Declaration

The query form 

%solve c : A.

will search for the first solution M of A and then define 

c : A = M.

If there are any free variables remaining in M or A after search, they will be implicitly quantified in the new definition. This form of definition is particularly useful to compute and name inputs to future queries. An example of this feature from the file `examples/nd/lam.elf' can be found in section 9.5 Proof Realizations.

5.3 Interactive Queries

An interactive top-level can be invoked using the SML expression Twelf.top ();. The top-level prompts with `?- ' and awaits the input of a query, terminated by a period `.' and a RET.

After the query has been parsed, Twelf reconstructs implicit type information, issuing a warning if constraints remain. The result is executed as a query. At any point during the processing of a query the user may interrupt with C-c (that is, CTRL and c) to drop back into ML's interactive top-level.

When Twelf has found a solution, it prints the answer substitution for all free variables in the query, including the proof term variable if one was given. It also notes if there are remaining equational constraints, but currently does not print them.

The top-level then waits for input, which is interpreted as follows

y, Y, or ;
backtrack and search for another solution
q or Q
quit Twelf's top-level and return to ML
n, N, or anything else
return to prompt for another query

5.4 Sample Trace

As an example we consider lists of propositions and some simple operations on them, as they might be used when programming a theorem prover. 

list : type.
nil  : list.
cons : o -> list -> list.

First, we want to write a program to append two lists to obtain their concatenation. This is expressed as a relation between the three lists, which in turn is implemented as a type family 

append  : list -> list -> list -> type.

appNil  : append nil K K.
appCons : append (cons X L) K (cons X M)
           <- append L K M.

Here, we use the synonym A <- B for B -> A to improve readability. We say A if B.

The first sample query concatenates the singleton lists containing true and false. We proceed as if we had loaded the appropriate files and started a top-level with Twelf.top ();. 

?- append (cons true nil) (cons false nil) L.

Here, L is a free existential variable. We search for an object M : append (cons true nil) (cons false nil) L, even though this object will not be shown in this form or query. Each constant declaration in the signature is tried in turn, unifying the head with the goal above. In this manner, we obtain the following sequence of goals and actions. Note that the intermediate forms and comments are not printed when this is run. They are added here to illustrate the behavior. 

% original goal after parsing and type reconstruction
?- append (cons true nil) (cons false nil) L.
[try appNil:
     append nil K1 K1
   = append (cons true nil) (cons false nil) L
 unification fails with constant clash: nil <> cons
]
[try appCons:
     append (cons X1 L1) K2 (cons X1 M1)
   = append (cons true nil) (cons false nil) L
 unification succeeds with
 X1 = true, L1 = nil, K2 = cons false nil, L = cons true M1
]
% subgoal
?- append nil (cons false nil) M1.
[try appNil:
     append nil K3 K3
   = append nil (cons false nil) M1
 unification and subgoal succeeds with
 K3 = cons false nil, M1 = cons false nil
]

At this point the overall goal succeeds and we read off the answer substitution for the only free variable in the query, namely L. It was first determined to be cons true M1 and then M1 was instantiated to cons false nil, leading to the instantiation 

L = cons true (cons false nil).

If instead we pose the query 

?- X : append (cons true nil) (cons false nil) L.

we also obtain the proof term 

L = cons true (cons false nil);
X = appCons appNil.

As another example we consider a query with several solutions which are enumerated when we ask for further results. This time we do not trace the steps of the execution, but show the interaction verbatim. 

?- append L K (cons true (cons false nil)).
Solving...
K = cons true (cons false nil);
L = nil.
More? y
K = cons false nil;
L = cons true nil.
More? y
K = nil;
L = cons true (cons false nil).
More? y
No more solutions

5.5 Operational Semantics

The operational semantics of Twelf is a form of typed constraint logic programming. We will use standard terminology from this area. A type family which is used in a program or goal is called a predicate. A constant declaration in a signature which is available during search is called a clause. A clause typically has the form c : a M1 ... Mm <- A1 <- ... <- An, where a M1 ... Mm is the head of the clause and A1 through An are the subgoals. A clause is used to reduce a goal to subgoals by a process called backchaining. Backchaining unifies the head of the clause with the current goal to generate subgoals. Next, we select one of the subgoals as a current goal and continue the search process. Actually, instead of unification (which is undecidable in LF), Twelf employs constraint simplification and carries along equational constraints in a normal form.

A hypothesis which is introduced during search is a local assumption; a parameter is a local parameter. Parameters act like constants in unification, except that their occurrences might be restricted due to parameter dependency.

Without going into a formal description, here are the central ideas of the operational semantics.

Clause selection.
The clauses are tried in the following order: from most recent to least recent local assumption, then from first to last clause in the global signature.
Subgoal selection.
Subgoals are solved from the inside out. For example, when a clause c : A <- B <- C. is applied to solve the goal ?- A. then the first subgoal is B and the second subgoal C. Truly dependent variables will only be subject to unification and never give rise to a subgoal. For example c : {X:b} a X <- a c is a clause with head a X, subgoal a c, and existential variable X.
Unification.
An atomic goal is unified with the clause head using higher-order pattern unification. All equations outside this fragment are postponed and carried along as constraints.
Local assumptions.
A goal of the form ?- A -> B. introduces a local assumption A and then solves B under this assumption. To solve atomic goals, local assumptions are tried before global clauses, using the most recently made assumption first. Note that this is different from Prolog assert in that A is available only for solving B.
Local parameters.
Parameters are introduced into proof search by goals of the form ?- {x:A} B. which generates a new parameter a and then solves the result of substituting a for x in B. Parameters are also called universal variables since they are not subject to instantiation during unification. Local parameters will never be used as local assumptions during search.

5.6 Sample Program

As an example, we consider simple type inference for the pure lambda-calculus. An extension of this example to Mini-ML is given in the course notes Pfenning 1992, Computation and Deduction. The code below can be found in the file `examples/guide/lam.elf'. 

% Simple types
tp : type.                              %name tp T.

arrow : tp -> tp -> tp.                 % T1 => T2

% Expressions
exp : type.                             %name exp E.

lam   : (exp -> exp) -> exp.            % lam x. E
app   : exp -> exp -> exp.              % (E1 E2)

% Type inference 
% |- E : T  (expression E has type T)

of : exp -> tp -> type.                 %name of P.

tp_lam : of (lam E) (arrow T1 T2)       % |- lam x. E : T1 => T2
          <- ({x:exp}                   % if  x:T1 |- E : T2.
                of x T1 -> of (E x) T2).

tp_app : of (app E1 E2) T1              % |- E1 E2 : T1
          <- of E1 (arrow T2 T1)        % if  |- E1 : T2 => T1
          <- of E2 T2.                  % and |- E2 : T2.

Again, we have used the notation A <- B to emphasize the interpretation of constant declarations as clauses. We now trace the query which infers the most general type of the identity function, represented as lam [x:exp] x. We indicate the scope of hypotheses which are introduced during search by indentation. 

% original query, T free
?- of (lam [x:exp] x) T.
% use tp_lam with E = ([x:exp] x) and T = arrow T1 T2
% subgoal
?- {x:exp} of x T1 -> of x T2.
% introduce parameter e
?- of e T1 -> of e T2.
% introduce hypothesis labelled p
p:of e T1
 ?- of e T2.
 % succeed by hypothesis p with T1 = T2

At this point the query succeeds and prints the answer substitution. 

T = arrow T1 T1.
More? y
No more solutions

We requested more solution by typing y, but there are no further possibilities. The free variable T1 in the answer substitution means that every instance of arrow T1 T1 provides a solution to the original query. In other words, lam [x:exp] x has type arrow T1 T1 for all types T1.

As a second example we verify that self-application is not well-typed in the simply-typed lambda-calculus. 

?- of (lam [x:exp] app x x) T.
% use tp_lam with T = arrow T1 T2
% subgoal
?- {x:exp} of x T1 -> of (app x x) T2.
% introduce parameter e
?- of e T1 -> of (app e e) T2.
% introduce hypothesis p:of a T1
p:of e T1
 ?- of (app e e) T2.
 % use tp_app
 % first subgoal
 ?- of e (arrow T3 T2).
 % succeed by hypothesis p with T1 = arrow T3 T2
 % second subgoal
 ?- of e T3.
 % fail, since T3 = arrow T3 T2 has no solution

At the point where the second subgoals fails we backtrack. However, all other alternatives fail immediately, since the clause head does not unify with the goal and the overall query fails.

Go to the first, previous, next, last section, table of contents.