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.
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 thatA
has exactly one solution %query 1 1 A. % check thatA
has at least one solution %query * 3 A. %A
has infinitely many solutions, check 3 %query * * A. % fails ifA
has finitely many solutions %query 1 0 A. % skip this query
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 8.5 Proof Realizations.
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
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
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.
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
.
?- 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
.
?- {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.
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. % usetp_lam
withE = ([x:exp] x)
andT = arrow T1 T2
% subgoal ?- {x:exp} of x T1 -> of x T2. % introduce parametere
?- of e T1 -> of e T2. % introduce hypothesis labelledp
p:of e T1 ?- of e T2. % succeed by hypothesisp
withT1 = 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. % usetp_lam
withT = arrow T1 T2
% subgoal ?- {x:exp} of x T1 -> of (app x x) T2. % introduce parametere
?- of e T1 -> of (app e e) T2. % introduce hypothesisp:of a T1
p:of e T1 ?- of (app e e) T2. % usetp_app
% first subgoal ?- of e (arrow T3 T2). % succeed by hypothesisp
withT1 = arrow T3 T2
% second subgoal ?- of e T3. % fail, sinceT3 = 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.