RE: Mizar Syntax

["Frode L. Odegard" <frode@odegard.com>]

Hi Andrzej,

Happy new year to you too :)

I apologize if this is (also) an old question that has already been dealt
with, but have you also considered multiple concrete syntaxes?  For example,
ISO VDM-SL (a specification language used by computer scientists and
software engineers in the formal methods community) defines both an
ASCII syntax and a mathematical syntax; the latter includes various
mathematical symbols and is good for publishing, the former is better
suited to text editors, etc.  Because the semantics of VDM-SL is defined
over the abstract syntax there is a lot of flexibility as to what to do
with the concrete syntax.

Best wishes,


Frode L. Odegard

-----Original Message-----
From: owner-mizar-forum@mizar.uwb.edu.pl
[mailto:owner-mizar-forum@mizar.uwb.edu.pl]On Behalf Of Andrzej Trybulec
Sent: Saturday, January 02, 1999 5:13 AM
To: mizar-forum@mizar.uwb.edu.pl
Subject: RE: Mizar Syntax




On Mon, 28 Dec 1998, Frode L. Odegard wrote:

> Perhaps the best thing to do would be to start with an abstract
> syntax?  Once that has been nailed down, it is easier to discuss
> alternatives in the concrete syntax.
>

You are right, of course. Actually the message you had cited was related
to the work on abstract syntax. There are two different things:

1. The requirement that a scheme must be justified by a proof, that
   again may be split:
  1.1 An implementation restriction
  1.2 The abstract syntax
2. Concrete representation, e.g. what I wrote that eventually the word
  "proof" will be omitted.

However, we are quite concerned with the concrete syntax. Because of
two reasons:

1. For the user a comfortable syntax is more important that
   intricacies of semantics.
2. Semantics evolves faster than concrete syntax. (the same goes
   for natural languages).

Happy New Year,
Andrzej