Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/type.tex @ 31:9dc9c50a28bd
Writing lambda
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 Jan 2017 17:16:18 +0900 |
| parents | 55f67e448dcc |
| children | 63bbbf54d541 |
| 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 |
|
55f67e448dcc
Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
69 \section{型なしラムダ計算} |
| 31 | 70 まず、プログラミング言語における計算を形式的に定義する。 |
| 71 プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61 | |
| 72 この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算だった。 | |
| 73 ラムダ計算は Alonzo Church が発明した形式的体系の一つである。 % TODO: ref | |
| 74 ラムダ計算では全ての計算が関数定義と関数適用の基本的な演算に帰着される。 | |
| 75 ラムダ計算はプログラミング言語の機能の仕様記述や、言語設計と実装、型システムの研究に多く使われている。 | |
| 76 この計算体系の重要な点は、ラムダ計算内部で計算が記述できるプログラミング言語であると同時に、それ自身について厳格な証明が可能な数学的対象としてみなせる点にある。 | |
| 28 | 77 |
| 31 | 78 ラムダ計算はいろいろな方法で拡張できる。 |
| 79 数や組やレコードなどはラムダ計算そのもので模倣することができるが、記述が冗長になってしまう。 | |
| 80 それらの機能のための具体的な特殊構文を加えることは言語の利用者の視点で便利である。 | |
| 81 他にも書き換え可能な参照セルや非局所的な例外といった複雑な機能を表現することもできるが、膨大な変換を用いなければモデル化できない。 | |
| 82 それらを言語として備えた拡張に ML や Haskell といったものがある。 % TODO: ref | |
| 83 | |
| 84 ラムダ計算(または $ \lambda $ 計算) とは、関数定義と関数適用を純粋な形で表現する。 | |
| 85 ラムダ計算においてはすべてが関数である。 | |
| 86 関数によって受け付ける引数も関数であり、関数が返す結果もまた関数である。 | |
| 87 | |
| 88 ラムダ計算の項は変数と抽象と適用の3種類の項からなり、以下の文法に要約される。 | |
| 89 変数 $ x $ は項であり、項 $ t_1 $ から変数 $ x $ を抽象化した $ \lambda x . t_1 $ も項であり、項 $ t_1 $ を他の項 $ t_2 $ に適用した $ t_1 t_2 $ も項である。 | |
| 90 | |
| 91 \begin{multline*} | |
| 92 t ::= \\ | |
| 93 x \\ | |
| 94 \lambda x . t \\ | |
| 95 t \, t \\ | |
| 96 \end{multline*} | |
| 97 | |
| 98 ラムダ計算において関数適用は左結合とする。 | |
| 99 つまり、 $ s \, t \, u $ は $ (s \, t) \, u $ となる。 | |
| 100 | |
| 101 また、抽象の本体はできる限り右側へと拡大する。 | |
| 102 例えば $ \lambda x . \; \lambda y . \; x \, y \, x $ は $ \lambda x . (\lambda . y ((x \, y) \, x)) $ となる。 | |
| 103 | |
| 104 ラムダ計算には変数のスコープが存在する。 | |
| 105 抽象 $ \lambda x . t $ の本体 $ t $ の中に変数 $ x $ がある時、 $ x $ の出現は束縛されていると言う。 | |
| 106 同様に、 $ \lambda x $ は $ t $ をスコープとする束縛子であると言う。 | |
| 107 なお、 $ x $ を囲む抽象によって束縛されていない場所の $ x $ の出現は自由であると言う。 | |
| 108 例えば $ x \; y $ や $ \lambda y . \; x \; y $ における $ x $ の出現は自由だが、 $ \lambda x . x $ や $ \lambda z . \lambda x . \lambda y . x (y \; z) $ における $ x $ の出現は束縛されている。 | |
| 109 $ (\lambda x . x) \;x $ においては、最初の $ x $ の出現は束縛されているが、2つ目の出現は自由である。 | |
| 110 | |
| 111 ラムダ計算において、計算とは引数に対する関数の適用である。 | |
| 112 抽象に対して項を適用した場合、抽象の本体に存在する束縛変数に適用する項を代入したもので書き換える。 | |
| 113 図式的には | |
| 114 | |
| 115 \begin{equation*} | |
| 116 (\lambda x . t_{12}) t_2 \rightarrow [ x \mapsto t_2] t_{12} | |
| 117 \end{equation*} | |
| 118 | |
| 119 と記述する。 | |
| 120 ここで $ [ x \mapsto t_2] t_{12} $ とは、$ t_12 $ 中の自由な $ x $ を全て $ t_2 $ で置換した項を意味する。 | |
| 121 例えば、 $ (\lambda x . x) \; y $ は $ y $ となり、項 $ (\lambda x . x (\lambda x . x)) (y \; z) $ は $ y \; z \; (\lambda x . x) $ となる。 | |
| 122 | |
| 123 なお、 $ (\lambda x . t_{12}) t_2 $ という形の項を簡約基(redex, reducible expression) と呼び、上記の規則で簡約基を置換する操作をベータ簡約と呼ぶ。 | |
| 124 ラムダ計算のための評価戦略には数種類の戦略がある。 | |
| 125 | |
| 126 \begin{itemize} | |
| 127 \item 完全ベータ簡約 | |
| 128 | |
| 129 任意の簡約基がいつでも簡約されうる。 | |
| 130 つまり項の中からどの順番で簡約しても良い。 | |
| 131 | |
| 132 \item 正規順序簡約 | |
| 133 | |
| 134 最も左で最も外側の簡約基が最初に簡約される。 | |
| 135 | |
| 136 \item 名前呼び | |
| 137 | |
| 138 正規順序の中でも抽象の内部での簡約を許さない。 | |
| 139 名前呼びの変種は Algol-60 や Haskell で利用されている。 | |
| 140 なお、Haskell においては必要呼びという最適化された変種を利用している。 | |
| 141 | |
| 142 \item 値呼び | |
| 143 | |
| 144 ほとんどの言語はこの戦略を用いている。 | |
| 145 基本的には最も左の簡約基をを簡約するが、右側が既に値(計算が終了してもう簡約できない閉じた項)になっている簡約基のみを簡約する。 | |
| 146 \end{itemize} | |
| 147 | |
| 148 値呼び戦略は関数の引数が本体で使われるかに関わらず評価され、これは正格と呼ばれる。 | |
| 149 名前呼びなどの非正格な戦略は引数が使われる時のみ評価され、これは遅延評価とも呼ばれる。 | |
| 150 | |
| 151 ラムダ計算において、複数の引数は、関数を返り値として返す高階関数として定義できる。 | |
| 28 | 152 |
| 153 \section{単純型付きラムダ計算} | |
| 154 \section{部分型付け} | |
| 155 \section{部分型と Continuation based C} |