Re: [CoFI] CASL Concrete Syntax

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Christine,

>>page 7, conjunction and disjunction:
>>Isn't it common to give conjunction a higher precedence than disjunction?
>
>and 
>
>>page 7, implication:
>>It is quite standard that implication associates to the right,
>>i.e. A => B => C is parsed as A => (B => C)
>>(see eg. Shoenfield, Mathematical logic, 1967).
>
>I asked again a colleague in Paris who is a logician and has been
>teaching logics for years: she says that on these grounds there is
>no standard and that it varies with the authors...
>Therefore, if we were to make some choice, I don't think it could
>be on the grounds that it is standard anywhere...
>(and Peter was reminding us that :
>> some of us have argued that software
> engineers do not have such a strong tradition for this. )

I still think that it is quite common to compare conjunction with
multiplication and disjunction with addition, and by this analogy,
conjunction has a higher precedence.
But may be that some people give disjunction a higher precedence
to conjunction - that depends on prefering disjunctive normal
from or conjunctive normal form.
So perhaps it is better to leave this to precedence annotations.

[OK, so at least that part of the issue may perhaps be settled?
--PDM] 

Concerning implication, I cannot imagine any reason for
parsing A => B => C as (A => B) => C, while parsing it
as A => (B => C) makes very much sense:
A => (B => C) is equivalent to (A /\ B) => C,
and this equivalence can be exploiting as follows:
Suppose that we have a proof p of (A /\ B) => C and a proof a of A. 
 From p we get a proof curry(p) of  A => (B => C). Then, we can apply 
modus ponens  to get a proof MP(curry(p),a) of B => C.
Thus we actually can read
   A => B => C => ... Z
as
   (A /\ B /\ C ....) => Z.

Now there is a deep analogy between:
        formulae     and types
        proofs       and terms
        modus ponens and application
known as the "Curry-Howard-Isomorphism".
Thus, we also have the equivalence  of
A -> (B -> C) and (A x B) -> C
in the type system of higher-order languages.
This is known as "currying".
Again, if you have f:(A x B) -> C and a:A,
you can move to curry(f):A -> (B -> C), and by "modus ponens",
we get Apply(curry(f),a):B -> C.
It therefore makes very much sense to parse A -> B -> C
as A -> (B -> C), and in fact, this is adopted by many higer-order
systems.
Then we actually can read
   A -> B -> C -> ... Z
as
   (A x B x C ....) => Z
(in fact, Isabelle displays it close to the latter form).

By the Curry-Howard-Isomorphism, both A => B => C and
A -> B -> C should be treated in the same way.

[Perhaps software engineers are in any case unlikely to use axioms with
 iterated implications (or higher-order functions) - in which case it
 shouldn't cause any confusion to allow the omission of the parens in 
 A => (B => C), as advocated by Till, Don, and others.  It seems that
 when iterated implications are allowed, the grouping is indeed always
 to the right - or can someone cite a particular book or framework
 where the opposite grouping is assumed?  --PDM]

Greetings,
Till