From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,99e73f65ea2533b9 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!news.germany.com!newsfeeder.ewetel.de!npeer.de.kpn-eurorings.net!npeer-ng2.kpn.DE!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: and then... (a curiosity) Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <18b41828-bda4-4484-8884-ad62ce1c831d@f36g2000hsa.googlegroups.com> <57qdnfULQ9tzKCHVnZ2dnUVZ_tHinZ2d@comcast.com> <48bd0003$1@news.post.ch> <12prmxev8newf.lvc4m055okkb$.dlg@40tude.net> Date: Thu, 4 Sep 2008 22:28:00 +0200 Message-ID: <1vmbk6d18az86$.hfgj8yjrvho8$.dlg@40tude.net> NNTP-Posting-Date: 04 Sep 2008 22:28:04 CEST NNTP-Posting-Host: c7144fe0.newsspool3.arcor-online.net X-Trace: DXC=QLfZ\QoE\k485[]]\]T081McF=Q^Z^V384Fo<]lROoR1Fl8W>\BH3Y2?GcH7@feoS9DNcfSJ;bb[5IRnRBaCdfFoIMmcR229P_^cQ5OChi> X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:1928 Date: 2008-09-04T22:28:04+02:00 List-Id: 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