Appendex 3 Grammer of THEAX

Page 1


         

 1000 ' ****************************************************              

 1010 ' *                                                  * 

 1020 ' *        SYNTAX OF THEAX LANGUAGE Ver.1.0          * 

 1030 ' *                                                  * 

 1040 ' ****************************************************

1050 '

1060 ' Symbol¥ means none or some spaces. Symbolž means one or some spaces
are necessary if there is no separator( [](),=:; ) in both sides.

1070 '

1080 '<text>::=<text.line><refered.block><text.body><end.text.line>|
<text.line><text.body><end.text.line>

1090 ' <text.line>::=¥Textž<text.name>¥;

1100 ' <text.name>::=<name>

1110 ' <name>::=\<c.name>

1120 ' <c.name>::=<name.symbol>|<name.symbol><c.name>

1130 ' <name.symbol> ::=A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|
T|U|V|W|X|Y|Z|a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|0|1|2|3|
4|5|6|7|8|9|.|/

1140 ' <end.text.line>::=¥End Text¥;

1150 ' <refered.block>::=<refered.ident.line><refered.text.name.block>
<refered.end.line>

1160 ' <refered.ident.line>::=¥Refered¥;

1170 ' <refered.text.name.block>::=<refered.name.line>|
<refered.name.line><refered.text.name.block>

1180 ' <refered.name.line>::=<r.text.name>¥;|<r.text.name>
<change.name.list>¥;

1190 ' <r.text.name>::=<name>

1200 ' <change.name.list>::¥(<change.terms>¥)

1210 ' <change.terms>::=<name.pair>|<name.pair>¥,
<change.terms>

1220 ' <name.pair>::=<old.name>œtoœ<newname>

1230 ' <old.name>::=<name>|¥L:<name>

1240 ' <new.name>::=<name>

1250 ' <refered.end.line>::=¥End Refered¥;

1260 ' <text.body>::=<text.block>|<text.block><text.body>

1270 '<text.block>::=<axiom.block>|<theorem.block>|<def.block>

1280 ' <axiom.block>::=<axiom.line><proper.name.list.line>
<formulae.line><condition.block><end.axiom.line>

1290 ' <axiom.line>::=¥Axiom¥;

1300 ' <proper.name.list.line>::=<proper.name>|<proper.name>
<proper.name.list.line>

1310 ' <proper.name>::=<name>

1320 ' <formulae.line>::=¥Formulae¥;

1330 ' <condition.block>::=<condition.line>|<condition.line>
<condition.block>

1340 ' <condition.line>::=<label>¥:<general.formula>¥;