On Sun, Jan 25, 2009 at 1:08 AM, Daniel Fischer <daniel.is.fischer@web.de> wrote:
Am Sonntag, 25. Januar 2009 00:55 schrieb Conal Elliott:
> > It's obvious because () is a defined value, while bottom is not - per
> > definitionem.
>
> I wonder if this argument is circular.
>
> I'm not aware of "defined" and "not defined" as more than informal terms.

They are informal. I could've written one is a terminating computation while
the other is not.
> Which definition(s) are you referring to?
>
>   - Conal

I think I smell the same sort of circularity in this shifted "per definitionem" argument as well.  Here's how I imagine making this implicit argument explicit:

Define "terminating" (or undefined) to mean "/= _|_" and "not terminating" (undefined) to mean "== _|_".  Then, since () is obviously terminating (defined), it follows that () /= _|_ .

Is that the argument you had in mind?

Does anyone see the flaw in that logic (and hence the purpose of "obviously").

   - Conal