Papers/2018/nozomi-master: paper/agda.tex comparison

comparison paper/agda.tex @ 55:70bea06ebdf3

Add reasoning

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Tue, 31 Jan 2017 17:30:07 +0900
parents	9902994fbd1a
children	10a550bf7e4a

comparison

equal deleted inserted replaced

-:ef9730f3db8d
+:70bea06ebdf3
 部分型を用いて具体的なCbCの型システムを定義する前に、型システムの一方のメリットである証明について触れる。
 依存型という型を持つ証明支援系言語 Agda を用いて証明が行なえることを示す。
 % {{{ Natural Deduction
 \section{Natural Deduction}
+\label{section:natural_deduction}
 まず始めに証明を行なうためにNatural Deduction(自然演繹)を示す。
 証明には natural deduction(自然演繹)を用いる。
 natural deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。
 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。
 \label{tbl:curry_howard_isomorphism}
 \end{table}
 \end{center}
 % }}}
+% {{{ 依存型を持つ証明支援系言語 Agda
 \section{依存型を持つ証明支援系言語 Agda}
 型システムを用いて証明を行なうことができる言語に Agda が存在する。% ref Agda のref
 Agda は依存型という強力な型システムを持っている。
 依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
 この節では Agda の文法的な紹介を行なう~\cite{agda-documentation}。 % ref pdf のアレ
 具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。
 \lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda}
 ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
-型Nat が Eq の上位型であることを記述するとリスト~\ref{src-agda-instance}のようになる。
+型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。
 \lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}
 これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。
 例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。
 そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。
 \verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。
 \lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda}
+% }}}
+% {{{ Reasoning
 \section{Reasoning}
+次に Agda における証明を記述していく。
+例題として、自然数の加法の可換法則を示す。
+証明を行なうためにまずは自然数を定義する。
+今回用いる自然数の定義は以下のようなものである。
+\begin{itemize}
+\item 0 は自然数である
+\item 任意の自然数には後続数が存在する
+\item 0 はいかなる自然数の後続数でもない
+\item 異なる自然数どうしの後続数は異なる ($ n \neq m \rightarrow S n \neq S m $)
+\item 0がある性質を満たし、aがある性質を満たせばその後続数 S(n) も自然数である
+\end{itemize}
+この定義は peano arithmetic における自然数の定義である。
+Agda で自然数型 Nat を定義するとリスト \ref{src:agda-nat-2} のようになる。
+\lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda}
+自然数型 Nat は2つのコンストラクタを持つ。
+\begin{itemize}
+\item O
+引数を持たないコンストラクタ。これが0に相当する。
+\item S
+Nat を引数に取るコンストラクタ。これが後続数に相当する。
+\end{itemize}
+よって、数値の 3 は \verb/S (S (S O))/ のように表現される。
+Sの個数が数値に対応する。
+次に加算を定義する(リスト\ref{src:agda-nat-add})。
+\lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda}
+加算は中置関数 \verb/_+_/ として定義する。
+2つの Nat を取り、Natを返す。
+関数 \verb/_+_/ はパターンマッチにより処理を変える。
+0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。
+S を左の数から右の数へ1つずつ再帰的に移していくような加算である。
+例えば 3 + 1 といった計算は (S (S (S O))) + (S O) のように記述される。
+ここで 3 + 1 が 4と等しいことの証明を行なう。
+等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。
+\lstinputlisting[label=src:agda-equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/Equiv.agda.replaced}
+Agda において等式は、等式を示すデータ型 $ \equiv $ により定義される。
+$ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。
+実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:agda-three-plus-one})。
+\lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda}
+3+1 という関数を定義し、その型として証明すべき式を記述し、証明を関数の定義として定義する。
+証明する式は \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ である。
+今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
+$ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。
+\begin{itemize}
+\item sym  : $ x \equiv y \rightarrow y \equiv x $
+等式が証明できればその等式の左辺と右辺を反転しても等しい。
+\item cong : $ f \rightarrow x \equiv y \rightarrow f x \equiv f y $
+証明した等式に同じ関数を与えても等式は保たれる。
+\item trans : $ x \equiv y \rightarrow y \equiv z \rightarrow x \equiv z $
+2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。
+\end{itemize}
+ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:agda-nat-add-sym})。
+\lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda}
+証明する式は $ n + m \equiv m + n $ である。
+n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。
+そのためにパターンは4通りある。
+\begin{itemize}
+\item n = O, m = O
++ の定義により、 O に簡約されるため refl で証明できる。
+\item n = O, m = S m
+$ O + (S m) \equiv (S m) + O $  を証明することになる。
+この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
+$ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。
+この2つの証明はこのような意味を持つ。
+n が 0 であるとき、 m も 0 なら簡約により等式が成立する。
+n が 0 であり、 m が 0 でないとき、 m は後続数である。
+よって m が (S x) と書かれる時、 x は m の前の値である。
+前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。
+ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。
+\item n = S n, m = O
+$ (S n) + O \equiv O + (S n) $ を証明する。
+この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。
+さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。
+よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。
+ここで、 $ O + n  \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
++ の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。
+\item n = S n, m = S m
+3つのパターンは証明したが、このパターンは少々長くなるため別に解説することとする。
+\end{itemize}
+3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。
+しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。
+長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。
+$ \equiv $-Reasoning では等式の左辺を begin の後に記述し、等式の変形を $ \equiv \langle expression \rangle $ に記述することで変形していく。
+最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。
+自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:agda-reasoning}である。
+特に n と m が1以上である時の証明に注目する。
+\lstinputlisting[label=src:agda-reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/Reasoning.agda.replaced}
+まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。
+よって refl で導かれる。
+なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。
+次に \verb/S (n + (S m)) / に対して addSym を用いて交換し、 cong によって S を追加することで \verb/ S ((S m) + n) / を得る。
+これは、前3パターンにおいて + の右辺の項が 1以上であっても上手く交換法則が定義できたことを利用して項を変形している。
+このように同じ法則の中でも、違うパターンで証明できた部分を用いて別パターンの証明を行なうこともある。
+最後に \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得なくてはならない。
+しかし、 + の定義には右辺に対して S を移動する演算が含まれていない。
+よってこのままでは証明することができない。
+そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。
+addToRight の証明の解説は省略する。
+addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。
+これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $  の証明が完了した。
+自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。
+このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。
+% }}}

Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/agda.tex @ 55:70bea06ebdf3