-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> 

Unicode入力

<a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html"> Unicode入力 </a>

--重要

    空白が入らないものは一単語になる (A→A は一単語、A → A とは別)

    A:Set は間違いで、A : Set

    A → B → C は、 A → ( B → C )  のこと

　　f x y は (f x) y のこと


---問題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/record1.agda"> record1</a> <!---  Exercise 2.2 --->

--Sum type

<a href="sumtype.html"> Sum type 排他的論理和</a>