-title: 証明と関数型言語、Agda

問題は、メールでSubjectを (a01 の 問題2.5ならば)
    Subject: Report on Automaton Lecture 2.5 
として、問題毎に提出すること。

kono@ie.u-ryukyu.ac.jp まで送ること。
番号のついてない問題はオプションです。

学籍番号をメールの中に記述すること。
問題番号は正確に記述すること。
出席しない場合でも、問題解答を送れば出席扱いとします。

提出期限は ura.ie.classes.automaton で知らせます。


--証明と関数型言語の関係

証明とは、論理式それを結ぶ推論からなる数学的な構造である。また、関数型言語は集合である型とそれを結ぶ関数からなる数学的構造である。

型つきλ計算と論理が対応するように、データ構造と論理演算子(∧とか∨)を対応させることにより

論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。


--あらすじ

1) 論理式を変数とそれを結ぶ演算子(connectives)で定義する
    これは構文定義、あるいは、論理式の作り方に相当する

2) 演算子を導入する推論と、除去する推論を定義する。
　　これには証明図を使う

3) 推論に対応する関数を表す項を考える
   項は関数型言語の要素になる

　　項の導入 ...  データ構造のconstructor
　　項の除去 ...  データ構造のaccesor

    導入は関数の出力の型に現れる
    除去は関数の入力の型に現れる

これを演算子の数の分だけ繰り返す。

次に等式論理を学ぶ。

4) x = x の導入と除去

5) 項が等しいとはとういうことかを学ぶ　　
    正規形

    正規形を得ることが関数型言語の計算(項の操作)

以上のことを Agda (Haskell に似た構文を持つ証明支援系)で記述する。

--証明の基本

A は論理式を表す変数。あるいは型Aという集合。論理式は変数と論理演算子で表される木構造。変数や演算子は構文要素。

     A → B

これは「AならばB」というのに対応する。関数の視点からは、Aという型からBという型への関数。
AとBは型を表す論理式。

      A
  -----------
      B

Aを仮定して、Bが証明されたことを表す図。証明図。

--関数適用による証明

導入                          除去

       A                   
       :
       B                    A       A → B
   -------------         ------------------
      A → B                     B

対応する項。項とは、関数型プログラムを構成する構文要素。木構造で表される。


    λ x → y

x は変数、y は項。y は複雑な項(関数のbody)でも良い。これは構文定義でもある。変数 x と項yから 
λ x → y という項を作れる。 x は構文的にスコープを持っている。つまり、関数の引数と同じ扱いとする。

項には型が対応する。これは、再帰的に定義される

    x : A

は、x という項が型Aを持つと言うのを表している。

x : A かつ y : B の時に、

    λ x → y : A → B

と定義する。



---Agdaの構文

<a href="agda-install.html"> Agda のinstallの方法 </a>
<br>

型と値

名前の作り方

indent

implicit variable

infix operator and operator order

<a href="agda.html"> agda の細かい構文の話 </a> 


---問題2.1 Agdaによる関数と証明


以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。

<a href="agda/lambda.agda"> lambda </a> <!---  Exercise 2.1 --->


--record または ∧

導入                          除去

     A    B                 A ∧ B           A ∧ B 
   -------------         ----------- π1   ---------- π2
      A ∧ B                   A               B

除去は複数あるので名前を区別する必要がある。つまり、それぞれに項を用意する必要がある。

A ∧ B は新しく導入した型である。
型Aと型Bから作るデータ構造であり、オブジェクトあるいは構造体だと思って良い。
π1 π2 は構造体から  field を抜き出す accesor によって実装できる。



record によって  

   record _∧_ A B : Set
     field
         π1 : A
         π2 : B

_∧_　は中置演算子を表す。

     _∧_ A B

は

     A ∧  B

とかける。(Haskell では (∧) を使う)

は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。

   record { π1 = x ; π2 = y }    


---例題

     A → B  ∧  B → C  →  A → C 

まず、正しくかっこを付ける。

     (( A → B ) ∧  ( B → C )) → ( A → C  )

線を上に引く。

              :
  -------------------------------------------------
     (( A → B ) ∧  ( B → C )) → ( A → C  )

: はこれから埋めていく部分。まず適用するのは→のintro duction である。 ( A → B ) ∧  ( B → C )を仮定で使えるようになる。 

             :
           A → C  
  -------------------------------------------------
     (( A → B ) ∧  ( B → C )) → ( A → C  )

さらに→introを使う。Aを仮定で使えるようになる。

             :
             C
  -------------------------------------------------
           A → C  
  -------------------------------------------------
     (( A → B ) ∧  ( B → C )) → ( A → C  )

仮定でCを生成できるのは  B → C しかない。

         B       B → C
      ---------------------
             C

これは→elim である。 B → C は仮定( A → B ) ∧  ( B → C )の左側が使える

      ( A → B ) ∧  ( B → C )
      ---------------------   π2
            B → C

B の方もがんばると、最終的に

      [ ( A → B ) ∧  ( B → C )]*1
  --------------------------------- π1
      [A]*2    A → B                      [ ( A → B ) ∧  ( B → C ) ]*1
     ---------------- →elim              -------------------------------   π2
             B                                 B → C
          ----------------------------------------------- →elim
                      C
  ------------------------------------------------- →intro 2
                     A → C
  ------------------------------------------------- →intro 1
     (( A → B ) ∧  ( B → C )) → ( A → C  )

となる。

Agda では、

    lemma : (( A → B ) ∧  ( B → C )) → ( A → C  )
    lemma = ?

とすると、A B C が未定義だと言われる。

    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
    lemma = ?

引数が一つあるので、それに名前を付ける。

    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
    lemma f∧g = ?

いや引数は二つだった。

    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
    lemma f∧g a = ?

f∧g は直積なので、

    π1 f∧g :  A → B
    π2 f∧g :  B → C

なことを考えると、

    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
    lemma f∧g a = π2 f∧g ?

ここで、π2 f∧g ? は (π2 f∧g) ? であることを思い出そう。最終的に、

    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
    lemma f∧g a = π2 f∧g (π1 f∧g) a

(ここで、(π2 f∧g (π1 f∧g)) a と書かなくても良いのは何故か?)

前の証明図と、Agdaで証明とどこがどう対応しているのかを考えてみよう。

---問題2.2 Agdaによる関数と証明


以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。

最低限5題をまとめてレポートで提出せよ

<a href="agda/practice-logic.agda"> practice-logic</a> <!---  Exercise 2.2 --->



--data または 排他的論理和(Sum)

ここで扱っている論理(直観主義論理)では∧に対称的な形で∨を定義することはしない。導入は対称的になるが除去はおかしくなってしまう。
そこで次のように定義することになっている。

除去                           導入
               A      B
               :      :
      A ∨ B    C      C            A               B
   ------------------------  ----------- p1   ---------- p2
           C                     A ∨ B           A ∨ B 


    data _∨_ (A B : Set) : Set where
      p1 : A → A ∨ B
      p2 : B → A ∨ B

dataはCで言えばcase文とunion に相当する。Scala のCase Classもこれである。Cと違いunionにはどの型が入っているかを区別するtagが付いている。

p1 と p2 は A ∨ B を構成する constructor (推論ではintroduction)であり、case 文が eliminator に相当する。

Haskellと同様にp1/p2はパターンマッチで場合分けする。

    ex3 : {A B : Set} → ( A ∨ A ) → A 
    ex3 = ?

場合分けには、? の部分にcursolを合わせて C-C C-C すると場合分けを生成してくれる。

    ex3 : {A B : Set} → ( A ∨ A ) → A 
    ex3 (p1 x) = ?
    ex3 (p2 x) = ?


---問題2.3 Agdaのdata


<a href="agda/data1.agda"> data </a> <!---  Exercise 2.3 --->

--有限な集合と Nat 

data は有限な要素を持つ集合を構成できる。

    data Three : Set where
      t1 : Three
      t2 : Three
      t3 : Three

    open Three

    data 3Ring : (dom cod : Three) → Set where
       r1 : 3Ring t1 t2
       r2 : 3Ring t2 t3
       r3 : 3Ring t3 t1

これは、三つのVertexとEdgeを持つグラフをdataで表してみたものである。

任意の個数を表すためには自然数(Natural Number)を作る必要がある。ペアノの公理が有名だが、dataを使って以下のように構成する。

    data Nat : Set where
      zero : Nat
      suc  : Nat →  Nat

    add : ( a b : Nat ) → Nat
    add zero x = x
    add (suc x) y = suc ( add x y )

    mul : ( a b : Nat ) → Nat
    mul zero x = ?
    mul (suc x) y = ?

--問題2.4 Nat 

? を埋めて掛け算を完成させよう。

<a href="agda/practice-nat.agda"> data </a> <!---  Exercise 2.4 --->

--Equality

自然数を導入したので方程式を記述したい。そのためには等式を導入する必要がある。導入は

   ---------------
      x == x

だが、ここには隠れた仮定がある。x は何かの集合の要素なはず。

     { x : A }
   ---------------
      x == x

さらに左辺と右辺は等しいが、

     add zero zero == zero

では左辺と右辺は項として同じではない。計算して同じということにして欲しい。つまり、

　　Agdaの項には計算していくと決まった形に落ちる

という性質があって欲しい。この計算はλ項に対して定義する必要がある。この計算をreduction(縮約)、
決まった形をnormal form(正規形)と言う。

<a href="reduction.html">Reduction</a>

Agda での定義は以下のようになる。

    data _==_ {A : Set } : A → A → Set where
       refl :  {x : A} → x == x

refl は reflection (反映) の略である。refl は 等式のconstructorになる。

Elmination は変数の置き換えになる。

      x == y    f x y
   ------------------------
          f x x

x == y は入力の型であり、refl とうパターンでしか受けられない。この時に、x と y が等しい必要がある。

しかし、x と y は項なので変数を含むことがある。Agda に等しいことを確信させる必要がある。
この問題はパターンマッチの時にもすででていた。これは項(正規化された)を再帰的に比較していく
手順が必要になる。これは単一化(Unification)と呼ばれる。

<a href="unification.html">Unification</a>

    ex1 : {A : Set} {x : A } → x == x
    ex1  = ?

    ex2 : {A : Set} {x y : A } → x == y → y == x
    ex2 = ?

    ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
    ex3 = ?

    ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
    ex4 = ?

--問題 2.4

以上の証明を refl を使って完成させてみよう。

<a href="agda/equality.agda"> equality </a> <!---  Exercise 2.4 --->

--問題 2.5

<a href="agda/practice-nat.agda"> nat の例題 </a> <!---  Exercise 2.5 --->

--集合のLevel 

論理式は型であり、それは基本的はSetになっている。例えば、A → B は Set である。

    ex1 : { A B : Set} → Set
    ex1 {A} {B} =  A → B

Agda は高階論理なので、論理式自体を返す論理式も作ることができる。

    ex2 : { A B : Set} →  ( A → B ) → Set
    ex2 {A} {B}  A→B  =  ex1 {A} {B}


では、これを論理式を要素として持つ直積を作ってみよう。

    record FuncBad (A B : Set) : Set where
      field
         func : A → B → Set

Agda は以下のように文句をいう。

    The type of the constructor does not fit in the sort of the
    datatype, since Set₁ is not less or equal than Set
    when checking the definition of FuncBad

自己参照的な集合の定義を避けるために集合には階(level)という概念が導入されている。

    open import Level
    record Func {n : Level} (A B : Set n ) : Set (suc n) where
      field
        func : A → B → Set n

のように集合の階(Level)を明示する必要がある。

--問題1.5 集合のLevel 

level が合うように ? を埋めよ。

<a href="agda/level1.agda"> level </a> <!---  Exercise 2.5 --->

--問題2.6 List

List は cons か nil かどちらかの構造で、cons は List を再帰的に含んでいる。

    postulate A : Set

    postulate a : A
    postulate b : A
    postulate c : A


    infixr 40 _::_
    data  List  (A : Set ) : Set  where
       [] : List A
       _::_ : A → List A → List A


    infixl 30 _++_
    _++_ :   {A : Set } → List A → List A → List A
    []        ++ ys = ys
    (x :: xs) ++ ys = x :: (xs ++ ys)

    l1 = a :: []
    l2 = a :: b :: a :: c ::  []

    l3 = l1 ++ l2

等式の変形を利用して、List の結合法則を証明してみよう。

    open  import  Relation.Binary.PropositionalEquality

    ++-assoc :  (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
    ++-assoc A [] ys zs = let open ≡-Reasoning in
      begin -- to prove ([] ++ ys) ++ zs  ≡ [] ++ (ys ++ zs)
       ( [] ++ ys ) ++ zs
      ≡⟨ refl ⟩
        ys ++ zs
      ≡⟨⟩
        [] ++ ( ys ++ zs )
      ∎
    ++-assoc A (x :: xs) ys zs = let open  ≡-Reasoning in ?

≡⟨⟩ などの定義はどこにあるのか?

--問題2.6 List

lemma を等式の変形を利用して証明してみよ。

<a href="agda/list.agda"> List </a> <!---  Exercise 2.6 --->

--DAGと否定

グラフには接続されてない二点が存在する。それを表現するために否定¬と矛盾⊥を導入する。

       ⊥
    ------------- ⊥-elim
       A

矛盾からは何でも導くことができる。この場合、A はSetである。⊥ を導入する推論規則はない。

これは、contructor のない data で表すことができる。

    data ⊥ : Set where

⊥-elim は以下のように証明できる。

    ⊥-elim : {A : Set } -> ⊥ -> A
    ⊥-elim ()

() は「何にもmatchしないパターン」である。これは型を指定した時に「可能な入力がない」必要がある。つまり、このケースは起こり得ない
ことを Agda が納得する必要がある。納得できないと error message がでる。

    λ ()

という構文も存在する。

⊥ を使って否定は以下のように定義される。

    ¬_ : Set → Set
    ¬ A = A → ⊥

否定には入力があることを意識しておこう。

         f0
      -----→
   t0         t1
      -----→
         f1

というグラフは以下のように記述する。

    data  TwoObject   : Set  where
           t0 : TwoObject
           t1 : TwoObject


    data TwoArrow  : TwoObject → TwoObject → Set  where
           f0 :  TwoArrow t0 t1
           f1 :  TwoArrow t0 t1

ループのあるグラフを作ってみよう。

         r0
       -----→
    t0         t1
       ←-----
         r1

    data Circle  : TwoObject → TwoObject → Set  where
           r0 :  Circle t0 t1
           r1 :  Circle t1 t0

矢印をたどって繋がっている点は接続(connected)されていると言う。

    data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
        direct :   E x y -> connected E x y
        indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y

直接繋がっているか、間接的に繋がっているかどちからになる。この構造は自然数に似ている。

t0 と t1 が TwoArrow の場合に繋がっていることを証明してみる。

    lemma1 : connected TwoArrow t0 t1
    lemma1 =  ?

t1 から t0 にはいけない。

    lemma2 : ¬ ( connected TwoArrow t1 t0 )
    lemma2  = ?

dag (Directed Acyclic Graph) は、すべての点(Vertex)で自分自身につながる経路(Edge)がないグラフ

    dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
    dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )

--問題2.7 DAGと否定

TwoArrow が dag で、Circle が dag ではないことを証明してみよう。

    lemma4 : dag TwoArrow
    lemma4 = ?

    lemma5 :  ¬ ( dag Circle )
    lemma5 = ?

<a href="agda/dag.agda"> DAG </a> <!---  Exercise 2.7 --->

--教科書の第一章

<a href="../agda/chap0.agda"> chapter 0 </a>