Chapter 5

modeについて

5.1　mode

　次にmode (モード) についての話をします．Mizar には mode という概念があります．mode とは，Pascal (コンピュータ言語の一種)　などでの型　(タイプ)　に相当するもので，一般的な mode としては set があります．その他に代表的な mode として Nat, Real などがあり，またユーザーが mode を定義することができます．また mode は図の様に set (すべて)の中に Real (実数)があって，さらにその中に Nat (自然数)があるというふうに階層構造をなしています．そして，functor などは mode に従属しています．このことはプログラミング言語と似ています．なお set と Any は同じとみなされます.

　例えば，次のような例を考えてみます．ここでは + は Real についてのみ定義されているとします．

　　　　reserve A,B for Real;
　　　　　　　　　　　C,D for Function;
　　　　L:C=A+B:
　　　　　......
　　　　　D=A by...;
　　　　　then C=D+B by L;


　A,B が Real，C が Function のときに，C=A+B とD=A が証明されたとします．ここで D=A という式を C=A+B に代入して，C=D+B by L とするとるとエラーになります．どうしてかというと，これは代入できるはずですが，D と B は mode が違うわけです．+ という演算子は Real に対してのみ定義されているのであって，Function については定義されていないわけです．ですから，unknown functor というエラーになります．
　このエラーは変数 D の mode を拡張することにより解決することができます．Function である D を Real でもあることがいえればいいわけです．