[metis-users] TermNets

[James Bridge]

Hi Joe,

Thank you for the explanation.

Just to ensure that I have a proper understanding, when you say

>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 

is there ever a case where there is branching behaviour after a long
single sequence or do all Single sequences always terminate in a
Result without connecting to a Multiple (branch) point on the way?
(From the code it looks like Single sequences grow from Results upwards
and are converted to Multiple at a branching point which, if my reading
is correct, implies that Singles must connect to a Result and never to
a Multiple.)

Thanks,

James



On Sep 25 2012, Joe Leslie-Hurd wrote:

>[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
>