[metis-users] TermNets

[James Bridge]

Thanks Joe, that has clarified things.

James

On Sep 26 2012, Joe Leslie-Hurd wrote:

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