Re: Expressions versus the value they represent

On Apr 12, 10:57 pm, Bob Badour <bbad..._at_pei.sympatico.ca> wrote:
> David BL wrote:
> > On Apr 12, 2:37 pm, Keith H Duggar <dug..._at_alum.mit.edu> wrote:
>
> >>On Apr 12, 1:13 am, David BL <davi..._at_iinet.net.au> wrote:
>
> <snip>
>
> >>>The term ellipse(point(0,0),1,1) is distinct from circle(point(0,0),1)
> >>>even though we may regard them as both encoding a unit circle.
>
> >>What is the point here? If we are talking about a multi-sorted FOL
> >>then those two terms have distinct types. If either is equal to some
> >>other expression say "UnitCircle()" or whatever, then that must be
> >>derivable from the stated axioms and type definitions.
>
> > Actually I was considering single sorted FOL with equality. Sorry for
> > not being clear.
>
> > My point was that under interpretation, distinct terms can represent
> > the same value. This leads to an equivalence relation on terms. I was
> > actually thinking about an analogy to the D&D type system (where
> > circle is a subtype of ellipse).
>
> The type system in question is a conditional. It is predicated on
> someone wanting something like inheritance in their type system. If you
> want something like that, then D&D show how to do it with some consistency.
>
> If you don't want a type system with something like inheritance, don't
> do that.

Agreed. In any case I think the D&D approach translates nicely into definitions of equivalence of FOL terms, so it should work very well in practise. Also I think it's wrong to expect terms to be unique in general. E.g. 3 = 1+2 = 1+1+1 = 6/2 = ....

Even so, canonical representations of values appears very useful (both at an abstract level where it can allow equality to be defined implicitly) and at the physical implementation level (where testing for equivalence can otherwise be computationally expensive). The idea of a Most Specific Type of a value has utility for canonical representations of values.

BTW the possrep idea is related to this discussion. E.g. polar(1,pi) = cartesian(-1,0) is an example of equivalence of two FOL terms under interpretation. Received on Tue Apr 13 2010 - 09:18:27 CEST