Re: [Toss-devel] New Speagram: terms with sharing

[Lukasz K. <luk...@gm...>]

> Nullary (with regard to subterms) terms are translated as predicates
> over a single element, unary terms as relations between the element
> corresponding to the term and the element corresponding to the
> subterm, arity N terms into arity N+1 relations. All supertypes are
> translated as predicates / relations whose first argument is the same
> element as the element generated for the whole term. That's the idea
> behind translating terms to structures: a new element for each subterm
> unless it is shared, but no new elements for supertypes. If you
> recall, in the "formal" notation we represent terms by "f (supertypes
> ; subterms)", and supertypes are of this form as well so can introduce
> more subterms.

You are absolutely right - I somehow misunderstood the previous mail
very badly. Do you think we could get back formulas from the structures
generated by terms relatively easily? That would be a good motivation,
at least for me, to think about implementing this translation finally :).
But I am still not entirely sure how this will help with formulas (even
though now I think I start to see the point). Best!

Lukasz