Constraint domain

From The Twelf Project
Jump to: navigation, search

A constraint domain, also called a Twelf(X) extension, is an extension to Twelf that allow users to work easily with an object, such as the integers, that can be tedious or inefficient to explicitly formalize within Twelf. Constraint domains are introduced with the %use declaration.

You should never use constraint domains and coverage checking in the same signature, but they are useful when using Twelf as a logic programming system or when reasoning in an object language. This document shows brief examples of each of the constraint domains, which are treated more formally in the chapter on constraint domains in the User's Guide.

Rational numbers with equality: %use equality/rationals

The rational numbers with equality add a new type family, rational, and operators for rational addition, subtraction, multiplication, and negation.

%use equality/rationals.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

rational : type. ~ : rational -> rational. %prefix 9999 ~. + : rational -> rational -> rational. %infix left 9997 +. - : rational -> rational -> rational. %infix left 9997 -. * : rational -> rational -> rational. %infix left 9998 *.

%% OK %%

The rational numbers are automatically simplified by Twelf

mynum = 1/4 + ~ 9/2.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mynum : rational = ~17/4.

%% OK %%

Because of this automatic simplification, equality is not actually added by the %use declaration, becuase it can be introduced the same way identity is introduced for any other type family in Twelf.

eq : rational -> rational -> type.
eq/is : eq X X.



Rational numbers with inequality: %use inequality/rationals

This declaration introduces everything introduced by %use equality/rationals, as well as ways to check for

%use inequality/rationals.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

rational : type. ~ : rational -> rational. %prefix 9999 ~. + : rational -> rational -> rational. %infix left 9997 +. - : rational -> rational -> rational. %infix left 9997 -. * : rational -> rational -> rational. %infix left 9998 *. > : rational -> rational -> type. %infix none 0 >. >= : rational -> rational -> type. %infix none 0 >=. +> : {X:rational} {Y:rational} {Z:rational} X > Y -> Z + X > Z + Y. +>= : {X:rational} {Y:rational} {Z:rational} X >= Y -> Z + X >= Z + Y. >>= : {X:rational} {Y:rational} X > Y -> X >= Y. 0>=0 : 0 >= 0.

%% OK %%

Inequality relations can be used like normal goals, as they are in the next example, even though the User's Guide explains that their internal behavior is different than other goals.

more-than-two : rational -> rational -> type.
more-than-two/i : more-than-two R1 R2
                   <- R1 + R2 > 2.
See Twelf's output



Integers with equality: %use equality/integers

The introduction of integers with equality looks similar to the introduction of rationals with equality, but with a different type family, integer.

%use equality/integers.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

integer : type. ~ : integer -> integer. %prefix 9999 ~. + : integer -> integer -> integer. %infix left 9997 +. - : integer -> integer -> integer. %infix left 9997 -. * : integer -> integer -> integer. %infix left 9998 *.

%% OK %%



Integers with inequality: %use inequality/integers

The introduction of integers with inequality is a good bit shorter than the introduction of rationals with inequality, because Twelf can take advantage of the facts like X + 1 > Y iff X >= Y.

%use inequality/integers.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

integer : type. ~ : integer -> integer. %prefix 9999 ~. + : integer -> integer -> integer. %infix left 9997 +. - : integer -> integer -> integer. %infix left 9997 -. * : integer -> integer -> integer. %infix left 9998 *. >= : integer -> integer -> type. %infix none 0 >=. +>= : {X:integer} {Y:integer} {Z:integer} X >= Y -> Z + X >= Z + Y.

%% OK %%



Strings: %use equality/strings

This constraint domain allows Twelf to include strings of characters.

%use equality/strings.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

string : type. ++ : string -> string -> string. %infix right 9999 ++.

%% OK %%

Like the other constriant domains, using the operators automatically simplifies the operators away. The only one provided is concatenation, ++, which is shown below:

mystring = "Hello" ++ " " ++ "World" ++ "!".
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mystring : string = "Hello World!".

%% OK %%



32-bit integers: %use word32.

The word32 extension behaves very differently than the others - operators are relations, not functions, and so Twelf does not simplify their application away.

%use word32.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

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.

%% OK %%

Behind the scenes, using the word32 extension adds axioms to the signature like 3+15 shown in the below example. The prove+ relations that are defined act like effectiveness lemmas for these relations.

myproof = 3+15.

%solve _ : prove+ 92 _ 105 _.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

myproof : + 3 15 18 = 3+15. %solve prove+ 92 X1 105 X2. OK _ : prove+ 92 13 105 92+13 = proof+ 92 13 105 92+13.

%% OK %%


See also