Re: and then... (a curiosity)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 4 Sep 2008 21:05:02 +0200, stefan-lucks@see-the.signature wrote:

>>>> Nevertheless Boolean logic /= Belnap logic, though the former is contained
>>>> in the latter. 
>>> 
>>> I never said "Boolean logic", I said "logic", which was ment to include 
>>> multi-valued logic. ;-)
>> 
>> There are many multi-valued logics. 
> 
> You are trying to build an overly complex theory,

I though you wanted to expose these values. But see below.

> which I am not interested in.

(You should be interested in making a consistent proposal...)

> The issue is very simple:
>
> 1. If the A- or the B-part in "if A and B" raises an exception, but the 
>    other part is false, the "right thing" (TM) to do would be to transfer 
>    control to the else clause (or below "end if", when there is no else). 
>    The intermediate result can be viewed as a three-valued logic 
>    expression, but the final outcome of the Boolean expression must be 
>    Boolean, of course. 

   0 /\ T = 0  (as you see the theory is very simple)

> 2. If both raise A and B an exception, of if one raises an exception and 
>    the other one is true, an exception is propagated. (*)

   T /\ T = T (ditto)
 
> 3. I would be willing to pragmatically sacrifice mathematical purity for a 
>    shortcut rule:

There is absolutely no reason to sacrifice purity for impurity.

>    If A is false, the expression is false, whatever B does. 
>    If A raises an exception, of if A is true and B raises an exception, 
>    the exception is propagated.

   1 /\ T = T (it works!)

As you see the theory works fine, even if you don't like it.

Anyway now I see what you want. That is (more or less formally):

Boolean'Base is Belnap logical values. All Boolean expressions are
evaluated in Boolean'Base, as it is already done for numeric types. Nothing
drastically new. (Compare also how Float overflow is converted to IEEE
Infinity.) Like universal numbers, Boolean'Base may have no variables
declared.

> (*) Funny problem: *Which* exception should be propagated? 

This is not funny. This one kills the idea, unless you forcefully convert
all exceptions into Constraint_Error, when a non-Boolean value is converted
to Boolean.

But the main problem is that this is not what people want. They do lazy
evaluation in order to control side effects (and exception is considered
rather as a side effect). Your proposal does not deal with eagerness. Yes
the compiler might optimize away evaluation of one of the arguments of
"and" if another is False. But to do so it still needs a proof that there
is no side effects other than an exception. Unlikely to exceptions, you
cannot pack all side effects into T or _|_.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de