Chapter 5

modeについて


5.1 mode

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

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


reserve A,B for Real;

C,D for Nat;

L:C=A+B;

......

D=A by...;

then C=D+B by L;

A,B が Real,C が Nat のときに,C=A+B と D=A が証明されたとします.ここで D=A という式を C=A+B に代入して,C=D+B by L とするとるとエラーになります.どうしてかというと,これは代入できるはずですが,D と B は mode が違うわけです.+ という演算子は Real に対してのみ定義されているのであって,Nat については定義されていないわけです.ですから,unknown functor というエラーになります.

このエラーは変数 D のmodeを拡張することにより解決することができます.Nat である D を,Real でもあることがいえればいいわけです.