Re: The future of Spark . Spark 2014 : a wreckage

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

On Tue, 09 Jul 2013 18:51:36 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 08 Jul 2013 22:59:30 +0200, Florian Weimer wrote:
>>> This is nothing new.  Boolean implication p → q is already written as
>>> P <= Q in Ada.
>>
>> Where?
>> 
>> It would be plain wrong, ...
> 
> Less-or-equal on Booleans is indeed equivalent to implication.
> But that's a hack.  Considering Booleans as ordered is questionable --
> I never heard of such a thing in mathematical logic.

Truth values are ordered in some logics. In others they are not.

>>...because logical implication (not P or Q) must be
>> denoted as P => Q.
> 
> It must be?

Yes, if logical implication is indeed meant here, of which I am not sure.

> In Eiffel, it is denoted by the "implies" keyword.
> In Ada 2012, one writes "(if P then Q)", which is shorthand for
> "(if P then Q else True)".

But this is not an implication (Boolean operation). It is a rule based on
implication. E.g. Modus ponens:

P, P=>Q
------------
Q

So "implies" and "if-then" are correct, while P->Q looks wrong even when
spelled correctly as P=>Q.

If there should be a symbol, I think,

   P |= Q  or P |- Q

would be more appropriate.

Why had we introduced Unicode? After all, there is a code point for this:

  P ⊧ Q    U+22A7  Logical consequence

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