Mercurial > hg > Papers > 2015 > atton-thesis
comparison agda.tex @ 45:12c5e455fe55
Writing description proofs of monad-laws for delta
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 15 Feb 2015 10:33:47 +0900 |
| parents | 4f1107f1f6aa |
| children | bf136bd59e7a |
comparison
equal
deleted
inserted
replaced
| 44:4f1107f1f6aa | 45:12c5e455fe55 |
|---|---|
| 1 \chapter{証明支援系言語 Agda による証明手法} | 1 \chapter{証明支援系言語 Agda による証明手法} |
| 2 \label{chapter:agda} | 2 \label{chapter:agda} |
| 3 第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。 | 3 第\ref{chapter:category}章では functor, natural transformation, monad の定義を行ない、第\ref{chapter:functional_programming}章では functional programming における対応を述べた。 |
| 4 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。 | 4 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。 |
| 5 functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。 | 5 functional programming において、あるデータ型と対応する計算が Functor 則を満たすかの保証は言語の実装に依存している。 |
| 6 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。 | 6 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックを行なう。 |
| 7 そのため、型チェックは通るが Functor 則を満たさない functor が定義可能となってしまう。 | 7 そのため、型チェックは通るが Functor 則を満たさない functor が定義できてしまう。 |
| 8 | 8 よって Haskell において Delta Monad を定義しただけでは証明が存在しない。 |
| 9 そこで、証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明することとする。 | 9 そこで証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明する。 |
| 10 そのためにまずは Agda における証明手法について述べる。 | 10 |
| 11 第\ref{chapter:agda}章は Agda における証明手法について述べる。 | |
| 11 | 12 |
| 12 % {{{ Natural Deduction | 13 % {{{ Natural Deduction |
| 13 | 14 |
| 14 \section{Natural Deduction} | 15 \section{Natural Deduction} |
| 15 \label{section:natural_deduction} | 16 \label{section:natural_deduction} |