%determinstic

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

Example: Tree search

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

Graphical representation of the tree testtree used in this example.

%sort label %.
%term a label %.
%term b label %.
%term c label %.
%term d label %.
%sort tree %.
%term node %pi tree %-> tree %-> tree %.
%term leaf %pi label %-> tree %.
%define 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 STELF 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.

%sort findlabel {_ tree} {_ label} %.
%term findlabel/leaf findlabel (leaf L) L %.
%term findlabel/left %pi (findlabel (node T1 T2) L) %<- (findlabel T1 L) %.
%term findlabel/right %pi (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 %.

%deterministic findlabel.
%query 1 * findlabel testtree L.

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.

%sort eq {_ label} {_ label} %.
%term eq/refl eq L L %.
%sort searchfor {_ tree} {_ label} %.
%term _ %pi (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' equal to a, then b, then c.

%query 1 _ _ %the (searchfor testtree c) P %.

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.

See also

• Deterministic Type Families (guide §5.30)
• Cut on Wikipedia