# 6 Constraint Domains

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

1. modifying type reconstruction to accommodate other equivalences beyond those entailed by traditional beta-eta-conversion;
2. defining special types, on which proof search is performed using ad-hoc decision procedures rather than traditional depth-first strategy;
3. adding countably many new symbols to the language, signifying all the elements of the domain.

## 6.1 Installing an Extension

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.

## 6.2 Equalities over Rational Numbers

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.

## 6.3 Inequalities over Rational Numbers

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).

## 6.4 Integer Constraints

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.

## 6.5 Equalities over Strings

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.

## 6.6 32-bit Integers

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.
```

## 6.7 Sample Constraint Programs

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.
```

## 6.8 Restrictions and Caveats

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.