Re: [isabelle] undefined & None



I was not happy when "arbitrary" was changed to "undefined" because I saw the
confusion this would cause. I would support a new name (after the release) and
"unspecified" seems a good candidate.

Concerning Larry's nothingness: just like Michael Fourman I have to point out
that there are many approaches to logics with partial functions where terms may
simply not denote. In fact, that is how many mathematicians would explain 1/0.

Tobias

Am 30/09/2013 18:11, schrieb Lawrence Paulson:
> I would argue that "undefined" and "unspecified" mean essentially the same thing, and it would be a bit like renaming "azure" to "blue". It is only a problem for people who imagine that "undefined" designates some sort of magical nothingness. There is no such thing in mathematics.
> 
> Larry
> 
> On 30 Sep 2013, at 16:45, Jasmin Blanchette <jasmin.blanchette at gmail.com> wrote:
> 
>> Am 30.09.2013 um 17:16 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
>>
>>> We just need to be very clear about what this constant actually denotes.
>>
>> My experience is that it's much easier to explain what something is when its name is not positively confusing.
>>
>> Imagine you need to name a constant for the color green. There are three levels of naming:
>>
>>    Good naming: green
>>    Neutral naming: kijani [*]
>>    Confusing naming: red
>>
>> It's easy to train one's brain to map "kijani" to "green", but having to teach the whole world that "red" means "green" just adds one layer of obfuscation.
>>
>> If it was possible to muster the courage to perform such an unfortunate renaming in the first place, surely it shouldn't be too hard to do it again in favor of a good name -- and I would be happy to actually perform the renaming.
>>
>> Jasmin
>>
>> [*] unless you know Swahili, in which case this becomes a good name
>>
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.