Deterministic declaration

From The Twelf Project
Jump to: navigation, search

The %determinstic declaration influences the way logic programming behaves in Twelf. If a type family is deterministic, then once Twelf finds a single solution through logic programming search it cannot backtrack to find different solutions.

Example: Tree search

Graphical representation of the tree testtree used in this example.

We define a tree with labeled nodes, and a distinguished tree testtree

label : type.
a : label.
b : label.
c : label.
d : label.

tree : type.
node : tree -> tree -> tree.
leaf : label -> tree.

testtree = node (node (leaf a) (leaf b)) (node (leaf c) (leaf d)).

Searching for a leaf

We also define a judgment, findlabel, that looks for a label at leaves of the tree. Because Twelf tries to use the first-defined rule first, the operational behavior of this is to search for the leftmost node, then to backtrack and find the next-to-leftmost node, etc.

findlabel : tree -> label -> type.
findlabel/leaf : findlabel (leaf L) L.
findlabel/left : findlabel (node T1 T2) L
                  <- findlabel T1 L.
findlabel/right : findlabel (node T1 T2) L
                  <- findlabel T2 L.

If findlabel is not declared deterministic, all four solutions can be returned, but with findlabel declared deterministic only one will be found.

%query 4 * findlabel testtree L.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%query 4 * findlabel testtree L. ---------- Solution 1 ---------- L = a. ---------- Solution 2 ---------- L = b. ---------- Solution 3 ---------- L = c. ---------- Solution 4 ---------- L = d. ____________________________________________

%% OK %%
%deterministic findlabel.
%query 1 * findlabel testtree L.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%deterministic findlabel. %query 1 * findlabel testtree L. ---------- Solution 1 ---------- L = a. ____________________________________________

%% OK %%


Causing search to fail

When using %deterministic, finite failure no longer means that no derivation can be found, becuase the deterministic search may put constraints on later results that causes them to fail. Take the searchfor predicate, which first looks up a label with findlabel and then checks to see if it is equal to some other label.

eq : label -> label -> type.
eq/refl : eq L L.

searchfor : tree -> label -> type.
- : searchfor T L
     <- findlabel T L'
     <- eq L L'.

Using searchfor to look for c in our test tree will cause backtracking, because findlabel first make L'<tt> equal to <tt>a, then b, then c.

%query 1 * P : searchfor testtree c.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%query 1 * searchfor testtree c. ---------- Solution 1 ---------- Empty Substitution. P = - eq/refl (findlabel/right (findlabel/left findlabel/leaf)). ____________________________________________

%% OK %%

If findlabel is deterministic, then the same search will make L' equal a, and will then be unable to backtrack.

%deterministic findlabel.
%query 1 * P : searchfor testtree c.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%deterministic findlabel. %query 1 * searchfor testtree c. Error: Query error -- wrong number of solutions: expected 1 in * tries, but found 0

%% ABORT %%

See also