Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/type.tex @ 77:50c2d2f1a186
Update chapter akasha
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Feb 2017 14:27:06 +0900 |
| parents | e9ff08a232f7 |
| children | 897fda8e39c5 |
| rev | line source |
|---|---|
| 28 | 1 \chapter{ラムダ計算と型システム} |
| 2 \label{chapter:type} | |
| 77 | 3 \ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。 |
| 4 しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。 | |
| 5 | |
| 6 そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。 | |
| 7 CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。 | |
| 8 証明を行なう機構として注目したのが型システムである。 | |
| 9 | |
| 10 \ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment を定義する。 | |
| 11 また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。 | |
| 12 | |
| 13 | |
| 28 | 14 しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。 |
| 15 CbC は直接自身を証明する機構が存在しない。 | |
| 16 プログラムの性質を証明するには CbC の形式的な定義が必須となる。 | |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
17 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
18 % {{{ 型システムとは |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
19 \section{型システムとは} |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
20 型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
21 ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
22 例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
23 % TODO: C の warning? |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
24 この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
25 加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
26 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
27 型システムで行なえることには以下のようなものが存在する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
28 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
29 \begin{itemize} |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
30 \item エラーの検出 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
31 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
32 文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
33 この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
34 多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
35 他にも、ある種のプログラムにとっては型は保守のためのツールともなる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
36 複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
37 |
| 31 | 38 \item 抽象化 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
39 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
40 型は大規模プログラムの抽象化の単位にもなる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
41 例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
42 モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
43 このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
44 |
| 31 | 45 \item ドキュメント化 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
46 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
47 型はプログラムを理解する際にも有用である。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
48 関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
49 また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
50 |
| 31 | 51 \item 言語の安全性 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
52 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
53 安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
54 例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
55 しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
56 より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
57 |
| 31 | 58 \item 効率性 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
59 |
| 74 | 60 そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける式の区別であった。 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
61 整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
62 型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
63 昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
64 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
65 \end{itemize} |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
66 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
67 型システムの定義には多くの定義が存在する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
68 型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
69 例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
70 これは Haskell が C言語よりも厳密な型システムを採用しているからである。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
71 具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
72 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
73 型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
74 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
75 % }}} |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
76 |
| 38 | 77 % {{{ 型無し算術式 |
| 34 | 78 \section{型無し算術式} |
| 79 まず、型システムやその性質について述べるためにプログラミング言語そのものの基本的な性質について述べる。 | |
| 40 | 80 プログラムの構文と意味論、推論について考えるために自然数とブール値のみで構成される小さな言語を扱いながら考察する。 |
| 34 | 81 この言語は二種類の値しか持たないが、項の帰納的定義や証明、評価、実行時エラーのモデル化を表現することができる。 |
| 82 | |
| 83 この言語はブール定数 $ true $ と $ false $ 、条件式、数値定数 0 、算術演算子 $ succ $ と $ pred $ 、判定演算子 $ iszero $ のみからなる。 | |
| 84 算術演算子 $ succ $ は与えられた数の次の数を返し、 $ pred $ はその前の数を返す。 | |
| 85 判定演算子$ iszero $ は与えられた項が 0 なら $ true $ を返し、それ以外は $ false $ を返す。 | |
| 86 これらを文法として定義すると以下のリスト\ref{src:expr-term}のようになる。 | |
| 87 | |
| 88 \lstinputlisting[label=src:expr-term, caption=算術式の項定義] {src/expr-term.txt} | |
| 89 | |
| 90 この定義では算術式の項 $ t $ を定義している。 | |
| 91 $ ::= $ は項の集合の定義を表であり、$ t $ は項の変数のようなものである。 | |
| 92 それに続くすべての行は、構文の選択肢である。 | |
| 93 構文の選択肢内に存在する記号 $ t $ は任意の項を代入できることを表現している。 | |
| 94 このように再帰的に定義することにより、 \verb/ if (ifzero (succ 0)) then true else (pred (succ 0)) / といった項もこの定義に含まれる。 | |
| 95 例において、 $ succ $ 、 $ pred $ 、 $ iszero $ に複合的な引数を渡す場合は読みやすさのために括弧でくくっている。 | |
| 96 括弧の定義は項の定義には含んでいない。 | |
| 97 コンパイラなど具体的な字句をパースする必要がある場合、曖昧な構文を排除するために括弧の定義は必須である。 | |
| 98 しかし、今回は型システムに言及するために曖昧な構文は明示的に括弧で指示することで排除し、抽象的な構文のみを取り扱うこととする。 | |
| 99 | |
| 100 現在、項と式という用語は同一である。 | |
| 101 型のような別の構文表現を持つ計算体系においては式はあらゆる種類の構文を表す。 | |
| 102 項は計算の構文的表現という意味である。 | |
| 103 | |
| 104 この言語におけるプログラムとは上述の文法で与えられた形からなる項である。 | |
| 105 評価の結果は常にブール定数か自然数のどちらかになる。 | |
| 106 これら項は値と呼ばれ、項の評価順序の形式化において区別が必要となる。 | |
| 107 | |
| 108 なお、この項の定義においては \verb/succ true/ といった怪しい項の形成を許してしまう。 | |
| 109 実際、これらのプログラムは無意味なものであり、このような項表現を排除するために型システムを利用する。 | |
| 110 | |
| 111 ある言語の構文を定義する際に、他の表現かいくつか存在する。 | |
| 112 先程の定義は次の帰納的な定義のためのコンパクトな記法である。 | |
| 113 | |
| 114 \begin{definition} | |
| 115 項の集合とは以下の条件を満たす最小の集合 $ T $ である。 | |
| 116 \begin{eqnarray*} | |
| 117 \label{eq:expr} | |
| 118 \{true , false , 0\} \subseteq T \\ | |
| 119 t_1 \in T ならば \{succ \; t_1 , pred \; t_1 , iszero \; t_1\} \subseteq T \\ | |
| 120 t_1 \in T かつ t_2 \in T かつ t_3 \in T ならば if \; t_1 \; then \; t_2 else \; t_3 \subseteq T | |
| 121 \end{eqnarray*} | |
| 122 \end{definition} | |
| 123 | |
| 124 まず1つめの条件は、$ T $ に属する3つの式を挙げている。 | |
| 125 2つめと3つめの条件は、ある種の複合的な式が $ T $ に属することを判断するための規則を表している。 | |
| 126 最後の「最小」という単語は $ T $ がこの3つの条件によって要求される要素以外の要素を持たないことを表している。 | |
| 127 | |
| 128 また、項の帰納的表現の略記法として、二次元の推論規則形式を用いる方法もある。 | |
| 129 これは論理体系を自然演繹スタイルで表現するためによく使われる。 | |
| 74 | 130 自然演繹による証明は\ref{chapter:agda}章内で触れるが、今回は項表現として導入する。 |
| 34 | 131 |
| 132 \begin{definition} | |
| 36 | 133 項の集合は次の規則によって定義される。 |
| 134 | |
| 135 \begin{prooftree} | |
| 136 \AxiomC{$ true \in T $} | |
| 137 \end{prooftree} | |
| 138 | |
| 139 \begin{prooftree} | |
| 140 \AxiomC{$ false \in T $} | |
| 141 \end{prooftree} | |
| 142 | |
| 143 \begin{prooftree} | |
| 144 \AxiomC{$ 0 \in T $} | |
| 145 \end{prooftree} | |
| 146 | |
| 147 \begin{prooftree} | |
| 148 \AxiomC{$ t_1 \in T $} | |
| 149 \UnaryInfC{$ succ \; t_1 \in T$} | |
| 150 \end{prooftree} | |
| 151 | |
| 152 \begin{prooftree} | |
| 153 \AxiomC{$ t_1 \in T $} | |
| 154 \UnaryInfC{$ pred \; t_1 \in T$} | |
| 155 \end{prooftree} | |
| 156 | |
| 157 \begin{prooftree} | |
| 158 \AxiomC{$ t_1 \in T $} | |
| 159 \UnaryInfC{$ iszero \; t_1 \in T$} | |
| 160 \end{prooftree} | |
| 161 | |
| 162 \begin{prooftree} | |
| 163 \AxiomC{$ t_1 \in T $} | |
| 164 \AxiomC{$ t_2 \in T $} | |
| 165 \AxiomC{$ t_3 \in T $} | |
| 166 \TrinaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \in T$} | |
| 167 \end{prooftree} | |
| 168 | |
| 34 | 169 \end{definition} |
| 170 | |
| 36 | 171 最初の$ true, \; false, \; 0 $の3つ規則は再帰的定義の1つめの条件と同じである。 |
| 172 それ以外の4つの規則は再帰的定義の2つめと3つめの条件と同じである。 | |
| 173 それぞれの規則は「もし線の上に列挙して前提が成立するのならば、線の下の結論を導出できる」と読む。 | |
| 174 $ T $ がこれらの規則を満たす最小の集合である事実は明示的に述べられない。 | |
| 175 | |
| 176 言語の構文は定義できたので、次は項がどう評価されるかの意味論について触れていく。 | |
| 177 意味論の形式化には操作的意味論や表示的意味論、公理的意味論やゲーム意味論などがあるが、ここでは操作的意味論について述べる。 | |
| 178 操作的意味論とは、言語の抽象機械を定義することにより言語の振舞いを規程する。 | |
| 179 この抽象機械が示す抽象とは、扱う命令がプロセッサの命令セットなどの具体的なものでないことを表している。 | |
| 180 単純な言語の抽象機械における状態は単なる項であり、機械の振舞いは遷移関数で定義される。 | |
| 181 この関数は各状態において項の単純化ステップを実行して次の状態を与えるか、機械を停止させる。 | |
| 182 ここで項 $ t $ の意味は、$ t $ を初期状態として動き始めた機械が達する最終状態である。 | |
| 183 | |
| 184 なお、一つの言語に複数の操作的意味論を与えることもある。 | |
| 185 例えば、プログラマが扱う項に似た機械状態を持つ意味論の他に、コンパイラの内部表現やインタプリタが扱う意味論を定義する。 | |
| 186 これらの振舞いが同じプログラムを実行した時に何かしらの意味であれば、結果としてその言語の実装の正しさを証明することに繋がる。 | |
| 187 | |
| 188 まずはブール式のみの操作的意味論を定義する。 | |
| 189 | |
| 190 \begin{definition} | |
| 37 | 191 ブール値(B) |
| 36 | 192 |
| 38 | 193 項 |
| 36 | 194 \begin{align*} |
| 195 t ::= && \text{項} \\ | |
| 196 true && \text{定数真} \\ | |
| 197 false && \text{定数偽} \\ | |
| 198 if \; t \; then \; t \; else \; t && \text{条件式} | |
| 199 \end{align*} | |
| 200 | |
| 201 値 | |
| 202 \begin{align*} | |
| 203 v ::= && \text{値} \\ | |
| 204 true && \text{真} \\ | |
| 205 false && \text{偽} | |
| 206 \end{align*} | |
| 207 | |
| 208 評価 | |
| 209 \begin{align*} | |
| 210 if \; true \; then \; t_2 \; else t_3 \rightarrow t_2 && \text{(E-IFTRUE)} \\ | |
| 211 if \; false \; then \; t_2 \; else t_3 \rightarrow t_3 && \text{(E-IFFALSE)} \\ | |
| 212 \AxiomC{$ t_1 \rightarrow t_1'$} | |
| 213 \UnaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \rightarrow if \; t_1' \; then t_2 \; else \;t_3 $} | |
| 214 \DisplayProof | |
| 215 && \text{(E-IF)} | |
| 216 \end{align*} | |
| 37 | 217 |
| 218 \end{definition} | |
| 219 | |
| 220 評価の最終結果になりえる項である値は定数 $ true $ と $ false $ のみである。 | |
| 221 評価の定義は評価関係の定義である。 | |
| 222 評価関係 $ t \rightarrow t' $ は「$ t $ が1ステップで $ t' $ に評価される」と読む。 | |
| 223 直感的には抽象機械の状態が $ t $ ならば $ t' $ が手に入るという意味である。 | |
| 224 | |
| 225 評価関係は3つあるが、2つは前提を持たないため、2つの公理と1つの規則から成る。 | |
| 226 1つめの規則 E-IFTRUE の意味は、評価の対象となる項の条件式が定数 $ true $ である時に、then 節にある $ t_2 $ を残して他の全ての項を捨てるという意味である。 | |
| 227 E-EIFFALSE も同様に条件式が $ false $ の時に $ t_3 $ のみを残す。 | |
| 228 3つ目の規則 E-IF は条件式の評価である。 | |
| 229 条件式 $ t $ が $ t'$ に評価されうるのならば then 節と else 節を変えずに条件部のみを評価する。 | |
| 230 | |
| 231 評価の定義から分かることの中に、if の中の then節 と else 節は条件部より先に評価されないことがある。 | |
| 232 よって、この言語は条件式の評価に対し条件部から評価が優先されるという評価戦略を持つことが分かる。 | |
| 233 | |
| 234 \begin{definition} | |
| 235 推論規則のインスタンスとは、規則の結論や前提に対し、一貫して同じ項による書き換えを行なったものである。 | |
| 236 \end{definition} | |
| 237 | |
| 238 例えば、 | |
| 47 | 239 $ if \; true \; then \; true \; else \; ( \;if \; false \; then \; false \; else \; false) $ |
| 240 は E-IFTRUE のインスタンスであり、 E-IFTRUEの $ t_2 $ が \verb/true/ かつ、 | |
| 241 $ t_3 $ が $ if \; false \; then \; false \; else \; false \;$ の時に相当する。 | |
| 37 | 242 |
| 243 \begin{definition} | |
| 244 1ステップ評価関係 $ \rightarrow $ とは、3つの評価の規則を満たす、項に関する最小の二項関係である。 | |
| 245 $ (t, \; t') $ がこの関係の元である時、「評価関係式 $ t \rightarrow t'$ は導出可能である」と言う。 | |
| 36 | 246 \end{definition} |
| 247 | |
| 37 | 248 ここで「最小」という言葉が表れるため、評価関係式 $ t \rightarrow t'$ が導出可能である時かつその時に限り、その関係式は規則によって正当化される。 |
| 249 すなわち評価関係式は公理 E-IFTRUE か E-IFFALSE 、前提が成り立つ時の E-IF のインスタンスとなる。 | |
| 250 与えられた評価関係式が導出可能であることを証明するには、葉が E-IFTRUE か E-IFFALSE であり、内部ノードのラベルが E-IF のインスタンスである導出木が示せれば良い。 | |
| 251 例えば以下の略記の元 $ if \; t \; then \; false \; then \; false \rightarrow if \; u \; then \; false \; else \; false $ の導出可能性は以下のような導出木によって示せる。 | |
| 36 | 252 |
| 37 | 253 \begin{itemize} |
| 254 \item $ s = if \; true \; then \; false \; else \; false $ | |
| 255 \item $ t = if \; s \; then \; true \; else \; true $ | |
| 256 \item $ u = if \; false \; then \; true \; else \; true $ | |
| 257 \end{itemize} | |
| 258 | |
| 259 | |
| 260 \begin{prooftree} | |
| 261 \AxiomC{} | |
| 262 \RightLabel{E-IFTRUE} | |
| 263 \UnaryInfC{ $ s \rightarrow true $ } | |
| 264 \RightLabel{E-IF} | |
| 265 \UnaryInfC{ $ t \rightarrow u $} | |
| 266 \RightLabel{E-IF} | |
| 267 \UnaryInfC{ $ if \; t \; then \; false \; then \; false/ \rightarrow if \; u \; then \; false \; else \; false $} | |
| 268 \end{prooftree} | |
| 269 | |
| 270 1ステップ評価関係は与えられた項に対して抽象機械の状態遷移を定義する。 | |
| 271 この時、機械がそれ以上ステップを進められない時にそれが最終結果となる。 | |
| 272 | |
| 273 \begin{definition} | |
| 274 正規形 | |
| 275 | |
| 276 項 $ t $ が正規形であるとは、$ t \rightarrow t'$となる評価規則が存在しないことである。 | |
| 277 \end{definition} | |
| 278 | |
| 279 この言語において $ true $ や $ false $ は正規形である。 | |
| 280 逆に言えば、構文的に正しい if が用いられている場合は評価することが可能なため正規形ではない。 | |
| 281 極端に言えばこの言語における全ての値は正規形なのである。 | |
| 282 しかし、他の言語における値は一般的に正規形ではない。 | |
| 283 実のところ、値でない正規形は実行時エラーとなって表れる。 | |
| 284 | |
| 40 | 285 実際にこの言語に自然数を導入し、値では無い正規形を確認していく。 |
| 34 | 286 |
| 287 | |
| 38 | 288 \begin{definition} |
| 289 算術式BN (B の拡張) の項 | |
| 290 \begin{align*} | |
| 291 t ::= && \text{項} \\ | |
| 292 true && \text{定数真} \\ | |
| 293 false && \text{定数偽} \\ | |
| 294 if \; t \; then \; t \; else \; t && \text{条件式} \\ | |
| 295 0 && \text{定数ゼロ} \\ | |
| 296 succ \; t && \text{後者値} \\ | |
| 297 pred \; t && \text{前者値} \\ | |
| 298 iszero \; t && \text{ゼロ判定} | |
| 299 \end{align*} | |
| 300 \end{definition} | |
| 301 | |
| 302 \begin{definition} | |
| 303 算術式BN の値 | |
| 304 \begin{align*} | |
| 305 v ::= && \text{値} \\ | |
| 306 true && \text{真} \\ | |
| 307 false && \text{偽} \\ | |
| 308 nv && \text{数値} \\ | |
| 309 \end{align*} | |
| 310 \end{definition} | |
| 311 | |
| 312 \begin{definition} | |
| 313 算術式BNの数値 | |
| 314 \begin{align*} | |
| 315 nv ::= && \text{数値} \\ | |
| 316 0 && \text{ゼロ} \\ | |
| 317 succ nv && \text{後者値} | |
| 318 \end{align*} | |
| 319 \end{definition} | |
| 320 | |
| 321 \begin{definition} | |
| 322 算術式BNの評価($ t \rightarrow t' $) | |
| 323 \begin{align*} | |
| 324 if \; true \; then \; t_2 \; else t_3 \rightarrow t_2 && \text{(E-IFTRUE)} \\ | |
| 325 if \; false \; then \; t_2 \; else t_3 \rightarrow t_3 && \text{(E-IFFALSE)} \\ | |
| 326 \AxiomC{$ t_1 \rightarrow t_1'$} | |
| 327 \UnaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \rightarrow if \; t_1' \; then t_2 \; else \;t_3 $} | |
| 328 \DisplayProof && \text{(E-IF)} \\ | |
| 329 \AxiomC{$ pred \; 0 \rightarrow 0$} | |
| 330 \DisplayProof && \text{(E-PREDZERO)} \\ | |
| 331 \AxiomC{$ pred \; (succ \; nv_1) \rightarrow nv_1$} | |
| 332 \DisplayProof && \text{(E-PREDSUCC)} \\ | |
| 333 \AxiomC{$ t_1 \rightarrow t_1'$} | |
| 334 \UnaryInfC{$ pred \; t_1 \rightarrow pred \; t_1'$} | |
| 335 \DisplayProof && \text{(E-PRED)} \\ | |
| 336 \AxiomC{$ iszero \; 0 \rightarrow true$} | |
| 337 \DisplayProof && \text{(E-ISZEROZERO)} \\ | |
| 338 \AxiomC{$ iszero \; (succ \; nv_1) \rightarrow false$} | |
| 339 \DisplayProof && \text{(E-ISZEROSUCC)} \\ | |
| 340 \AxiomC{$ t_1 \rightarrow t_1'$} | |
| 341 \UnaryInfC{$ iszero \; t_1 \rightarrow iszero \; t_1'$} | |
| 342 \DisplayProof && \text{(E-ISZERO)} \\ | |
| 343 \end{align*} | |
| 344 \end{definition} | |
| 345 | |
| 346 今回値の定義に数値を表す構文要素が追加されている。 | |
| 347 数は0かある数に後者関数を適用したもののどちらかである。 | |
| 348 評価規則 E-PREDZERO、E-PREDSUCC、E-ISZEROZERO、E-ISZEROSUCC は演算 \verb/pred/ と \verb/iszero/ が数に適用された時にどう振る舞うかを定義している。 | |
| 349 E-SUCC 、 E-PRED 、 E-ISZERO の合同規則も E-IF のように部分項から先に評価することを示している。 | |
| 350 | |
| 351 数値の構文要素(nv)はこの定義によって重要な役割をはたす。 | |
| 352 例えば、 E-PREDSUCC 規則が適用できる項は任意の項 $ t $ ではなく数値 $nv_1$である。 | |
| 353 これは $ pred \; (succ \; (pred \; 0)) $ を $ pred 0 $ に評価できないことを意味する。 | |
| 354 なぜなら $ pred \; 0 $ は数値に含まれないからである。 | |
| 355 | |
| 356 ここで言語の操作的意味論について考える時、すべての項に関する振舞いを定義する必要がある。 | |
| 357 すべての項には $ pred \; 0 $ や $ succ false $ のような項も含まれる。 | |
| 358 しかし、 $ succ $ を $ false $ に適用する評価結果は定義されていないため、 $ succ \; false $ は正規形である。 | |
| 359 このような、正規形であるが値でない項は行き詰まり状態であるという。 | |
| 360 つまり、実行時エラーとは行き詰まり状態の項を指す。 | |
| 361 直感的な解釈としてはプログラムが無意味な状態になったこと示しておい、操作的意味論が次に何も行なえないことを特徴付けているのである。 | |
| 362 プログラング言語において実行時エラーはセグメンテーションフォールトや不正な命令などいくつかのものが挙げられるが、型システムを考える際にはこれらのエラーは行き詰まり状態という単一の概念で表す。 | |
| 363 | |
| 364 % }}} | |
| 34 | 365 |
| 41 | 366 % {{{ 単純型 |
| 367 | |
| 40 | 368 \section{単純型} |
| 369 先程定義した算術式には $ pred \; false $ のようなこれ以上評価できない行き詰まり状態が存在する。 | |
| 370 項を実際に評価する前に評価が行き詰まり状態にならないことを保証したい。 | |
| 371 そのために、自然数に評価される項とブール値に評価される項とを区別する必要がある。 | |
| 372 項を分類するために2つの型 Nat と Bool を定義する。 | |
| 373 | |
| 374 ここで、項$t$が型 $T$を持つ、という表現を用いた場合、$t$を評価した結果が明らかに適切な形の値になることを意味する。 | |
| 375 明らかに、という意味は項を実行することなく静的に分かるという意味である。 | |
| 376 例えば項 $ if \; true \; then \; false \; else \; true $ は Bool 型を持ち、$ pred \; (succ \; (succ \; 0)) $ はNat 型を持つ。 | |
| 377 しかし、項の型の分析は保守的であり、$ if \; true \; then \; 0 \; else \; false $ のような項は実際には行き詰まりにならないが型を持てない。 | |
| 378 | |
| 379 算術式のための型付け関係は $ t : T $ と書き、項に型を割り当てる推論規則の集合によって定義される。 | |
| 380 具体的な数値とブール値に関する拡張は以下である。 | |
| 381 | |
| 382 \begin{definition} | |
| 383 NB(型付き) の新しい構文形式 | |
| 384 \begin{align*} | |
| 385 T ::= && \text{型 :} \\ | |
| 386 Bool && \text{ブール型} \\ | |
| 387 Nat && \text{自然数型} \\ | |
| 388 \end{align*} | |
| 389 \end{definition} | |
| 390 | |
| 391 | |
| 392 \begin{definition} | |
| 393 NB(型付き)の型付け規則 | |
| 394 \begin{align*} | |
| 395 true : Bool && \text{T-TRUE} \\ | |
| 396 false : Bool && \text{T-FALSE} \\ | |
| 397 \AxiomC{$t_1 : Bool$} | |
| 398 \AxiomC{$t_2 : T$} | |
| 399 \AxiomC{$t_3 : T$} | |
| 400 \TrinaryInfC{$if \; t_1 \; then \; t_2 \; else \; t_3 : T$} | |
| 401 \DisplayProof && \text{T-IF} \\ | |
| 402 0 : Nat && \text{T-ZERO} \\ | |
| 403 \AxiomC{$t_1 : Nat$} | |
| 404 \UnaryInfC{$ succ \; t_1 : Nat $} | |
| 405 \DisplayProof && \text{T-SUCC} \\ | |
| 406 \AxiomC{$t_1 : Nat$} | |
| 407 \UnaryInfC{$ pred \; t_1 : Nat $} | |
| 408 \DisplayProof && \text{T-PRED} \\ | |
| 409 \AxiomC{$t_1 : Nat$} | |
| 410 \UnaryInfC{$ iszero \; t_1 : Bool $} | |
| 411 \DisplayProof && \text{T-BOOL} | |
| 412 \end{align*} | |
| 413 \end{definition} | |
| 414 | |
| 415 T-TRUE と T-FALSE はブール定数に Bool 型を割り当てている。 | |
| 416 T-IFは条件式の部分にBool型を、部分式に関しては同じ型を要求している。 | |
| 417 これは同じ変数 $ T $ を二回使用することで制約を表している。 | |
| 418 | |
| 419 また、数に関しては T-ZERO は Nat 型を $ 0 $ に割り当てている。 | |
| 420 T-SUCC と T-PRED は $ t_1 $ が Nat である時に限り Nat 型となる。 | |
| 421 同様に、 T-ISZERO は $ t_1 $ が Nat である時に Bool となる。 | |
| 422 | |
| 423 \begin{definition} | |
| 424 算術式のための型付け関係とは、NBにおける規則のすべてのインスタンスを満たす、項と型の二項関係である。 | |
| 425 項$ t $ に対してある型 $ T $ が存在して $ t : T $ である時、 $ t $ は型付け可能である(または正しく型付けされている)という。 | |
| 426 \end{definition} | |
| 427 | |
| 41 | 428 型推論をを行なう時、$succ t_1$という項が何らかの型を持つならばそれは Nat 型である、といった言及を行なう。 |
| 429 型付け関係を逆転させた補題を定義することで型推論の基本的なアルゴリズムを考えることができる。 | |
| 430 なお、逆転補題は型付け関係の定義により直ちに成り立つ。 | |
| 431 | |
| 432 \begin{lemma} | |
| 433 型付け関係の逆転 | |
| 434 \begin{enumerate} | |
| 435 \item $ true : R $ ならば $ R = Bool $ である | |
| 436 \item $ false : R $ ならば $ R = Bool $ である | |
| 437 \item $ if \; t_1 \; then \; t_2 \; else \; t_3 : R $ ならば $ t_1 : Bool $ かつ $ t_2 : R $ かつ $ t_3 : R $ である。 | |
| 438 \item $ 0 : R $ ならば $ R = Nat $ である | |
| 439 \item $ succ \; t_1 : R $ ならば $ R = Nat $ かつ $ t_1 : Nat $ である | |
| 440 \item $ pred \; t_1 : R $ ならば $ R = Nat $ かつ $ t_1 : Nat $ である | |
| 441 \item $ iszero \; t_1 : R $ ならば $ R = Bool $ かつ $ t_1 : Nat $ である | |
| 442 \end{enumerate} | |
| 443 \end{lemma} | |
| 444 | |
| 445 逆転補題は型付け関係のための生成補題と呼ばれることもある。 | |
| 446 なぜならば、与えられた型付け判断式に対してその証明がどのように生成されたかを示すからである。 | |
| 447 | |
| 40 | 448 型無し算術式の評価導出のように型付けも導出可能であり、それも規則のインスタンスの木である。 |
| 449 型付け関係に含まれる二つ組 $(t, \; T)$は $ t : T $ を結論とする型付け導出により正当化される。 | |
| 450 例えば $ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat $ の型付け判断の導出木である。 | |
| 451 | |
| 452 \begin{prooftree} | |
| 453 \AxiomC{} | |
| 454 \RightLabel{T-ZERO} | |
| 455 \UnaryInfC{$ 0 : Nat$} | |
| 456 \RightLabel{T-ISZERO} | |
| 457 \UnaryInfC{$ iszero \; 0 : Bool$} | |
| 458 \AxiomC{} | |
| 459 \RightLabel{T-ZERO} | |
| 460 \UnaryInfC{$ 0 : Nat$} | |
| 461 \AxiomC{} | |
| 462 \RightLabel{T-ZERO} | |
| 463 \UnaryInfC{$ 0 : Nat$} | |
| 464 \RightLabel{T-PRED} | |
| 465 \UnaryInfC{$ pred \; 0 : Bool$} | |
| 466 \RightLabel{T-IF} | |
| 467 \TrinaryInfC{ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat } | |
| 468 \end{prooftree} | |
| 469 | |
| 41 | 470 項その型付けの定義より、型システムが行き詰まり状態にならないことを示す。 |
| 471 その証明は指向定理と保存定理によって証明する。 | |
| 472 | |
| 473 \begin{itemize} | |
| 474 \item 進行とは、正しく型付けされた項は行き詰まり状態では無いことである | |
| 475 \item 保存とは、評価可能な正しく型付けされた項は評価後も正しく型付けされていることである。 | |
| 476 \end{itemize} | |
| 477 | |
| 478 型システムがこれらの性質を持つ時、正しく型付けされた項は行き詰まり状態になりえない。 | |
| 479 | |
| 480 進行定理の証明の為に Bool 型と Nat 型の標準形(それらの型を持つ正しく型付けされた値)を示す。 | |
| 481 | |
| 482 \begin{lemma} | |
| 483 標準形 | |
| 484 | |
| 485 \begin{enumerate} | |
| 486 \item $ v $ が $Bool$ 型の値ならば $v$ は $true$ または $false$ である。 | |
| 487 \item $v$ が $Nat$ 型の値ならば、$0$ もしくは $Nat$ に対して $succ$ を適用した値である。 | |
| 488 \end{enumerate} | |
| 489 \end{lemma} | |
| 490 | |
| 491 標準形の証明に関しては値における構造的帰納法を用いる。 | |
| 492 この言語における値とは $ true $ と $false $ と $ 0$ と $ succ \; nv$ のいずれかの形をしている。 | |
| 493 Bool型に関して注目した時、 $ true $ と $ false $ は定義によって正しい。 | |
| 494 $ 0 $ と $ succ \; nv $ に関しては逆転補題より Nat 型を持つため、Bool型を持つ値は $ true $ と $ false $ のどちらかとなる。 | |
| 495 Nat についても同様である。 | |
| 496 | |
| 497 \begin{theorem} | |
| 498 進行 | |
| 499 | |
| 500 $ t$ が正しく型付けされたと仮定すると、$ t$ は値であるか、またはある $t'$ が存在して$ t \rightarrow t' $ となる。 | |
| 501 \end{theorem} | |
| 502 | |
| 503 証明は $ t : T $ の導出に関する帰納法による。 | |
| 504 T-TRUE 、 T-FALSE 、 T-ZERO の場合は$t$が値であることより成立する。 | |
| 505 | |
| 506 T-IF の場合、帰納法の仮定により $ t1 $ は値であるか、$t_1'$ が存在して $ t_1 \rightarrow t_1'$ を満たす。 | |
| 507 $ t_1 $ が値ならば、標準形補題により $ true $ か $ false $ であり、その場合は E-IFTRUE か E-IFFALSE が適用可能である。 | |
| 508 一方 $ t_1 \rightarrow t_1' $ ならば E-IF が適用できる。 | |
| 509 | |
| 510 T-SUCC の場合も帰納法の仮定により $ t1 $ は値であるか、$t_1'$ が存在して $ t_1 \rightarrow t_1'$ を満たす。 | |
| 511 $ t_1 $ が値ならば標準形補題により数値でなければならず、その場合 $ t $ も数値であるため成り立つ。 | |
| 512 一方 $ t_1 \rightarrow t_1' $ ならば E-SUCC が適用できる。 | |
| 513 | |
| 514 T-SUCC の場合も同様で、 $ t_1 $ が値ならば標準形補題により数値でなければならず、その場合 E-PREDZERO か E-PREDSUCC が使える。 | |
| 515 $ t_1 \rightarrow t_1' $ ならば E-PRED が適用できる。 | |
| 516 | |
| 517 T-ISZERO の場合も値ならば標準形補題により $ t_1 $ は数値であり、どちらの場合でも E-ISZEROZERO と E-ISZEROSUCC が適用できる。 | |
| 518 $ t_1 \rightarrow t_1' $ ならば E-ISZERO が適用できる。 | |
| 519 | |
| 520 \begin{theorem} | |
| 521 保存 | |
| 522 | |
| 523 $ t : T $ かつ $ t \rightarrow t' $ ならば $ t' : T $ となる。 | |
| 524 \end{theorem} | |
| 525 | |
| 526 保存定理も $ t : T $ の導出に関する帰納法によって導ける。 | |
| 527 帰納法の各ステップにおいて全ての部分導出に関して所望の性質が成り立つと仮定し、導出の最後の規則についての場合分けで証明を行なう。 | |
| 528 | |
| 529 導入の最後の規則がT-TRUE の場合、その規則の形から $ t $ は定数 $ true $ でなければならず、 $ T $ は $ Bool$ となる。 | |
| 530 そして $ t $ は値であるためにどのような $ t' $ も存在せず、定理の要求は満たされる。 | |
| 531 T-FALSE と T-ZERO の場合も同様である。 | |
| 532 | |
| 533 導入の最後の規則 T-IF の場合は、$ t $ はある $ t_1, \; t_2 \; t_3 $ に対して $ if \; t_1 then t_2 else t_3 $ という形となる。 | |
| 534 さらに $ t_1 : Bool $ と $ t_2 : T $ と $ t_3 : T $ となる部分導出がある。 | |
| 535 ここで if を持つ評価規則において $ t \rightarrow t'$ を導入できる規則は E-IFTRUE と E-IFFALSE と E-IF のみである。 | |
| 536 それぞれの場合について別々に場合分けをして考える。 | |
| 537 | |
| 538 \begin{itemize} | |
| 539 \item E-IFTRUE の場合(E-IFFALSE も同様) | |
| 540 | |
| 541 $ t \rightarrow t' $ が E-IFTRUE を使った導出ならば、 $ t_1$ は $ true $ であり、結果の項 $ t' $ は $ t_2 $ となる。 | |
| 542 このことより $ t_2 : T $ であることが分かるため、条件を満たす。 | |
| 543 | |
| 544 \item E-IF の場合 | |
| 545 | |
| 546 場合分け T-IF の仮定より $ t_1 : Bool $が結論となる、部分導出が得られる。 | |
| 547 帰納法の仮定を部分導出に適用して $ t_1' : Bool $ とし、 $ t_2 : T $ と $ t_3 : T $ を合わせると規則 T-IF が適用できる。 | |
| 548 T-IF を適用すると $ if \; t_1' \; then \; t_2 \; else \; t_3$となり、$ t' : T $ が成り立つ。 | |
| 549 \end{itemize} | |
| 550 | |
| 551 T-SUCC が導入の最後であれば、 $ t \rightarrow t'$ を導くためには E-SUCC のみであり、この形から $ t_1 \rightarrow t_1'$が分かる。 | |
| 552 $ t_1 : Nat $ であることも分かるため、帰納法の仮定より $ t_1' : Nat $ が得られる。 | |
| 553 この時 T-SUCC が適用できるため $ succ \; t_1 : Nat$となって $ t' : T $ が成り立つ。 | |
| 554 T-PRED も同様である。 | |
| 555 | |
| 556 % }}} | |
| 40 | 557 |
| 32 | 558 % {{{ 型なしラムダ計算 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
559 \section{型なしラムダ計算} |
| 38 | 560 計算とは何か、エラーとは何か、を算術式を定義することによって示してきた。 |
| 41 | 561 また、型を導入することにより行き詰まり状態を回避することも示した。 |
| 38 | 562 ここで、プログラミング言語における計算を形式的に定義していく。 |
| 74 | 563 プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した~\cite{Landin64}。 |
| 38 | 564 この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算であった。 |
| 74 | 565 ラムダ計算は Alonzo Church が発明した形式的体系の一つである~\cite{GlossarWiki:Church:1941}。 |
| 31 | 566 ラムダ計算では全ての計算が関数定義と関数適用の基本的な演算に帰着される。 |
| 567 ラムダ計算はプログラミング言語の機能の仕様記述や、言語設計と実装、型システムの研究に多く使われている。 | |
| 568 この計算体系の重要な点は、ラムダ計算内部で計算が記述できるプログラミング言語であると同時に、それ自身について厳格な証明が可能な数学的対象としてみなせる点にある。 | |
| 28 | 569 |
| 31 | 570 ラムダ計算はいろいろな方法で拡張できる。 |
| 571 数や組やレコードなどはラムダ計算そのもので模倣することができるが、記述が冗長になってしまう。 | |
| 572 それらの機能のための具体的な特殊構文を加えることは言語の利用者の視点で便利である。 | |
| 573 他にも書き換え可能な参照セルや非局所的な例外といった複雑な機能を表現することもできるが、膨大な変換を用いなければモデル化できない。 | |
| 74 | 574 それの機能を言語として備えた拡張に ML や Haskell~\cite{haskell-sigplan} といったものがある。 |
| 31 | 575 |
| 576 ラムダ計算(または $ \lambda $ 計算) とは、関数定義と関数適用を純粋な形で表現する。 | |
| 577 ラムダ計算においてはすべてが関数である。 | |
| 578 関数によって受け付ける引数も関数であり、関数が返す結果もまた関数である。 | |
| 579 | |
| 580 ラムダ計算の項は変数と抽象と適用の3種類の項からなり、以下の文法に要約される。 | |
| 581 変数 $ x $ は項であり、項 $ t_1 $ から変数 $ x $ を抽象化した $ \lambda x . t_1 $ も項であり、項 $ t_1 $ を他の項 $ t_2 $ に適用した $ t_1 t_2 $ も項である。 | |
| 582 | |
| 583 \begin{multline*} | |
| 584 t ::= \\ | |
| 585 x \\ | |
| 586 \lambda x . t \\ | |
| 587 t \, t \\ | |
| 588 \end{multline*} | |
| 589 | |
| 590 ラムダ計算において関数適用は左結合とする。 | |
| 591 つまり、 $ s \, t \, u $ は $ (s \, t) \, u $ となる。 | |
| 592 | |
| 593 また、抽象の本体はできる限り右側へと拡大する。 | |
| 47 | 594 例えば $ \lambda x . \; \lambda y . \; x \, y \, x $ は$ \lambda x . (\lambda . y ((x \, y) \, x)) $ となる。 |
| 31 | 595 |
| 596 ラムダ計算には変数のスコープが存在する。 | |
| 597 抽象 $ \lambda x . t $ の本体 $ t $ の中に変数 $ x $ がある時、 $ x $ の出現は束縛されていると言う。 | |
| 598 同様に、 $ \lambda x $ は $ t $ をスコープとする束縛子であると言う。 | |
| 599 なお、 $ x $ を囲む抽象によって束縛されていない場所の $ x $ の出現は自由であると言う。 | |
| 600 例えば $ x \; y $ や $ \lambda y . \; x \; y $ における $ x $ の出現は自由だが、 $ \lambda x . x $ や $ \lambda z . \lambda x . \lambda y . x (y \; z) $ における $ x $ の出現は束縛されている。 | |
| 601 $ (\lambda x . x) \;x $ においては、最初の $ x $ の出現は束縛されているが、2つ目の出現は自由である。 | |
| 602 | |
| 603 ラムダ計算において、計算とは引数に対する関数の適用である。 | |
| 604 抽象に対して項を適用した場合、抽象の本体に存在する束縛変数に適用する項を代入したもので書き換える。 | |
| 605 図式的には | |
| 606 | |
| 607 \begin{equation*} | |
| 608 (\lambda x . t_{12}) t_2 \rightarrow [ x \mapsto t_2] t_{12} | |
| 609 \end{equation*} | |
| 610 | |
| 611 と記述する。 | |
| 612 ここで $ [ x \mapsto t_2] t_{12} $ とは、$ t_12 $ 中の自由な $ x $ を全て $ t_2 $ で置換した項を意味する。 | |
| 613 例えば、 $ (\lambda x . x) \; y $ は $ y $ となり、項 $ (\lambda x . x (\lambda x . x)) (y \; z) $ は $ y \; z \; (\lambda x . x) $ となる。 | |
| 614 | |
| 615 なお、 $ (\lambda x . t_{12}) t_2 $ という形の項を簡約基(redex, reducible expression) と呼び、上記の規則で簡約基を置換する操作をベータ簡約と呼ぶ。 | |
| 616 ラムダ計算のための評価戦略には数種類の戦略がある。 | |
| 617 | |
| 618 \begin{itemize} | |
| 619 \item 完全ベータ簡約 | |
| 620 | |
| 621 任意の簡約基がいつでも簡約されうる。 | |
| 622 つまり項の中からどの順番で簡約しても良い。 | |
| 623 | |
| 624 \item 正規順序簡約 | |
| 625 | |
| 626 最も左で最も外側の簡約基が最初に簡約される。 | |
| 627 | |
| 628 \item 名前呼び | |
| 629 | |
| 630 正規順序の中でも抽象の内部での簡約を許さない。 | |
| 631 名前呼びの変種は Algol-60 や Haskell で利用されている。 | |
| 632 なお、Haskell においては必要呼びという最適化された変種を利用している。 | |
| 633 | |
| 634 \item 値呼び | |
| 635 | |
| 636 ほとんどの言語はこの戦略を用いている。 | |
| 637 基本的には最も左の簡約基をを簡約するが、右側が既に値(計算が終了してもう簡約できない閉じた項)になっている簡約基のみを簡約する。 | |
| 638 \end{itemize} | |
| 639 | |
| 640 値呼び戦略は関数の引数が本体で使われるかに関わらず評価され、これは正格と呼ばれる。 | |
| 641 名前呼びなどの非正格な戦略は引数が使われる時のみ評価され、これは遅延評価とも呼ばれる。 | |
| 642 | |
| 643 ラムダ計算において、複数の引数は、関数を返り値として返す高階関数として定義できる。 | |
| 32 | 644 項 $ s $ が二つの自由変数 $ x $ と $ y $ を含むとすれば、 $ \lambda x . \lambda y . s $ と書くことで二つの引数を持つ関数を表現できる。 |
| 645 これは $ x $ に $ v $ が与えられた時、$ y $ を受けとり、 $ s $ の抽象内の自由な $ x $ を $ v $ に置き換えた部分を置換する関数、を返す。 | |
| 646 例えば $ (\lambda x . \lambda y . s) \; v \; w $ は $ (\lambda y . [x \mapsto v] s) w $ に簡約され、 $ [y \mapsto w][x \mapsto v]s $ に簡約される。 | |
| 647 なお、複数の引数を取る関数を高階関数に変換することはカリー化と呼ばれる。 | |
| 648 | |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
649 % TODO: ラムダの再帰とかペアとかの解説 直積直和 |
| 39 | 650 |
| 651 ラムダ計算の帰納的な項は以下のように定義される。 | |
| 652 | |
| 653 \begin{definition} | |
| 654 $ V $ を変数名の加算集合とする。項の集合は以下を満たす最小の集合 $ T $ である。 | |
| 655 | |
| 656 \begin{eqnarray*} | |
| 657 任意の x \in V について x \in T \\ | |
| 658 t_1 \in T かつ x in V ならば \lambda x . t \in T \\ | |
| 659 t_1 \in T かつ t_2 \in T ならば t_1 \; t_2 \in T | |
| 660 \end{eqnarray*} | |
| 661 \end{definition} | |
| 662 | |
| 663 また、形式的な自由変数の定義を与える。 | |
| 664 | |
| 665 \begin{definition} | |
| 666 項 $ t $ の自由変数の集合は $ FV(t)$と書き、以下のように定義される。 | |
| 667 | |
| 668 \begin{eqnarray*} | |
| 669 FV(x) = \{ x \} \\ | |
| 670 FV(\lambda . t_1 x) = FV(t_1) \setminus \{ x \} \\ | |
| 671 FV(t_1 \; t_2) = FV(t_1) \cup FV(t_2) | |
| 672 \end{eqnarray*} | |
| 673 \end{definition} | |
| 674 | |
| 675 記号 $ \setminus $ は集合に対する二項演算子であり、$ S \setminus T := {x \in S : x \notin T}$ である。 | |
| 676 つまり、$ t_1 $の内部の自由変数の集合から $ x $ を抜いた集合である。 | |
| 677 | |
| 678 最後に代入について定義する。 | |
| 32 | 679 代入の操作は直感的には置換であるが、変数の束縛に注意しなくてはならない。 |
| 680 例えば抽象への代入を以下のように定義する。 | |
| 681 | |
| 682 \begin{equation*} | |
| 683 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1 | |
| 684 \end{equation*} | |
| 685 | |
| 686 この場合、束縛変数の名前によっては定義が破綻してしまう。例えば以下のようになる。 | |
| 687 | |
| 688 \begin{equation*} | |
| 689 [x \mapsto y](\lambda x . x) = \lambda x . y | |
| 690 \end{equation*} | |
| 691 | |
| 692 $ \lambda $ よって束縛されているはずの $ x $ が書き変わっている。 | |
| 693 これはスコープとして振る舞っていないので誤っている。 | |
| 694 この問題は項 $ t $ 内の変数 $ x $ の自由な出現と束縛された出現を区別しなかったために出現した誤りである。 | |
| 695 | |
| 696 そこで、$ x $ を束縛する項に対しては置換行なわないように定義を変える。 | |
| 697 | |
| 698 \begin{itemize} | |
| 699 \item $ y = x $ の場合 | |
| 700 \begin{equation*} | |
| 701 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . t_1 | |
| 702 \end{equation*} | |
| 703 | |
| 704 \item $ y \neq x $ の場合 | |
| 705 \begin{equation*} | |
| 706 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1 | |
| 707 \end{equation*} | |
| 708 \end{itemize} | |
| 709 | |
| 710 この場合は束縛された変数を上書きしないが、逆に自由変数を束縛するケースが発生する。 | |
| 711 具体的には以下である。 | |
| 712 | |
| 713 \begin{equation*} | |
| 714 [ x \mapsto z] (\lambda z . x) = \lambda z . z | |
| 715 \end{equation*} | |
| 716 | |
| 717 項 $ s $ 中の自由変数が項 $ t $ に代入されて束縛される現象は変数捕獲と呼ばれる。 | |
| 718 これを避けるためには $ t $ の束縛変数の名前が $ s $ の自由変数の名前と異なることを保証する必要がある。 | |
| 719 変数捕獲を回避した代入操作は捕獲回避代入と呼ばれる。 | |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
720 代入における名前の衝突を回避するために項の束縛変数の名前を一貫して変更することで変数捕獲を回避する方法も存在する。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
721 束縛変数の名前を一貫して変更することをアルファ変換と呼ばれる。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
722 これは関数抽象に対する束縛変数は問わないという直感からくるもので、 $ \lambda x . x $ も $ \lambda y . y $ も振舞いとしては同じ関数であるとみなすものである。 |
| 32 | 723 捕獲回避の条件を追加した代入の定義は以下のような定義となる。 |
| 724 | |
| 725 \begin{itemize} | |
| 726 \item 変数への代入 | |
| 727 | |
| 728 \begin{equation*} | |
| 729 [ x \mapsto s ] x = s | |
| 730 \end{equation*} | |
| 731 | |
| 732 \item 存在しない変数への代入($ y \neq x $ の時) | |
| 733 | |
| 734 \begin{equation*} | |
| 735 [ x \mapsto s ] y = y | |
| 736 \end{equation*} | |
| 737 | |
| 738 \item 抽象内の項への代入($ y \neq x $ かつ $ y $ が $ s $ の自由変数でない) | |
| 739 | |
| 740 \begin{equation*} | |
| 741 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1 | |
| 742 \end{equation*} | |
| 743 | |
| 744 \item 適用への代入 | |
| 745 | |
| 746 \begin{equation*} | |
| 747 [x \mapsto s] (t_1 \; t_2) = (t_1[x\mapsto s])([x \mapsto s] t_2) | |
| 748 \end{equation*} | |
| 749 | |
| 750 \end{itemize} | |
| 751 | |
| 752 この定義は少なくとも代入が行なわれる際には正しく代入が行なえる。 | |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
753 さらに、抽象が束縛している変数を名前では無く数字として扱う名無し表現も存在する。 |
| 74 | 754 これは De Brujin 表現~\cite{DEBRUIJN1972381}と呼ばれ、コンパイラ内部などでの項表現として用いられる。 |
| 32 | 755 |
| 39 | 756 最終的な型無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。 |
| 757 | |
| 758 \begin{definition} | |
| 759 $ \rightarrow $ (型無し) | |
| 760 | |
| 761 項 | |
| 762 \begin{align*} | |
| 763 t ::= && \text{項} \\ | |
| 764 \lambda x . t && \text{ラムダ抽象} \\ | |
| 765 t \; t && \text{関数適用} | |
| 766 \end{align*} | |
| 767 | |
| 768 値 | |
| 769 \begin{align*} | |
| 770 v ::= && \text{値} \\ | |
| 771 \lambda x . t && \text{ラムダ抽象値} | |
| 772 \end{align*} | |
| 773 | |
| 774 評価( $ t \rightarrow t' $) | |
| 775 | |
| 776 \begin{align*} | |
| 777 \AxiomC{$ t_1 \rightarrow t_1'$} | |
| 778 \UnaryInfC{$t_1 \; t_2 \rightarrow t_1' t_2$} | |
| 779 \DisplayProof && \text{E-APP1} \\ | |
| 780 \AxiomC{$ t_2 \rightarrow t_2'$} | |
| 781 \UnaryInfC{$v_1 \; t_2 \rightarrow v_1 t_2'$} | |
| 782 \DisplayProof && \text{E-APP2} \\ | |
| 783 (\lambda x . t_{12}) \; v_2 \rightarrow [ x \mapsto v_2] t_{12} | |
| 784 && \text{E-APPABS} | |
| 785 \end{align*} | |
| 786 \end{definition} | |
| 32 | 787 |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
788 項は変数かラムダ抽象か関数適用の3つにより構成される。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
789 また、ラムダ抽象値は全て値である。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
790 加えて評価は関数適用を行なう E-APPABS 計算規則と、適用の項を書き換える E-APP1 と E-APP2 合同規則により定義される。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
791 |
| 39 | 792 この定義からも評価戦略と評価順序が分かる。 |
| 793 関数を適用する E-APPABS は左側が抽象であり、右側が値である $v_2$ の時にしか適用されない。 | |
| 794 逆に、規則 E-APP1 の$t_1$は任意の項にマッチするため関数部分が値でない関数適用に用いる。 | |
| 795 一方、E-APP2 は左辺が値であるようになるまで評価されない。 | |
| 796 よって、関数適用 $ t_1 \; t_2 $ の評価順は、まずE-APP1を用いて$t_1$が値となった後にE-APP2を用いて$t_2$を値とし、最後にE-APPABSで関数を適用を行なう。 | |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
797 |
| 32 | 798 |
| 799 % }}} | |
| 28 | 800 |
| 43 | 801 % {{{ 単純型付きラムダ計算 |
| 802 | |
| 28 | 803 \section{単純型付きラムダ計算} |
| 42 | 804 型無しラムダ計算に対して単純型を適用する場合、ラムダ抽象の型について考える必要がある。 |
| 805 ラムダ抽象は値を取って値を返すため、関数として考えることもできる。 | |
| 806 差し当たりBool型における関数の型を $ \lambda x . t : \rightarrow $ と定義する。 | |
| 807 この定義においては $ \lambda x . true $ についても $\lambda x . \lambda y . y $ のような型も同一の型を持つ。 | |
| 808 この二つの項は値を適用すると値を返すという点では同じであるが、前者は $ true $ を返し、後者は $ \lambda y . y $ を返す。 | |
| 809 これでは関数を適用した際に返す値の型は関数の型から予測できず、加えてどの値に対して適用可能かも分からない。 | |
| 810 そのために引数にどのような型を期待しているのか、正しい型の値を適用するとどの型の値を返すのかを型情報に追加する。 | |
| 811 具体的には以下のように $ \rightarrow $ を $ T_1 \rightarrow T_2 $ の形をした無限の型の族に置き換える。 | |
| 812 | |
| 813 \begin{definition} | |
| 814 型 Bool 上の単純型の集合は次の文法により生成される。 | |
| 815 | |
| 816 \begin{align*} | |
| 817 t ::= && 型 : \\ | |
| 818 T \rightarrow T && 関数の型 \\ | |
| 819 Bool && ブール値型 | |
| 820 \end{align*} | |
| 821 \end{definition} | |
| 822 | |
| 823 なお、型構築子 $ \rightarrow $ は右結合である。 | |
| 824 つまり $ T_1 \rightarrow T_2 \rightarrow T_3 $ は$ T_1 \rightarrow (T_2 \rightarrow T_3) $となる。 | |
| 825 | |
| 826 $ \lambda x . t $ に対して型を割り当てる時、明示的に型付けする方法と暗黙的に型付けする方法がある。 | |
| 827 明示的に型付けを行なう場合はプログラマが項に型の注釈を記述する。 | |
| 828 暗黙的に型付けを行なう場合は型検査器に情報を推論させ、型を再構築させる。 | |
| 829 型推論は $ \lambda $ 計算の文献内では型割り当て体系と呼ぶこともある。 | |
| 830 今回は明示的に型を指定する方法を取る。 | |
| 831 | |
| 832 $ \lambda $ 抽象の引数の型が分かれば、結果の型は本体 $ t_2 $となる。 | |
| 833 ここで、$ t_2 $内における $ x $ の出現は型 $ T_1 $ の項を表すと仮定する必要がある。 | |
| 834 これは引数に対して正しい型の値が渡されたにも関わらず抽象内で異なる型として振る舞うのを禁止するためである。 | |
| 835 この $ \lambda $ 抽象の型付けは以下の T-ABS によって定義される。 | |
| 836 | |
| 837 | |
| 838 \begin{align*} | |
| 839 \AxiomC{$x : T_1 \vdash t_2 : T_2$} | |
| 840 \UnaryInfC{$ \vdash \lambda x : T_1 . t_2 : T_1 \rightarrow T_2$} | |
| 841 \DisplayProof && \text{T-ABS} | |
| 842 \end{align*} | |
| 843 | |
| 844 項は抽象を入れ子で持つ可能性があるため、引数の仮定は複数持ちうる。 | |
| 845 このため型付け関係は二項関係 $ t : T $ から、三項関係 $ \Gamma \vdash t : T $ となる。 | |
| 846 ここで $ \Gamma $ とは $ t $ に表われる自由変数の型の仮定の集合である。 | |
| 847 $ \Gamma $ は型付け文脈や型環境と呼ばれ、$ \Gamma \vdash t : T $ は「型付け文脈 $ \Gamma $ において項 $ t$ は型$T$を持つ」と読む。 | |
| 848 空の文脈は $ \emptyset$ と書かえることもあるが、通常は省略して $ \vdash t : T $ と書く。 | |
| 849 また、型環境に対する $ , $ 演算子は $ \Gamma $ の右に新しい束縛を加えて拡張する。 | |
| 850 | |
| 851 新しい束縛と既に $ \Gamma $ に表われている束縛は混同しないように名前 $ x$は$\Gamma $に存在しない名前から選ばれるものとする。 | |
| 852 これはアルファ変換により$\lambda$抽象の束縛名は一貫して変更ができるため、常に満たせる。 | |
| 853 | |
| 854 ラムダ抽象に型を持たせる規則の一般的な形は | |
| 855 | |
| 856 \begin{align*} | |
| 857 \AxiomC{$ \Gamma, x : T_1 \vdash t_2 : T_2$} | |
| 858 \UnaryInfC{$ \Gamma \vdash \lambda x : T_1 . t_2 : T_1 \rightarrow T_2$} | |
| 859 \DisplayProof && \text{T-ABS} | |
| 860 \end{align*} | |
| 861 | |
| 862 であり、変数の型付け規則は | |
| 863 | |
| 864 \begin{align*} | |
| 865 \AxiomC{$ x : T \in \Gamma $} | |
| 866 \UnaryInfC{$ \Gamma \vdash x : T$} | |
| 867 \DisplayProof && \text{T-VAR} | |
| 868 \end{align*} | |
| 869 | |
| 870 である。 | |
| 871 $ x : T \in T $ は 、$ \Gamma$において $x$ に仮定された型は $ T $ である、と読む。 | |
| 872 | |
| 873 最後に関数適用の型付け規則を定義する。 | |
| 874 | |
| 875 \begin{align*} | |
| 876 \AxiomC{$ \Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$} | |
| 43 | 877 \AxiomC{$ \Gamma \vdash t_2 : T_{11}$} |
| 42 | 878 \BinaryInfC{$ \Gamma \vdash t_1 \; t_2 : T_{12}$} |
| 879 \DisplayProof && \text{T-APP} | |
| 880 \end{align*} | |
| 881 | |
| 882 もし $t_1$ が$ T_{11}$の引数を $ T_{12}$の計算結果に移す関数へ評価され、$ t_2$が型$T_{11}$の計算結果にに評価されるのであれば、$t_1$ を $ t_2$に適用した計算結果は $ T_{12}$の型を持つ。 | |
| 883 ブール定数と条件式の型付け規則は型付き算術式と時と同様である。 | |
| 884 | |
| 43 | 885 最終的な純粋単純型付きラムダ計算の規則を示す。 |
| 886 純粋とは基本型を持たないという意味であり、純粋単純型付きラムダ計算にはブールのような型を持たない。 | |
| 887 この純粋単純型付きラムダ計算でブール値を扱う場合は型環境$\Gamma$を考慮してブール値の規則を追加すれば良い。 | |
| 42 | 888 |
| 889 \begin{definition} | |
| 43 | 890 $ \rightarrow $ (型付き)の構文 |
| 42 | 891 |
| 892 \begin{align*} | |
| 893 t ::= && \text{項} \\ | |
| 894 x && \text{変数} \\ | |
| 895 \lambda x : T . t && \text{ラムダ抽象} \\ | |
| 896 t \; t && \text{関数適用} \\ | |
| 897 \end{align*} | |
| 43 | 898 |
| 899 \begin{align*} | |
| 900 v ::= && \text{項} \\ | |
| 901 \lambda x : T . t && \text{ラムダ抽象値} \\ | |
| 902 \end{align*} | |
| 903 | |
| 904 \begin{align*} | |
| 905 T ::= && \text{型} \\ | |
| 906 T \rightarrow T && \text{関数型} \\ | |
| 907 \end{align*} | |
| 908 | |
| 909 \begin{align*} | |
| 910 \Gamma ::= && \text{文脈} \\ | |
| 911 \emptyset && \text{空の文脈} \\ | |
| 912 \Gamma , x : T && \text{項変数の束縛} \\ | |
| 913 \end{align*} | |
| 42 | 914 \end{definition} |
| 915 | |
| 43 | 916 \begin{definition} |
| 917 $ \rightarrow $ (型付き)の評価($ t \rightarrow t'$) | |
| 918 | |
| 919 \begin{align*} | |
| 920 \AxiomC{$t_1 \rightarrow t_1'$} | |
| 921 \UnaryInfC{$t_1 \; t_2 \rightarrow t_1' \; t_2$} | |
| 922 \DisplayProof && \text{E-APP1} \\ | |
| 923 \AxiomC{$t_2 \rightarrow t_2'$} | |
| 924 \UnaryInfC{$v_1 \; t_2 \rightarrow v_1 \; t_2'$} | |
| 925 \DisplayProof && \text{E-APP2} \\ | |
| 926 (\lambda x : T_{11} . t_{12}) v_2 \rightarrow [ x \mapsto v_2] t_{12} && | |
| 927 \text{E-APPABS} | |
| 928 \end{align*} | |
| 929 \end{definition} | |
| 930 | |
| 931 \begin{definition} | |
| 932 $ \rightarrow $ (型付き)の型付け($\Gamma \vdash t : T $) | |
| 933 | |
| 934 \begin{align*} | |
| 935 \AxiomC{$ x : T \in \Gamma$} | |
| 936 \UnaryInfC{$\Gamma \vdash x : T $} | |
| 937 \DisplayProof && \text{T-VAR} \\ | |
| 938 \AxiomC{$\Gamma , x : T_1 \vdash t_2 : T_2$} | |
| 939 \UnaryInfC{$\Gamma \vdash \lambda x : T_1 . t_2 : T_1 \rightarrow T_2$} | |
| 940 \DisplayProof && \text{E-ABS} \\ | |
| 941 \AxiomC{$ \Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$} | |
| 942 \AxiomC{$ \Gamma \vdash t_2 : T_{11}$} | |
| 943 \BinaryInfC{$\Gamma \vdash t_1 \; t_2 : t_{12}$} | |
| 944 \DisplayProof && \text{T-APP} | |
| 945 \end{align*} | |
| 946 \end{definition} | |
| 947 | |
| 948 単純型付きラムダ計算の型付け規則のインスタンスも型付き算術式のように導出木をすることで示せる。 | |
| 949 例えば $ (\lambda x : Bool\; x) \; true $ が空の文脈において $ Bool$を持つことは以下の木で表せる。 | |
| 950 | |
| 951 \begin{prooftree} | |
| 952 \AxiomC{$ x : Bool \in x : Bool$} | |
| 953 \RightLabel{T-VAR} | |
| 954 \UnaryInfC{$x : Bool \vdash x : Bool$} | |
| 955 \RightLabel{T-ABS} | |
| 956 \UnaryInfC{$\vdash \lambda x : Bool . x : Bool \rightarrow Bool$} | |
| 957 \AxiomC{} | |
| 958 \RightLabel{T-TRUE} | |
| 959 \UnaryInfC{$\vdash true : Bool$} | |
| 960 \RightLabel{T-APP} | |
| 961 \BinaryInfC{$\vdash (\lambda x : Bool . x) \; true : Bool $} | |
| 962 \end{prooftree} | |
| 963 | |
| 47 | 964 純粋型付きラムダ計算の型システムにおいて、閉じた項に対して進行定理と保存定理は成り立つ\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。 % FIXME: 進行定理と保存定理の証明。 |
| 43 | 965 閉じた項、という制限が付いているのは $ f \; true $ といった自由変数が存在する項は正規形ではあるが値でないからである。 |
| 966 しかし、開いた項に関しては評価が行なえないために型システムの検査対象に含まれない。 | |
| 967 | |
| 968 % }}} | |
| 969 | |
| 46 | 970 % {{{ 部分型付け |
| 971 | |
| 28 | 972 \section{部分型付け} |
| 44 | 973 単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。 |
| 974 ここで、 単純型の拡張として、レコードを導入する。 | |
| 975 | |
| 976 レコードとは名前の付いた複数の値を保持するデータである。 | |
| 977 C 言語における構造体などがレコードに相当する。 | |
| 978 値を保持する各フィールド $ t_1 $ はあらかじめ定められた集合 L からラベル $ l_i$ を名前として持つ。 | |
| 979 例えば $ { x : Nat } $ や $ {no : 100, point 33}$ などがこれに相当する。 | |
| 980 なお、あるレコードの項や値に表れるラベルはすべて相異なるとする。 | |
| 981 レコードから値を取り出す際にはラベルを指定して値を射影する。 | |
| 982 | |
| 983 レコードの拡張の定義は以下である。 | |
| 984 | |
| 985 \begin{definition} | |
| 986 レコードの拡張に用いる新しい構文形式 | |
| 987 | |
| 988 \begin{align*} | |
| 989 t :: = ... && \text{項 :} \\ | |
| 990 \{l_i = t_i^{\; i \in 1 .. n}\} && \text{レコード} \\ | |
| 991 t.l && \text{射影} \\ | |
| 992 \end{align*} | |
| 993 | |
| 994 \begin{align*} | |
| 995 v :: = ... && \text{値 :} \\ | |
| 996 {l_i : v_i^{\; i \in 1..n}} && \text{レコードの値} | |
| 997 \end{align*} | |
| 998 | |
| 999 \begin{align*} | |
| 1000 T :: = ... && \text{型 :} \\ | |
| 1001 \{l_i : T_i^{\; i \in 1..n}\} && \text{レコードの型} | |
| 1002 \end{align*} | |
| 1003 \end{definition} | |
| 1004 | |
| 1005 \begin{definition} | |
| 1006 レコードの拡張に用いる新しい評価規則 | |
| 1007 | |
| 1008 \begin{align*} | |
| 1009 \{l_i = v_i^{\; i \in 1..n}.l_j \rightarrow v_j\} && \text{E-PROJRCD} \\ | |
| 1010 \AxiomC{$t_1 \rightarrow t_1'$} | |
| 1011 \UnaryInfC{$t_1.l \rightarrow t_1'.l$} | |
| 1012 \DisplayProof && \text{E-PROJ} \\ | |
| 1013 \AxiomC{$ t_j \rightarrow t_j'$} | |
| 1014 \UnaryInfC{$ \{l_i = v_i^{i \in 1..j-1}, l_j = t_j, l_k = t_k^{k \in j+1 .. n}\} | |
| 1015 \rightarrow | |
| 1016 \{l_i = v_i^{i \in 1..j-1}, l_j = t_j', l_k = t_k^{k \in j+1 .. n}\} | |
| 1017 $} | |
| 1018 \DisplayProof && \text{E-RCD} \\ | |
| 1019 \end{align*} | |
| 1020 \end{definition} | |
| 1021 | |
| 1022 \begin{definition} | |
| 1023 レコードの拡張に用いる新しい型付け規則 | |
| 1024 | |
| 1025 \begin{align*} | |
| 1026 \AxiomC{各iに対して$ \Gamma \vdash t_i : T_i$} | |
| 1027 \UnaryInfC{$ \Gamma \vdash \{ l_i = t_i^{\; i \in 1..n} : \{l_i : T_i^{\; i \in 1..n}\}$} | |
| 1028 \DisplayProof && \text{T-RCD} \\ | |
| 1029 \AxiomC{$ \Gamma \vdash t_1 : \{ l_i : T_i^{\; i \in 1.. n}\}$} | |
| 1030 \UnaryInfC{$\Gamma \vdash t_1.lj : T_j$} | |
| 1031 \DisplayProof && \text{T-PROJ} | |
| 1032 \end{align*} | |
| 1033 \end{definition} | |
| 1034 | |
| 1035 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。 | |
| 45 | 1036 しかし、引数にレコードを取る場合、その型と完全に一致させる必要がある。 |
| 1037 例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。 | |
| 1038 しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。 | |
| 1039 | |
| 1040 部分型付けの目標は上記のような場合の項を許すように型付けを改良することにある。 | |
| 1041 つまり型 $ S $ の任意の項が、型 $ T $ の項が期待される文脈において安全に利用できることを示す。 | |
| 1042 この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。 | |
| 1043 これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。 | |
| 1044 $ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。 | |
| 1045 | |
| 1046 型付け関係と部分型関係をつなぐための新しい型付け規則を考える。 | |
| 1047 | |
| 1048 \begin{align*} | |
| 1049 \AxiomC{$\Gamma \vdash t : S $} | |
| 1050 \AxiomC{$ S <: T $} | |
| 1051 \BinaryInfC{$ \Gamma \vdash t : T$} | |
| 46 | 1052 \DisplayProof && \text {T-SUB} |
| 45 | 1053 \end{align*} |
| 1054 | |
| 1055 この規則は $ S <: T $ ならば $ S $ 型の要素 $ t$はすべて $ T $の要素であると言っている。 | |
| 1056 例えば、先程の $ \{ x : Nat \} $ と $ \{ x : Nat , y : Bool\}$ が $ \{ x : Nat , y : Bool\} <: \{ x : Nat \}$ となるように部分型関係を定義した時に $ \Gamma \vdash \{x=0, y=1\} : \{ x : Nat \}$ を導ける。 | |
| 44 | 1057 |
| 46 | 1058 部分型関係は $ S <: T $ という形式の部分型付け式を導入するための推論規則の集まりとして定式化される。 |
| 1059 始めに、部分型付けの一般的な規定から考える。 | |
| 1060 部分型は反射的であり、推移的である。 | |
| 1061 | |
| 1062 \begin{align*} | |
| 1063 S <: S && \text{S-REFL} \\ | |
| 1064 \AxiomC{$S <: U$} | |
| 1065 \AxiomC{$U <: T$} | |
| 1066 \BinaryInfC{$ S <: T $} | |
| 1067 \DisplayProof && \text{S-TRANS} | |
| 1068 \end{align*} | |
| 1069 | |
| 1070 これらの規則は安全代入に対する直感より正しい。 | |
| 1071 次に、基本型や関数型、レコード型などの型それぞれに対して、その形の型の要素が期待される部分に対して上位型の要素を利用しても安全である、という規則を導入していく。 | |
| 1072 | |
| 1073 レコード型については型 $ T = \{ l_i : T_1 ... l_n : T_n\} $が持つフィールドが型 $ S = \{ k_1 : S_1 ... k_n : T_n\} $のものよりも少なければ $S$ を $T$の部分型とする。 | |
| 1074 つまりレコードの終端フィールドのいくつかを忘れてしまっても安全である、ということを意味する。 | |
| 1075 この直感は幅部分型付け規則となる。 | |
| 1076 | |
| 1077 \begin{align*} | |
| 1078 \{l_i : T_i^{\; i \in 1..n+k} \} <: \{l_i : T_i^{\; i \in 1..n}\} | |
| 1079 && \text{S-RCDWIDTH} | |
| 1080 \end{align*} | |
| 1081 | |
| 1082 フィールドの多い方が部分型となるのは名前に反するように思える。 | |
| 1083 しかし、フィールドが多いレコードほど制約が多くなり表すことのできる集合の範囲は小さくなる。 | |
| 1084 集合の大きさで見ると明かにフィールドの多い方が小さいのである。 | |
| 1085 | |
| 1086 幅部分型付け規則が適用可能なのは、共通のフィールドの型が全く同じな場合のみである。 | |
| 1087 しかし、その場合フィールドの型に部分型を導入できず、フィールドの型の扱いで同じ問題を抱えることとなる。 | |
| 1088 そのために導入するのが深さ部分型付けである。 | |
| 1089 二つのレコードの中で対応するフィールドの型が部分型付け関係にある時に個々のフィールドの型が異なることを許す。 | |
| 1090 これは具体的には以下の規則となる。 | |
| 1091 | |
| 1092 \begin{align*} | |
| 1093 \AxiomC{各iに対して $S_i <: T_i$} | |
| 1094 \UnaryInfC{$\{ l_i : S_i^{\; i \in 1..n}\} <: \{l_i : T_i^{\; i \in 1..n}\}$} | |
| 1095 \DisplayProof && \text{S-RCDDEPTH} | |
| 1096 \end{align*} | |
| 1097 | |
| 1098 これらを用いて $ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\}$ が $ \{x : \{ a : Nat\}, y : \{\}\}$の部分型であることは以下のように導出できる。 | |
| 1099 | |
| 1100 \begin{prooftree} | |
| 1101 \AxiomC{} | |
| 1102 \RightLabel{S-RCDWIDTH} | |
| 1103 \UnaryInfC{$ \{a : Nat, b : Nat\} <: \{a : Nat\}$} | |
| 1104 \AxiomC{} | |
| 1105 \RightLabel{S-RCDWIDTH} | |
| 1106 \UnaryInfC{$ \{m : Nat\} <: \{\}$} | |
| 1107 \RightLabel{S-RCDDEPTH} | |
| 1108 \BinaryInfC{$ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\} <: \{x : \{ a : Nat\}, y : \{\}\}$} | |
| 1109 \end{prooftree} | |
| 1110 | |
| 1111 最後に、レコードを利用する際はフィールドさえ揃っていれば順序は異なっても良いという規則を示す。 | |
| 1112 | |
| 1113 \begin{align*} | |
| 1114 \AxiomC{$ \{ k_j : S_j^{\; i \in 1 .. n} \}$ は $ \{ l_i : T_i^{\; i \in 1 ..n}\} $ の並べ替えである} | |
| 1115 \UnaryInfC{$ \{k_j : S_j^{\; j \in 1..n} \} <: \{l_i : T_i^{\; i \in 1..n }\}$} | |
| 1116 \DisplayProof && \text{S-RCDPERM} | |
| 1117 \end{align*} | |
| 1118 | |
| 1119 S-RCDPERM を用いることで、終端フィールドだけではなく任意の位置のフィールドを削ることができる。 | |
| 1120 | |
| 1121 レコードの部分型は定義できたので、次は関数の部分型を定義していく。 | |
| 1122 関数の部分型は以下 S-ARROW として定義できる。 | |
| 1123 | |
| 1124 \begin{align*} | |
| 1125 \AxiomC{$ T_1 <: S_1$} | |
| 1126 \AxiomC{$ S_2 <: T_2$} | |
| 1127 \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $} | |
| 1128 \DisplayProof && \text{S-ARROW} | |
| 1129 \end{align*} | |
| 1130 | |
| 1131 前提の条件二つを見ると部分型の関係が逆転している。 | |
| 1132 左側の条件は関数型自身の型と逆になっているため反変と言い、返り値の型は同じ向きであるため共変と言う。 | |
| 1133 引数について考えた時、求める型よりも大きい型であれば明らかに安全に呼ぶことができるために関数の引数の型の方が上位型になる。 | |
| 1134 返り値については関数が返す型が部分型であれば上位型を返すことができるため、関数の返り値の方が部分型になる。 | |
| 1135 | |
| 1136 別の見方をすると、型 $ S_1 \rightarrow S_2 $ の関数を別の型 $ T_1 \rightarrow T_2 $が期待される文脈で用いることが安全な時とは | |
| 1137 | |
| 1138 \begin{itemize} | |
| 1139 \item 関数に渡される引数がその関数にとって想定外でない($ T_1 <: S_1$) | |
| 1140 \item 関数が返す値も文脈にとって想定外でない($ S_2 <: T_2 $) | |
| 1141 \end{itemize} | |
| 1142 | |
| 1143 という場合に限る。 | |
| 1144 | |
| 1145 % }}} | |
| 1146 | |
| 48 | 1147 % {{{ 部分型と Continuation based C |
| 46 | 1148 |
| 28 | 1149 \section{部分型と Continuation based C} |
| 48 | 1150 部分型を用いて Conituation based C の型システムを定義していく。 |
| 1151 | |
| 1152 まず、DataSegment の型から定義してく。 | |
| 1153 DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。 | |
| 1154 例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。 | |
| 1155 | |
| 1156 \lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h} | |
| 1157 この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ であると見なせる。 | |
| 1158 CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。 | |
| 1159 | |
| 1160 次に Meta DataSegment について考える。 | |
| 1161 Meta DataSegment はプログラムに出現する DataSegment の共用体であった。 | |
| 1162 これを DataSegment の構造体に変更する。 | |
| 1163 こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。 | |
| 1164 もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。 | |
| 1165 第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。 | |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
1166 なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だか持つ実装になっている。 |
| 48 | 1167 |
| 1168 具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。 | |
| 1169 \lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h} | |
| 1170 | |
| 1171 部分型として定義するなら以下のような定義となる。 | |
| 1172 | |
| 1173 \begin{definition} | |
| 1174 Meta DataSegment の定義 | |
| 1175 | |
| 1176 \begin{align*} | |
| 1177 Meta \; DataSegment <: DataSegment_i^{i \in N} && \text{S-MDS} | |
| 1178 \end{align*} | |
| 1179 \end{definition} | |
| 1180 | |
| 1181 なお、$N$はあるプログラムに出現するデータセグメントの名前の集合であるとする。 | |
| 1182 | |
| 1183 次に CodeSegment の型について考える。 | |
| 1184 CodeSegment は DataSegment を DataSegment へと移す関数型とする。 | |
| 1185 | |
| 1186 \begin{definition} | |
| 1187 CodeSegment の定義 | |
| 1188 | |
| 1189 \begin{align*} | |
| 1190 DataSegment \rightarrow DataSegment && \text{T-CS} | |
| 1191 \end{align*} | |
| 1192 \end{definition} | |
| 1193 | |
| 1194 そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。 | |
| 1195 | |
| 1196 \begin{definition} | |
| 1197 Meta CodeSegment の定義 | |
| 1198 | |
| 1199 \begin{align*} | |
| 1200 Meta \; DataSegment \rightarrow Meta \; DataSegment && \text{T-MCS} | |
| 1201 \end{align*} | |
| 1202 \end{definition} | |
| 1203 | |
| 1204 ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。 | |
| 1205 | |
| 1206 \lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c} | |
| 1207 | |
| 1208 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。 | |
| 1209 現状は \verb/Context/ も継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。 | |
| 1210 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} $ となる。 | |
| 1211 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。 | |
| 1212 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。 | |
| 1213 $ Context $ の型は Meta DataSegment なので、 subtype の S-ARROW より $Context $の上位型への変更ができる。 | |
| 1214 | |
| 1215 $ \{ allocat; : Allocate , akashaInfo : AkahsaInfo\} $ を $X$と置いて、\verb/getMinHeignt/ を $ X \rightarrow X $ とする際の導出木は以下である。 | |
| 1216 | |
| 1217 \begin{prooftree} | |
| 1218 \AxiomC{} | |
| 1219 \RightLabel{S-REFL} | |
| 1220 \UnaryInfC{$ X <: X $} | |
| 1221 \AxiomC{} | |
| 1222 \RightLabel{S-MDS} | |
| 1223 \UnaryInfC{$ Conttext <: X$} | |
| 1224 \RightLabel{S-ARROW} | |
| 1225 \BinaryInfC{$ X \rightarrow Context <: X \rightarrow X$} | |
| 1226 \end{prooftree} | |
| 1227 | |
| 1228 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。 | |
| 1229 プログラムによっては遷移先は確定しているために部分型にする必要性は無いが、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に包摂関係から具体型を導けば良い。 | |
| 1230 例えばコンパイル時に解決すればライブラリの静的リンク時実行コード生成が行なえ、ランタイム時に解決すればネットワークを経由するプログラムとの接続初期化に利用できる。 | |
| 1231 例えば、プロトコルがバージョンを持つ場合に接続先のプログラムが利用しているプロトコルと互換性があるかの判断を Context どうしの部分型関係で判断できる。 | |
| 1232 | |
| 1233 また、stub のみに注目すると、stub は Context から具体的なDataSegment X を取り出す操作に相当し、S-ARROWの左側の前提のような振舞いをする。 | |
| 1234 加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、S-ARROWの右側の前提のような振舞いを行なう。 | |
| 1235 このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。 | |
| 1236 型付けにDataSegment の集合としての Meta DataSegment が必須になるが、これは構造体として定義可能なためコンパイル時に生成することで CbC に組み込むことができる。 | |
| 1237 | |
| 1238 なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。 | |
| 1239 ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。 | |
| 1240 このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。 | |
| 1241 | |
| 1242 % }}} |