CoFI: Cyclic sections - PROPOSAL TO DROP THEM

[pdmosses@brics.dk]

Concerning CYCLIC SECTIONS, also TYPE DEFINITION GROUPS:

> From: Chris George <cwg@iist.unu.edu>
> Subject: CoFI: Cyclic sections
>
> Peter,
> 
> I have not been keeping up with the CoFI discussions at all recently -
> I haven't had the time.  But I have noticed there is some discussion
> about "cyclic sections" - whether they are needed and if so how to
> give a semantics.  I am only guessing about what this involves but
> perhaps it is the same problem as I would term in RSL "mutually
> dependent modules".  

Correct.

> These are not allowed in RSL, and
> the only occasion I can recall when their usefulness was remarked on
> was some work DDC International were doing using RSL to specify Ada
> tools.  They wanted to have one module describing statements and
> another describing expressions - and the mutual dependency is
> immediate.  Having to put the complete abstract syntax in one module
> they found inconvenient (and reasonably so).
> ...

Thanks for your valuable comments!

One possible way out for abstract syntax is to specify a module that
merely declares the *sorts* for statements and expressions, then to
extend this with the *definition* of the statement syntax, and
separately with that of the expression syntax.  Likewise for
specifying mutually-recursive functions in separate modules: declare
the profiles of the functions in one module, then extend it separately
to other modules with the definitions of the functions.

For a somewhat different style of example where linear modules would
be inconvenient, see the paper "Formal Specification as a Design Tool"
by John Guttag and Jim Horning, Proc. POPL'80.  It specifies
mutually-dependent modules for Picture, Contents, Component, and View
for a windows interface.

But if such examples are really so infrequent, and there is a
reasonable alternative way of specifying them using linear modules,
one cannot use them to justify complicating the syntax and semantics
of the CoFI language with cyclic sections.  (As usual, we may suggest
that cyclic sections could be provided in an extension language...)

Note that the one(?) framework that allows mutual recursion, ASF+SDF,
does not allow either translation or compound sort identifiers, so the
syntactic unfolding there is very straightforward.

Unfortunately, with the current (tentative) intended semantics for type
definition groups in CoFI, a type definition both declares and defines
a sort, and redeclaration of sorts in extensions is not allowed... 
This prohibits the linearization suggested above.  So if cyclic
sections are left out, it seems advisable to adjust the semantics of
type definition groups so that one can give type definition for sorts
that were already declared in what is being extended.  This appears to
be simply a matter of relaxing the well-formedness conditions on type
definitions, not affecting the algebraic semantics at all.

My impression is that (thanks partly to Andrzej's energetic exposure
of the semantic complications) the support for including cyclic
sections has disappeared.  Therefore I'd like to see whether we can
settle this issue now:

PROPOSALS

* CYCLIC SECTIONS are to be dropped from the CoFI language-without-a-name.  

* The well-formedness conditions on TYPE DEFINITION GROUPS are to be
  relaxed to allow (or maybe require?) the separate declaration of the
  sorts being defined.

DEADLINE FOR COMMENTS, AMENDMENTS, COUNTER-PROPOSALS: 1st November.

----   --------------------------------------------
\  /  | Peter D Mosses         <pdmosses@brics.dk> |
CoFI  | Common Framework Initiative  - Coordinator |
/  \  | WWW URL: http://www.brics.dk/Projects/CoFI |
----   --------------------------------------------