# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400833535 -32400
# Node ID f65aa05c8c52b23501ad46a7d11d7c4e05e06dc8
# Parent  b82e226f56ffc5857636cb107c4099ca089aef48
mini fixes

diff -r b82e226f56ff -r f65aa05c8c52 slide.md
--- a/slide.md	Fri May 23 16:42:38 2014 +0900
+++ b/slide.md	Fri May 23 17:25:35 2014 +0900
@@ -31,7 +31,7 @@
 
 # Agda をはじめよう
 * emacs に agda-mode があります
-* module < filename > where
+* module filename where
 * を先頭に書く必要があります
 * 証明を定義していく
 * C-c C-l で型チェック(証明チェック)ができます
@@ -50,12 +50,12 @@
 * data 型を使います
 
 ```
-    data Int : Set where
-      O : Int
-      S : Int -> Int
+  data Int : Set where
+    O : Int
+    S : Int -> Int
 ```
-* O は Int, S は Int を受けとって Int を返す、と読めます
-* Set は組込みで存在する型です。「成り立つ」といった感じです。
+* Int は O か、 Int に S がかかったもののみ
+* Set は組込みで存在する型です。「成り立つ」と考えてもらえれば良いです。
 
 
 # 自然数の例
@@ -75,10 +75,10 @@
 
 # Agda における自然数に対する演算の定義
 ```
-    infixl 30 _+_
-    _+_ : Int -> Int -> Int
-    x + O     = x
-    x + (S y) = S (x + y)
+  infixl 30 _+_
+  _+_ : Int -> Int -> Int
+  x + O     = x
+  x + (S y) = S (x + y)
 ```
 
 * Agda tips : C-c C-n すると式を評価することができます
@@ -87,13 +87,13 @@
 
 # Agda における関数定義のSyntax
 * Agda において、関数は
-  * 関数名                        : 型
-  * 関数名 <スペース区切りで引数> = 関数の定義や値
+  * 関数名                      : 型
+  * 関数名 引数はスペース区切り = 関数の定義や値
 * のように定義します
 * 中置関数は _ で挟みます
 
 
-# Agda における引数を持つ関数の型の表記法
+# Agda で複数の引数がある関数の型
 * func : A -> (A -> B) -> B
 
 * 引数の型 -> 返り値の型
@@ -105,6 +105,7 @@
 # パターンマッチ
 * Agda においてはデータ型は引数で分解することができます
 * ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
+* Int は O か Int に S が付いたもの、でした
   * double : Int -> Int
   * double O     = O
   * double (S x) = S (S (double x))
@@ -113,10 +114,10 @@
 
 # もういちど : 自然数に対する演算の定義
 ```
-    infixl 30 _+_
-    _+_ : Int -> Int -> Int
-    x + O     = x
-    x + (S y) = S (x + y)
+  infixl 30 _+_
+  _+_ : Int -> Int -> Int
+  x + O     = x
+  x + (S y) = S (x + y)
 ```
 * 中置、関数、パターンマッチが使われています
 * infixl は左結合を意味します。数値は結合強度です
@@ -145,7 +146,7 @@
 * 関数なら normal form が同じなら同じ
   * lambda-term : (A : Set)  -> (\(x : A) -> x) ≡ (\(y : A) -> y)
   * lambda-term A = refl
-* 関数による変形は形が違う等しいものとして扱います
+* 関数による式変形は等しいものとして扱います
 
 
 # 交換法則を型として定義する
@@ -156,11 +157,11 @@
 
 # 交換法則を証明していく
 ```
-sum-sym : (x y : Int)  -> x + y ≡ y + x
-sum-sym    O     O  = refl
-sum-sym    O  (S y) = cong S (sum-sym O y)
-sum-sym (S x)    O  = cong S (sum-sym x O)
-sum-sym (S x) (S y) = ?
+  sum-sym : (x y : Int)  -> x + y ≡ y + x
+  sum-sym    O     O  = refl
+  sum-sym    O  (S y) = cong S (sum-sym O y)
+  sum-sym (S x)    O  = cong S (sum-sym x O)
+  sum-sym (S x) (S y) = ?
 ```
 
 # trans による等式変形
@@ -177,22 +178,22 @@
 * ≡-reasoning という等式変形の拡張構文が Standard Library にあります
 
 ```
-   begin
-     変換前の式
-       ≡⟨ 変換する関数 ⟩
-     変換後の式
-   ∎
+  begin
+    変換前の式
+      ≡⟨ 変換する関数 ⟩
+    変換後の式
+  ∎
 ```
 
 
 # ≡-reasoning による最初の定義
 
 ```
-sum-sym (S x) (S y) = begin
-    (S x) + (S y)
-  ≡⟨ ? ⟩
-    (S y) + (S x)
-  ∎
+  sum-sym (S x) (S y) = begin
+      (S x) + (S y)
+    ≡⟨ ? ⟩
+      (S y) + (S x)
+    ∎
 ```
 
 
@@ -200,13 +201,13 @@
 * 上から + の定義により変形
 
 ```
-sum-sym (S x) (S y) = begin
-    (S x) + (S y)
-  ≡⟨ refl ⟩
-    S (S x + y)
-  ≡⟨ ? ⟩
-    (S y) + (S x)
-  ∎
+  sum-sym (S x) (S y) = begin
+      (S x) + (S y)
+    ≡⟨ refl ⟩
+      S (S x + y)
+    ≡⟨ ? ⟩
+      (S y) + (S x)
+    ∎
 ```
 
 
@@ -221,11 +222,12 @@
 ```
 
 
-# 交換法則の証明 : 加法の時に左側からSを移動させることができない
+# 加法の時に左側からSを移動させられない
 
 * 加法の定義は
   * x + (S y) = S (x + y)
-* left-operand から S を取る方法が無い
+* left-operand にかかっている S を移動させる方法が無い
+* たしかに
   * S (y + S x) ≡ S y + S x
 * にあてはまるものを入れてくれ、と出てきている
 
@@ -242,7 +244,7 @@
 
 
 # left-operand からSを移動させる
-* left-increment は (S x) + y ≡ S (x + y) なので逆にしないと使えない
+* left-increment は (S x) + y ≡ S (x + y) なので逆にして使う
 
 ```
     ...
@@ -255,15 +257,15 @@
 
 # 加法の交換法則 : (x + y) = (y + x)
 ```
-sum-sym (S x) (S y) = begin
-    (S x) + (S y)
-  ≡⟨ refl ⟩
-    S ((S x) + y)
-  ≡⟨ cong S (sum-sym (S x) y) ⟩
-    S (y + (S x))
-  ≡⟨ (sym (left-increment y (S x))) ⟩
-    (S y) + (S x)
-  ∎
+  sum-sym (S x) (S y) = begin
+      (S x) + (S y)
+    ≡⟨ refl ⟩
+      S ((S x) + y)
+    ≡⟨ cong S (sum-sym (S x) y) ⟩
+      S (y + (S x))
+    ≡⟨ (sym (left-increment y (S x))) ⟩
+      (S y) + (S x)
+    ∎
 ```
 
 
@@ -273,6 +275,7 @@
   * ≡ で証明したい式を定義
   * 定義に証明を書く
   * 必要ならば等式を変形していく
+* ちなみに x + y + z は infixl なので ((x + y) + z) となります
 
 
 # Agda による証明方法のまとめ
@@ -285,28 +288,38 @@
 
 # 乗法の定義
 ```
-infixl 40 _*_
-_*_ : Int -> Int -> Int
-n *    O  = O
-n * (S O) = n
-n * (S m) = n + (n * m)
+  infixl 40 _*_
+  _*_ : Int -> Int -> Int
+  n *    O  = O
+  n * (S O) = n
+  n * (S m) = n + (n * m)
 ```
 
-* _+_ よりも結合強度を上げる必要がある
+* _+_ よりも結合強度を上げるといわゆる自然数の演算
 
 
-# 乗法の交換法則 : (a * b) = (b * a)
+# 乗法の交換法則 : (x * y) = (y * x)
 ```
-mult-sym : (n m : Int) -> n * m ≡ m * n
+  mult-sym : (x y : Int) -> x * y ≡ y * x
 ```
 
 途中で
 
 ```
-(n m : Int) -> (S n) * m ≡ m + (n * m)
+  (x y : Int) -> (S x) * y ≡ y + (x * y)
 ```
 
-が必要になる
+が必要になることが分かる
+
+
+# Agdaにおいて何ができるのか
+* 証明の正しさを対話的に教えてくれる
+  * それに必要な証明が結果的に分かることもある
+* 今回は Int に対する演算だった
+  * lambda-term に落とせれば Agda で証明していける
+* 他にも命題論理の証明などがある
+* プログラミング言語そのものに対するアプローチ
+  * lambda-term の等価性によってリファクタリングなど
 
 
 <!-- vim: set filetype=markdown.slide: -->