RE: Mizar Syntax

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

Dear Andrzej,

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.

Frode Odegard
Odegard Labs, Inc.
San Diego, Calif.
http://www.odegard.com

-----Original Message-----
From: owner-mizar-forum@mizar.uw.bialystok.pl
[mailto:owner-mizar-forum@mizar.uw.bialystok.pl]On Behalf Of Andrzej
Trybulec
Sent: Tuesday, December 08, 1998 5:47 AM
To: Mizar Forum
Subject: Mizar Syntax


We started recently to work on precise description of a superficial
level of the Mizar language (syntax and so on). It is mostly
the interface rather than the system. It is very important
for the practical reason, but rather dull.

I am not certain if mizar-forum is a proper list to send information
related (developer-forum might be better).
On the other hand, some members of mizar-forum might be interested,
so I want to compromise, the message related to intricacies ( :-))
of Mizar syntax will have the subject "Mizar Syntax". You are not
interested, do not read them, sorry.

==================================================

Here starts the substantial part of the message (you have been
warned).

It is a dogma that an Item in Mizar ends with semicolon (it is not
exactly the definition of an Item, because semicolons sometimes occur
inside an item), and every semicolon ends an Item.

An item sometimes includes a Block. A Block is a sequence of Items.
It usually starts with a specific reserved word ("proof", "now",
"case", "suppose") and sometimes ends with "end".

In this way we have a very rough description of a Mizar article.
We call it "Block & Items". It has no semantic meaning, of course.
It only facilitates the design of software.

An item may be a part of another item only if it occurs in a Block
that is a part of the (second) item.

Unfortunately the rule that "a Block may be part of another
Block only if it is a part of an Item that is a member of the (second)
Block" is false, as yet.

The Scheme is an exception.

It is an arbitrary decision that a Scheme is a Block. The reason is
that after such decision we have a rule that Labels are local in a Block.

But the syntax of the scheme is now like this:

  [ "scheme" ] Scheme-Body Justification ";"

and the Scheme is an Item on the level of the Text Proper, it means
that ";" ends this item. If a Scheme is a Block, it consists
of Items - at least one, in this case exactly one - and the Item
must end with a semicolon, so we need a second semicolon here.

So we decided (by "we" I mean mostly Bylinski and me) that
a Scheme is a Block (consisting of one Item) that is a part
of another Block (the Text Proper).

Nobody protested when I proposed the rule that a Scheme must be
justified by a Proof. However, I cheated (a bit), what I really want
is to omit the word "proof" and to have the syntax like:

  [ "scheme" ]
   Scheme-Body ";"
   Reasoning
  "end" ";"

Then the first semicolon ends the first item of the Block in
the Scheme, and the last semicolon ends the Scheme Item on the level
of the Text Proper.

Andrzej Trybulec