Re: Expressions versus the value they represent

From: Bob Badour <bbadour_at_pei.sympatico.ca>
Date: Mon, 12 Apr 2010 11:57:49 -0300
Message-ID: <4bc33370$0$12464$9a566e8b_at_news.aliant.net>


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. Received on Mon Apr 12 2010 - 16:57:49 CEST

Original text of this message