Constraint domain
From The Twelf Project
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.
Contents |
[edit] 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.5R3, Aug 30, 2005 (%trustme)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.5R3, Aug 30, 2005 (%trustme)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.
[edit] 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.5R3, Aug 30, 2005 (%trustme)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
[edit] 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.5R3, Aug 30, 2005 (%trustme)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 %%
[edit] 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.5R3, Aug 30, 2005 (%trustme)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 %%
[edit] Strings: %use equality/strings
This constraint domain allows Twelf to include strings of characters.
%use equality/strings.Twelf 1.5R3, Aug 30, 2005 (%trustme)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.5R3, Aug 30, 2005 (%trustme)mystring : string = "Hello World!".
%% OK %%
[edit] 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.5R3, Aug 30, 2005 (%trustme)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.5R3, Aug 30, 2005 (%trustme)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 %%
[edit] See also
- %use
- Constraint domains in the User's Guide
