# HG changeset patch # User Yasutaka Higa # Date 1400846921 -32400 # Node ID 9876354c1c1958cb0ff8f6f1aea5837cf22986ac # Parent b32e19ea592b09adb1bd220d47c5938ebb19297c Update to OSC diff -r b32e19ea592b -r 9876354c1c19 slide.html --- 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 @@ @@ -79,10 +79,10 @@
  • Haskell で実装されています
    • -
  • dependent type の言語 です +
  • 型が非常に強力で表現力が高いです
    • @@ -118,6 +118,31 @@
    +

    命題と定義, 仕様と実装

    +
    + + +
      +
    • どうしてプログラムで証明できるかというと
      • +
    • (命題 と 定義) は (仕様 と 実装) のように対応します +
        +
      • int chars_to_int(char * chars)
        • +
      • つまり char * から int は作れる、という命題に対応している
        • +
      • 実装は { itoa(chars) }
        • +
      +
      • +
    • char * から int は作れる、という仕様(型, 命題)は
      • +
    • atoi という実装(定義)により証明された
      • +
    + + + +
    +
    + +
    +
    +

    Agda をはじめよう

    @@ -135,7 +160,7 @@
    -
    +

    自然数の定義 : Peano Arithmetic

    @@ -144,11 +169,11 @@
    • 自然数 0 が存在する
      • -
    • 任意の自然数 a にはその後続数 suc(a) が存在する
      • +
    • 任意の自然数 x にはその後続数 S (x) が存在する
    • 0 より前の自然数は存在しない
    • 異なる自然数は異なる後続数を持つ
        -
      • a != b のとき suc(a) != suc(b) となる
        • +
      • x != y のとき S(x) != S(y) となる
    • 0 が性質を満たし、a も性質を満たせばその後続数も性質を満たすとき、すべての自然数はその性質を満たす
      • @@ -159,7 +184,7 @@
    -
    +

    Agda における自然数の定義

    @@ -175,8 +200,8 @@ S : Int -> Int
      -
    • Int は O か、 Int に S がかかったもののみ
      • -
    • Set は組込みで存在する型です。「成り立つ」と考えてもらえれば良いです。
      • +
    • Int は O か、 Int に S がかかったもののみで構成される
      • +
    • Set は組込みで存在する型で、”成り立つ”と考えてもらうと良いです。
    @@ -184,10 +209,10 @@
    -
    +
    -

    自然数の例

    +

    自然数の例

    @@ -203,15 +228,15 @@
    -
    +
    -

    自然数に対する演算の定義

    +

    自然数に対する演算の定義

      -
    • x と y の加算 : x にかかっている S の分だけ S を b に適用する
      • +
    • x と y の加算 : x にかかっている S の分だけ S を y に適用する

    • x と y の乗算 : x にかかっている S の分だけ y を 0 に加算する

      • @@ -224,7 +249,7 @@
    -
    +

    Agda における自然数に対する演算の定義

    @@ -247,7 +272,7 @@
    -
    +

    Agda における関数定義のSyntax

    @@ -257,12 +282,13 @@
    • Agda において、関数は
        +
      • _ + _ : Int -> Int -> Int
      • 関数名 : 型
      • 関数名 引数はスペース区切り = 関数の定義や値
    • のように定義します
      • -
    • 中置関数は _ で挟みます
      • +
    • 中置関数は、引数があるべきところに _ を書くことでできます
    @@ -270,7 +296,7 @@
    -
    +

    Agda で複数の引数がある関数の型

    @@ -278,6 +304,7 @@
      +
    • _ + _ : Int -> Int -> Int

    • func : A -> (A -> B) -> B

      • @@ -295,10 +322,10 @@
    -
    +
    -

    パターンマッチ

    +

    パターンマッチ

    @@ -307,9 +334,8 @@
  • ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
  • Int は O か Int に S が付いたもの、でした
      -
    • double : Int -> Int
      • -
    • double O = O
      • -
    • double (S x) = S (S (double x))
      • +
    • x + O = x
      • +
    • x + (S y) = S (x + y)
  • 関数名 (引数のパターン) = 定義
    • @@ -320,10 +346,10 @@
    -
    +
    -

    もういちど : 自然数に対する演算の定義

    +

    もういちど : 自然数に対する演算の定義

    @@ -342,10 +368,10 @@
    -
    +
    -

    これから証明していきたいこと

    +

    これから証明していきたいこと

    @@ -355,31 +381,7 @@

    加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン

  • 乗法の交換法則 : (x * y) = (y * x)
    • - - - - -
    -
    - -
    -
    -
    -

    ‘等しい’ ということ

    -
    - - -
      -
    • ‘等しい’という型 _ ≡ _ を定義する -
        -
      • refl : x ≡ x
        • -
      • sym : x ≡ y -> y ≡ x
        • -
      • cong : (f : A -> B) -> x ≡ y -> f x ≡ f y
        • -
      • trans : x ≡ y -> y ≡ z -> y ≡ z
        • -
      -
      • -
    • defined : Relation.Binary.PropositionalEquality in Standard Library
      • -
    • Agda tips : 記号は \ の後に文字列を入れると出てきます。 ‘≡’ は “\ ==”
      • +
    • 乗法の結合法則 : (x * y) * z = x * (y * z)
    @@ -390,7 +392,54 @@
    -

    ‘同じもの’とは

    +

    ‘等しい’ ということ

    +
    + + +
      +
    • ‘等しい’という型 _ ≡ _ を 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 : 記号は \ の後に文字列を入れると出てきます。 ‘≡’ は “\ ==”
      • +
    + + + +
    +
    + +
    +
    +
    +

    ‘同じもの’とは

    @@ -403,7 +452,7 @@
  • 関数なら normal form が同じなら同じ
      -
    • lambda-term : (A : Set) -> ((x : A) -> x) ≡ ((y : A) -> y)
      • +
    • lambda-term : (A : Set) -> (\ (x : A) -> x) ≡ (\ (y : A) -> y)
    • lambda-term A = refl
    • @@ -415,10 +464,29 @@
    -
    +
    -

    交換法則を型として定義する

    +

    単純な証明 : 1 + 1 = 2

    +
    + + +
      +
    • 型として (S O) + (S O) ≡ (S (S O)) を定義
      • +
    • 証明を書く
      • +
    • ‘同じもの’ の refl でおしまい
      • +
    • 自明に同じものになるのなら refl で証明ができます
      • +
    + + + +
    +
    + +
    +
    +
    +

    交換法則を型として定義する

    @@ -436,10 +504,10 @@
    -
    +
    -

    交換法則を証明していく

    +

    交換法則を証明していく

    @@ -455,7 +523,50 @@
    -
    +
    +
    +
    +

    O, O の場合

    +
    + + +
      +
    • sum-sym O O = refl
      • +
    • 両方ともO の時、証明したい命題は O + O ≡ O + O
      • +
    • _ + _ の定義の x + O = x より
      • +
    • O ≡ O を構成したい
      • +
    • refl によって構成する
      • +
    • refl O と考えてもらえると良い
      • +
    + + + +
    +
    + +
    +
    +
    +

    片方が O, 片方に S が付いている場合

    +
    + + +
      +
    • sum-sym O (S y) = cong S (sum-sym O y)
      • +
    • 式的には O + (S y) ≡ (S y) + O
      • +
    • _ + _ の定義 x + (S y) = S (x + y) より
      • +
    • O + (S y) ≡ S (O + y)
      • +
    • O と y を交換して O + (S y) ≡ S (y + O)
      • +
    • つまり y と O を交換して S をかけると良い
      • +
    • 交換して S をかける -> cong S (sum-sym O y)
      • +
    + + + +
    +
    + +

    trans による等式変形

    @@ -467,10 +578,10 @@

  • 等しさを保ったまま式を変形していくことが必要になります

    • -
  • sum-sym (S x) (S y) = trans (a ≡ b) (b ≡ c) +
  • sum-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c)
    • trans (refl) ?
      • -
    • trans (trans refl (cong S (left-add-one x y)) ?
      • +
    • trans (trans refl (cong S (sum-sym (S x) y)) ?
    • @@ -480,7 +591,7 @@
    -
    +

    ≡-reasoning による等式変形

    @@ -489,7 +600,8 @@
    • trans が何段もネストしていくと分かりづらい
      • -
    • ≡-reasoning という等式変形の拡張構文が Standard Library にあります
      • +
    • ≡-reasoning という等式変形の構文が Standard Library にあります
      • +
    • Agda では見掛け上構文のような関数をAgdaでは定義できます
      begin
@@ -504,7 +616,7 @@
    -
    +

    ≡-reasoning による最初の定義

    @@ -524,15 +636,19 @@
    -
    +
    -

    交換法則の証明 : + の定義による変形

    +

    交換法則の証明 : + の定義による変形

      -
    • 上から + の定義により変形
      • +
    • +
        +
      • の定義である x + (S y) = S (x + y) により変形
        • +
      + 
      sum-sym (S x) (S y) = begin
@@ -549,7 +665,7 @@
    -
    +

    cong と sum-sym を使って交換

    @@ -571,7 +687,7 @@
    -
    +

    加法の時に左側からSを移動させられない

    @@ -586,7 +702,7 @@
  • left-operand にかかっている S を移動させる方法が無い
    • -
  • たしかに +
  • たしかに ? のについて
    • S (y + S x) ≡ S y + S x
    @@ -599,7 +715,7 @@
    • -
    +

    left-operand からSを操作する証明を定義

    @@ -624,7 +740,7 @@
    -
    +

    left-operand からSを移動させる

    @@ -647,7 +763,7 @@
    -
    +

    加法の交換法則 : (x + y) = (y + x)

    @@ -670,7 +786,7 @@
    -
    +

    加法の結合法則 : (x + y) + z = x + (y + z)

    @@ -694,7 +810,7 @@
    -
    +

    Agda による証明方法のまとめ

    @@ -717,10 +833,10 @@
    -
    +
    -

    乗法の定義

    +

    乗法の定義

    @@ -740,7 +856,7 @@
    -
    +

    乗法の交換法則 : (x * y) = (y * x)

    @@ -762,7 +878,7 @@
    -
    +

    Agdaにおいて何ができるのか

    @@ -788,6 +904,31 @@ + + +
    +
    + +
    +
    +
    +

    良くあるエラー

    +
    + + +
      +
    • parse error +
        +
      • スペースある無しで意味が変わります
        • +
      • A: Set <- NG
        • +
      • A : Set <- OK
        • +
      • A: という term がありえるから
        • +
      +
      • +
    • 型が合わない -> 赤で警告されます
      • +
    • 情報が足りない -> 黄色で警告されます
      • +
    + diff -r b32e19ea592b -r 9876354c1c19 slide.md --- 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)