Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/type.tex @ 37:881bd1d12a45
Writing expression ...
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 28 Jan 2017 11:28:38 +0900 |
| parents | 34812c1b33c2 |
| children | 5d4097922243 |
| rev | line source |
|---|---|
| 28 | 1 \chapter{ラムダ計算と型システム} |
| 2 \label{chapter:type} | |
| 3 \ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。 | |
| 4 しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。 | |
| 5 CbC は直接自身を証明する機構が存在しない。 | |
| 6 プログラムの性質を証明するには CbC の形式的な定義が必須となる。 | |
| 7 \ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。 | |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
8 また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
9 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
10 % {{{ 型システムとは |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
11 \section{型システムとは} |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
12 型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
13 ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
14 例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
15 % TODO: C の warning? |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
16 この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。 |
|
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 型システムで行なえることには以下のようなものが存在する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
20 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
21 \begin{itemize} |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
22 \item エラーの検出 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
23 |
|
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 |
| 31 | 30 \item 抽象化 |
|
30
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 |
| 31 | 37 \item ドキュメント化 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
38 |
|
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 |
| 31 | 43 \item 言語の安全性 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
44 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
45 安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。 |
|
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 |
| 31 | 50 \item 効率性 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
51 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
52 そもそも、科学計算機における最初の型システムは Fortran などにおける式の区別であった。% TODO ref fortran |
|
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 \end{itemize} |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
58 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
59 型システムの定義には多くの定義が存在する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
60 型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
61 例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
62 これは Haskell が C言語よりも厳密な型システムを採用しているからである。 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
63 具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。 |
|
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 型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。 |
|
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 |
| 34 | 69 \section{型無し算術式} |
| 70 まず、型システムやその性質について述べるためにプログラミング言語そのものの基本的な性質について述べる。 | |
| 71 プログラムの構文と意味論、推論について考えるために整数とブール値のみで構成される小さな言語を扱いながら考察する。 | |
| 72 この言語は二種類の値しか持たないが、項の帰納的定義や証明、評価、実行時エラーのモデル化を表現することができる。 | |
| 73 | |
| 74 この言語はブール定数 $ true $ と $ false $ 、条件式、数値定数 0 、算術演算子 $ succ $ と $ pred $ 、判定演算子 $ iszero $ のみからなる。 | |
| 75 算術演算子 $ succ $ は与えられた数の次の数を返し、 $ pred $ はその前の数を返す。 | |
| 76 判定演算子$ iszero $ は与えられた項が 0 なら $ true $ を返し、それ以外は $ false $ を返す。 | |
| 77 これらを文法として定義すると以下のリスト\ref{src:expr-term}のようになる。 | |
| 78 | |
| 79 \lstinputlisting[label=src:expr-term, caption=算術式の項定義] {src/expr-term.txt} | |
| 80 | |
| 81 この定義では算術式の項 $ t $ を定義している。 | |
| 82 $ ::= $ は項の集合の定義を表であり、$ t $ は項の変数のようなものである。 | |
| 83 それに続くすべての行は、構文の選択肢である。 | |
| 84 構文の選択肢内に存在する記号 $ t $ は任意の項を代入できることを表現している。 | |
| 85 このように再帰的に定義することにより、 \verb/ if (ifzero (succ 0)) then true else (pred (succ 0)) / といった項もこの定義に含まれる。 | |
| 86 例において、 $ succ $ 、 $ pred $ 、 $ iszero $ に複合的な引数を渡す場合は読みやすさのために括弧でくくっている。 | |
| 87 括弧の定義は項の定義には含んでいない。 | |
| 88 コンパイラなど具体的な字句をパースする必要がある場合、曖昧な構文を排除するために括弧の定義は必須である。 | |
| 89 しかし、今回は型システムに言及するために曖昧な構文は明示的に括弧で指示することで排除し、抽象的な構文のみを取り扱うこととする。 | |
| 90 | |
| 91 現在、項と式という用語は同一である。 | |
| 92 型のような別の構文表現を持つ計算体系においては式はあらゆる種類の構文を表す。 | |
| 93 項は計算の構文的表現という意味である。 | |
| 94 | |
| 95 この言語におけるプログラムとは上述の文法で与えられた形からなる項である。 | |
| 96 評価の結果は常にブール定数か自然数のどちらかになる。 | |
| 97 これら項は値と呼ばれ、項の評価順序の形式化において区別が必要となる。 | |
| 98 | |
| 99 なお、この項の定義においては \verb/succ true/ といった怪しい項の形成を許してしまう。 | |
| 100 実際、これらのプログラムは無意味なものであり、このような項表現を排除するために型システムを利用する。 | |
| 101 | |
| 102 ある言語の構文を定義する際に、他の表現かいくつか存在する。 | |
| 103 先程の定義は次の帰納的な定義のためのコンパクトな記法である。 | |
| 104 | |
| 105 \begin{definition} | |
| 106 項の集合とは以下の条件を満たす最小の集合 $ T $ である。 | |
| 107 \begin{eqnarray*} | |
| 108 \label{eq:expr} | |
| 109 \{true , false , 0\} \subseteq T \\ | |
| 110 t_1 \in T ならば \{succ \; t_1 , pred \; t_1 , iszero \; t_1\} \subseteq T \\ | |
| 111 t_1 \in T かつ t_2 \in T かつ t_3 \in T ならば if \; t_1 \; then \; t_2 else \; t_3 \subseteq T | |
| 112 \end{eqnarray*} | |
| 113 \end{definition} | |
| 114 | |
| 115 まず1つめの条件は、$ T $ に属する3つの式を挙げている。 | |
| 116 2つめと3つめの条件は、ある種の複合的な式が $ T $ に属することを判断するための規則を表している。 | |
| 117 最後の「最小」という単語は $ T $ がこの3つの条件によって要求される要素以外の要素を持たないことを表している。 | |
| 118 | |
| 119 また、項の帰納的表現の略記法として、二次元の推論規則形式を用いる方法もある。 | |
| 120 これは論理体系を自然演繹スタイルで表現するためによく使われる。 | |
| 121 自然演繹による証明は\ref{agda}章内で触れるが、今回は項表現として導入する。 | |
| 122 | |
| 123 \begin{definition} | |
| 36 | 124 項の集合は次の規則によって定義される。 |
| 125 | |
| 126 \begin{prooftree} | |
| 127 \AxiomC{$ true \in T $} | |
| 128 \end{prooftree} | |
| 129 | |
| 130 \begin{prooftree} | |
| 131 \AxiomC{$ false \in T $} | |
| 132 \end{prooftree} | |
| 133 | |
| 134 \begin{prooftree} | |
| 135 \AxiomC{$ 0 \in T $} | |
| 136 \end{prooftree} | |
| 137 | |
| 138 \begin{prooftree} | |
| 139 \AxiomC{$ t_1 \in T $} | |
| 140 \UnaryInfC{$ succ \; t_1 \in T$} | |
| 141 \end{prooftree} | |
| 142 | |
| 143 \begin{prooftree} | |
| 144 \AxiomC{$ t_1 \in T $} | |
| 145 \UnaryInfC{$ pred \; t_1 \in T$} | |
| 146 \end{prooftree} | |
| 147 | |
| 148 \begin{prooftree} | |
| 149 \AxiomC{$ t_1 \in T $} | |
| 150 \UnaryInfC{$ iszero \; t_1 \in T$} | |
| 151 \end{prooftree} | |
| 152 | |
| 153 \begin{prooftree} | |
| 154 \AxiomC{$ t_1 \in T $} | |
| 155 \AxiomC{$ t_2 \in T $} | |
| 156 \AxiomC{$ t_3 \in T $} | |
| 157 \TrinaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \in T$} | |
| 158 \end{prooftree} | |
| 159 | |
| 34 | 160 \end{definition} |
| 161 | |
| 36 | 162 最初の$ true, \; false, \; 0 $の3つ規則は再帰的定義の1つめの条件と同じである。 |
| 163 それ以外の4つの規則は再帰的定義の2つめと3つめの条件と同じである。 | |
| 164 それぞれの規則は「もし線の上に列挙して前提が成立するのならば、線の下の結論を導出できる」と読む。 | |
| 165 $ T $ がこれらの規則を満たす最小の集合である事実は明示的に述べられない。 | |
| 166 | |
| 167 言語の構文は定義できたので、次は項がどう評価されるかの意味論について触れていく。 | |
| 168 意味論の形式化には操作的意味論や表示的意味論、公理的意味論やゲーム意味論などがあるが、ここでは操作的意味論について述べる。 | |
| 169 操作的意味論とは、言語の抽象機械を定義することにより言語の振舞いを規程する。 | |
| 170 この抽象機械が示す抽象とは、扱う命令がプロセッサの命令セットなどの具体的なものでないことを表している。 | |
| 171 単純な言語の抽象機械における状態は単なる項であり、機械の振舞いは遷移関数で定義される。 | |
| 172 この関数は各状態において項の単純化ステップを実行して次の状態を与えるか、機械を停止させる。 | |
| 173 ここで項 $ t $ の意味は、$ t $ を初期状態として動き始めた機械が達する最終状態である。 | |
| 174 | |
| 175 なお、一つの言語に複数の操作的意味論を与えることもある。 | |
| 176 例えば、プログラマが扱う項に似た機械状態を持つ意味論の他に、コンパイラの内部表現やインタプリタが扱う意味論を定義する。 | |
| 177 これらの振舞いが同じプログラムを実行した時に何かしらの意味であれば、結果としてその言語の実装の正しさを証明することに繋がる。 | |
| 178 | |
| 179 まずはブール式のみの操作的意味論を定義する。 | |
| 180 | |
| 181 \begin{definition} | |
| 37 | 182 ブール値(B) |
| 36 | 183 |
| 184 構文 | |
| 185 \begin{align*} | |
| 186 t ::= && \text{項} \\ | |
| 187 true && \text{定数真} \\ | |
| 188 false && \text{定数偽} \\ | |
| 189 if \; t \; then \; t \; else \; t && \text{条件式} | |
| 190 \end{align*} | |
| 191 | |
| 192 値 | |
| 193 \begin{align*} | |
| 194 v ::= && \text{値} \\ | |
| 195 true && \text{真} \\ | |
| 196 false && \text{偽} | |
| 197 \end{align*} | |
| 198 | |
| 199 評価 | |
| 200 \begin{align*} | |
| 201 if \; true \; then \; t_2 \; else t_3 \rightarrow t_2 && \text{(E-IFTRUE)} \\ | |
| 202 if \; false \; then \; t_2 \; else t_3 \rightarrow t_3 && \text{(E-IFFALSE)} \\ | |
| 203 \AxiomC{$ t_1 \rightarrow t_1'$} | |
| 204 \UnaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \rightarrow if \; t_1' \; then t_2 \; else \;t_3 $} | |
| 205 \DisplayProof | |
| 206 && \text{(E-IF)} | |
| 207 \end{align*} | |
| 37 | 208 |
| 209 \end{definition} | |
| 210 | |
| 211 評価の最終結果になりえる項である値は定数 $ true $ と $ false $ のみである。 | |
| 212 評価の定義は評価関係の定義である。 | |
| 213 評価関係 $ t \rightarrow t' $ は「$ t $ が1ステップで $ t' $ に評価される」と読む。 | |
| 214 直感的には抽象機械の状態が $ t $ ならば $ t' $ が手に入るという意味である。 | |
| 215 | |
| 216 評価関係は3つあるが、2つは前提を持たないため、2つの公理と1つの規則から成る。 | |
| 217 1つめの規則 E-IFTRUE の意味は、評価の対象となる項の条件式が定数 $ true $ である時に、then 節にある $ t_2 $ を残して他の全ての項を捨てるという意味である。 | |
| 218 E-EIFFALSE も同様に条件式が $ false $ の時に $ t_3 $ のみを残す。 | |
| 219 3つ目の規則 E-IF は条件式の評価である。 | |
| 220 条件式 $ t $ が $ t'$ に評価されうるのならば then 節と else 節を変えずに条件部のみを評価する。 | |
| 221 | |
| 222 評価の定義から分かることの中に、if の中の then節 と else 節は条件部より先に評価されないことがある。 | |
| 223 よって、この言語は条件式の評価に対し条件部から評価が優先されるという評価戦略を持つことが分かる。 | |
| 224 | |
| 225 \begin{definition} | |
| 226 推論規則のインスタンスとは、規則の結論や前提に対し、一貫して同じ項による書き換えを行なったものである。 | |
| 227 \end{definition} | |
| 228 | |
| 229 例えば、 | |
| 230 | |
| 231 \verb/if true then true else (if false then false else false)/ | |
| 232 | |
| 233 は E-IFTRUE のインスタンスであり、 E-IFTRUEの $ t_2 $ が \verb/true/ かつ $ t_3 $ が \verb/if false then false else false/ の時である。 | |
| 234 | |
| 235 \begin{definition} | |
| 236 1ステップ評価関係 $ \rightarrow $ とは、3つの評価の規則を満たす、項に関する最小の二項関係である。 | |
| 237 $ (t, \; t') $ がこの関係の元である時、「評価関係式 $ t \rightarrow t'$ は導出可能である」と言う。 | |
| 36 | 238 \end{definition} |
| 239 | |
| 37 | 240 ここで「最小」という言葉が表れるため、評価関係式 $ t \rightarrow t'$ が導出可能である時かつその時に限り、その関係式は規則によって正当化される。 |
| 241 すなわち評価関係式は公理 E-IFTRUE か E-IFFALSE 、前提が成り立つ時の E-IF のインスタンスとなる。 | |
| 242 与えられた評価関係式が導出可能であることを証明するには、葉が E-IFTRUE か E-IFFALSE であり、内部ノードのラベルが E-IF のインスタンスである導出木が示せれば良い。 | |
| 243 例えば以下の略記の元 $ if \; t \; then \; false \; then \; false \rightarrow if \; u \; then \; false \; else \; false $ の導出可能性は以下のような導出木によって示せる。 | |
| 36 | 244 |
| 37 | 245 \begin{itemize} |
| 246 \item $ s = if \; true \; then \; false \; else \; false $ | |
| 247 \item $ t = if \; s \; then \; true \; else \; true $ | |
| 248 \item $ u = if \; false \; then \; true \; else \; true $ | |
| 249 \end{itemize} | |
| 250 | |
| 251 | |
| 252 \begin{prooftree} | |
| 253 \AxiomC{} | |
| 254 \RightLabel{E-IFTRUE} | |
| 255 \UnaryInfC{ $ s \rightarrow true $ } | |
| 256 \RightLabel{E-IF} | |
| 257 \UnaryInfC{ $ t \rightarrow u $} | |
| 258 \RightLabel{E-IF} | |
| 259 \UnaryInfC{ $ if \; t \; then \; false \; then \; false/ \rightarrow if \; u \; then \; false \; else \; false $} | |
| 260 \end{prooftree} | |
| 261 | |
| 262 1ステップ評価関係は与えられた項に対して抽象機械の状態遷移を定義する。 | |
| 263 この時、機械がそれ以上ステップを進められない時にそれが最終結果となる。 | |
| 264 | |
| 265 \begin{definition} | |
| 266 正規形 | |
| 267 | |
| 268 項 $ t $ が正規形であるとは、$ t \rightarrow t'$となる評価規則が存在しないことである。 | |
| 269 \end{definition} | |
| 270 | |
| 271 この言語において $ true $ や $ false $ は正規形である。 | |
| 272 逆に言えば、構文的に正しい if が用いられている場合は評価することが可能なため正規形ではない。 | |
| 273 極端に言えばこの言語における全ての値は正規形なのである。 | |
| 274 しかし、他の言語における値は一般的に正規形ではない。 | |
| 275 実のところ、値でない正規形は実行時エラーとなって表れる。 | |
| 276 | |
| 277 実際にこの言語に整数を導入して値では無い正規形を確認していく。 | |
| 34 | 278 |
| 279 | |
| 280 | |
| 32 | 281 % {{{ 型なしラムダ計算 |
|
30
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
282 \section{型なしラムダ計算} |
| 31 | 283 まず、プログラミング言語における計算を形式的に定義する。 |
| 284 プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61 | |
| 285 この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算だった。 | |
| 286 ラムダ計算は Alonzo Church が発明した形式的体系の一つである。 % TODO: ref | |
| 287 ラムダ計算では全ての計算が関数定義と関数適用の基本的な演算に帰着される。 | |
| 288 ラムダ計算はプログラミング言語の機能の仕様記述や、言語設計と実装、型システムの研究に多く使われている。 | |
| 289 この計算体系の重要な点は、ラムダ計算内部で計算が記述できるプログラミング言語であると同時に、それ自身について厳格な証明が可能な数学的対象としてみなせる点にある。 | |
| 28 | 290 |
| 31 | 291 ラムダ計算はいろいろな方法で拡張できる。 |
| 292 数や組やレコードなどはラムダ計算そのもので模倣することができるが、記述が冗長になってしまう。 | |
| 293 それらの機能のための具体的な特殊構文を加えることは言語の利用者の視点で便利である。 | |
| 294 他にも書き換え可能な参照セルや非局所的な例外といった複雑な機能を表現することもできるが、膨大な変換を用いなければモデル化できない。 | |
| 295 それらを言語として備えた拡張に ML や Haskell といったものがある。 % TODO: ref | |
| 296 | |
| 297 ラムダ計算(または $ \lambda $ 計算) とは、関数定義と関数適用を純粋な形で表現する。 | |
| 298 ラムダ計算においてはすべてが関数である。 | |
| 299 関数によって受け付ける引数も関数であり、関数が返す結果もまた関数である。 | |
| 300 | |
| 301 ラムダ計算の項は変数と抽象と適用の3種類の項からなり、以下の文法に要約される。 | |
| 302 変数 $ x $ は項であり、項 $ t_1 $ から変数 $ x $ を抽象化した $ \lambda x . t_1 $ も項であり、項 $ t_1 $ を他の項 $ t_2 $ に適用した $ t_1 t_2 $ も項である。 | |
| 303 | |
| 304 \begin{multline*} | |
| 305 t ::= \\ | |
| 306 x \\ | |
| 307 \lambda x . t \\ | |
| 308 t \, t \\ | |
| 309 \end{multline*} | |
| 310 | |
| 311 ラムダ計算において関数適用は左結合とする。 | |
| 312 つまり、 $ s \, t \, u $ は $ (s \, t) \, u $ となる。 | |
| 313 | |
| 314 また、抽象の本体はできる限り右側へと拡大する。 | |
| 315 例えば $ \lambda x . \; \lambda y . \; x \, y \, x $ は $ \lambda x . (\lambda . y ((x \, y) \, x)) $ となる。 | |
| 316 | |
| 317 ラムダ計算には変数のスコープが存在する。 | |
| 318 抽象 $ \lambda x . t $ の本体 $ t $ の中に変数 $ x $ がある時、 $ x $ の出現は束縛されていると言う。 | |
| 319 同様に、 $ \lambda x $ は $ t $ をスコープとする束縛子であると言う。 | |
| 320 なお、 $ x $ を囲む抽象によって束縛されていない場所の $ x $ の出現は自由であると言う。 | |
| 321 例えば $ x \; y $ や $ \lambda y . \; x \; y $ における $ x $ の出現は自由だが、 $ \lambda x . x $ や $ \lambda z . \lambda x . \lambda y . x (y \; z) $ における $ x $ の出現は束縛されている。 | |
| 322 $ (\lambda x . x) \;x $ においては、最初の $ x $ の出現は束縛されているが、2つ目の出現は自由である。 | |
| 323 | |
| 324 ラムダ計算において、計算とは引数に対する関数の適用である。 | |
| 325 抽象に対して項を適用した場合、抽象の本体に存在する束縛変数に適用する項を代入したもので書き換える。 | |
| 326 図式的には | |
| 327 | |
| 328 \begin{equation*} | |
| 329 (\lambda x . t_{12}) t_2 \rightarrow [ x \mapsto t_2] t_{12} | |
| 330 \end{equation*} | |
| 331 | |
| 332 と記述する。 | |
| 333 ここで $ [ x \mapsto t_2] t_{12} $ とは、$ t_12 $ 中の自由な $ x $ を全て $ t_2 $ で置換した項を意味する。 | |
| 334 例えば、 $ (\lambda x . x) \; y $ は $ y $ となり、項 $ (\lambda x . x (\lambda x . x)) (y \; z) $ は $ y \; z \; (\lambda x . x) $ となる。 | |
| 335 | |
| 336 なお、 $ (\lambda x . t_{12}) t_2 $ という形の項を簡約基(redex, reducible expression) と呼び、上記の規則で簡約基を置換する操作をベータ簡約と呼ぶ。 | |
| 337 ラムダ計算のための評価戦略には数種類の戦略がある。 | |
| 338 | |
| 339 \begin{itemize} | |
| 340 \item 完全ベータ簡約 | |
| 341 | |
| 342 任意の簡約基がいつでも簡約されうる。 | |
| 343 つまり項の中からどの順番で簡約しても良い。 | |
| 344 | |
| 345 \item 正規順序簡約 | |
| 346 | |
| 347 最も左で最も外側の簡約基が最初に簡約される。 | |
| 348 | |
| 349 \item 名前呼び | |
| 350 | |
| 351 正規順序の中でも抽象の内部での簡約を許さない。 | |
| 352 名前呼びの変種は Algol-60 や Haskell で利用されている。 | |
| 353 なお、Haskell においては必要呼びという最適化された変種を利用している。 | |
| 354 | |
| 355 \item 値呼び | |
| 356 | |
| 357 ほとんどの言語はこの戦略を用いている。 | |
| 358 基本的には最も左の簡約基をを簡約するが、右側が既に値(計算が終了してもう簡約できない閉じた項)になっている簡約基のみを簡約する。 | |
| 359 \end{itemize} | |
| 360 | |
| 361 値呼び戦略は関数の引数が本体で使われるかに関わらず評価され、これは正格と呼ばれる。 | |
| 362 名前呼びなどの非正格な戦略は引数が使われる時のみ評価され、これは遅延評価とも呼ばれる。 | |
| 363 | |
| 364 ラムダ計算において、複数の引数は、関数を返り値として返す高階関数として定義できる。 | |
| 32 | 365 項 $ s $ が二つの自由変数 $ x $ と $ y $ を含むとすれば、 $ \lambda x . \lambda y . s $ と書くことで二つの引数を持つ関数を表現できる。 |
| 366 これは $ x $ に $ v $ が与えられた時、$ y $ を受けとり、 $ s $ の抽象内の自由な $ x $ を $ v $ に置き換えた部分を置換する関数、を返す。 | |
| 367 例えば $ (\lambda x . \lambda y . s) \; v \; w $ は $ (\lambda y . [x \mapsto v] s) w $ に簡約され、 $ [y \mapsto w][x \mapsto v]s $ に簡約される。 | |
| 368 なお、複数の引数を取る関数を高階関数に変換することはカリー化と呼ばれる。 | |
| 369 | |
| 370 代入の操作は直感的には置換であるが、変数の束縛に注意しなくてはならない。 | |
| 371 例えば抽象への代入を以下のように定義する。 | |
| 372 | |
| 373 \begin{equation*} | |
| 374 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1 | |
| 375 \end{equation*} | |
| 376 | |
| 377 この場合、束縛変数の名前によっては定義が破綻してしまう。例えば以下のようになる。 | |
| 378 | |
| 379 \begin{equation*} | |
| 380 [x \mapsto y](\lambda x . x) = \lambda x . y | |
| 381 \end{equation*} | |
| 382 | |
| 383 $ \lambda $ よって束縛されているはずの $ x $ が書き変わっている。 | |
| 384 これはスコープとして振る舞っていないので誤っている。 | |
| 385 この問題は項 $ t $ 内の変数 $ x $ の自由な出現と束縛された出現を区別しなかったために出現した誤りである。 | |
| 386 | |
| 387 そこで、$ x $ を束縛する項に対しては置換行なわないように定義を変える。 | |
| 388 | |
| 389 \begin{itemize} | |
| 390 \item $ y = x $ の場合 | |
| 391 \begin{equation*} | |
| 392 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . t_1 | |
| 393 \end{equation*} | |
| 394 | |
| 395 \item $ y \neq x $ の場合 | |
| 396 \begin{equation*} | |
| 397 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1 | |
| 398 \end{equation*} | |
| 399 \end{itemize} | |
| 400 | |
| 401 この場合は束縛された変数を上書きしないが、逆に自由変数を束縛するケースが発生する。 | |
| 402 具体的には以下である。 | |
| 403 | |
| 404 \begin{equation*} | |
| 405 [ x \mapsto z] (\lambda z . x) = \lambda z . z | |
| 406 \end{equation*} | |
| 407 | |
| 408 項 $ s $ 中の自由変数が項 $ t $ に代入されて束縛される現象は変数捕獲と呼ばれる。 | |
| 409 これを避けるためには $ t $ の束縛変数の名前が $ s $ の自由変数の名前と異なることを保証する必要がある。 | |
| 410 変数捕獲を回避した代入操作は捕獲回避代入と呼ばれる。 | |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
411 代入における名前の衝突を回避するために項の束縛変数の名前を一貫して変更することで変数捕獲を回避する方法も存在する。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
412 束縛変数の名前を一貫して変更することをアルファ変換と呼ばれる。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
413 これは関数抽象に対する束縛変数は問わないという直感からくるもので、 $ \lambda x . x $ も $ \lambda y . y $ も振舞いとしては同じ関数であるとみなすものである。 |
| 32 | 414 捕獲回避の条件を追加した代入の定義は以下のような定義となる。 |
| 415 | |
| 416 \begin{itemize} | |
| 417 \item 変数への代入 | |
| 418 | |
| 419 \begin{equation*} | |
| 420 [ x \mapsto s ] x = s | |
| 421 \end{equation*} | |
| 422 | |
| 423 \item 存在しない変数への代入($ y \neq x $ の時) | |
| 424 | |
| 425 \begin{equation*} | |
| 426 [ x \mapsto s ] y = y | |
| 427 \end{equation*} | |
| 428 | |
| 429 \item 抽象内の項への代入($ y \neq x $ かつ $ y $ が $ s $ の自由変数でない) | |
| 430 | |
| 431 \begin{equation*} | |
| 432 [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1 | |
| 433 \end{equation*} | |
| 434 | |
| 435 \item 適用への代入 | |
| 436 | |
| 437 \begin{equation*} | |
| 438 [x \mapsto s] (t_1 \; t_2) = (t_1[x\mapsto s])([x \mapsto s] t_2) | |
| 439 \end{equation*} | |
| 440 | |
| 441 \end{itemize} | |
| 442 | |
| 443 この定義は少なくとも代入が行なわれる際には正しく代入が行なえる。 | |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
444 さらに、抽象が束縛している変数を名前では無く数字として扱う名無し表現も存在する。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
445 これは De Brujin 表現と呼ばれ、コンパイラ内部などでの項表現として用いられる。 % TODO: ref and spell check |
| 32 | 446 |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
447 最終的に形無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
448 % TODO: TaPL 54 の図5-3 |
| 32 | 449 |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
450 項は変数かラムダ抽象か関数適用の3つにより構成される。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
451 また、ラムダ抽象値は全て値である。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
452 加えて評価は関数適用を行なう E-APPABS 計算規則と、適用の項を書き換える E-APP1 と E-APP2 合同規則により定義される。 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
453 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
454 % TODO: ラムダの再帰とかペアとかの解説 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
455 |
|
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
456 %TODO ラムダの操作的意味論の説明。それとも算術式を前のセクションに入れるか? |
| 32 | 457 |
| 458 % }}} | |
| 28 | 459 |
|
33
74a29a48575a
Update lambda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
460 \section{単純型} |
| 28 | 461 \section{単純型付きラムダ計算} |
| 462 \section{部分型付け} | |
| 463 \section{部分型と Continuation based C} |