annotation for implies

[Peter Mosses <mosses@csl.sri.com>]

Dear Bernd,

I must apologise for my long silence, and for the delay with
implementing the changes to the Summary: I simply ran out of time
before going off for (unavoidable :-) vacation with no net access.
I'm now back, and about to update the Summary(-Changes).

> Markus Roggenbach schrieb:
> > 
> > Dear Peter, dear Michel,
> > 
> > sorry for beeing late -- here is our proposal for an annotation implies
> > (in agreement with Michel; he mailed us:
> > 
> > > I will not mind at all if despite what has been suggested in Amsterdam,
> > > **you** make a proposal for implies. I will be more than happy to react
on
> > > your proposal. You may have more time than I have at the moment.
> > >
> > 
> > )
> > 
> > Greetings
> >   Till and Markus
> > 
> > \newcommand{\annoimpl}{\%{\bf implies}\ }
> > 
> > The syntax of an \annoimpl annotation (which
> > may be inserted after a specification) is as follows:
> > 
> > \begin{Items}
> > \I\{$SP$}
> > \I\annoimpl
> > \I{\%\Vars} \ldots
> > \I{\%\Axioms} \ldots
> > \end{Items}
> > 
> > That is, after \annoimpl annotation, a list of
> > axioms (possibly introduced by local variable declarations)
> > may follow.
> > The axioms must be preceeded by a percent sign.

BTW, Markus: kindly use plain text input syntax for examples in
e-mail, since the latex mark-up is not so perspicuous.

> I am not particularly happy about this; it would be better to consider
> the annotation as a classification of an axiom to be an intended
> consequence but make it part of the specification (for my taste). It
> does generate a proof obligation, perhaps optionally, if you want to
> make use of the property of the annotation.
> Note that otherwise a number of problems/questions arise:
> - do variable declarations need to be introduced?
> (I would prefer the local variable declarations, but never mind).
> - just a percent sign in front is not enough to distinguish from other
> annotations (unless a clumsy "end" of some sort is introduced); or am I
> wrong in this?
> - conversely, if you insist on these axioms to reside outside the
> semanctics of the spec, and we do not have any other annotations FOR (as
> opposed to ON) axioms to classify them, then the "implies" keyword could
> be omitted and any axiom (or local var axiom) with a percent sign is
> considered an implication. In other words, the keywords "axiom" and
> "var" AFTER a percent sign would introduce the implied axioms
> - can there be annotations ON such axioms again (recursively)?
> this may be useful/needed, e.g. to specify them as rewrite rules etc.

It seems that the only difference between regarding the (hopefully)
implied axioms as part of the spec or not is in the case that they are
not actually consequences of the other axioms.  I don't know much
about methodological issues, but I guess that anyone reading a spec
will probably take the implied axioms on trust, regardless of their
syntactic status, so I'm inclined to agree with you (Bernd) that one
might just as well regard them as part of the spec.  Presumably all
the annotated axioms should follow from all the non-annotated ones -
maybe inductively, if the spec is a free extension (?).

My personal preference would be to annotate each axiom with %implied
at the start.  I'm afraid that it would be too confusing to start
reusing keywords to form annotations.

> > This is needed to distinguish
> > the axioms belonging to the annotation from
> > the normal axioms of the specification.
> > The \annoimpl annotation does not change the
> > semantics of a specification, in particular, the
> > axioms of the annotation are {\em not} added
> > to the specification.

Sorry, but I don't see any strong motivation for this way of doing it.
Just annotating existing axioms seems to have the advantage of keeping
the syntax of annotations as simple as possible.

If I've missed something and there is a good motivation for letting
implied "axioms" be outside the spec, one might consider the syntax

  SPEC %implies GROUP-SPEC

which would allow reference to a named group of axioms, as well as an
explicit list of variable declarations and axioms.  We have { } for
grouping lists of items; let's not use devices like repeated %'s.

If we're to incorporate any such annotation in the new release of the
Summary, it had better be proposed on cofi-language rather soon, I think.

Cheers,

-- Peter
_________________________________________________________
Dr. Peter D. Mosses             International Fellow  (*)

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-2200
333 Ravenswood Avenue           fax:   +1 (650)  859-2844
Menlo Park, CA 94025, USA       http://www.brics.dk/~pdm/