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