Constraint domains and coverage checking

From The Twelf Project
Jump to: navigation, search
You should not attach any particular significance to the fact that Twelf returns OK (or raises an uncaught exception, or starts playing the theme music to M*A*S*H...) on a signature that mentions a constraint domain and also tries to prove coverage or totality metatheorems. - Kevin Watkins

It is tempting to try to use constraint domains to do seemingly innocent helpful things. However, at the present time, constraint domains should be seen as completely incompatible with features that Twelf uses to prove metatheorems, such as %mode, %covers, and %total.

One particular way that this error happens is when users attempt to formalize a language with exceptions, and want to index their language with strings.

%use equality/strings. 

exp : type.
error : string -> exp.

This should be avoided at all costs in favor of explicitly defining a type of error messages within the signature.

errormessage : type.

bad-value : errormessage.
type-error : errormessage. 
% ...etc...

exp : type.
error : errormessage -> exp.

Example: apparent unsoundness with constraint domains

The essential problem is that the interaction between constraint domains and the Twelf coverage checker is not well defined. Take the following example:

%use word32. 

exp : type.

x : word32 -> exp.
y : exp.
z : exp.

q : exp -> exp -> type.
%mode q +A1 -A2. 

q/y : q y y.

q/z : q z z.

Twelf appears to allow us to prove that, for any input in the first position, q will always run successfully and return an output in the second position.

ERROR: option 'name' deprecated or invalid
%worlds () (q _ _). 
%total T (q T _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds () (q _ _). %total T (q T _).

%% OK %%

However, Twelf's assertion of totality here is completely bogus, which we can see if we try to run q as a logic program with (x 5) in the first position.

ERROR: option 'include' deprecated or invalid
%solve _ : q (x 5) _.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve q (x 5) X1. Error: No solution to %solve found

%% ABORT %%

Analysis

This article or section needs copy editing.

One way of looking at the problem above is that the above proof isn't quite a proof of what it seems to be a proof of. The %worlds statement for the above theorem is empty, which means that one way to state the theorem theorem is "if the only things that exist in the things that were explicitly defined in the signature." This is a closed-world assumption. Because the identifier 5 never was explicitly defined in the signature, but was implicitly introduced by the %use word32 declaration, then the metatheorem above is true - if we're not allowed use any object of type word32, the we can't feed q any input that will allow it to fail.

If we modify our worlds declaration to specify that there may be some word32s around—because there are some word32s around, there are of them!—then the theorem fails as it should.

%block some-word32s : block {x: word32}.

%worlds (some-word32s) (q _ _).
%total T (q T _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: No solution to %solve found %% ABORT %% %% OK %% %block some-word32s : block {x:word32}. %worlds (some-word32s) (q _ _). Error: Coverage error --- missing cases: {#some-word32s:{x:word32}} {X1:exp} |- q (x #some-word32s_x) X1.

%% ABORT %%

However, as there is no account for exactly what %use does to the signature, it is very difficult to be certain, when we are using constraint domains, that we have proven the theorems we think we have proven. This is precisely why constraint domains and metatheorem declarations like %covers and %total should never be used in the same signature.