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

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

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

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

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


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

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

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

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

この章の内容は基本的には Girad 先生の Proofs and Typesに書いてある内容です。

--あらすじ

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>

--Agda introduction

<a href="https://gitlab.ie.u-ryukyu.ac.jp/teacher/kono/agda-introduction"> Agda introduction </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 where
     field
         π1 : A
         π2 : B

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

     _∧_ A B

は

     A ∧  B

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

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

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

--data -- Sum type

record は  ∧ に対応するが、∨はどうすれば良いのか。残念ながら∧と対称につくることはできない。(なぜか?)

Agda では data という場合分けをする型を導入する。Curry Howard対応が成立する様に、論理記号に対応する
型を導入する。型には導入と削除がある。

導入のない data を定義すると、それを矛盾として使うことができる。それを使って否定を定義する。

さらに

  有限な要素を持つ集合(型)
  自然数
  λ項の等しさとしての等式
  不等号

も data を使って定義できる。

data は invariant あるいは、制約付きのデータ構造を表すこともできる。

さらに、

　規則にしたがって生成される集合

も表すことができる。一つ一つ、ゆっくり片付けていこう。

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

以下は必要に応じて説明していく。

--λ計算の進み方

Agda の値と型は項で定義されていて、それを簡約化することにより計算が進む。
   
Agda (そして Haskell )は、項を簡約化していくことにより計算が進むプログラミング言語である。

簡約化の順序には自由度があり、それは実装にって変わる。

　関数適用にる置き換え
　場合分けによる変数の確定
  確定した変数での置き換え

自由度に関係なく、項は決まった形に簡約化されるようにλ計算は作られている。(合流性 -- 要証明だが、割と難しい)

(Agda で Agda を実装できるのか?)

合流性があるので、data で定義された等号が正しく動作する。

変数が含まれている場合の等号は単一化と呼ばれる。変数の置き換えが置きるのは data の場合分けと、関数呼び出しの二種類になる。

--停止性の問題

入力を data の場合分けで分解していくことは、入力が決まった大きさの項なので、必ず有限回しかできない。

つまり、そういう計算が止まることは Agda にはわかる。例えば List や Nat の分解である。

分解は再帰的なので、再帰呼び出しがとまるかどうかは、再帰呼び出しの引数が、dataの分解になっているかどうかで判断される。

これは一般的なプログラムでは自明にはならない。その時には型チェックエラーになる。 {-# TERMINATING #-} を指定することにより
それを抑制できる。その場合は、そういう止まるとすればという仮定を持つ計算あるいは証明になる。

-- induction

自明な停止条件でない推論もいくつかある。

   引数が直接 data を分解しないが、引数が減少する自然数に対応する場合
   生成される引数パターンが有限だと分かっている場合

の二つの場合は Agda で induction を定義できる。

--古典論理、一階述語論理との差

Agda の → ∧ ∨ は、項の型として定義されている。

  _∧_  : Set → Set → Set 

古典論理では真と偽の二つしかない。

   data Bool : Set where
       true : Bool
       false : Bool

この差は、二重否定の扱いに現れる。

    _/\_ : Bool → Bool → Bool 
    true /\ true = true
    _ /\ _ = false

    _\/_ : Bool → Bool → Bool 
    false \/ false = false
    _ \/ _ = true

    not_ : Bool → Bool 
    not true = false
    not false = true 


とする。

以下は Bool では証明できるが、Set では示せない。

    lem-in-bool :  (b : Bool) →  not p \/ p
    lem-in-bool = ? 

    double-negation-bool :  {B : Bool}  → not (not B) → B
    double-negation-bool = ?

Set の方では対偶は一方向しか成立しない。また、二重否定や排中律も成立しない。

    contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
    contra-position {n} {m} {A} {B}  f ¬b a ?

これは、Agdaの Set が具体的なλ項を要求するためである。つまり、

　　実際に構成できる証明しか Set は受け付けない

Bool の場合は最初から true / false がわかっている。Set の場合は、そこに入る項がある、入らないことを証明する項がある。
そして、どちらかわからない場合がある。

実際にわからない場合があることが証明されている(不完全性定理)。一方で、

　　証明するべき式が恒真(すべての可能な入力について真)なら、証明がある(完全性)

であることも証明されている。恒真かどうかはわからないので、この二つは矛盾しない。


--一階述語論理の定義

Agda を使って一階述語論理を定義することもできる。










---問題2.3 sum type の問題

問題2.9 まで

<a href=""> </a> <!--- Exercise 2.3 --->
<a href=""> </a> <!--- Exercise 2.4 --->
<a href=""> </a> <!--- Exercise 2.5 --->
<a href=""> </a> <!--- Exercise 2.6 --->
<a href=""> </a> <!--- Exercise 2.7 --->
<a href=""> </a> <!--- Exercise 2.8 --->
<a href=""> </a> <!--- Exercise 2.9 --->
<a href=""> </a> <!--- Exercise 2.8 --->
<a href=""> </a> <!--- Exercise 2.9 --->