Mercurial > hg > Papers > 2015 > atton-thesis

changeset 83:5f7fd7632608

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix slides
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 19 Feb 2015 07:39:04 +0900
parents bde5e3c7de99
children 751e83a23d82
files presentation/slide.md
diffstat 1 files changed, 6 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.md	Wed Feb 18 19:31:05 2015 +0900
+++ b/presentation/slide.md	Thu Feb 19 07:39:04 2015 +0900
@@ -12,7 +12,7 @@
 
 # 研究目標
 * Monad を用いてプログラムの変更を形式化する
-* プログラムにおける Monad とはメタ計算を表現するための手法である
+* プログラムにおける Monad はメタ計算を表現するために用いる
 * メタ計算とは計算を実現するための計算である
 * プログラムの変更を表すメタ計算を Delta Monad として提案する
 * Delta Monad が Monad 則を満たすか Agda により証明する
@@ -20,8 +20,8 @@
 
 # プログラムの変更の形式化
 * 形式手法とはソフトウェアの検証に数学や論理学を用いる手法
-* Monad は圏によって形式化されている
-* プログラムにおいてはメタ計算の形式化に用いられる
+* 論理と対応する lambda 計算を用いたプログラムの解析などがある
+* Moggi らによれば圏論のMonad は関数とメタ計算を含む関数との対応
 * メタ計算として変更を定義することで形式的な定義を与える
 * 「過去の変更を全て保存する」メタ計算 Delta Monad を提案する
 
@@ -59,8 +59,8 @@
 # Haskell におけるメタ計算の定義
 * Haskell においてメタ計算を定義する
 * Delta Monad により表現されるプログラムでは
-    * 値 : 値のバージョン毎の集合
-    * 関数 : 値からバージョン毎の値の集合へのマッピング
+    * 値       : 値のバージョン毎の集合
+    * 関数     : 値からバージョン毎の値の集合へのマッピング
     * 関数適用 : バージョンごとに関数適用する
 
 # Haskell における Monad の instance 定義
@@ -123,6 +123,7 @@
 * ログを取る Writer Monad と組み合せた numberCount の実行結果
 
 ```
+*Main> numberCountM 1000
 DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
                            "[2,3,5,7]",
                            "4"]))