[metis-users] TermNets

[Joe Leslie-Hurd]

[cc'ing to the metis-users mailing list]

Hi James,

Sorry for the late reply: I just got back from my honeymoon.

> I've been looking at the TermNet code with the aim of understanding it. I
> have a few quick questions regarding the forward pointers you refer to in
> your e-mail.
>
> First, are these the same as McCune's Jump Lists as in his 1990 paper
> "Experiments with Discrimination-Tree Indexing and Path Indexing for Term
> Retrieval" ?

(Caveat: I've just today seen this paper, and my implementation was
developed independently.) In the paper it seems jump lists always
include forward pointers, and plain discrimination trees never do. My
term-nets include forward pointers only for Single constructors (see
below).

> In the actual implementation, is this the purpose of the
>
> Single qterm* a' net
> constructor in the a' net datatype?
>
> Lastly, with a Single constructor is the a' net part always of type Result ?
> (i.e. is it always a single path down to the tree leaf?)

The term-net works by flattening each term to a list (using a
pre-order traversal) and then combining terms with a common list
prefix to form a tree with Multiple nodes at the branch points and
Result nodes at the leaves. My initial implementation had just these
constructors, but the common case is that when traversing the tree
from root to leaf there will be some initial Multiple constructors
with more than one child, then a long sequence of Multiple
constructors with just one child branch eventually leading to a
Result. The Single constructor is an optimization for the long
sequence portion of the tree by storing whole subterms instead of
flattening them into lists. As a side-benefit the Single constructor
allows you to easily skip subterms a la jump lists.

Hope this helps to explain what's going on.

Cheers,

Joe