[metis-users] TermNets

[Joe Leslie-Hurd]

Hi James,

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

Though the Single constructor was created with the purpose of
optimizing long Single sequences leading to Results, they can appear
in other places too. For example, consider adding the two terms

f(t,u)
f(t,v)

to an empty term-net. The resulting term-net will look something like

Multiple (NONE, f/2 |-> Single (t, Multiple (...)))

where the Single is used to indicate that at the subterm position
"first argument of f" it has only ever seen one term "t". The second
argument of the Single constructor is a choice point using Multiple,
because there are two terms "u" and "v" to be discriminated at the
next subterm position "second argument of f".

Hope that helps,

Joe