3.2.2　notation部．constructors部

　新しい理論を作る際， 古い(ライブラリ中の)概念を使いたいときがあります． 例えばFunction とか Function-like という概念を使いたいとします．このとき， これらの用語はFUNC.VOC という vocabulary ファイルに登録されていますので， vocabulary 部に FUNC を加えます．また， これらの用語は FUNCT_1 の中で( MIZ 又は ABS ファイル )定義されていますので， notation 部に FUNCT-1 を加えます．そして， 多くの場合 constructors 部にも FUNCT_1 を加えます．
　例


　　　　environ
　　　　  vocabulary FUNC;
　　　　  notation FUNCT_1 ;
　　　　  constructors FUNCT_1 ;
　　　　begin
　　　　reserve X for Function;
　　　　theorem X is Function-like;


　notation 部と constructors 部の間の違いですが，昔の MIZAR のバージョンではsignature 部というのが1つだけあって， 両者は統合されていました．そこから概念間の階層構造等の関係と個々の概念の定義が， コンピュータのメモリに展開されました．しかし前者は重複する部分が多かった為， メモリの節約のために分離されたのです．前者はconstructors 部に入れることになりました．そのため， より包含的な構造をもつファイルがあれば， より小さい構造のファイルは constructors 部から省略でき， メモリの節約ができるようになったのです．例えば，上の例のかわりに，


　　　　environ
　　　　  vocabulary FUNC;
　　　　  notation FUNCT_1;
　　　　  constructors TOPREAL1 ;


　　　　begin
　　　　reserve X for Function;
　　　　theorem X is Function-like;


　としてもエラーは出ません，従って TOPREAL1 が constructors 部にあらかじめ入っている場合には，そこに FUNCT_1は入れなくてよいのです．
　最初は notation 部と constructors 部両方にファイル名を順に入れてゆき，完成後，よりベーシックなファイルを constructors 部から削ってみると環境部をより単純にすることができ， またメモリも節約できます．

　notation 部には， vocabulary ファイル中に書いたシンボルを使用したい場合， そのシンボルが定義されている article のファイル名を　ここに書いておきます．article の定義部( definition の部分 )では，そのシンボルの意味付けがなされています(どういうアーギュメントをいくつ持つのか，そのシンボル自身がどういうモードになるのか等)．

　例えば， article BOOLE と PRE_TOPC にはどちらにも∩ ( インターセクション )が定義されています(後者は再定義)．しかし， そのシンボルの使われ方が異なっているのです．

< article BOOLE >

definition
  let X,Y;
  func X /\ Y -> set means
  x c= it iff x in X & x in Y;
end;

< article PRE_TOPC >

definition
  let TP, P, Q;
  redefine
  func P /\ Q -> Subset of TP;
end;

　BOOLE での/\ (∩のこと）は，それ自身 set を意味し， アーギュメントとして set を両側に持ちます．
それに対して PRE_TOPC でのそれは，自分自身を TP ( トポロジカルスペース )のSubset とし， アーギュメントとして TP の Subset を両側に持ちます．
　/\を使った article をこれから書こうとする場合， それを set として使用したければnotation 部に BOOLE と書き， TP の Subset としたければ PRE_TOPC と書かなければいけません．