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 でもあることがいえればいいわけです．