[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] Minutes of the Language Design Group Meeting
Dear colleagues and friends,
sorry for the dealy due to Easter vacation, rush of new semester and a
silly virus (not PC, I'm afraid) ...
Best regards
Bernd
--------------------------------------------
Minutes of the Language Design Group Meeting, Amsterdam
Sunday, 28. March 1999
Markus Roggenbach and Bernd Krieg-Brückner
Participants
============
Hubert Baumeister - Michel Bidoit - Mark van den Brand -
Christine Choppy - Magne Haveraaen - Heinrich Hussmann - Hélène Kirchner -
Bernd Krieg-Brueckner - Heiko Mantel - Till Mossakowski - Peter Mosses -
Gianna Reggio - Markus Roggenbach - Don Sannella - Axel Schairer -
Pippo Scollo - P.S. Subramanian - Andrzej Tarlecki - Françoise Tort -
Martin Wirsing - Alexandre Zamulin.
The meeting was partially held as a joint meeting with the Tools Group.
Mixfix Ids
==========
Analysis proceeds in the following phases (tools may choose to overlap
some of them):
[Chars] -LexicalAnalysis-> [Lexemes] -ContextFreeSyntaxAnalysis->
[SyntaxTreeWithEmbeddedAtoms] -MixfixPatternCollection->
[SyntaxTreeWithEmbeddedAtoms] -MixfixGroupingAnalysis->
[ASTree] -StaticAnalysis,OverloadingResolution-> [ASTree+GlobalEnvironment]
The format of Lexemes and SyntaxTreeWithEmbeddedAtoms is internal to
tools (one would expect the latter to be almost the same as ASTree),
while ASTree, the output of the Lexical and Syntax Analysis phases, is
an Aterm as (to be) standardized by the Language Summary etc., as is the
GlobalEnvironment.
[the GlobalEnvironment issue (as defined in the Semantics) was discussed
at the Tools Group meeting. It is unclear, at the moment, how much about
it should be said in the Summary.]
As to the two proposals for mixfix ids, they are to be refined,
implemented and experimented with in the Amsterdam Parser
and the Bremen Parser
Discussion will proceed via Email, with the END OF MAY as deadline.
In the joint meeting with Tools it was discussed how to deal with
comments (and annotations), which are problematic if they can occur
anywhere. Peter Mosses has since proposed the following addition to Summary-Changes:
App. C.5, p. C-10:
It is unclear how to cope with the possibility of comments occurring
everywhere using standard parser-generators, when the comments are
not to be discarded by attached to abstract syntax trees. Should
the positions where comments may occur be (severely) restricted, as
foreseen for annotations?
[it is my, BKBs, hope that discussion via Email will resolve this issue
by the END OF MAY.]
Vote on the LaTeX-Formatting of CASL:
=====================================
Peter's proposals:
1) as now
2) keywords always bold
3) italic within atoms
4) structure keywords bold
As there was no clear consensus about this relatively minor issue, a
vote was taken (as an exception to the usual agreement by consensus):
first vote (multiple assents possible):
proposal | 1) | 2) | 3) | 4)
-------------------------------------
number of votes | 4 | 6 | 4 | 6
second vote (exclusive):
proposal | 2) | 4)
---------------------------
number of votes | 4 | 8
Thus the decision is to follow proposal 4).
Free Data Types
===============
The semantics group has discussed the theorem that
free type xxx
is equivalent to
free {type xxx}
under suitable restrictions. It was left to a decision
of the Language Design Group whether these restrictions
should be imposed in the Language Summary, or if they should
appear as side conditions to the theorem.
As was suggested by Heiko Mantel from DFKI Saarbruecken, it was decided to
leave out the condition from the Summary that total selectors must occur
for each alternative, and add it as a side condition to the above theorem.
Experience with the Inka 5.0 system that supports CASL [and the KIV
system]
shows that underspecification with total selectors (in FOL=, the total many-
sorted sublanguage of CASL) works fine.
All other conditions (modulo the necessary corrections) are left in the
Language Summary.
The proposal to add the above side side conditions to the theorem has
been
accepted - if there arise unpredicted problems with the semantics of
CASL,
the language design group has to make a new decision.
At the meeting, we actually agreed to follow the suggestion of the
Semantics meeting and require that the names of constructors and
selectors be distinct. However, it was realized after the meeting that
requiring selectors in free
datatype declarations to be distinct was too restrictive: one might
well want to use the same name (e.g., "left") for several selectors on
distinct constructors of the same data type (e.g., when specifying the
abstract syntax of CASL in CASL). Thus we would essentially revert to
the proposal in the Changes document, i.e. selectors and constructors
must not be in overloading relation with each other and the local environment.
The following amendment (for types without subsorts) is suggested:
Sect. 2.1.4.2, p. 15 - CHANGE MAY NOW READ AS FOLLOWS:
After the sentence starting:
This construct is only well-formed
insert:
Moreover, the declared sorts must be distinct from each other,
and from those declared in the local environment; also the
declared constructors and selectors must be distinct
(as qualified symbols) from each other.
(THE CHANGE PROPOSED FOR SECT. 4.1.2.1, P. 30 IS THEN STILL NEEDED AS
FORMULATED.)
Note L-11: Proposal of Some Annotations and Literal Syntax in CASL
==================================================================
The language design group discussed the proposed annotations of L-11
(presented by Till) with the following results (the names of the annotations
might still be improved):
a) Annotation "%cons":
The annotation "%cons" was accepted with the following two supplements
on its description in L-11:
-> the annotation is left associative
-> the annotation may not be used in case of an import (to prevent
recursion)
An annotation "%imply" was considered as a desirable alternative to
"%cons". While the annotation "%cons" may be followed by a whole
specification, the annotation "%imply" is followed by a list of axioms.
Michel was asked to present a proposal for such an annotation
"%imply".
b) Annotation "%def":
accepted.
Note: if the syntax is of a restricted form, then tools can statically
prove the assoc. proof obligation, e.g. as in the the HOL proof system.
c) Annotations on Operator Precedences:
The proposal of L-11 was accepted with the following supplement:
-> operator lists of more than one item are grouped by curly brackets.
d) Annotations on Associativity:
"%left assoc" and "%right assoc" were both accepted.
Extended Syntax for Literals:
Concerning the proposals of L-11 on extended syntax is was decided
that the extended syntax shall be part of the language summary. A new
proposal implementing the discussion of the meeting in Amsterdam has
now been worked out. It can be found at
http://www.informatik.uni-bremen.de/~cofi/LiteralExtension/literal.dvi
or [tex/ps/ps.gz]
Discussion will proceed via Email, with the END OF MAY as deadline.
The Extended Syntax for Literals will be incorporated in the language
summary eventually.
--
________________________________________________________________
Prof. Dr. Bernd Krieg-Brückner courier mail only:
Bremer Institut für Sichere Systeme MZH 8071
FB3 Mathematik und Informatik FB3
Universität Bremen Universität Bremen
Postfach 330 440 Bibliothekstr. 1
D-28334 Bremen D-28359 Bremen
Telefon: (+49) 421-218-3660 telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE privat: (+49) 421-25-1024
http://www.informatik.uni-bremen.de/~bkb, ~agbkb
http://www.uni-bremen.de/~sppraum (Kognitive Robotik)