!standard 5.5.2(2/3)                                  15-06-03  AI12-0161-1/01
!standard 5.5.2(5/4)
!standard 5.5.2(7/3)
!class Amendment 15-06-03
!status No Action (8-0-0) 15-06-27
!status work item 15-06-03
!status received 15-03-20
!priority Low
!difficulty Easy
!subject Unicode equivalents for Ada operator symbols
!summary

!problem

Now that Unicode is widespread and allowed in Ada since a decade, please
also make Ada allow the proper mathematical signs as synonyms for the
existing operator symbols.

[This is hardly a "problem" statement, but it's all the author sent.
Apparently, we're supposed to guess why this would be necessary/valuable
 - Editor.]

!proposal

(See Summary.)

!wording

** TBD.

!discussion

Whether these are truly equivalent is a matter for debate (see the Appendix).

One also could imagine allowing additional Unicode operator symbols (union
and intersection come to mind). This was considered during the Ada 2005 work
(see AI95-0322-1), but it was ultimately rejected because of a lack of
consensus on what to do. (The ARG was split into three camps: very limited new
operators from the Latin-1 set, new operators from Unicode characters only,
operators for existing predefined operations. There was no consensus for
any of these ideas.)

!ASIS

[Not sure. It seems like some new capabilities might be needed for operators,
but I didn't check - Editor.]

!ACATS test

An ACATS C-Test is needed to check that the new capabilities are supported.


!appendix

!topic Allow Unicode mathematical signs in Ada
!reference Ada 2012 RM4.4(2)
!from Erik Sigra 15-03-20
!keywords Unicode mathematical sign digraph keyword unary binary
operator negation inequality ordering relation universal existential
quantification quantifier quantified expression logical conjunction
disjunction ¬ not ? and ? or ? /= = <= = >= ? ? for all some
choice_expression factor logical_operator relational_operator
highest_precedence_operator
!discussion

Now that Unicode is widespread and allowed in Ada since a decade, please
also make Ada allow the proper mathematical signs as synonyms for the
existing digraphs[1]/keywords:
mathematical sign : currently allowed digraph or keyword(s)
¬                 : not
?                 : and
?                 : or
?                 : /=
=                 : <=
=                 : >=
?                 : for all
?                 : for some

[1][http://en.wikipedia.org/wiki/Digraph_(computing)]

[Note: The author apparently failed to remember that plain text e-mail is
strictly 8-bit, thus most of his message got converted to ?. This is exactly
as I received it; that may make a point different than the author
intended. - Editor.]

****************************************************************

From: Phil Clayton
Sent: Saturday, March 21, 2015  7:46 AM

These mathematical operators, commonly used in propositional and predicate
calculus in a purely logical sense, are not exactly synonymous with their Ada
namesakes because a proposition is not exactly the same as an Ada boolean
expression.

In propositional calculus, a proposition is either true or false, is dependent
only on its free variables and it has no other effect.  So we have these
properties of propositions P, Q and P ? Q.  In Ada, "P and Q" may be neither
true nor false because either P or Q may raise an exception and P and Q may
have side effects which could affect one another's value if there was a
dependency.  These differences are significant because order of evaluation
matters in Ada.  (This sort of problem is well known and restrictions to avoid
it are well established in subsets like SPARK.)  Consequently, the expected
rules of propositional calculus would not translate into Ada.  I've given some
examples below.

If it is possible to restrict the use of these mathematical operators in Ada
such that the usual rules of mathematical logic apply, then this may be a
worthwhile improvement.  Otherwise, I would find the notation misleading.
Possibly, this means ensuring that the operands are pure (no side effects) and
cannot raise exceptions.

---

In propositional calculus, P ? Q can be replaced by Q ? P because it does not
change the value of the overall proposition.  In Ada, we cannot, in general,
replace "P and Q" by "Q and P" whilst preserving behaviour.  If P and Q can
raise different exceptions, the overall expressions may raise different
exceptions.  If P and Q have side effects whose order of composition affects
the overall effect, the overall effect can be different.

Using mathematical operators for Ada short-circuit operators would be more
sensitive to the above issues because only one of the arguments needs to raise
an exception or have a side effect for the overall result to be different.
For example, consider introducing
    P ? Q
for the Ada expression
   if P then Q
In propositional calculus, P ? Q can be replaced by ¬ Q ? ¬ P (the
'contrapositive rule') but, in general, in Ada, "if P then Q" cannot be
replaced by "if not Q then not P".

****************************************************************

From: Georg Bauhaus
Sent: Tuesday, April 7, 2015  5:08 AM

This is a misconception, IMHO, but there is also an easy way out:

First, mathematics of computer programs should not be confused with mathematics
of publications. The discipline of software engineering deserves a notation of
its own that reminds programmers of what they are doing:
writing programs, not publications, nor general mathematics.

Second, whenever publication is needed, the formal syntax of Ada programs
provides for easy rendition in publications, translating to more
mathematically looking symbols as needed. (There used to be an edition of
Knuth's "literate programming" for Ada; there are some pretty printers.)

But even so, it becomes less clear which set of mathematical properties "="
hould convey: does it imply linear ordering? Finiteness? Since the properties
are defined by Ada (plus overriding) and not by general mathematics, more
mathematically looking symbols would give the wrong impressions. APL did
choose mathematically looking symbols, but it also supplied its own
definitions for these symbols, and they look suitably different in context.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, June 3, 2015 10:07 PM

While filing this mail, I realized that there was some misconceptions that
probably ought to be corrected so future readers aren't mislead.

...
> In propositional calculus, P ? Q can be replaced by Q ? P because it
> does not change the value of the overall proposition.  In Ada, we
> cannot, in general, replace "P and Q" by "Q and P" whilst preserving
> behaviour.  If P and Q can raise different exceptions, the overall
> expressions may raise different exceptions.  If P and Q have side
> effects whose order of composition affects the overall effect, the
> overall effect can be different.

While your general point is probably valid, the above is 100% wrong.
Specifically, Ada does not specify the order of evaluation of operands for
binary operators (short circuit operations like "and then" are not formally
operators). So for Ada (in the abstract), either P or Q can be evaluated first
for "P and Q" and for "Q and P", and both operands will be evaluated unless
the first one raises an exception; there is no definitional difference between
them (in the abstract sense that one ought to be reading programs).

Now you might have been thinking of a more practical meaning as to what a
compiler actually does. But here, too, one cannot make any assumptions about
the order of evaluation of operands. That could be chosen for any number of
reasons, including (as the joke goes) the phase of the moon. (An early MS-DOS
version of Janus/Ada had a bug such that the order of evaluation was partially
determined by some uninitialized components in the expression tree. Because
MS-DOS didn't clear memory between programs, that meant that the order of
evaluation could depend on which program had been run (or file had been
edited) before the compiler ran. Not quite the "phase of the moon", but close.)

An Ada compiler is likely to evaluate these operands in whatever order
generates the best code (for some meaning of "best"), and if P and Q are
sufficiently different, it's quite likely that they'll be evaluated in the
same order regardless of whether the expression was written "P and Q" or
"Q and P".

So, while it's true that one might get different results in practice if
P and Q have side effects, that can happen without changing anything except
compiler switches (for different optimization levels) or targets. (And if the
compiler has a bug as in my above story, it might change for no reason at
all.) Any of the possible results is a correct result for an Ada program, and
the order that the expression is written in has no effect at all on that.

Thus replacing "P and Q" by "Q and P" is a completely semantics-preserving
change in (abstract) Ada; there is absolutely no difference in the possible
set of results. Of course those results include the possibility of raising an
exception, which obviously isn't a possibility in propositional calculus, so
arguably your underlying point remains.

P.S. The fact that one can't send Unicode characters in 8-bit text e-mails
(such as the ones sent in this thread) illustrates a different problem with
using them in programs. :-) Whether that is a concern or not depends on
whether or not you want to work with the widest possible audience (and your
definition of that).

****************************************************************

From: Jeff Cousins
Sent: Thursday, June 4, 2015  4:21 AM

I think I agree...

****************************************************************

From: Phil Clayton
Sent: Monday, June 8, 2015  4:20 PM

Randy, I think we may be talking at cross-purposes here.  I used the phrase
"preserving behaviour", below, to mean "keep the same choice of evaluation
order", which is not the same as what you mean by "semantics-preserving"
("giving the same set of results").  I have rephrased that paragraph below to
reiterate the point.

I hadn't considered that a valid compiler could change the evaluation order of
the arguments because it was run at a different time in the lunar cycle.  (Or,
perhaps it could even defer the choice to run-time?) With no guarantee that "P
and Q" = "P and Q", that is another reason why these Ada expressions shouldn't
look like propositional logic IMHO.

> While filing this mail, I realized that there was some misconceptions
> that probably ought to be corrected so future readers aren't mislead.
>
> ...
>> In propositional calculus, P ? Q can be replaced by Q ? P because it
>> does not change the value of the overall proposition.  In Ada, we
>> cannot, in general, replace "P and Q" by "Q and P" whilst preserving
>> behaviour.  If P and Q can raise different exceptions, the overall
>> expressions may raise different exceptions.  If P and Q have side
>> effects whose order of composition affects the overall effect, the
>> overall effect can be different.

This meant to say that replacing "P and Q" by "Q and P" in Ada source code and
recompiling (with the same valid compiler keeping all other things equal) could
produce executable code that gives a different (valid) result for the overall
boolean expression.  (Consider a compiler that always chooses to evaluate the
left argument of "and" first...) This commutativity example is easy to relate to
in practice: see attached example where swapping P and Q causes the result to
change with GNAT but remain the same if the program is not changed.  That should
hammer home the point why these expressions should not look like propositional
logic, where one can freely replace "P /\ Q" by "Q /\ P" and not change the
value of the overall proposition.

--- Attachment: Test1.Adb

with Text_IO;
procedure Test1
is
  N : Integer;

  function P return Boolean
  is
  begin
    N := N * 2;
    return N < 2;
  end P;

  function Q return Boolean
  is
  begin
    N := N + 1;
    return N < 2;
  end Q;

begin
  N := 0;
  if P and Q  -- changing this condition to "Q and P" changes its value
              -- when compiling with GNAT 4.6.3 with default options
  then
    Text_IO.Put_Line ("True");
  else
    Text_IO.Put_Line ("False");
  end if;

end Test1;

****************************************************************

From: Randy Brukardt
Sent: Monday, June 8, 2015  5:15 PM

> Randy, I think we may be talking at cross-purposes here.  I used the
> phrase "preserving behaviour", below, to mean "keep the same choice of
> evaluation order", which is not the same as what you mean by
> "semantics-preserving" ("giving the same set of results").  I have
> rephrased that paragraph below to reiterate the point.

Sure, but that's the point I tried to make: that someone reading Ada code should
not be caring about what a particular compiler might do, but rather what the
language says about a particular expression. Else you are tying your
understanding to the compiler version, switches, and possibly phase of the moon.

> > ...
> >> In propositional calculus, P ? Q can be replaced by Q ? P because
> >> it does not change the value of the overall proposition.  In Ada,
> >> we cannot, in general, replace "P and Q" by "Q and P" whilst
> >> preserving behaviour.  If P and Q can raise different exceptions,
> >> the overall expressions may raise different exceptions.  If P and Q
> >> have side effects whose order of composition affects the overall
> >> effect, the overall effect can be different.
>
> This meant to say that replacing "P and Q" by "Q and P" in Ada source
> code and recompiling (with the same valid compiler keeping all other
> things equal) could produce executable code that gives a different
> (valid) result for the overall boolean expression.  (Consider a
> compiler that always chooses to evaluate the left argument of "and"
> first...)

Aside: That's not always possible (although I think it is for predefined Boolean
"and"). A compiler that does that in all cases is going to generate code that
misbehaves in a few cases.

> This commutativity example is easy to relate to in practice: see
> attached example where swapping P and Q causes the result to change
> with GNAT but remain the same if the program is not changed.

GNAT /= Ada.

> That should hammer home
> the point why these expressions should not look like propositional
> logic, where one can freely replace "P /\ Q" by "Q /\ P" and not
> change the value of the overall proposition.

My overriding point is that this is irrelevant. No one should care what a
particular program does so long as it is one of the set of allowed results. If
you're reasoning about Ada code, you have to consider all of the possible
results that a correct compiler might generate. (One hopes that these are all
the same.)

The set of allowed results for the predefined and used in (P and Q) is:

    (P and then Q), (Q and then P)

And of course the same set of results is allowed for (Q and P). Thus they're
completely identical.

The difference (for Boolean) between the abstract operation and the Ada
operation is the possibility of exceptions from the operands, no more and no
less.

Perhaps if you're trying to debug some code, you might care what a particular
implementation does. But if you find that the order matters, then your code is
unnecessarily fragile. (That's why many coding standards require the use of "and
then" if there is any possibility of it mattering.)

It would be a huge mistake to replace "and then" by that symbol that doesn't
show up here, but "and" would be benign.

The reason I find your complaint somewhat valid is that the situation is
different for mathematical operators -- there's a lot more differences than just
the possibility of exceptions. (There's no overflow in integer mathematics, no
precision loss in float mathematics, etc.) And I don't see much value to making
code harder to process [and read if you don't have the right tools] just to
prettify it (that's the job of editors, the code itself doesn't need to be
messed up). But I also don't see much reason to not do it anyway, making some
slightly misguided people happy isn't that big a deal (there's lots of things in
Ada that are best used very sparingly; we like to say that's a management
problem, not a language problem). So I'm prepared to go with the flow here.

****************************************************************

From: Phil Clayton
Sent: Tuesday, June 9, 2015  1:55 AM

Right, I understand your point.  You're saying that a programmer shouldn't care
about order of evaluation when writing "P and Q" and, if they did care, then
their code is overly fragile (possibly moon-dependent etc.)  I agree.

My concern is that overly fragile code is more likely to be written
unintentionally because "P /\ Q" makes P and Q look like propositions:
propositions don't have side effects or raise exceptions so the
programmer/reader may not consider whether they do.  The example about replacing
"P and Q" with "Q and P" was just to show that overly fragile code can lead to
problems.  (Instead, I could have just pointed to potential moon-dependence etc.
but didn't think of that and couldn't produce a concrete example.)  Sorry if
that wasn't clear in my original post.  Another reply, from Georg Bauhaus, said:
"The discipline of software engineering deserves a notation of its own that
reminds programmers of what they are doing..." which I fully agree with.

****************************************************************

From: Peter Chapin
Sent: Tuesday, June 9, 2015  6:51 AM

> My concern is that overly fragile code is more likely to be written
> unintentionally because "P /\ Q" makes P and Q look like propositions:
> propositions don't have side effects or raise exceptions so the
> programmer/reader may not consider whether they do.

Don't we already have this problem with '+'? An expression like A + B might have
side effects and might raise exceptions. Yet we use the mathematical symbol '+'
for this operation.

****************************************************************

From: Randy Brukardt
Sent: Tuesday, June 9, 2015  3:51 PM

Exactly. I think the problem with "P /\ Q" is just remembering what it means (I
don't recall having read anything using those symbols rather than "and" or "or"
in many years). The other issue would be that there'd be no guarantee that the
operator means what you think it does (it probably wouldn't if user-defined
"and" operators are defined in existing code, since it would not also be
defined). We don't make any requirement on user-defined operators now, we surely
wouldn't do that on these either.

To amplify: I see any new operators as just that, new operator symbols. They
might have renames in the predefined/language-defined case so that they can be
applied to with their "obvious" meaning. But I would be strongly opposed to
going further than that. Ada 83 has lexical replacements, an idea which has
caused plenty of trouble over the years and one which we would never want to
expand. And I surely don't want to see "P /\ then Q", "type P is new Q /\ Interf
with private;", and similar nonsense in Ada programs ("and" is not just used as
an operator in Ada syntax). Ada 83 also defined "/=" automatically from "=",
another idea that sounds good but has caused no end of semantic problems
(especially as it's kept solely for compatibility these days). Repeating that
madness would be insane.

I do think some extra operator symbols would be valuable for writing Ada
programs, especially ones that don't have much connotation for the average
programmer. But that idea did not get much traction in 2002 and it's not at all
clear to me what has changed in the interim.

****************************************************************