Mercurial > hg > Papers > 2020 > soto-midterm
view tex/agda.tex @ 6:4bf00f7ba825
add description of agda
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Mon, 14 Sep 2020 02:58:14 +0900 |
parents | 35f0e5f12fe6 |
children | acad18934981 |
line wrap: on
line source
\section{Agda} Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で は記述したプログラムを証明することができる。 \subsection{プログラムの読み方} 以下は Agda プログラムの一例となる。 本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、 後述する Agda コードの理解を容易にすることを目的としている。 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda} \begin{itemize} \item 基本事項 \begin{itemize} \item ℕ というのは自然数 (Natulal Number) のことである。 また、- (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、 ここでは関数を実行した際の例を記述している。 したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。 \end{itemize} \item 定義部分 \begin{itemize} \item コードの1行目に : (セミコロン)がある。 この : の前が関数名になり、その後ろがその関数の定義となる。\\ : の後ろの (x y : ℕ ) は関数は x, y の自然数2つを受けとる。 という意味になる。 → の後ろは関数が返す型を記述している。 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、 自然数を返すという定義になる。 \end{itemize} \item 実装部分 \begin{itemize} \item 関数の定義をしたコードの直下で実装を行うのが常である。 関数名を記述した後に引数を記述して受け取り、= (イコール) の後ろで 引数に対応し実装を作を記述していく。 今回の場合では、 plus x zero であれば +0 である為、そのまま x を返す。 2行目の方では受け取った y の値を減らし、x の値を増やして再び plus の関数に 遷移している。 受け取った y は+1されていたことにすることでyの値を減らしている。 実装部分もまとめると、x と y の値を足す為に、y から x に数値を1つずつ渡す。 y が 0 になった際に計算が終了となっている。 指折りでの足し算を実装していると捉えても良い \end{itemize} \end{itemize} \subsection{Data 型} Deta 型とは分岐のことである。 そのため、それぞれの動作について実装する必要がある。 例として既出で Data 型である ℕ の実装を見てみる。 \lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda} 実装から、ℕ という型は zero と suc の2つのコンストラクタを持っていることが分かる。 それぞれの仕様を見てみると、zeroは ℕ のみであるが、suc は (n : ℕ) → ℕ である。 つまり、suc 自体の型は ℕ であるが、そこから ℕ に遷移するということである。 そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。 したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。 Data型にはそれぞれの動作について実装する必要があると述べたが、 言い換えればパターンマッチをする必要があると言える。 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。 \subsection{Record 型} Record 型とはオブジェクトあるいは構造体ののようなものである。 以下の関数は AND となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 \lstinputlisting[label=And, caption=And] {src/agda/And.agda} また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。 これを使用して三段論法を定義することができる。 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。 コードを以下に示す。 \lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda} コードの解説をすると、引数として x と a が関数に与えられている。 引数 x の中身は((A → B) ∧ (B → C))、引数 a の中身は A である。 したがって、(\_∧\_.p1 x a) で (A → B) に A を与えて B を取得し、 \_∧\_.p2 x で (B → C) であるため、これに B を与えると C が取得できる。 よって A を与えて C を取得することができたため、三段論法を定義できた。 %\subsection{Agdaの基本操作} %\subsection{定理証明支援器としての Agda} %\subsectoin{}