Mercurial > hg > Papers > 2015 > atton-osc
changeset 11:9876354c1c19
Update to OSC
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 May 2014 21:08:41 +0900 |
| parents | b32e19ea592b |
| children | dfa919e8fb20 |
| files | slide.html slide.md |
| diffstat | 2 files changed, 246 insertions(+), 86 deletions(-) [+] |
line wrap: on
line diff
--- a/slide.html Fri May 23 20:05:05 2014 +0900 +++ b/slide.html Fri May 23 21:08:41 2014 +0900 @@ -43,7 +43,7 @@ <!-- === begin markdown block === generated by markdown 1.1.1 on Ruby 2.1.2 (2014-05-08) [x86_64-darwin13.0] - on 2014-05-23 17:56:31 +0900 with Markdown engine kramdown (1.3.3) + on 2014-05-23 21:08:27 +0900 with Markdown engine kramdown (1.3.3) using options {} --> @@ -79,10 +79,10 @@ </ul> </li> <li>Haskell で実装されています</li> - <li>dependent type の言語 です + <li>型が非常に強力で表現力が高いです <ul> - <li>型を第一級オブジェクトとして扱える</li> - <li>X -> X, f x, a == b のような型を扱うことができます</li> + <li>命題や仕様を表す論理式を型として定義することができます</li> + <li>例えば 1 + 1 = 2 とか</li> </ul> </li> </ul> @@ -118,6 +118,31 @@ <div class="slide" id="5"><div> <section> <header> + <h1 id="section-1">命題と定義, 仕様と実装</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>どうしてプログラムで証明できるかというと</li> + <li>(命題 と 定義) は (仕様 と 実装) のように対応します + <ul> + <li>int chars_to_int(char * chars)</li> + <li>つまり char * から int は作れる、という命題に対応している</li> + <li>実装は { itoa(chars) }</li> + </ul> + </li> + <li>char * から int は作れる、という仕様(型, 命題)は</li> + <li>atoi という実装(定義)により証明された</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="6"><div> + <section> + <header> <h1 id="agda--1">Agda をはじめよう</h1> </header> <!-- _S9SLIDE_ --> @@ -135,7 +160,7 @@ </section> </div></div> -<div class="slide" id="6"><div> +<div class="slide" id="7"><div> <section> <header> <h1 id="peano-arithmetic">自然数の定義 : Peano Arithmetic</h1> @@ -144,11 +169,11 @@ <ul> <li>自然数 0 が存在する</li> - <li>任意の自然数 a にはその後続数 suc(a) が存在する</li> + <li>任意の自然数 x にはその後続数 S (x) が存在する</li> <li>0 より前の自然数は存在しない</li> <li>異なる自然数は異なる後続数を持つ <ul> - <li>a != b のとき suc(a) != suc(b) となる</li> + <li>x != y のとき S(x) != S(y) となる</li> </ul> </li> <li>0 が性質を満たし、a も性質を満たせばその後続数も性質を満たすとき、すべての自然数はその性質を満たす</li> @@ -159,7 +184,7 @@ </section> </div></div> -<div class="slide" id="7"><div> +<div class="slide" id="8"><div> <section> <header> <h1 id="agda--2">Agda における自然数の定義</h1> @@ -175,8 +200,8 @@ S : Int -> Int </code></pre> <ul> - <li>Int は O か、 Int に S がかかったもののみ</li> - <li>Set は組込みで存在する型です。「成り立つ」と考えてもらえれば良いです。</li> + <li>Int は O か、 Int に S がかかったもののみで構成される</li> + <li>Set は組込みで存在する型で、”成り立つ”と考えてもらうと良いです。</li> </ul> @@ -184,10 +209,10 @@ </section> </div></div> -<div class="slide" id="8"><div> +<div class="slide" id="9"><div> <section> <header> - <h1 id="section-1">自然数の例</h1> + <h1 id="section-2">自然数の例</h1> </header> <!-- _S9SLIDE_ --> @@ -203,15 +228,15 @@ </section> </div></div> -<div class="slide" id="9"><div> +<div class="slide" id="10"><div> <section> <header> - <h1 id="section-2">自然数に対する演算の定義</h1> + <h1 id="section-3">自然数に対する演算の定義</h1> </header> <!-- _S9SLIDE_ --> <ul> - <li>x と y の加算 : x にかかっている S の分だけ S を b に適用する</li> + <li>x と y の加算 : x にかかっている S の分だけ S を y に適用する</li> <li> <p>x と y の乗算 : x にかかっている S の分だけ y を 0 に加算する</p> </li> @@ -224,7 +249,7 @@ </section> </div></div> -<div class="slide" id="10"><div> +<div class="slide" id="11"><div> <section> <header> <h1 id="agda--3">Agda における自然数に対する演算の定義</h1> @@ -247,7 +272,7 @@ </section> </div></div> -<div class="slide" id="11"><div> +<div class="slide" id="12"><div> <section> <header> <h1 id="agda-syntax">Agda における関数定義のSyntax</h1> @@ -257,12 +282,13 @@ <ul> <li>Agda において、関数は <ul> + <li>_ + _ : Int -> Int -> Int</li> <li>関数名 : 型</li> <li>関数名 引数はスペース区切り = 関数の定義や値</li> </ul> </li> <li>のように定義します</li> - <li>中置関数は _ で挟みます</li> + <li>中置関数は、引数があるべきところに _ を書くことでできます</li> </ul> @@ -270,7 +296,7 @@ </section> </div></div> -<div class="slide" id="12"><div> +<div class="slide" id="13"><div> <section> <header> <h1 id="agda--4">Agda で複数の引数がある関数の型</h1> @@ -278,6 +304,7 @@ <!-- _S9SLIDE_ --> <ul> + <li>_ + _ : Int -> Int -> Int</li> <li> <p>func : A -> (A -> B) -> B</p> </li> @@ -295,10 +322,10 @@ </section> </div></div> -<div class="slide" id="13"><div> +<div class="slide" id="14"><div> <section> <header> - <h1 id="section-3">パターンマッチ</h1> + <h1 id="section-4">パターンマッチ</h1> </header> <!-- _S9SLIDE_ --> @@ -307,9 +334,8 @@ <li>ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます</li> <li>Int は O か Int に S が付いたもの、でした <ul> - <li>double : Int -> Int</li> - <li>double O = O</li> - <li>double (S x) = S (S (double x))</li> + <li>x + O = x</li> + <li>x + (S y) = S (x + y)</li> </ul> </li> <li>関数名 (引数のパターン) = 定義</li> @@ -320,10 +346,10 @@ </section> </div></div> -<div class="slide" id="14"><div> +<div class="slide" id="15"><div> <section> <header> - <h1 id="section-4">もういちど : 自然数に対する演算の定義</h1> + <h1 id="section-5">もういちど : 自然数に対する演算の定義</h1> </header> <!-- _S9SLIDE_ --> @@ -342,10 +368,10 @@ </section> </div></div> -<div class="slide" id="15"><div> +<div class="slide" id="16"><div> <section> <header> - <h1 id="section-5">これから証明していきたいこと</h1> + <h1 id="section-6">これから証明していきたいこと</h1> </header> <!-- _S9SLIDE_ --> @@ -355,31 +381,7 @@ <p>加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン</p> </li> <li>乗法の交換法則 : (x * y) = (y * x)</li> -</ul> - - - - </section> -</div></div> - -<div class="slide" id="16"><div> - <section> - <header> - <h1 id="section-6">‘等しい’ ということ</h1> - </header> - <!-- _S9SLIDE_ --> - -<ul> - <li>‘等しい’という型 _ ≡ _ を定義する - <ul> - <li>refl : x ≡ x</li> - <li>sym : x ≡ y -> y ≡ x</li> - <li>cong : (f : A -> B) -> x ≡ y -> f x ≡ f y</li> - <li>trans : x ≡ y -> y ≡ z -> y ≡ z</li> - </ul> - </li> - <li>defined : Relation.Binary.PropositionalEquality in Standard Library</li> - <li>Agda tips : 記号は \ の後に文字列を入れると出てきます。 ‘≡’ は “\ ==”</li> + <li>乗法の結合法則 : (x * y) * z = x * (y * z)</li> </ul> @@ -390,7 +392,54 @@ <div class="slide" id="17"><div> <section> <header> - <h1 id="section-7">‘同じもの’とは</h1> + <h1 id="section-7">‘等しい’ ということ</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>‘等しい’という型 _ ≡ _ を data で定義します。</li> +</ul> + +<pre><code> data _≡_ {A : Set} : A -> A -> Set where + refl : {x : A} -> x == x +</code></pre> + +<ul> + <li>defined : Relation.Binary.PropositionalEquality in Standard Library</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="18"><div> + <section> + <header> + <h1 id="section-8">等しさを保ったままできること</h1> + </header> + <!-- _S9SLIDE_ --> + +<p>等しさを保ったまま変換する関数を作ると良い</p> + +<ul> + <li>sym refl = refl</li> + <li>cong : {A B : Set} {x y : A} -> (f : A -> B) -> x ≡ y -> f x ≡ f y</li> + <li> + <p>trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z</p> + </li> + <li>Agda tips : 記号は \ の後に文字列を入れると出てきます。 ‘≡’ は “\ ==”</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="19"><div> + <section> + <header> + <h1 id="section-9">‘同じもの’とは</h1> </header> <!-- _S9SLIDE_ --> @@ -403,7 +452,7 @@ </li> <li>関数なら normal form が同じなら同じ <ul> - <li>lambda-term : (A : Set) -> ((x : A) -> x) ≡ ((y : A) -> y)</li> + <li>lambda-term : (A : Set) -> (\ (x : A) -> x) ≡ (\ (y : A) -> y)</li> <li>lambda-term A = refl</li> </ul> </li> @@ -415,10 +464,29 @@ </section> </div></div> -<div class="slide" id="18"><div> +<div class="slide" id="20"><div> <section> <header> - <h1 id="section-8">交換法則を型として定義する</h1> + <h1 id="section-10">単純な証明 : 1 + 1 = 2</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>型として (S O) + (S O) ≡ (S (S O)) を定義</li> + <li>証明を書く</li> + <li>‘同じもの’ の refl でおしまい</li> + <li>自明に同じものになるのなら refl で証明ができます</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="21"><div> + <section> + <header> + <h1 id="section-11">交換法則を型として定義する</h1> </header> <!-- _S9SLIDE_ --> @@ -436,10 +504,10 @@ </section> </div></div> -<div class="slide" id="19"><div> +<div class="slide" id="22"><div> <section> <header> - <h1 id="section-9">交換法則を証明していく</h1> + <h1 id="section-12">交換法則を証明していく</h1> </header> <!-- _S9SLIDE_ --> @@ -455,7 +523,50 @@ </section> </div></div> -<div class="slide" id="20"><div> +<div class="slide" id="23"><div> + <section> + <header> + <h1 id="o-o-">O, O の場合</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>sum-sym O O = refl</li> + <li>両方ともO の時、証明したい命題は O + O ≡ O + O</li> + <li>_ + _ の定義の x + O = x より</li> + <li>O ≡ O を構成したい</li> + <li>refl によって構成する</li> + <li>refl O と考えてもらえると良い</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="24"><div> + <section> + <header> + <h1 id="o--s-">片方が O, 片方に S が付いている場合</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>sum-sym O (S y) = cong S (sum-sym O y)</li> + <li>式的には O + (S y) ≡ (S y) + O</li> + <li>_ + _ の定義 x + (S y) = S (x + y) より</li> + <li>O + (S y) ≡ S (O + y)</li> + <li>O と y を交換して O + (S y) ≡ S (y + O)</li> + <li>つまり y と O を交換して S をかけると良い</li> + <li>交換して S をかける -> cong S (sum-sym O y)</li> +</ul> + + + + </section> +</div></div> + +<div class="slide" id="25"><div> <section> <header> <h1 id="trans-">trans による等式変形</h1> @@ -467,10 +578,10 @@ <li> <p>等しさを保ったまま式を変形していくことが必要になります</p> </li> - <li>sum-sym (S x) (S y) = trans (a ≡ b) (b ≡ c) + <li>sum-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c) <ul> <li>trans (refl) ?</li> - <li>trans (trans refl (cong S (left-add-one x y)) ?</li> + <li>trans (trans refl (cong S (sum-sym (S x) y)) ?</li> </ul> </li> </ul> @@ -480,7 +591,7 @@ </section> </div></div> -<div class="slide" id="21"><div> +<div class="slide" id="26"><div> <section> <header> <h1 id="reasoning-">≡-reasoning による等式変形</h1> @@ -489,7 +600,8 @@ <ul> <li>trans が何段もネストしていくと分かりづらい</li> - <li>≡-reasoning という等式変形の拡張構文が Standard Library にあります</li> + <li>≡-reasoning という等式変形の構文が Standard Library にあります</li> + <li>Agda では見掛け上構文のような関数をAgdaでは定義できます</li> </ul> <pre><code> begin @@ -504,7 +616,7 @@ </section> </div></div> -<div class="slide" id="22"><div> +<div class="slide" id="27"><div> <section> <header> <h1 id="reasoning--1">≡-reasoning による最初の定義</h1> @@ -524,15 +636,19 @@ </section> </div></div> -<div class="slide" id="23"><div> +<div class="slide" id="28"><div> <section> <header> - <h1 id="section-10">交換法則の証明 : + の定義による変形</h1> + <h1 id="section-13">交換法則の証明 : + の定義による変形</h1> </header> <!-- _S9SLIDE_ --> <ul> - <li>上から + の定義により変形</li> + <li> + <ul> + <li>の定義である x + (S y) = S (x + y) により変形</li> + </ul> + </li> </ul> <pre><code> sum-sym (S x) (S y) = begin @@ -549,7 +665,7 @@ </section> </div></div> -<div class="slide" id="24"><div> +<div class="slide" id="29"><div> <section> <header> <h1 id="cong--sum-sym-">cong と sum-sym を使って交換</h1> @@ -571,7 +687,7 @@ </section> </div></div> -<div class="slide" id="25"><div> +<div class="slide" id="30"><div> <section> <header> <h1 id="s">加法の時に左側からSを移動させられない</h1> @@ -586,7 +702,7 @@ </ul> </li> <li>left-operand にかかっている S を移動させる方法が無い</li> - <li>たしかに + <li>たしかに ? のについて <ul> <li>S (y + S x) ≡ S y + S x</li> </ul> @@ -599,7 +715,7 @@ </section> </div></div> -<div class="slide" id="26"><div> +<div class="slide" id="31"><div> <section> <header> <h1 id="left-operand-s">left-operand からSを操作する証明を定義</h1> @@ -624,7 +740,7 @@ </section> </div></div> -<div class="slide" id="27"><div> +<div class="slide" id="32"><div> <section> <header> <h1 id="left-operand-s-1">left-operand からSを移動させる</h1> @@ -647,7 +763,7 @@ </section> </div></div> -<div class="slide" id="28"><div> +<div class="slide" id="33"><div> <section> <header> <h1 id="x--y--y--x">加法の交換法則 : (x + y) = (y + x)</h1> @@ -670,7 +786,7 @@ </section> </div></div> -<div class="slide" id="29"><div> +<div class="slide" id="34"><div> <section> <header> <h1 id="x--y--z--x--y--z">加法の結合法則 : (x + y) + z = x + (y + z)</h1> @@ -694,7 +810,7 @@ </section> </div></div> -<div class="slide" id="30"><div> +<div class="slide" id="35"><div> <section> <header> <h1 id="agda--5">Agda による証明方法のまとめ</h1> @@ -717,10 +833,10 @@ </section> </div></div> -<div class="slide" id="31"><div> +<div class="slide" id="36"><div> <section> <header> - <h1 id="section-11">乗法の定義</h1> + <h1 id="section-14">乗法の定義</h1> </header> <!-- _S9SLIDE_ --> @@ -740,7 +856,7 @@ </section> </div></div> -<div class="slide" id="32"><div> +<div class="slide" id="37"><div> <section> <header> <h1 id="x--y--y--x-1">乗法の交換法則 : (x * y) = (y * x)</h1> @@ -762,7 +878,7 @@ </section> </div></div> -<div class="slide" id="33"><div> +<div class="slide" id="38"><div> <section> <header> <h1 id="agda">Agdaにおいて何ができるのか</h1> @@ -788,6 +904,31 @@ </li> </ul> + + + </section> +</div></div> + +<div class="slide" id="39"><div> + <section> + <header> + <h1 id="section-15">良くあるエラー</h1> + </header> + <!-- _S9SLIDE_ --> + +<ul> + <li>parse error + <ul> + <li>スペースある無しで意味が変わります</li> + <li>A: Set <- NG</li> + <li>A : Set <- OK</li> + <li>A: という term がありえるから</li> + </ul> + </li> + <li>型が合わない -> 赤で警告されます</li> + <li>情報が足りない -> 黄色で警告されます</li> +</ul> + <!-- vim: set filetype=markdown.slide: --> <!-- === end markdown block === -->
--- a/slide.md Fri May 23 20:05:05 2014 +0900 +++ b/slide.md Fri May 23 21:08:41 2014 +0900 @@ -142,12 +142,23 @@ # '等しい' ということ -* '等しい'という型 _ ≡ _ を data で定義します。コンストラクタは以下。 - * refl : x ≡ x - * sym : x ≡ y -> y ≡ x - * cong : (f : A -> B) -> x ≡ y -> f x ≡ f y - * trans : x ≡ y -> y ≡ z -> x ≡ z +* '等しい'という型 _ ≡ _ を data で定義します。 + +``` + data _≡_ {A : Set} : A -> A -> Set where + refl : {x : A} -> x == x +``` + * defined : Relation.Binary.PropositionalEquality in Standard Library + + +# 等しさを保ったままできること +等しさを保ったまま変換する関数を作ると良い + +* sym refl = refl +* cong : {A B : Set} {x y : A} -> (f : A -> B) -> x ≡ y -> f x ≡ f y +* trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z + * Agda tips : 記号は \ の後に文字列を入れると出てきます。 '≡' は "\ ==" @@ -161,6 +172,14 @@ * 関数による式変形は等しいものとして扱います +# 単純な証明 : 1 + 1 = 2 +* 型として (S O) + (S O) ≡ (S (S O)) を定義 +* 証明を書く +* '同じもの' の refl でおしまい +* 自明に同じものになるのなら refl で証明ができます + + + # 交換法則を型として定義する * ≡を用いて * (x : Int) -> (y : Int) -> x + y ≡ y + x @@ -191,7 +210,7 @@ * 式的には O + (S y) ≡ (S y) + O * _ + _ の定義 x + (S y) = S (x + y) より * O + (S y) ≡ S (O + y) -* 交換して O + (S y) ≡ S (y + O) +* O と y を交換して O + (S y) ≡ S (y + O) * つまり y と O を交換して S をかけると良い * 交換して S をかける -> cong S (sum-sym O y)