Sorry, I forgot to reply to the list. On 07/26/2012 11:53 AM, Alexander Solla wrote:

...

(consider, e.g., 'head undefined' vs. 'head [undefined]') This was a typo, I meant 'tail undefined' vs. 'tail [undefined]'.

I'm not arguing one way or the other (I know what I do, unless there's a need to do the other). What I'm saying is there are lots of ways to interpret a language, and we can choose between them. If you want to analyze Haskell, you will have to choose an interpretation for it. Haskell, as a logic, is paraconsistent (i.e., it's unsound. So your theory for Haskell either needs to keep contradiction in the object language (the "partial" case where we do not identify bottoms) or take it out of the object language and put it into the analytical meta-language. The intention is not to use Haskell as a logic, but to use an existing logic (HOLCF, reference in an earlier mail; thus the interpretation is already fixed to a high degree) to formally verify Haskell programs. In order to do that the program to be verified has to be "rewritten" inside the logic and everything that is proved about this "formal variant" of the program should be transferable to the real program (assuming that "Haskell's semantics" was captured correctly).

Another problem is if the formalization is too strict, i.e., requires properties from functions that are not satisfied in practice and that's where my original question about commutativity of (==) came from. If there are "reasonable" Haskell programs for which (==) is non-commutative, we should not require it, since we could not formalize those programs then. cheers chris

The classically valid inference:

(x == y) = _|_ => (y == x) = _|_

On 7/25/12, Christian Sternagel wrote:

...

Dear Alexander,

Let me clarify again: by "we identify all bottoms" I mean that any error and also nontermination is identified with _|_ . However, I did not mean that [_|_] is identified with _|_ (since the point of a formal treatment is exactly to correctly consider the lazy semantics of Haskell). In Haskell there definitely is a difference between 'undefined' and '[undefined]' (consider, e.g., 'head undefined' vs. 'head [undefined]') so this must be taken in to account in a rigorous treatment.

Btw: I didn't get which inference you meant when you where saying it is "classically valid".

cheers

chris

On 07/26/2012 11:13 AM, Alexander Solla wrote:

...

Depending on the context, it may or may not be wise to distinguish between undefined and [undefined]. This is a matter of strictness, laziness, and totality. If you identify all bottoms as one, you essentially restrict yourself to (what might as well be, for the purposes of this discussion) a strict subset of the Haskell language.

If you distinguish between values that "contain" bottom and "are" bottom, then you need to deal with the semantics of laziness.

Like I said, it is classically valid, so choosing these semantics means that it will be safe. But the undecidability of comparing distinct bottoms means that you have to make a choice.

On 7/24/12, Christian Sternagel wrote:

...

...

It's a classically valid inference, so you're "safe" in that respect, and it is true that evaluating x == y requires traversing x and y, so that if x or y "are" bottom, (x == y) and (y == x) will both be bottom. Well, (x == y) could result in bottom, even if neither x nor y are bottom, e.g., [undefined] == [undefined]. -cheers chris