%unique

From The Twelf Project

This article or section describes an undocumented feature of Twelf.
The information may be incomplete and subject to change.

A %unique declaration attempts to automatically check whether some positions of a relation (its outputs) are uniquely determined by some other positions (its inputs). It uses the same syntax as %mode.

Currently there is no way to utilize the result of a successful %unique declaration and so its use is not suggested - an equivalent result can be established by a uniqueness lemma.

[edit] Example

We define the oft-used example of addition of natural numbers:

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
pz : plus z N N.
ps : plus (s N1) N2 (s N3)
      <- plus N1 N2 N3.

We can then check for uniqueness using %unique (a %worlds declaration is also required).

%worlds () (plus _ _ _).
%unique plus +N1 +N2 -1N3.

Twelf 1.5R3, Aug 30, 2005 (%trustme)
%worlds () (plus _ _ _).
%unique +{N1:nat} +{N2:nat} -1{N3:nat} (plus N1 N2 N3).

%% OK %%

If we had created a non-unique definition of plus, for instance by adding an additional, broken version of ps2, Twelf would have indicated an error upon checking for uniqueness:

ps2 : plus (s N1) N2 N3 
      <- plus N1 N2 N3.

%worlds () (plus _ _ _).
%unique plus +N1 +N2 -1N3.

Twelf 1.5R3, Aug 30, 2005 (%trustme)
%worlds () (plus _ _ _).
Error:  Uniqueness checking plus:
Constants ps and ps2 overlap

%% ABORT %%

[edit] Mutual recursion

Checking the uniqueness of mutually recursive predicates creates a problem, because uniqueness (unlike %mode) cannot be checked incrementally. We therefore introduce a simultaneous form of uniqueness declarations, in analogy with other simultaneous declarations.

nat : type.
z : nat.
s : nat -> nat.

div2 : nat -> nat -> type.
div2' : nat -> nat -> type.
d2s : div2 (s N) (s M)
      <- div2' N M.
d2z : div2 z z.
d2's : div2' (s N) M
       <- div2 N M.

%worlds () (div2 _ _) (div2' _ _).

%unique (div2 +N -1M) (div2' +N' -1M').