Mercurial > hg > Papers > 2015 > atton-thesis
diff 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 |
line wrap: on
line diff
--- a/agda.tex Fri Feb 13 18:10:07 2015 +0900 +++ b/agda.tex Sun Feb 15 10:33:47 2015 +0900 @@ -1,13 +1,14 @@ \chapter{証明支援系言語 Agda による証明手法} \label{chapter:agda} -第\ref{chapter:category}章においては functor, natural transformation, monad の定義と functional programming における対応について述べた。 +第\ref{chapter:category}章では functor, natural transformation, monad の定義を行ない、第\ref{chapter:functional_programming}章では functional programming における対応を述べた。 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。 -functional programming において、あるデータ型やそれに対応する計算が Functor 則を満たすことを保証することは言語の実装に依存していい。 -例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックに留まっている。 -そのため、型チェックは通るが Functor 則を満たさない functor が定義可能となってしまう。 +functional programming において、あるデータ型と対応する計算が Functor 則を満たすかの保証は言語の実装に依存している。 +例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックを行なう。 +そのため、型チェックは通るが Functor 則を満たさない functor が定義できてしまう。 +よって Haskell において Delta Monad を定義しただけでは証明が存在しない。 +そこで証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明する。 -そこで、証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明することとする。 -そのためにまずは Agda における証明手法について述べる。 +第\ref{chapter:agda}章は Agda における証明手法について述べる。 % {{{ Natural Deduction