\chapter{ラムダ計算と型システム}
\label{chapter:type}
\ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。
CbC は直接自身を証明する機構が存在しない。
プログラムの性質を証明するには CbC の形式的な定義が必須となる。
\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。
また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。

% {{{ 型システムとは
\section{型システムとは}
型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。
% TODO: C の warning?
この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。
加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。

型システムで行なえることには以下のようなものが存在する。

\begin{itemize}
    \item エラーの検出

        文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。
        この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。
        多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。
        他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
        複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。

    \item 抽象化

        型は大規模プログラムの抽象化の単位にもなる。
        例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
        モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
        このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。

    \item ドキュメント化

        型はプログラムを理解する際にも有用である。
        関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
        また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。

    \item 言語の安全性

        安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
        例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
        しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
        より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。

    \item 効率性

        そもそも、科学計算機における最初の型システムは Fortran などにおける式の区別であった。% TODO ref fortran
        整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
        型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
        昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。

\end{itemize}

型システムの定義には多くの定義が存在する。
型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。
例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
これは Haskell が C言語よりも厳密な型システムを採用しているからである。
具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。

型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。

% }}}

% {{{ 型無し算術式
\section{型無し算術式}
まず、型システムやその性質について述べるためにプログラミング言語そのものの基本的な性質について述べる。
プログラムの構文と意味論、推論について考えるために自然数とブール値のみで構成される小さな言語を扱いながら考察する。
この言語は二種類の値しか持たないが、項の帰納的定義や証明、評価、実行時エラーのモデル化を表現することができる。

この言語はブール定数 $ true $ と $ false $ 、条件式、数値定数 0 、算術演算子 $ succ $ と $ pred $ 、判定演算子 $ iszero $ のみからなる。
算術演算子 $ succ $ は与えられた数の次の数を返し、 $ pred $ はその前の数を返す。
判定演算子$ iszero $ は与えられた項が 0 なら $ true $ を返し、それ以外は $ false $ を返す。
これらを文法として定義すると以下のリスト\ref{src:expr-term}のようになる。

\lstinputlisting[label=src:expr-term, caption=算術式の項定義] {src/expr-term.txt}

この定義では算術式の項 $ t $ を定義している。
$ ::= $ は項の集合の定義を表であり、$ t $ は項の変数のようなものである。
それに続くすべての行は、構文の選択肢である。
構文の選択肢内に存在する記号 $ t $ は任意の項を代入できることを表現している。
このように再帰的に定義することにより、 \verb/ if (ifzero (succ 0)) then true else (pred (succ 0)) / といった項もこの定義に含まれる。
例において、 $ succ $ 、 $ pred $ 、 $ iszero $ に複合的な引数を渡す場合は読みやすさのために括弧でくくっている。
括弧の定義は項の定義には含んでいない。
コンパイラなど具体的な字句をパースする必要がある場合、曖昧な構文を排除するために括弧の定義は必須である。
しかし、今回は型システムに言及するために曖昧な構文は明示的に括弧で指示することで排除し、抽象的な構文のみを取り扱うこととする。

現在、項と式という用語は同一である。
型のような別の構文表現を持つ計算体系においては式はあらゆる種類の構文を表す。
項は計算の構文的表現という意味である。

この言語におけるプログラムとは上述の文法で与えられた形からなる項である。
評価の結果は常にブール定数か自然数のどちらかになる。
これら項は値と呼ばれ、項の評価順序の形式化において区別が必要となる。

なお、この項の定義においては \verb/succ true/ といった怪しい項の形成を許してしまう。
実際、これらのプログラムは無意味なものであり、このような項表現を排除するために型システムを利用する。

ある言語の構文を定義する際に、他の表現かいくつか存在する。
先程の定義は次の帰納的な定義のためのコンパクトな記法である。

\begin{definition}
    項の集合とは以下の条件を満たす最小の集合 $ T $ である。
    \begin{eqnarray*}
        \label{eq:expr}
        \{true , false , 0\} \subseteq T \\
        t_1 \in T ならば \{succ \; t_1 , pred \; t_1 , iszero \; t_1\} \subseteq T \\
        t_1 \in T かつ t_2 \in T かつ t_3 \in T ならば if \; t_1 \; then \; t_2 else \; t_3 \subseteq T
    \end{eqnarray*}
\end{definition}

まず1つめの条件は、$ T $ に属する3つの式を挙げている。
2つめと3つめの条件は、ある種の複合的な式が $ T $ に属することを判断するための規則を表している。
最後の「最小」という単語は $ T $ がこの3つの条件によって要求される要素以外の要素を持たないことを表している。

また、項の帰納的表現の略記法として、二次元の推論規則形式を用いる方法もある。
これは論理体系を自然演繹スタイルで表現するためによく使われる。
自然演繹による証明は\ref{agda}章内で触れるが、今回は項表現として導入する。

\begin{definition}
    項の集合は次の規則によって定義される。

    \begin{prooftree}
        \AxiomC{$ true \in T $}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$ false \in T $}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$ 0 \in T $}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$ t_1 \in T $}
        \UnaryInfC{$ succ \; t_1 \in T$}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$ t_1 \in T $}
        \UnaryInfC{$ pred \; t_1 \in T$}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$ t_1 \in T $}
        \UnaryInfC{$ iszero \; t_1 \in T$}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$ t_1 \in T $}
        \AxiomC{$ t_2 \in T $}
        \AxiomC{$ t_3 \in T $}
        \TrinaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \in T$}
    \end{prooftree}

\end{definition}

最初の$ true, \; false, \; 0 $の3つ規則は再帰的定義の1つめの条件と同じである。
それ以外の4つの規則は再帰的定義の2つめと3つめの条件と同じである。
それぞれの規則は「もし線の上に列挙して前提が成立するのならば、線の下の結論を導出できる」と読む。
$ T $ がこれらの規則を満たす最小の集合である事実は明示的に述べられない。

言語の構文は定義できたので、次は項がどう評価されるかの意味論について触れていく。
意味論の形式化には操作的意味論や表示的意味論、公理的意味論やゲーム意味論などがあるが、ここでは操作的意味論について述べる。
操作的意味論とは、言語の抽象機械を定義することにより言語の振舞いを規程する。
この抽象機械が示す抽象とは、扱う命令がプロセッサの命令セットなどの具体的なものでないことを表している。
単純な言語の抽象機械における状態は単なる項であり、機械の振舞いは遷移関数で定義される。
この関数は各状態において項の単純化ステップを実行して次の状態を与えるか、機械を停止させる。
ここで項 $ t $ の意味は、$ t $ を初期状態として動き始めた機械が達する最終状態である。

なお、一つの言語に複数の操作的意味論を与えることもある。
例えば、プログラマが扱う項に似た機械状態を持つ意味論の他に、コンパイラの内部表現やインタプリタが扱う意味論を定義する。
これらの振舞いが同じプログラムを実行した時に何かしらの意味であれば、結果としてその言語の実装の正しさを証明することに繋がる。

まずはブール式のみの操作的意味論を定義する。

\begin{definition}
    ブール値(B)

    項
    \begin{align*}
        t ::=                             && \text{項}     \\
        true                              && \text{定数真} \\
        false                             && \text{定数偽} \\
        if \; t \; then \; t \; else \; t && \text{条件式}
    \end{align*}

    値
    \begin{align*}
        v ::=                             && \text{値} \\
        true                              && \text{真} \\
        false                             && \text{偽}
    \end{align*}

    評価
    \begin{align*}
        if \; true  \; then \; t_2 \; else t_3 \rightarrow t_2 && \text{(E-IFTRUE)}  \\
        if \; false \; then \; t_2 \; else t_3 \rightarrow t_3 && \text{(E-IFFALSE)} \\
        \AxiomC{$ t_1 \rightarrow t_1'$}
        \UnaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \rightarrow if \; t_1' \; then t_2 \; else \;t_3 $}
        \DisplayProof
        && \text{(E-IF)}
    \end{align*}

\end{definition}

評価の最終結果になりえる項である値は定数 $ true $ と $ false $ のみである。
評価の定義は評価関係の定義である。
評価関係 $ t \rightarrow t' $ は「$ t $ が1ステップで $ t' $ に評価される」と読む。
直感的には抽象機械の状態が $ t $ ならば $ t' $ が手に入るという意味である。

評価関係は3つあるが、2つは前提を持たないため、2つの公理と1つの規則から成る。
1つめの規則 E-IFTRUE の意味は、評価の対象となる項の条件式が定数 $ true $ である時に、then 節にある $ t_2 $ を残して他の全ての項を捨てるという意味である。
E-EIFFALSE も同様に条件式が $ false $ の時に $ t_3 $ のみを残す。
3つ目の規則 E-IF は条件式の評価である。
条件式 $ t $ が $ t'$ に評価されうるのならば then 節と else 節を変えずに条件部のみを評価する。

評価の定義から分かることの中に、if の中の then節 と else 節は条件部より先に評価されないことがある。
よって、この言語は条件式の評価に対し条件部から評価が優先されるという評価戦略を持つことが分かる。

\begin{definition}
推論規則のインスタンスとは、規則の結論や前提に対し、一貫して同じ項による書き換えを行なったものである。
\end{definition}

例えば、

\verb/if true then true else (if false then false else false)/

は E-IFTRUE のインスタンスであり、 E-IFTRUEの $ t_2 $ が \verb/true/ かつ $ t_3 $ が \verb/if false then false else false/ の時である。

\begin{definition}
1ステップ評価関係 $ \rightarrow $ とは、3つの評価の規則を満たす、項に関する最小の二項関係である。
$ (t, \; t') $ がこの関係の元である時、「評価関係式 $ t \rightarrow t'$ は導出可能である」と言う。
\end{definition}

ここで「最小」という言葉が表れるため、評価関係式 $ t \rightarrow t'$ が導出可能である時かつその時に限り、その関係式は規則によって正当化される。
すなわち評価関係式は公理 E-IFTRUE か E-IFFALSE 、前提が成り立つ時の E-IF のインスタンスとなる。
与えられた評価関係式が導出可能であることを証明するには、葉が E-IFTRUE か E-IFFALSE であり、内部ノードのラベルが E-IF のインスタンスである導出木が示せれば良い。
例えば以下の略記の元 $ if \; t \; then \; false \; then \; false  \rightarrow if \; u \; then \; false \; else \; false  $ の導出可能性は以下のような導出木によって示せる。

\begin{itemize}
    \item $ s = if \; true \;  then \; false \; else \; false $
    \item $ t = if \; s \;     then \; true \;  else \; true $
    \item $ u = if \; false \; then \; true \;  else \; true $
\end{itemize}


\begin{prooftree}
    \AxiomC{}
    \RightLabel{E-IFTRUE}
    \UnaryInfC{ $ s  \rightarrow true $ }
    \RightLabel{E-IF}
    \UnaryInfC{ $ t  \rightarrow  u $}
    \RightLabel{E-IF}
    \UnaryInfC{ $ if \; t \; then \; false \; then \; false/ \rightarrow if \; u \; then \; false \; else \; false $}
\end{prooftree}

1ステップ評価関係は与えられた項に対して抽象機械の状態遷移を定義する。
この時、機械がそれ以上ステップを進められない時にそれが最終結果となる。

\begin{definition}
    正規形

    項 $ t $ が正規形であるとは、$ t \rightarrow t'$となる評価規則が存在しないことである。
\end{definition}

この言語において $ true $ や $ false $ は正規形である。
逆に言えば、構文的に正しい if が用いられている場合は評価することが可能なため正規形ではない。
極端に言えばこの言語における全ての値は正規形なのである。
しかし、他の言語における値は一般的に正規形ではない。
実のところ、値でない正規形は実行時エラーとなって表れる。

実際にこの言語に自然数を導入し、値では無い正規形を確認していく。


\begin{definition}
    算術式BN (B の拡張) の項
    \begin{align*}
        t ::=                             && \text{項}     \\
        true                              && \text{定数真} \\
        false                             && \text{定数偽} \\
        if \; t \; then \; t \; else \; t && \text{条件式} \\
        0                                 && \text{定数ゼロ} \\
        succ \; t                         && \text{後者値} \\
        pred \; t                         && \text{前者値} \\
        iszero \; t                       && \text{ゼロ判定}
    \end{align*}
\end{definition}

\begin{definition}
    算術式BN  の値
    \begin{align*}
        v ::= && \text{値} \\
        true  && \text{真} \\
        false && \text{偽} \\
        nv    && \text{数値} \\
    \end{align*}
\end{definition}

\begin{definition}
    算術式BNの数値
    \begin{align*}
        nv ::=  && \text{数値} \\
        0       && \text{ゼロ} \\
        succ nv && \text{後者値}
    \end{align*}
\end{definition}

\begin{definition}
    算術式BNの評価($ t \rightarrow t' $)
    \begin{align*}
        if \; true  \; then \; t_2 \; else t_3 \rightarrow t_2 && \text{(E-IFTRUE)}  \\
        if \; false \; then \; t_2 \; else t_3 \rightarrow t_3 && \text{(E-IFFALSE)} \\
        \AxiomC{$ t_1 \rightarrow t_1'$}
        \UnaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \rightarrow if \; t_1' \; then t_2 \; else \;t_3 $}
        \DisplayProof && \text{(E-IF)} \\
        \AxiomC{$ pred \; 0 \rightarrow 0$}
        \DisplayProof && \text{(E-PREDZERO)} \\
        \AxiomC{$ pred \; (succ \; nv_1) \rightarrow nv_1$}
        \DisplayProof && \text{(E-PREDSUCC)} \\
        \AxiomC{$ t_1 \rightarrow t_1'$}
        \UnaryInfC{$ pred \; t_1 \rightarrow pred \; t_1'$}
        \DisplayProof && \text{(E-PRED)} \\
        \AxiomC{$ iszero \; 0 \rightarrow true$}
        \DisplayProof && \text{(E-ISZEROZERO)} \\
        \AxiomC{$ iszero \; (succ \; nv_1) \rightarrow false$}
        \DisplayProof && \text{(E-ISZEROSUCC)} \\
        \AxiomC{$ t_1 \rightarrow t_1'$}
        \UnaryInfC{$ iszero \; t_1 \rightarrow iszero \; t_1'$}
        \DisplayProof && \text{(E-ISZERO)} \\
    \end{align*}
\end{definition}

今回値の定義に数値を表す構文要素が追加されている。
数は0かある数に後者関数を適用したもののどちらかである。
評価規則 E-PREDZERO、E-PREDSUCC、E-ISZEROZERO、E-ISZEROSUCC は演算 \verb/pred/ と \verb/iszero/ が数に適用された時にどう振る舞うかを定義している。
E-SUCC 、 E-PRED 、 E-ISZERO の合同規則も E-IF のように部分項から先に評価することを示している。

数値の構文要素(nv)はこの定義によって重要な役割をはたす。
例えば、 E-PREDSUCC 規則が適用できる項は任意の項 $ t $ ではなく数値 $nv_1$である。
これは $ pred \; (succ \; (pred \; 0)) $ を $ pred 0 $ に評価できないことを意味する。
なぜなら $ pred \; 0 $ は数値に含まれないからである。

ここで言語の操作的意味論について考える時、すべての項に関する振舞いを定義する必要がある。
すべての項には $ pred \; 0 $ や $ succ false $ のような項も含まれる。
しかし、 $ succ $ を $ false $ に適用する評価結果は定義されていないため、 $ succ \; false $ は正規形である。
このような、正規形であるが値でない項は行き詰まり状態であるという。
つまり、実行時エラーとは行き詰まり状態の項を指す。
直感的な解釈としてはプログラムが無意味な状態になったこと示しておい、操作的意味論が次に何も行なえないことを特徴付けているのである。
プログラング言語において実行時エラーはセグメンテーションフォールトや不正な命令などいくつかのものが挙げられるが、型システムを考える際にはこれらのエラーは行き詰まり状態という単一の概念で表す。

% }}}

% {{{ 単純型

\section{単純型}
先程定義した算術式には $ pred \; false $ のようなこれ以上評価できない行き詰まり状態が存在する。
項を実際に評価する前に評価が行き詰まり状態にならないことを保証したい。
そのために、自然数に評価される項とブール値に評価される項とを区別する必要がある。
項を分類するために2つの型 Nat と Bool を定義する。

ここで、項$t$が型 $T$を持つ、という表現を用いた場合、$t$を評価した結果が明らかに適切な形の値になることを意味する。
明らかに、という意味は項を実行することなく静的に分かるという意味である。
例えば項 $ if \; true \; then \; false \; else \; true $ は Bool 型を持ち、$ pred \; (succ \; (succ \; 0)) $ はNat 型を持つ。
しかし、項の型の分析は保守的であり、$ if \; true \; then \; 0 \; else \; false $ のような項は実際には行き詰まりにならないが型を持てない。

算術式のための型付け関係は $ t : T $ と書き、項に型を割り当てる推論規則の集合によって定義される。
具体的な数値とブール値に関する拡張は以下である。

\begin{definition}
    NB(型付き) の新しい構文形式
    \begin{align*}
        T ::= && \text{型 :} \\
        Bool  && \text{ブール型} \\
        Nat   && \text{自然数型} \\
    \end{align*}
\end{definition}


\begin{definition}
    NB(型付き)の型付け規則
    \begin{align*}
        true : Bool  && \text{T-TRUE} \\
        false : Bool && \text{T-FALSE} \\
        \AxiomC{$t_1 : Bool$}
        \AxiomC{$t_2 : T$}
        \AxiomC{$t_3 : T$}
        \TrinaryInfC{$if \; t_1 \; then \; t_2 \; else \; t_3 : T$}
        \DisplayProof && \text{T-IF} \\
        0 : Nat && \text{T-ZERO} \\
        \AxiomC{$t_1 : Nat$}
        \UnaryInfC{$ succ \; t_1 : Nat $}
        \DisplayProof && \text{T-SUCC} \\
        \AxiomC{$t_1 : Nat$}
        \UnaryInfC{$ pred \; t_1 : Nat $}
        \DisplayProof && \text{T-PRED} \\
        \AxiomC{$t_1 : Nat$}
        \UnaryInfC{$ iszero \; t_1 : Bool $}
        \DisplayProof && \text{T-BOOL}
    \end{align*}
\end{definition}

T-TRUE と T-FALSE はブール定数に Bool 型を割り当てている。
T-IFは条件式の部分にBool型を、部分式に関しては同じ型を要求している。
これは同じ変数 $ T $ を二回使用することで制約を表している。

また、数に関しては T-ZERO は Nat 型を $ 0 $ に割り当てている。
T-SUCC と T-PRED は $ t_1 $ が Nat である時に限り Nat 型となる。
同様に、 T-ISZERO は $ t_1 $ が Nat である時に Bool となる。

\begin{definition}
算術式のための型付け関係とは、NBにおける規則のすべてのインスタンスを満たす、項と型の二項関係である。
項$ t $ に対してある型 $ T $ が存在して $ t : T $ である時、 $ t $ は型付け可能である(または正しく型付けされている)という。
\end{definition}

型推論をを行なう時、$succ t_1$という項が何らかの型を持つならばそれは Nat 型である、といった言及を行なう。
型付け関係を逆転させた補題を定義することで型推論の基本的なアルゴリズムを考えることができる。
なお、逆転補題は型付け関係の定義により直ちに成り立つ。

\begin{lemma}
    型付け関係の逆転
    \begin{enumerate}
        \item $ true : R $ ならば $ R = Bool $ である
        \item $ false : R $ ならば $ R = Bool $ である
        \item $ if \; t_1 \; then \; t_2 \; else \; t_3 : R $ ならば $ t_1 : Bool $ かつ $ t_2 : R $ かつ $ t_3 : R $ である。
        \item $ 0 : R $ ならば $ R = Nat $ である
        \item $ succ \; t_1 : R $ ならば $ R = Nat $ かつ $ t_1 : Nat $ である
        \item $ pred \; t_1 : R $ ならば $ R = Nat $ かつ $ t_1 : Nat $ である
        \item $ iszero \; t_1 : R $ ならば $ R = Bool $ かつ $ t_1 : Nat $ である
    \end{enumerate}
\end{lemma}

逆転補題は型付け関係のための生成補題と呼ばれることもある。
なぜならば、与えられた型付け判断式に対してその証明がどのように生成されたかを示すからである。

型無し算術式の評価導出のように型付けも導出可能であり、それも規則のインスタンスの木である。
型付け関係に含まれる二つ組 $(t, \; T)$は $ t : T $ を結論とする型付け導出により正当化される。
例えば $ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat $ の型付け判断の導出木である。

\begin{prooftree}
    \AxiomC{}
    \RightLabel{T-ZERO}
    \UnaryInfC{$ 0 : Nat$}
    \RightLabel{T-ISZERO}
    \UnaryInfC{$ iszero \; 0 : Bool$}
    \AxiomC{}
    \RightLabel{T-ZERO}
    \UnaryInfC{$ 0 : Nat$}
    \AxiomC{}
    \RightLabel{T-ZERO}
    \UnaryInfC{$ 0 : Nat$}
    \RightLabel{T-PRED}
    \UnaryInfC{$ pred \; 0 : Bool$}
    \RightLabel{T-IF}
    \TrinaryInfC{ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat }
\end{prooftree}

項その型付けの定義より、型システムが行き詰まり状態にならないことを示す。
その証明は指向定理と保存定理によって証明する。

\begin{itemize}
    \item 進行とは、正しく型付けされた項は行き詰まり状態では無いことである
    \item 保存とは、評価可能な正しく型付けされた項は評価後も正しく型付けされていることである。
\end{itemize}

型システムがこれらの性質を持つ時、正しく型付けされた項は行き詰まり状態になりえない。

進行定理の証明の為に Bool 型と Nat 型の標準形(それらの型を持つ正しく型付けされた値)を示す。

\begin{lemma}
    標準形

    \begin{enumerate}
        \item $ v $ が $Bool$ 型の値ならば $v$ は $true$ または $false$ である。
        \item $v$ が $Nat$ 型の値ならば、$0$ もしくは $Nat$ に対して $succ$ を適用した値である。
    \end{enumerate}
\end{lemma}

標準形の証明に関しては値における構造的帰納法を用いる。
この言語における値とは $ true $ と $false $ と $ 0$ と $ succ \; nv$ のいずれかの形をしている。
Bool型に関して注目した時、 $ true $ と $ false $ は定義によって正しい。
$ 0 $ と $ succ \; nv $ に関しては逆転補題より Nat 型を持つため、Bool型を持つ値は $ true $ と $ false $ のどちらかとなる。
Nat についても同様である。

\begin{theorem}
進行

$ t$ が正しく型付けされたと仮定すると、$ t$ は値であるか、またはある $t'$ が存在して$ t \rightarrow t' $ となる。
\end{theorem}

証明は $ t : T $ の導出に関する帰納法による。
T-TRUE 、 T-FALSE 、 T-ZERO の場合は$t$が値であることより成立する。

T-IF の場合、帰納法の仮定により $ t1 $ は値であるか、$t_1'$ が存在して $ t_1 \rightarrow t_1'$ を満たす。
$ t_1 $ が値ならば、標準形補題により $ true $ か $ false $ であり、その場合は E-IFTRUE か E-IFFALSE が適用可能である。
一方 $ t_1 \rightarrow t_1' $ ならば E-IF が適用できる。

T-SUCC の場合も帰納法の仮定により $ t1 $ は値であるか、$t_1'$ が存在して $ t_1 \rightarrow t_1'$ を満たす。
$ t_1 $ が値ならば標準形補題により数値でなければならず、その場合 $ t $ も数値であるため成り立つ。
一方 $ t_1 \rightarrow t_1' $ ならば E-SUCC が適用できる。

T-SUCC の場合も同様で、 $ t_1 $ が値ならば標準形補題により数値でなければならず、その場合 E-PREDZERO か E-PREDSUCC が使える。
$ t_1 \rightarrow t_1' $ ならば E-PRED が適用できる。

T-ISZERO の場合も値ならば標準形補題により $ t_1 $ は数値であり、どちらの場合でも E-ISZEROZERO と E-ISZEROSUCC が適用できる。
$ t_1 \rightarrow t_1' $ ならば E-ISZERO が適用できる。

\begin{theorem}
保存

$ t : T $ かつ $ t \rightarrow t' $ ならば $ t' : T $ となる。
\end{theorem}

保存定理も $ t : T $ の導出に関する帰納法によって導ける。
帰納法の各ステップにおいて全ての部分導出に関して所望の性質が成り立つと仮定し、導出の最後の規則についての場合分けで証明を行なう。

導入の最後の規則がT-TRUE の場合、その規則の形から $ t $ は定数 $ true $ でなければならず、 $ T $ は $ Bool$ となる。
そして $ t $ は値であるためにどのような $ t' $ も存在せず、定理の要求は満たされる。
T-FALSE と T-ZERO の場合も同様である。

導入の最後の規則 T-IF の場合は、$ t $ はある $ t_1, \; t_2 \; t_3 $ に対して $ if \; t_1 then t_2 else t_3 $ という形となる。
さらに $ t_1 : Bool $ と $ t_2 : T $ と $ t_3 : T $ となる部分導出がある。
ここで if を持つ評価規則において  $ t \rightarrow t'$ を導入できる規則は E-IFTRUE と E-IFFALSE と E-IF のみである。
それぞれの場合について別々に場合分けをして考える。

\begin{itemize}
    \item E-IFTRUE の場合(E-IFFALSE も同様)

        $ t \rightarrow t' $ が E-IFTRUE を使った導出ならば、 $ t_1$ は $ true $ であり、結果の項 $ t' $ は $ t_2 $ となる。
        このことより $ t_2 : T $ であることが分かるため、条件を満たす。

    \item E-IF の場合

        場合分け T-IF の仮定より $ t_1 : Bool $が結論となる、部分導出が得られる。
        帰納法の仮定を部分導出に適用して $ t_1' : Bool $ とし、 $ t_2 : T $ と  $ t_3 : T $ を合わせると規則 T-IF が適用できる。
        T-IF を適用すると  $ if \; t_1' \; then \; t_2 \; else \; t_3$となり、$ t' : T $ が成り立つ。
\end{itemize}

T-SUCC が導入の最後であれば、 $ t \rightarrow t'$ を導くためには E-SUCC のみであり、この形から $ t_1 \rightarrow t_1'$が分かる。
$ t_1 : Nat $ であることも分かるため、帰納法の仮定より $ t_1' : Nat $ が得られる。
この時 T-SUCC が適用できるため $ succ \; t_1 : Nat$となって $ t' : T $ が成り立つ。
T-PRED も同様である。

% }}}

% {{{ 型なしラムダ計算
\section{型なしラムダ計算}
計算とは何か、エラーとは何か、を算術式を定義することによって示してきた。
また、型を導入することにより行き詰まり状態を回避することも示した。
ここで、プログラミング言語における計算を形式的に定義していく。
プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61
この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算であった。
ラムダ計算は Alonzo Church が発明した形式的体系の一つである。 % TODO: ref
ラムダ計算では全ての計算が関数定義と関数適用の基本的な演算に帰着される。
ラムダ計算はプログラミング言語の機能の仕様記述や、言語設計と実装、型システムの研究に多く使われている。
この計算体系の重要な点は、ラムダ計算内部で計算が記述できるプログラミング言語であると同時に、それ自身について厳格な証明が可能な数学的対象としてみなせる点にある。

ラムダ計算はいろいろな方法で拡張できる。
数や組やレコードなどはラムダ計算そのもので模倣することができるが、記述が冗長になってしまう。
それらの機能のための具体的な特殊構文を加えることは言語の利用者の視点で便利である。
他にも書き換え可能な参照セルや非局所的な例外といった複雑な機能を表現することもできるが、膨大な変換を用いなければモデル化できない。
それらを言語として備えた拡張に ML や Haskell といったものがある。 % TODO: ref

ラムダ計算(または $ \lambda $ 計算) とは、関数定義と関数適用を純粋な形で表現する。
ラムダ計算においてはすべてが関数である。
関数によって受け付ける引数も関数であり、関数が返す結果もまた関数である。

ラムダ計算の項は変数と抽象と適用の3種類の項からなり、以下の文法に要約される。
変数 $ x $ は項であり、項 $ t_1 $ から変数 $ x $ を抽象化した $ \lambda x . t_1 $ も項であり、項 $ t_1 $ を他の項 $ t_2 $ に適用した $ t_1 t_2 $ も項である。

\begin{multline*}
    t ::= \\
        x \\
        \lambda x . t \\
        t \, t  \\
\end{multline*}

ラムダ計算において関数適用は左結合とする。
つまり、 $ s \, t \, u $ は $ (s \, t) \, u $ となる。

また、抽象の本体はできる限り右側へと拡大する。
例えば $ \lambda x . \;  \lambda y . \; x \, y \, x $ は $ \lambda x . (\lambda . y ((x \, y) \, x)) $ となる。

ラムダ計算には変数のスコープが存在する。
抽象 $ \lambda x . t $ の本体 $ t $ の中に変数 $ x $ がある時、 $ x $ の出現は束縛されていると言う。
同様に、 $ \lambda x $ は $ t $ をスコープとする束縛子であると言う。
なお、 $ x $ を囲む抽象によって束縛されていない場所の $ x $ の出現は自由であると言う。
例えば $ x \; y $ や $ \lambda y . \; x \; y $  における $ x $ の出現は自由だが、 $ \lambda x . x $ や $ \lambda z . \lambda x . \lambda y . x (y \; z) $ における $ x $ の出現は束縛されている。
$ (\lambda x . x) \;x $ においては、最初の $ x $ の出現は束縛されているが、2つ目の出現は自由である。

ラムダ計算において、計算とは引数に対する関数の適用である。
抽象に対して項を適用した場合、抽象の本体に存在する束縛変数に適用する項を代入したもので書き換える。
図式的には

\begin{equation*}
    (\lambda x . t_{12}) t_2 \rightarrow [ x \mapsto t_2] t_{12}
\end{equation*}

と記述する。
ここで $ [ x \mapsto t_2] t_{12} $ とは、$ t_12 $ 中の自由な $ x $ を全て $ t_2 $ で置換した項を意味する。
例えば、 $ (\lambda x . x) \; y $ は $ y $ となり、項 $ (\lambda x . x (\lambda x . x)) (y \; z) $ は $ y \; z \; (\lambda x . x) $ となる。

なお、 $ (\lambda x . t_{12}) t_2 $ という形の項を簡約基(redex, reducible expression) と呼び、上記の規則で簡約基を置換する操作をベータ簡約と呼ぶ。
ラムダ計算のための評価戦略には数種類の戦略がある。

\begin{itemize}
    \item 完全ベータ簡約

        任意の簡約基がいつでも簡約されうる。
        つまり項の中からどの順番で簡約しても良い。

    \item 正規順序簡約

        最も左で最も外側の簡約基が最初に簡約される。

    \item 名前呼び

        正規順序の中でも抽象の内部での簡約を許さない。
        名前呼びの変種は Algol-60 や Haskell で利用されている。
        なお、Haskell においては必要呼びという最適化された変種を利用している。

    \item 値呼び

        ほとんどの言語はこの戦略を用いている。
        基本的には最も左の簡約基をを簡約するが、右側が既に値(計算が終了してもう簡約できない閉じた項)になっている簡約基のみを簡約する。
\end{itemize}

値呼び戦略は関数の引数が本体で使われるかに関わらず評価され、これは正格と呼ばれる。
名前呼びなどの非正格な戦略は引数が使われる時のみ評価され、これは遅延評価とも呼ばれる。

ラムダ計算において、複数の引数は、関数を返り値として返す高階関数として定義できる。
項 $ s $ が二つの自由変数 $ x $ と $ y $ を含むとすれば、 $ \lambda x . \lambda y . s $ と書くことで二つの引数を持つ関数を表現できる。
これは $ x $ に $ v $ が与えられた時、$ y $ を受けとり、 $ s $ の抽象内の自由な $ x $ を $ v $ に置き換えた部分を置換する関数、を返す。
例えば $ (\lambda x . \lambda y . s) \; v \; w $ は $ (\lambda y . [x \mapsto v] s) w $ に簡約され、 $ [y \mapsto w][x \mapsto v]s $ に簡約される。
なお、複数の引数を取る関数を高階関数に変換することはカリー化と呼ばれる。

% TODO: ラムダの再帰とかペアとかの解説

ラムダ計算の帰納的な項は以下のように定義される。

\begin{definition}
    $ V $ を変数名の加算集合とする。項の集合は以下を満たす最小の集合 $ T $ である。

    \begin{eqnarray*}
        任意の x \in V について x \in T \\
        t_1 \in T かつ x in V ならば \lambda x . t \in T \\
        t_1 \in T かつ t_2 \in T ならば t_1 \; t_2 \in T
    \end{eqnarray*}
\end{definition}

また、形式的な自由変数の定義を与える。

\begin{definition}
    項 $ t $ の自由変数の集合は $ FV(t)$と書き、以下のように定義される。

    \begin{eqnarray*}
        FV(x) = \{ x \} \\
        FV(\lambda  . t_1 x) = FV(t_1) \setminus \{ x \} \\
        FV(t_1 \; t_2) = FV(t_1) \cup FV(t_2)
    \end{eqnarray*}
\end{definition}

記号 $ \setminus $ は集合に対する二項演算子であり、$ S \setminus T := {x \in S : x \notin T}$ である。
つまり、$ t_1 $の内部の自由変数の集合から $ x $ を抜いた集合である。

最後に代入について定義する。
代入の操作は直感的には置換であるが、変数の束縛に注意しなくてはならない。
例えば抽象への代入を以下のように定義する。

\begin{equation*}
    [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1
\end{equation*}

この場合、束縛変数の名前によっては定義が破綻してしまう。例えば以下のようになる。

\begin{equation*}
    [x \mapsto y](\lambda x . x) = \lambda x . y
\end{equation*}

$ \lambda $ よって束縛されているはずの $ x $ が書き変わっている。
これはスコープとして振る舞っていないので誤っている。
この問題は項 $ t $ 内の変数 $ x $ の自由な出現と束縛された出現を区別しなかったために出現した誤りである。

そこで、$ x $ を束縛する項に対しては置換行なわないように定義を変える。

\begin{itemize}
    \item $ y = x $ の場合
        \begin{equation*}
            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . t_1
        \end{equation*}

    \item $ y \neq x $ の場合
        \begin{equation*}
            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1
        \end{equation*}
\end{itemize}

この場合は束縛された変数を上書きしないが、逆に自由変数を束縛するケースが発生する。
具体的には以下である。

\begin{equation*}
    [ x \mapsto z] (\lambda z . x) = \lambda z . z
\end{equation*}

項 $ s $ 中の自由変数が項 $ t $ に代入されて束縛される現象は変数捕獲と呼ばれる。
これを避けるためには $ t $ の束縛変数の名前が $ s $ の自由変数の名前と異なることを保証する必要がある。
変数捕獲を回避した代入操作は捕獲回避代入と呼ばれる。
代入における名前の衝突を回避するために項の束縛変数の名前を一貫して変更することで変数捕獲を回避する方法も存在する。
束縛変数の名前を一貫して変更することをアルファ変換と呼ばれる。
これは関数抽象に対する束縛変数は問わないという直感からくるもので、 $ \lambda x . x $ も $ \lambda y . y $ も振舞いとしては同じ関数であるとみなすものである。
捕獲回避の条件を追加した代入の定義は以下のような定義となる。

\begin{itemize}
    \item 変数への代入

        \begin{equation*}
            [ x \mapsto s ] x = s
        \end{equation*}

    \item 存在しない変数への代入($ y \neq x $ の時)

        \begin{equation*}
            [ x \mapsto s ] y = y
        \end{equation*}

    \item 抽象内の項への代入($ y \neq x $ かつ $ y $ が $ s $ の自由変数でない)

        \begin{equation*}
            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1
        \end{equation*}

    \item 適用への代入

        \begin{equation*}
            [x \mapsto s] (t_1 \; t_2) = (t_1[x\mapsto s])([x \mapsto s] t_2)
        \end{equation*}

\end{itemize}

この定義は少なくとも代入が行なわれる際には正しく代入が行なえる。
さらに、抽象が束縛している変数を名前では無く数字として扱う名無し表現も存在する。
これは De Brujin 表現と呼ばれ、コンパイラ内部などでの項表現として用いられる。 % TODO: ref and spell check

最終的な型無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。

\begin{definition}
    $ \rightarrow $ (型無し)

    項
    \begin{align*}
        t ::=         && \text{項} \\
        \lambda x . t && \text{ラムダ抽象} \\
        t \; t        && \text{関数適用}
    \end{align*}

    値
    \begin{align*}
        v ::=         && \text{値} \\
        \lambda x . t && \text{ラムダ抽象値}
    \end{align*}

    評価( $ t \rightarrow t' $)

    \begin{align*}
        \AxiomC{$ t_1 \rightarrow t_1'$}
        \UnaryInfC{$t_1 \; t_2 \rightarrow t_1' t_2$}
        \DisplayProof && \text{E-APP1} \\
        \AxiomC{$ t_2 \rightarrow t_2'$}
        \UnaryInfC{$v_1 \; t_2 \rightarrow v_1 t_2'$}
        \DisplayProof && \text{E-APP2} \\
        (\lambda x . t_{12}) \; v_2 \rightarrow [ x \mapsto v_2] t_{12}
        && \text{E-APPABS}
    \end{align*}
\end{definition}

項は変数かラムダ抽象か関数適用の3つにより構成される。
また、ラムダ抽象値は全て値である。
加えて評価は関数適用を行なう E-APPABS 計算規則と、適用の項を書き換える E-APP1 と E-APP2 合同規則により定義される。

この定義からも評価戦略と評価順序が分かる。
関数を適用する E-APPABS は左側が抽象であり、右側が値である $v_2$ の時にしか適用されない。
逆に、規則 E-APP1 の$t_1$は任意の項にマッチするため関数部分が値でない関数適用に用いる。
一方、E-APP2 は左辺が値であるようになるまで評価されない。
よって、関数適用 $ t_1 \; t_2 $ の評価順は、まずE-APP1を用いて$t_1$が値となった後にE-APP2を用いて$t_2$を値とし、最後にE-APPABSで関数を適用を行なう。


% }}}

\section{単純型付きラムダ計算}
\section{部分型付け}
\section{部分型と Continuation based C}