Mercurial > hg > Papers > 2018 > nozomi-master

--- a/paper/agda.tex	Wed Feb 08 14:27:06 2017 +0900
+++ b/paper/agda.tex	Wed Feb 08 14:49:51 2017 +0900
@@ -1,8 +1,72 @@
 \chapter{証明支援系言語 Agda による証明手法}
 \label{chapter:agda}
-第~\ref{chapter:type}章では形無し算術式と型付き算術式による型システムの定義、ラムダ計算によるプログラミング言語の抽象化、部分型の導入とCbCの型が部分型で示せることを確認した。
-部分型を用いて具体的なCbCの型システムを定義する前に、型システムの一方のメリットである証明について触れる。
-依存型という型を持つ証明支援系言語 Agda を用いて証明が行なえることを示す。
+\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
+しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。
+
+そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
+CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
+証明を行なう機構として注目したのが型システムである。
+
+型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。
+依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。
+
+% {{{ 型システムとは TODO: もう少し大ざっぱに説明
+\section{型システムとは}
+型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
+ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
+例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。
+この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。
+加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。
+
+型システムで行なえることには以下のようなものが存在する。
+
+\begin{itemize}
+    \item エラーの検出
+
+        文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。
+        この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。
+        多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。
+        他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
+        複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。
+
+    \item 抽象化
+
+        型は大規模プログラムの抽象化の単位にもなる。
+        例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
+        モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
+        このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。
+
+    \item ドキュメント化
+
+        型はプログラムを理解する際にも有用である。
+        関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
+        また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。
+
+    \item 言語の安全性
+
+        安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
+        例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
+        しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
+        より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。
+
+    \item 効率性
+
+        そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける式の区別であった。
+        整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
+        型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
+        昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。
+
+\end{itemize}
+
+型システムの定義には多くの定義が存在する。
+型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。
+例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
+これは Haskell が C言語よりも厳密な型システムを採用しているからである。
+具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。
+
+型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。
+
+% }}}

 % {{{ Natural Deduction
 \section{Natural Deduction}
@@ -219,7 +283,7 @@

 % }}}

-% {{{ Curry-Howard Isomorphism
+% {{{ Curry-Howard Isomorphism TODO: もっと増やす(Agda でラムダ計算を説明する)
 \section{Curry-Howard Isomorphism}
 \label{section:curry_howard_isomorphism}
 \ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
--- a/paper/akasha.tex	Wed Feb 08 14:27:06 2017 +0900
+++ b/paper/akasha.tex	Wed Feb 08 14:49:51 2017 +0900
@@ -231,10 +231,5 @@
 実際、赤黒木に恣意的なバグを追加した際にも仕様の反例は得られず、CBMC で扱える範囲内では赤黒木の性質は検証できなかった。

 よって、CBMCでは検証できない範囲の検証を akasha で行なえることが確認できた。
-しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは言いづらい。
-より大きな数を扱っても現実的な速度で検証が行なえる必要がある。
-そのためには記号化なので状態の抽象化や、何らかの機構により状態の削減を行なう必要がある。
-CbC における状態の抽象化の内部表現や、状態を削減するための制約として、型に注目した。
-特に、型を値として利用できる

 % }}}
Binary file paper/atton-master.pdf has changed
--- a/paper/atton-master.tex	Wed Feb 08 14:27:06 2017 +0900
+++ b/paper/atton-master.tex	Wed Feb 08 14:49:51 2017 +0900
@@ -121,13 +121,12 @@
 \mainmatter

 %chapters
-%\input{introduction.tex}
+\input{introduction.tex}
 \input{cbc.tex}
 \input{akasha.tex}
-%\input{type.tex}
-%\input{agda.tex}
-%\input{cbc-type.tex}
-%\input{summary.tex}
+\input{agda.tex}
+\input{cbc-type.tex}
+\input{summary.tex}

 %謝辞
 \addcontentsline{toc}{chapter}{謝辞}
--- a/paper/cbc-type.tex	Wed Feb 08 14:27:06 2017 +0900
+++ b/paper/cbc-type.tex	Wed Feb 08 14:49:51 2017 +0900
@@ -1,8 +1,285 @@
 \chapter{Agda における Continuation based C の表現}
 \label{chapter:cbc-type}
-CbC の項を部分型を用いて Agda 上に記述していく。
-DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、 Agda 上で実行できることを確認する。
-また、Agda上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 上で証明していく。
+~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。
+加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。
+
+この章では CbC の型システムを部分型を利用して定義する。
+定義した型システムがきちんと検査されるかを確認するため、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、型付けされることを確認する。
+また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 証明する。
+
+% {{{ 部分型付け
+
+\section{部分型付け}
+単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
+ここで、 単純型の拡張として、レコードを導入する。
+
+レコードとは名前の付いた複数の値を保持するデータである。
+C 言語における構造体などがレコードに相当する。
+値を保持する各フィールド $ t_1 $ はあらかじめ定められた集合 L からラベル $ l_i$ を名前として持つ。
+例えば $ { x : Nat } $ や $ {no : 100, point 33}$ などがこれに相当する。
+なお、あるレコードの項や値に表れるラベルはすべて相異なるとする。
+レコードから値を取り出す際にはラベルを指定して値を射影する。
+
+レコードの拡張の定義は以下である。
+
+\begin{definition}
+    レコードの拡張に用いる新しい構文形式
+
+    \begin{align*}
+        t :: = ...                    && \text{項 :} \\
+        \{l_i = t_i^{\; i \in 1 .. n}\} && \text{レコード} \\
+        t.l                           && \text{射影} \\
+    \end{align*}
+
+    \begin{align*}
+        v :: = ...                  && \text{値 :} \\
+        {l_i : v_i^{\; i \in 1..n}} && \text{レコードの値}
+    \end{align*}
+
+    \begin{align*}
+        T :: = ...                  && \text{型 :} \\
+        \{l_i : T_i^{\; i \in 1..n}\} && \text{レコードの型}
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    レコードの拡張に用いる新しい評価規則
+
+    \begin{align*}
+        \{l_i = v_i^{\; i \in 1..n}.l_j \rightarrow v_j\} && \text{E-PROJRCD} \\
+        \AxiomC{$t_1 \rightarrow t_1'$}
+        \UnaryInfC{$t_1.l \rightarrow t_1'.l$}
+        \DisplayProof && \text{E-PROJ} \\
+        \AxiomC{$ t_j \rightarrow t_j'$}
+        \UnaryInfC{$ \{l_i = v_i^{i \in 1..j-1}, l_j = t_j, l_k = t_k^{k \in j+1 .. n}\}
+                     \rightarrow
+                     \{l_i = v_i^{i \in 1..j-1}, l_j = t_j', l_k = t_k^{k \in j+1 .. n}\}
+                   $}
+        \DisplayProof && \text{E-RCD} \\
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    レコードの拡張に用いる新しい型付け規則
+
+    \begin{align*}
+        \AxiomC{各iに対して$ \Gamma \vdash t_i : T_i$}
+        \UnaryInfC{$ \Gamma \vdash \{ l_i = t_i^{\; i \in 1..n} : \{l_i : T_i^{\; i \in 1..n}\}$}
+        \DisplayProof && \text{T-RCD} \\
+        \AxiomC{$ \Gamma \vdash t_1 : \{ l_i : T_i^{\; i \in 1.. n}\}$}
+        \UnaryInfC{$\Gamma \vdash t_1.lj : T_j$}
+        \DisplayProof && \text{T-PROJ}
+    \end{align*}
+\end{definition}
+
+レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
+しかし、引数にレコードを取る場合、その型と完全に一致させる必要がある。
+例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。
+しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。
+
+部分型付けの目標は上記のような場合の項を許すように型付けを改良することにある。
+つまり型 $ S $ の任意の項が、型 $ T $ の項が期待される文脈において安全に利用できることを示す。
+この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。
+これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。
+$ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。
+
+型付け関係と部分型関係をつなぐための新しい型付け規則を考える。
+
+\begin{align*}
+    \AxiomC{$\Gamma \vdash t : S $}
+    \AxiomC{$ S <: T $}
+    \BinaryInfC{$ \Gamma \vdash t : T$}
+    \DisplayProof && \text {T-SUB}
+\end{align*}
+
+この規則は $ S <: T $ ならば $ S $ 型の要素 $ t$はすべて $ T $の要素であると言っている。
+例えば、先程の $ \{ x : Nat \} $ と $ \{ x : Nat , y : Bool\}$ が $ \{ x : Nat , y : Bool\} <: \{ x : Nat \}$ となるように部分型関係を定義した時に $ \Gamma \vdash \{x=0, y=1\} : \{ x : Nat \}$ を導ける。
+
+部分型関係は $ S <: T $ という形式の部分型付け式を導入するための推論規則の集まりとして定式化される。
+始めに、部分型付けの一般的な規定から考える。
+部分型は反射的であり、推移的である。
+
+\begin{align*}
+    S <: S && \text{S-REFL} \\
+    \AxiomC{$S <: U$}
+    \AxiomC{$U <: T$}
+    \BinaryInfC{$ S <: T $}
+    \DisplayProof && \text{S-TRANS}
+\end{align*}
+
+これらの規則は安全代入に対する直感より正しい。
+次に、基本型や関数型、レコード型などの型それぞれに対して、その形の型の要素が期待される部分に対して上位型の要素を利用しても安全である、という規則を導入していく。
+
+レコード型については型 $ T = \{ l_i : T_1 ... l_n : T_n\} $が持つフィールドが型 $ S = \{ k_1 : S_1 ... k_n : T_n\} $のものよりも少なければ $S$ を $T$の部分型とする。
+つまりレコードの終端フィールドのいくつかを忘れてしまっても安全である、ということを意味する。
+この直感は幅部分型付け規則となる。
+
+\begin{align*}
+    \{l_i : T_i^{\; i \in 1..n+k} \} <: \{l_i : T_i^{\; i \in 1..n}\}
+    && \text{S-RCDWIDTH}
+\end{align*}
+
+フィールドの多い方が部分型となるのは名前に反するように思える。
+しかし、フィールドが多いレコードほど制約が多くなり表すことのできる集合の範囲は小さくなる。
+集合の大きさで見ると明かにフィールドの多い方が小さいのである。
+
+幅部分型付け規則が適用可能なのは、共通のフィールドの型が全く同じな場合のみである。
+しかし、その場合フィールドの型に部分型を導入できず、フィールドの型の扱いで同じ問題を抱えることとなる。
+そのために導入するのが深さ部分型付けである。
+二つのレコードの中で対応するフィールドの型が部分型付け関係にある時に個々のフィールドの型が異なることを許す。
+これは具体的には以下の規則となる。
+
+\begin{align*}
+    \AxiomC{各iに対して $S_i <: T_i$}
+    \UnaryInfC{$\{ l_i : S_i^{\; i \in 1..n}\} <: \{l_i : T_i^{\; i \in 1..n}\}$}
+    \DisplayProof && \text{S-RCDDEPTH}
+\end{align*}
+
+これらを用いて $ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\}$ が $ \{x : \{ a : Nat\}, y : \{\}\}$の部分型であることは以下のように導出できる。
+
+\begin{prooftree}
+    \AxiomC{}
+    \RightLabel{S-RCDWIDTH}
+    \UnaryInfC{$ \{a : Nat, b : Nat\} <: \{a : Nat\}$}
+    \AxiomC{}
+    \RightLabel{S-RCDWIDTH}
+    \UnaryInfC{$ \{m : Nat\} <: \{\}$}
+    \RightLabel{S-RCDDEPTH}
+    \BinaryInfC{$ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\} <:  \{x : \{ a : Nat\}, y : \{\}\}$}
+\end{prooftree}
+
+最後に、レコードを利用する際はフィールドさえ揃っていれば順序は異なっても良いという規則を示す。
+
+\begin{align*}
+    \AxiomC{$ \{ k_j : S_j^{\; i \in 1 .. n} \}$ は $ \{ l_i : T_i^{\; i \in 1 ..n}\} $ の並べ替えである}
+    \UnaryInfC{$ \{k_j : S_j^{\; j \in 1..n} \} <: \{l_i : T_i^{\; i \in 1..n }\}$}
+    \DisplayProof && \text{S-RCDPERM}
+\end{align*}
+
+S-RCDPERM を用いることで、終端フィールドだけではなく任意の位置のフィールドを削ることができる。
+
+レコードの部分型は定義できたので、次は関数の部分型を定義していく。
+関数の部分型は以下 S-ARROW として定義できる。
+
+\begin{align*}
+    \AxiomC{$ T_1 <: S_1$}
+    \AxiomC{$ S_2 <: T_2$}
+    \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $}
+    \DisplayProof && \text{S-ARROW}
+\end{align*}
+
+前提の条件二つを見ると部分型の関係が逆転している。
+左側の条件は関数型自身の型と逆になっているため反変と言い、返り値の型は同じ向きであるため共変と言う。
+引数について考えた時、求める型よりも大きい型であれば明らかに安全に呼ぶことができるために関数の引数の型の方が上位型になる。
+返り値については関数が返す型が部分型であれば上位型を返すことができるため、関数の返り値の方が部分型になる。
+
+別の見方をすると、型 $ S_1 \rightarrow S_2 $ の関数を別の型 $ T_1 \rightarrow T_2 $が期待される文脈で用いることが安全な時とは
+
+\begin{itemize}
+    \item 関数に渡される引数がその関数にとって想定外でない($ T_1 <: S_1$)
+    \item 関数が返す値も文脈にとって想定外でない($ S_2 <: T_2 $)
+\end{itemize}
+
+という場合に限る。
+
+% }}}
+
+% {{{ 部分型と Continuation based C
+
+\section{部分型と Continuation based C}
+部分型を用いて Conituation based C の型システムを定義していく。
+
+まず、DataSegment の型から定義してく。
+DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。
+例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。
+
+\lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h}
+この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ であると見なせる。
+CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。
+
+次に Meta DataSegment について考える。
+Meta DataSegment はプログラムに出現する DataSegment の共用体であった。
+これを DataSegment の構造体に変更する。
+こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。
+もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。
+第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。
+なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だか持つ実装になっている。
+
+具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。
+\lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h}
+
+部分型として定義するなら以下のような定義となる。
+
+\begin{definition}
+    Meta DataSegment の定義
+
+    \begin{align*}
+        Meta \; DataSegment <: DataSegment_i^{i \in N} && \text{S-MDS}
+    \end{align*}
+\end{definition}
+
+なお、$N$はあるプログラムに出現するデータセグメントの名前の集合であるとする。
+
+次に CodeSegment の型について考える。
+CodeSegment は DataSegment を DataSegment へと移す関数型とする。
+
+\begin{definition}
+    CodeSegment の定義
+
+    \begin{align*}
+        DataSegment \rightarrow DataSegment && \text{T-CS}
+    \end{align*}
+\end{definition}
+
+そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。
+
+\begin{definition}
+    Meta CodeSegment の定義
+
+    \begin{align*}
+        Meta \; DataSegment \rightarrow Meta \; DataSegment && \text{T-MCS}
+    \end{align*}
+\end{definition}
+
+ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。
+
+\lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c}
+
+CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。
+現状は \verb/Context/ も継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。
+その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\}  $ となる。
+また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。
+よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。
+$ Context $ の型は Meta DataSegment なので、 subtype の S-ARROW より $Context $の上位型への変更ができる。
+
+$ \{ allocat; : Allocate , akashaInfo : AkahsaInfo\}  $ を $X$と置いて、\verb/getMinHeignt/ を $ X \rightarrow X $ とする際の導出木は以下である。
+
+\begin{prooftree}
+    \AxiomC{}
+    \RightLabel{S-REFL}
+    \UnaryInfC{$ X <: X $}
+    \AxiomC{}
+    \RightLabel{S-MDS}
+    \UnaryInfC{$ Conttext <: X$}
+    \RightLabel{S-ARROW}
+    \BinaryInfC{$ X \rightarrow Context <: X \rightarrow X$}
+\end{prooftree}
+
+返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
+プログラムによっては遷移先は確定しているために部分型にする必要性は無いが、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に包摂関係から具体型を導けば良い。
+例えばコンパイル時に解決すればライブラリの静的リンク時実行コード生成が行なえ、ランタイム時に解決すればネットワークを経由するプログラムとの接続初期化に利用できる。
+例えば、プロトコルがバージョンを持つ場合に接続先のプログラムが利用しているプロトコルと互換性があるかの判断を Context どうしの部分型関係で判断できる。
+
+また、stub のみに注目すると、stub は Context から具体的なDataSegment X を取り出す操作に相当し、S-ARROWの左側の前提のような振舞いをする。
+加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、S-ARROWの右側の前提のような振舞いを行なう。
+このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。
+型付けにDataSegment の集合としての Meta DataSegment が必須になるが、これは構造体として定義可能なためコンパイル時に生成することで CbC に組み込むことができる。
+
+なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。
+ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。
+このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。
+
+% }}}

 % {{{ DataSegment の定義
 \section{DataSegment の定義}
--- a/paper/history.tex	Wed Feb 08 14:27:06 2017 +0900
+++ b/paper/history.tex	Wed Feb 08 14:49:51 2017 +0900
@@ -1,5 +1,6 @@
 \chapter*{発表履歴}
 \begin{itemize}
+\item 比嘉健太, 河野真治. Agda入門. オープンソースカンファレンス2014 Okinawa, May 2014.
 \item 比嘉健太, 河野真治. 形式手法を学び始めて思うことと、形式手法を広めるには. 情報処理学会ソフトウェア工学研究会(IPSJ SIGSE) ウィンターワークショップ2015・イン・宜野湾(WWS2015), Jan 2015.
 \item 比嘉健太, 河野真治.  Continuation based C を用いたプログラムの検証手法.  2016年並列／分散／協調処理に関する『松本』サマー・ワークショップ(SWoPP2016) 情報処理学会・プログラミング研究会 第110回プログラミング研究会(PRO-2016-2) Aug 2016.
 \end{itemize}
--- a/paper/type.tex	Wed Feb 08 14:27:06 2017 +0900
+++ b/paper/type.tex	Wed Feb 08 14:49:51 2017 +0900
@@ -1,11 +1,5 @@
 \chapter{ラムダ計算と型システム}
 \label{chapter:type}
-\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
-しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。
-
-そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
-CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
-証明を行なう機構として注目したのが型システムである。

 \ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment を定義する。
 また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。
@@ -15,64 +9,6 @@
 CbC は直接自身を証明する機構が存在しない。
 プログラムの性質を証明するには CbC の形式的な定義が必須となる。

-% {{{ 型システムとは
-\section{型システムとは}
-型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
-ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
-例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。
-% TODO: C の warning?
-この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。
-加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。
-
-型システムで行なえることには以下のようなものが存在する。
-
-\begin{itemize}
-    \item エラーの検出
-
-        文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。
-        この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。
-        多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。
-        他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
-        複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。
-
-    \item 抽象化
-
-        型は大規模プログラムの抽象化の単位にもなる。
-        例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
-        モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
-        このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。
-
-    \item ドキュメント化
-
-        型はプログラムを理解する際にも有用である。
-        関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
-        また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。
-
-    \item 言語の安全性
-
-        安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
-        例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
-        しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
-        より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。
-
-    \item 効率性
-
-        そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける式の区別であった。
-        整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
-        型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
-        昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。
-
-\end{itemize}
-
-型システムの定義には多くの定義が存在する。
-型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。
-例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
-これは Haskell が C言語よりも厳密な型システムを採用しているからである。
-具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。
-
-型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。
-
-% }}}

 % {{{ 型無し算術式
 \section{型無し算術式}
@@ -967,276 +903,3 @@

 % }}}

-% {{{ 部分型付け
-
-\section{部分型付け}
-単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
-ここで、 単純型の拡張として、レコードを導入する。
-
-レコードとは名前の付いた複数の値を保持するデータである。
-C 言語における構造体などがレコードに相当する。
-値を保持する各フィールド $ t_1 $ はあらかじめ定められた集合 L からラベル $ l_i$ を名前として持つ。
-例えば $ { x : Nat } $ や $ {no : 100, point 33}$ などがこれに相当する。
-なお、あるレコードの項や値に表れるラベルはすべて相異なるとする。
-レコードから値を取り出す際にはラベルを指定して値を射影する。
-
-レコードの拡張の定義は以下である。
-
-\begin{definition}
-    レコードの拡張に用いる新しい構文形式
-
-    \begin{align*}
-        t :: = ...                    && \text{項 :} \\
-        \{l_i = t_i^{\; i \in 1 .. n}\} && \text{レコード} \\
-        t.l                           && \text{射影} \\
-    \end{align*}
-
-    \begin{align*}
-        v :: = ...                  && \text{値 :} \\
-        {l_i : v_i^{\; i \in 1..n}} && \text{レコードの値}
-    \end{align*}
-
-    \begin{align*}
-        T :: = ...                  && \text{型 :} \\
-        \{l_i : T_i^{\; i \in 1..n}\} && \text{レコードの型}
-    \end{align*}
-\end{definition}
-
-\begin{definition}
-    レコードの拡張に用いる新しい評価規則
-
-    \begin{align*}
-        \{l_i = v_i^{\; i \in 1..n}.l_j \rightarrow v_j\} && \text{E-PROJRCD} \\
-        \AxiomC{$t_1 \rightarrow t_1'$}
-        \UnaryInfC{$t_1.l \rightarrow t_1'.l$}
-        \DisplayProof && \text{E-PROJ} \\
-        \AxiomC{$ t_j \rightarrow t_j'$}
-        \UnaryInfC{$ \{l_i = v_i^{i \in 1..j-1}, l_j = t_j, l_k = t_k^{k \in j+1 .. n}\}
-                     \rightarrow
-                     \{l_i = v_i^{i \in 1..j-1}, l_j = t_j', l_k = t_k^{k \in j+1 .. n}\}
-                   $}
-        \DisplayProof && \text{E-RCD} \\
-    \end{align*}
-\end{definition}
-
-\begin{definition}
-    レコードの拡張に用いる新しい型付け規則
-
-    \begin{align*}
-        \AxiomC{各iに対して$ \Gamma \vdash t_i : T_i$}
-        \UnaryInfC{$ \Gamma \vdash \{ l_i = t_i^{\; i \in 1..n} : \{l_i : T_i^{\; i \in 1..n}\}$}
-        \DisplayProof && \text{T-RCD} \\
-        \AxiomC{$ \Gamma \vdash t_1 : \{ l_i : T_i^{\; i \in 1.. n}\}$}
-        \UnaryInfC{$\Gamma \vdash t_1.lj : T_j$}
-        \DisplayProof && \text{T-PROJ}
-    \end{align*}
-\end{definition}
-
-レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
-しかし、引数にレコードを取る場合、その型と完全に一致させる必要がある。
-例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。
-しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。
-
-部分型付けの目標は上記のような場合の項を許すように型付けを改良することにある。
-つまり型 $ S $ の任意の項が、型 $ T $ の項が期待される文脈において安全に利用できることを示す。
-この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。
-これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。
-$ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。
-
-型付け関係と部分型関係をつなぐための新しい型付け規則を考える。
-
-\begin{align*}
-    \AxiomC{$\Gamma \vdash t : S $}
-    \AxiomC{$ S <: T $}
-    \BinaryInfC{$ \Gamma \vdash t : T$}
-    \DisplayProof && \text {T-SUB}
-\end{align*}
-
-この規則は $ S <: T $ ならば $ S $ 型の要素 $ t$はすべて $ T $の要素であると言っている。
-例えば、先程の $ \{ x : Nat \} $ と $ \{ x : Nat , y : Bool\}$ が $ \{ x : Nat , y : Bool\} <: \{ x : Nat \}$ となるように部分型関係を定義した時に $ \Gamma \vdash \{x=0, y=1\} : \{ x : Nat \}$ を導ける。
-
-部分型関係は $ S <: T $ という形式の部分型付け式を導入するための推論規則の集まりとして定式化される。
-始めに、部分型付けの一般的な規定から考える。
-部分型は反射的であり、推移的である。
-
-\begin{align*}
-    S <: S && \text{S-REFL} \\
-    \AxiomC{$S <: U$}
-    \AxiomC{$U <: T$}
-    \BinaryInfC{$ S <: T $}
-    \DisplayProof && \text{S-TRANS}
-\end{align*}
-
-これらの規則は安全代入に対する直感より正しい。
-次に、基本型や関数型、レコード型などの型それぞれに対して、その形の型の要素が期待される部分に対して上位型の要素を利用しても安全である、という規則を導入していく。
-
-レコード型については型 $ T = \{ l_i : T_1 ... l_n : T_n\} $が持つフィールドが型 $ S = \{ k_1 : S_1 ... k_n : T_n\} $のものよりも少なければ $S$ を $T$の部分型とする。
-つまりレコードの終端フィールドのいくつかを忘れてしまっても安全である、ということを意味する。
-この直感は幅部分型付け規則となる。
-
-\begin{align*}
-    \{l_i : T_i^{\; i \in 1..n+k} \} <: \{l_i : T_i^{\; i \in 1..n}\}
-    && \text{S-RCDWIDTH}
-\end{align*}
-
-フィールドの多い方が部分型となるのは名前に反するように思える。
-しかし、フィールドが多いレコードほど制約が多くなり表すことのできる集合の範囲は小さくなる。
-集合の大きさで見ると明かにフィールドの多い方が小さいのである。
-
-幅部分型付け規則が適用可能なのは、共通のフィールドの型が全く同じな場合のみである。
-しかし、その場合フィールドの型に部分型を導入できず、フィールドの型の扱いで同じ問題を抱えることとなる。
-そのために導入するのが深さ部分型付けである。
-二つのレコードの中で対応するフィールドの型が部分型付け関係にある時に個々のフィールドの型が異なることを許す。
-これは具体的には以下の規則となる。
-
-\begin{align*}
-    \AxiomC{各iに対して $S_i <: T_i$}
-    \UnaryInfC{$\{ l_i : S_i^{\; i \in 1..n}\} <: \{l_i : T_i^{\; i \in 1..n}\}$}
-    \DisplayProof && \text{S-RCDDEPTH}
-\end{align*}
-
-これらを用いて $ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\}$ が $ \{x : \{ a : Nat\}, y : \{\}\}$の部分型であることは以下のように導出できる。
-
-\begin{prooftree}
-    \AxiomC{}
-    \RightLabel{S-RCDWIDTH}
-    \UnaryInfC{$ \{a : Nat, b : Nat\} <: \{a : Nat\}$}
-    \AxiomC{}
-    \RightLabel{S-RCDWIDTH}
-    \UnaryInfC{$ \{m : Nat\} <: \{\}$}
-    \RightLabel{S-RCDDEPTH}
-    \BinaryInfC{$ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\} <:  \{x : \{ a : Nat\}, y : \{\}\}$}
-\end{prooftree}
-
-最後に、レコードを利用する際はフィールドさえ揃っていれば順序は異なっても良いという規則を示す。
-
-\begin{align*}
-    \AxiomC{$ \{ k_j : S_j^{\; i \in 1 .. n} \}$ は $ \{ l_i : T_i^{\; i \in 1 ..n}\} $ の並べ替えである}
-    \UnaryInfC{$ \{k_j : S_j^{\; j \in 1..n} \} <: \{l_i : T_i^{\; i \in 1..n }\}$}
-    \DisplayProof && \text{S-RCDPERM}
-\end{align*}
-
-S-RCDPERM を用いることで、終端フィールドだけではなく任意の位置のフィールドを削ることができる。
-
-レコードの部分型は定義できたので、次は関数の部分型を定義していく。
-関数の部分型は以下 S-ARROW として定義できる。
-
-\begin{align*}
-    \AxiomC{$ T_1 <: S_1$}
-    \AxiomC{$ S_2 <: T_2$}
-    \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $}
-    \DisplayProof && \text{S-ARROW}
-\end{align*}
-
-前提の条件二つを見ると部分型の関係が逆転している。
-左側の条件は関数型自身の型と逆になっているため反変と言い、返り値の型は同じ向きであるため共変と言う。
-引数について考えた時、求める型よりも大きい型であれば明らかに安全に呼ぶことができるために関数の引数の型の方が上位型になる。
-返り値については関数が返す型が部分型であれば上位型を返すことができるため、関数の返り値の方が部分型になる。
-
-別の見方をすると、型 $ S_1 \rightarrow S_2 $ の関数を別の型 $ T_1 \rightarrow T_2 $が期待される文脈で用いることが安全な時とは
-
-\begin{itemize}
-    \item 関数に渡される引数がその関数にとって想定外でない($ T_1 <: S_1$)
-    \item 関数が返す値も文脈にとって想定外でない($ S_2 <: T_2 $)
-\end{itemize}
-
-という場合に限る。
-
-% }}}
-
-% {{{ 部分型と Continuation based C
-
-\section{部分型と Continuation based C}
-部分型を用いて Conituation based C の型システムを定義していく。
-
-まず、DataSegment の型から定義してく。
-DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。
-例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。
-
-\lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h}
-この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ であると見なせる。
-CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。
-
-次に Meta DataSegment について考える。
-Meta DataSegment はプログラムに出現する DataSegment の共用体であった。
-これを DataSegment の構造体に変更する。
-こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。
-もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。
-第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。
-なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だか持つ実装になっている。
-
-具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。
-\lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h}
-
-部分型として定義するなら以下のような定義となる。
-
-\begin{definition}
-    Meta DataSegment の定義
-
-    \begin{align*}
-        Meta \; DataSegment <: DataSegment_i^{i \in N} && \text{S-MDS}
-    \end{align*}
-\end{definition}
-
-なお、$N$はあるプログラムに出現するデータセグメントの名前の集合であるとする。
-
-次に CodeSegment の型について考える。
-CodeSegment は DataSegment を DataSegment へと移す関数型とする。
-
-\begin{definition}
-    CodeSegment の定義
-
-    \begin{align*}
-        DataSegment \rightarrow DataSegment && \text{T-CS}
-    \end{align*}
-\end{definition}
-
-そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。
-
-\begin{definition}
-    Meta CodeSegment の定義
-
-    \begin{align*}
-        Meta \; DataSegment \rightarrow Meta \; DataSegment && \text{T-MCS}
-    \end{align*}
-\end{definition}
-
-ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。
-
-\lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c}
-
-CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。
-現状は \verb/Context/ も継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。
-その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\}  $ となる。
-また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。
-よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。
-$ Context $ の型は Meta DataSegment なので、 subtype の S-ARROW より $Context $の上位型への変更ができる。
-
-$ \{ allocat; : Allocate , akashaInfo : AkahsaInfo\}  $ を $X$と置いて、\verb/getMinHeignt/ を $ X \rightarrow X $ とする際の導出木は以下である。
-
-\begin{prooftree}
-    \AxiomC{}
-    \RightLabel{S-REFL}
-    \UnaryInfC{$ X <: X $}
-    \AxiomC{}
-    \RightLabel{S-MDS}
-    \UnaryInfC{$ Conttext <: X$}
-    \RightLabel{S-ARROW}
-    \BinaryInfC{$ X \rightarrow Context <: X \rightarrow X$}
-\end{prooftree}
-
-返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
-プログラムによっては遷移先は確定しているために部分型にする必要性は無いが、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に包摂関係から具体型を導けば良い。
-例えばコンパイル時に解決すればライブラリの静的リンク時実行コード生成が行なえ、ランタイム時に解決すればネットワークを経由するプログラムとの接続初期化に利用できる。
-例えば、プロトコルがバージョンを持つ場合に接続先のプログラムが利用しているプロトコルと互換性があるかの判断を Context どうしの部分型関係で判断できる。
-
-また、stub のみに注目すると、stub は Context から具体的なDataSegment X を取り出す操作に相当し、S-ARROWの左側の前提のような振舞いをする。
-加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、S-ARROWの右側の前提のような振舞いを行なう。
-このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。
-型付けにDataSegment の集合としての Meta DataSegment が必須になるが、これは構造体として定義可能なためコンパイル時に生成することで CbC に組み込むことができる。
-
-なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。
-ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。
-このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。
-
-% }}}