Constraints-based extensions are highly experimental and under active development. Use of extensions other than the ones pertaining rational arithmetic is strongly discouraged. We refer to extension by constraint domains as Twelf(X), where X refers different domains.
Twelf(X) extensions allow Twelf to deal more efficiently with some specific domains (e.g. numbers). They do so by
Extensions are installed using the declaration
%use extension name
For example,
%use equality/rationals.
loads the extension dealing with equality over the rationals. Typically,
an extension introduces new symbols in the signature. For example,
equality/rationals adds a type for rational numbers:
rational : type.
In addition to these symbols, a countably infinite set of "special"
ones may be also accepted by the system as the result of loading one
extension. In our example, after loading equality/rationals the
symbols
135 5/13 ~1/4
become valid constants of type rational.
Finally, it is possible for an extension to be built on top of others,
and therefore to depend on them. Hence, loading an extension usually
causes all the others it depends upon to be loaded as well, if they have
not been already. For example, the extension inequality/rationals
requires equality/rationals, and hence the declaration
%use inequality/rationals.
subsumes
%use equality/rationals.
Extensions must be installed prior to their use. For this reason, it is
a safe practice to put all the %use declarations at the
beginning of the program.
As mentioned before, the extension presiding equality over the rational
numbers is called equality/rationals, and it is therefore installed
by the declaration
%use equality/rationals.
This causes the declarations
rational : type. ~ : rational -> rational. %prefix 9999 ~. + : rational -> rational -> rational. %infix left 9997 +. - : rational -> rational -> rational. %infix left 9997 -. * : rational -> rational -> rational. %infix left 9998 *.
to be included in the current global signature.
Note that We do not add an equality predicate for rationals. This is unnecessary, since the extension modifies standard type checking so that arithmetic identities are taken into account. However, one can always define an equality predicate by declaring
== : rational -> rational -> type. %infix none 100 ==.
id : X == X.
This extension is also responsible for defining special constants for all the rational numbers. These follow the syntax
<rational> ::= ~<unsigned> | <unsigned>
<unsigned> ::= <digits> | <digits>/<digits>
<digits> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
| <digits> <digits>
It is important to notice the difference between ~ 10 and
~10. The former is the object obtained applying the unary minus
operator to the positive number 10; the second stands for the number
-10. The difference is, however, just syntactical, since the former
is automatically evaluated into the latter by Twelf(X). In general, one
should keep in mind that Twelf(X) extensions do not modify the behavior
of the lexer; hence, for example, multiplication of a variable X
by two still needs to be written as X * 2 (note the spaces
preceding and following the multiplication symbol), while X*2
will be interpreted by the system as a single variable named
"X*2".
Unification of arithmetic expressions is done by Gaussian elimination. Thus, unification problems that can be reduced to linear equations over existentially quantified variables are immediately solved; other problems not falling in this class are likely to be delayed as unificational constraints.
Arithmetical inequalities are handled by the extension
inequality/rationals. This relies on equality/rationals
for the definition of rational number, so a declaration of
%use inequality/rationals.
implicitly entails one of
%use equality/rationals.
This extension adds the following to the signature:
> : rational -> rational -> type. %infix none 0 >.
>= : rational -> rational -> type. %infix none 0 >=.
+> : {Z:rational} X > Y -> (X + Z) > (Y + Z).
+>= : {Z:rational} X >= Y -> (X + Z) >= (Y + Z).
>>= : X > Y -> X >= Y.
0>=0 : 0 >= 0.
It also adds countably many proof objects such as
45>0 : 45 > 0.
witnessing that positive numbers are greater than zero.
Goals of the form
M > N or M >= N
are evaluated using a modified version of the simplex algorithm, rather than the usual proof-search mechanism. This will incrementally collect inequalities, assigning them incomplete (i.e. partially instantiated) proof objects, until either an inconsistency is discovered (generating failure) or they can be shown to be satisfied a unique solution (causing the proof objects to be finally completed).
The extensions equality/integers and inequality/integers
deal with equalities and inequalities over the ring of integer numbers,
respectively. Since these two extensions are very similar to their
rationals counterparts, we will limit ourselves to outlining the
differences.
The signature introduced by equality/integers resembles
equality/rationals. The only difference lies in the name of
the main type:
integer : type. ~ : integer -> integer. %prefix 9999 ~. + : integer -> integer -> integer. %infix left 9997 +. - : integer -> integer -> integer. %infix left 9997 -. * : integer -> integer -> integer. %infix left 9998 *.
Like before, countably many special constants are added to the signature. They follow the syntax
<integer> ::= ~<digits> | <digits>
The extension equality/integers takes advantage of the fact that (unlike the rationals) the integers are not a dense ordering to considerably shorten the set of symbols needed:
>= : integer -> integer -> type. %infix none 0 >=.
+>= : {Z:integer} X >= Y -> (X + Z) >= (Y + Z).
It also declares countably many proof objects such as
37>=0 : 37 >= 0.
for all non-negative integers.
Notice that strict inequality > can be easily defined in this case:
> : integer -> integer -> type. %infix none 0 >. >=> : X >= (Y + 1) -> X > Y.
For solving linear inequalities over the integers, we again use the simplex method, but we add special routines that implement branch-and-bound search. Specifically, inequalities are internally interpreted over rationals, and a check is performed regularly (whenever a new inequality is added) to ensure the rational solution space contains integral points.
Note that all known methods for solving systems of integral linear
inequations are notoriously inefficient. In the branch-and-bound method
we adopted, the number of branches to consider is potentially
exponential with respect to the size of the problem. We recommend using
the inequality/rationals extension instead, whenever the situation
allows the two to be used interchangeably.
A third domain currently supported by the Twelf(X) extensions are strings of (printable) characters. The only operator provided is string concatenation. Installing
%use equality/strings.
causes the following signature to be loaded:
string : type. ++ : string -> string -> string. %infix right ++ 9999.
String constants are sequences of printable characters enclosed by double quotes:
"foobar" : string
Under these conventions, strings cannot therefore contain the double
quote character ". Escape sequences, such as "\n" have no
special meaning; moreover, we do not currently provide input/output
primitives.
Finally, it is required that string constants occupy a single line. The declaration
mystring : string = "foo
bar".
is not considered syntactically correct.
Another supported domain are 32-bit integers. This domain is used mainly in Proof Carrying Code applications, and because of this, it has fairly different structure and features than the extension for (unrestricted) integers (see section 6.4 Integer Constraints). First of all, the algorithms used were kept short and simple, so that they can be easily read and verified to be correct. Secondly, the set of arithmetic operators provided has been kept to a minimum. Also, each of these is implemented as a type family instead of a function symbol, so that unification of arithmetic expressions follows the same rule as that of regular terms. Finally, for each arithmetic operator, we also provide a type family which, in addition to carry out the computation, also provides a proof object for it.
Declaring
%uses word32.
causes the following signature to be loaded into the system:
word32 : type.
+ : word32 -> word32 -> word32 -> type.
* : word32 -> word32 -> word32 -> type.
/ : word32 -> word32 -> word32 -> type.
prove+ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} type.
proof+ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} prove+ X Y Z P.
prove* : {X:word32} {Y:word32} {Z:word32} {P:* X Y Z} type.
proof* : {X:word32} {Y:word32} {Z:word32} {P:* X Y Z} prove* X Y Z P.
prove/ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} type.
proof/ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} prove/ X Y Z P.
Goals involving + and * are immediately solved if at least
two of the arguments are ground objects (i.e. numbers), and delayed as
constraints otherwise. In particular
?- + 3 X 9.
is solved immediately and can be used to compute 9-3.
Goals involving / are delayed unless both the first and the second
argument are known. The type families prove+, prove*,
prove/ can be used to obtain proof object for the arithmetic
operation, and use them in the remaining part of the computation:
?- P : + 3 X 9. Solving... X = 6. P = 3+6. More? n ?- prove+ 3 X 9 P. Solving... P = 3+6; X = 6. More? n
It is important to stress that the domain modeled here is not the ring of integers modulo 32 but rather the restriction of the integer ring to the interval 0...4294967295, so that for example the query:
?- + 1 X 0.
will not admit a solution.
Using Twelf(X), we can write a modified version of append that
takes into account the size of the list involved:
%use equality/rationals.
item : type.
list : rational -> type.
a : type.
b : type.
...
nil : list 0.
cons : item -> list N -> list (N + 1).
append : list M -> list N -> list (M + N).
append_nil : append nil L L.
append_cons : append (cons X L1) L2 (cons X L3)
<- append L1 L2 L3.
Type checking the definition of append requires some algebraic manipulation. For example, validity of append_nil depends on the identity
0+M=M.
Most classic Constraint Logic Programming (CLP) examples found in the literature can be easily translated to Twelf(X). We present here a simple mortgage calculator:
%use inequality/rationals.
%% equality
== : rational -> rational -> type. %infix none 1000 ==.
id : X == X.
%% mortgage payments
mortgage : rational -> rational -> rational
-> rational -> rational -> type.
m0 : mortgage P T I MP B
<- T > 0
<- 1 >= T
<- Interest == T * P * I * 1/1200
<- B == P + Interest - (T * MP).
m1 : mortgage P T I MP B
<- T > 1
<- MI == P * I * 1/1200
<- mortgage (P + MI - MP) (T - 1) I MP B.
This CLP program takes four parameters: the principal P, the life
of the mortgage in months T, the annual interest rate (%)
I, the monthly payment MP, and the outstanding balance
B.
Finally, we use the string extensions to write a simple parser. Consider the following syntax for simple arithmetic expressions:
<expr> ::= <number> | <expr>+<expr>
| <expr>-<expr>
| <expr>*<expr>
| (<expr>)
<number> ::= <digit> | <digit><number>
<digit> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
This can be translated quite directly into Twelf by constructing parsing
predicates digit, number, expression as follows:
digit : string -> type.
d0 : digit "0".
d1 : digit "1".
d2 : digit "2".
d3 : digit "3".
d4 : digit "4".
d5 : digit "5".
d6 : digit "6".
d7 : digit "7".
d8 : digit "8".
d9 : digit "9".
number : string -> type.
nd : number X
<- digit X.
n++ : number (X ++ Y)
<- digit X
<- number Y.
expression : string -> type.
en : expression X
<- number X.
e* : expression (X ++ "*" ++ Y)
<- expression X
<- expression Y.
e+ : expression (X ++ "+" ++ Y)
<- expression X
<- expression Y.
e- : expression (X ++ "-" ++ Y)
<- expression X
<- expression Y.
ep : expression ("(" ++ X ++ ")")
<- expression X.
To ensure the consistency of the calculus, use of types defined by Twelf(X) extensions is restricted. Specifically, we do not allow them to be used as dynamic assumptions. This rules out meaningless (under the current operating semantics) goals like
?- 0 > 1 -> foo.
as well as meaningful, but intractable ones, such as
?- {X : rational} X * X >= 0
One important thing to keep in mind when using arithmetic is that this
currently is defined over the rationals, rather than the integers or the
set of natural numbers. While in many applications this is of no
consequence, it might generate in some cases surprising results. While
it is certainly possible to define the characteristic function of the
integer subset (see the content of clp-examples/integers/ in the
distribution) and use this to enforce all computations to take place in
the intended domains, this introduces a big performance penalty and
should in general be avoided.
Go to the first, previous, next, last section, table of contents.