Re: Expressions versus the value they represent
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