Re: Second Bremen Proposal on an Annotation IMPLIES

[Michel.Bidoit@lsv.ens-cachan.fr (Michel Bidoit)]

Dear CoFI Friends,

I am willing to support the recent
"Second Bremen Proposal on an Annotation IMPLIES", with the following
comments and restrictions.

(Below I am only including parts of the original message, with my comments
preceded by MB:, and skipping as much as possible of the original text to
keep this message reasonably short.)
[BKB: I agree with Michel]

APPENDIX

1) Why an Annotation "%implies"?
================================

This annotation is expected to help answering the question: "Am I
specifying the right thing?" This can be done by dividing the axioms
of operations and predicates into two classes: "normal axioms", which
define the operations and predicates, and "implied axioms". The
implied axioms specify properties that should follow from the normal
axioms.

MB: more generally, the implied axioms specify properties that should
MB: follow from the semantics of the specification that precedes the
MB: "implies" annotation (e.g., not only the normal axioms, but also any
MB: generatedness constraint, free constructs etc.)

A nice "side effect" of the annotation is that it helps to structure
consistency proofs: given a set N of normal axioms, and a set I of
implied axioms, (i) implies (ii):

 (i) N is consistent, and for all axioms A of I holds: N implies A.
(ii) (N cup I) is consistent

MB: I find this "side effect" totally unconvincing and suggest it to be
MB: removed from the proposal.

2) What "part" of a Spec Should Be Annotated With "%implies"?
=============================================================

.... skipping...

Thus the interesting aspect of "%implies" is that it introduces a
concept weaker than the annotation "%conservatively" or the CASL
construct of a view, namely: just axioms are allowed.
(BTW: This was Michel's original intention in Amsterdam.)

MB: I would also allow for generatedness constraints, which indeed are
MB: another kind of sentences in CASL.

3) Shall the annotated axioms be part of the specification?
===========================================================

.... skipping....

The second option means that we have to attach %imples to an existing
CASL construct, and the best-suited construct is "then".
However, this means that the implied axioms become part of the
specification.
Now this does no harm, it even has the positive effect
that provers can use the implied axioms before they have
been proven to be consequences of the specification
(of course, a proof obligation related to the %implies has to be
generated).

MB: OK

4) What is an approriate syntax for the annotation?
===================================================

We propose the following grammar (note that this is not a new grammar, 
but a restriction of the proper CASL grammar)


 SPEC ::= ...
         | SPEC then %implies AXIOM-ITEM+

 AXIOM-ITEM ::=  var/vars VAR-DECL; ... VAR-DECL;
               | var/vars VAR-DECL; ... VAR-DECL
                          "." FORMULA "." ... "." FORMULA ;
               | axiom/axioms FORMULA ; ...; FORMULA ;


Thus a tool capable to deal with the annotation "%implies" has the
opportunity to do an addidional syntax test concerning the correct use
of the annotation: A specification with the annotation "%implies" is
legal iff the annotation "%implies" is followed by a non-empty
sequence of AXIOM-ITEMs (see grammar above), where an AXIOM-ITEM is a
global variable declaration, a local variable declaration or an axiom.

MB: As suggested above, this should be revised to include also
MB: generatedness constraints. Moreover, I would strongly suggest that the
MB: fact that the piece of specification that follows the "implies" doesn't
MB: introduce any new item in the signature should be left as part of the
MB: proof obligation related to the "implies" annotation.

MB: In other words, I don't think it is consistent with CASL design of
MB: annotations to introduce any syntactic restriction here. But I agree
MB: with the intention, and the proof obligation induced by "implies" would
MB: therefore be:
MB: * no new signature items
BKB: OK, no syntactic restriction enforced in general 
BKB: (or requirement on all parsers), 
BKB: but tools may give a warning statically. I guess this was the intention
MB: * new axioms follow from what precedes
BKB: this is a real proof obligation

5) How is "%implies" related with the other annotations?
========================================================

... skipping...

Please note that if SP' consists only of AXIOM-ITEMs (see the grammar
above), the meaning of the annotations "%implies", "%def" and
"%conservatively" is the same. 

Thus, methodologically, the usage is as follows 
(in increasing order of complexity and decreasing order of projected 
number of occurrences):

a) %implies: to indicate that only implied axioms follow

b) %def: to define extensions such as e.g. function definitions

c) %conservatively: to define other conservative extensions

The last option is least needed and thus justifies (in our opinion)
a rather longer name to alert to its rather complicated semantics
(and proof obligations).

MB: I agree modulo my above remarks w.r.t. "only AXIOM-ITEMs".

Best regards,
Michel Bidoit