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 modules are very similar to their
rationals counterparts, we will limit ourselves to outlining the
differences.
The signature introduced by equality/integers is roughly the same
as 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 module 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.
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.