-
Notifications
You must be signed in to change notification settings - Fork 0
Structured terms
Many algorithms are naturally expressed in terms of structured terms, that is, terms that look like f (g a) (f b (g c))
rather than just like a
, b
, or c
. Datalog (forward-chaining) traditionally disallows structured terms, whereas they have always been a key part of Prolog (backward-chaining). L10 allows for the use of these structured terms; they must be given types before they are used, however.
The following L10 code declared a type of trees that store natural numbers on their leaves (the type nat
is one of two built-in types, the other is string
).
tree: type.
leaf: nat -> tree.
node: tree -> tree -> tree.
Given this type declaration, we can represent this tree...
*
/ \
* \
/ \ *
* 3 / \
/ \ 6 *
3 4 / \
3 4
...with this term:
node
(node
(node (leaf 3) (leaf 4))
(leaf 3))
(node
(leaf 6)
(node (leaf 3) (leaf 4)))
We can also use datatypes to represent paths into the tree: for instance, we get to the number 6
in our example tree by going right, then left; this can be represented by the term left (right top)
with type path
(you must read the instructions from right to left, starting at top
).
path: type.
top: path.
right: path -> path.
left: path -> path.
If we have a large term and we want to know, for a given subterm, what are all the paths that reach this subterm, we can encode this as a very simple L10 program.
pathTo: tree -> path -> rel.
pathTo (node TreeL TreeR) P
-> pathTo TreeL (left P),
pathTo TreeR (right P).
{-# QUERY pathsToTree pathTo + - #-}
Note that this program only terminates because the terms in the conclusion of the rule are no larger than the terms in the premises. (It is possible to "go the other way" and have programs with bigger terms in the conclusions, but doing so requires a more sophisticated use of L10, demand-driven saturation.)
We can ask for all the paths into a given tree by seeding a database with the tree we are interested in and the path top
representing the path to the top of that tree.
example = pathTo (node (node (node (leaf 3) (leaf 4)) (leaf 3))
(node (leaf 6) (node (leaf 3) (leaf 4)))) top.
Using the Elton compiler for L10, we can run this program on our example (the full program is TreePath.l10 in the examples directory). This snippet is edited to remove a lot of output from Elton and SML.
$ elton examples/TreePath.l10
$ sml -m '$SMACKAGE/cmlib/v1/cmlib.cm' examples/TreePath.l10.sml
- fun f (tree, ()) = print (" Path - "^Path.toString tree ^ "\n");
- TreePath.Query.pathsToTree f () TreePath.example (Tree.Leaf' 6);
Path - (Left (Right Top))
- TreePath.Query.pathsToTree f () TreePath.example (Tree.Leaf' 3);
Path - (Right (Left Top))
Path - (Left (Left (Left Top)))
Path - (Left (Right (Right Top)))
- TreePath.Query.pathsToTree f () TreePath.example
= (Tree.Node' (Tree.Leaf' 3, Tree.Leaf' 4));
Path - (Left (Left Top))
Path - (Right (Right Top))