Re: [Toss-devel] New Speagram: terms with sharing
Status: Beta
Brought to you by:
lukaszkaiser
From: Lukasz S. <luk...@gm...> - 2012-09-21 23:14:47
|
On Sat, Sep 22, 2012 at 12:54 AM, Lukasz Kaiser <luk...@gm...> wrote: > > I'm afraid that I do not fully understand - why are these quantified variants > of translating to structures, and why is that easier? I am surely in favour > of starting with the easier thing! 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. |