Members/kono/Proof/automaton: a02/lecture.ind comparison

comparison a02/lecture.ind @ 326:a3fb231feeb9

omega

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 21 Jan 2022 10:45:42 +0900
parents	e5cf49902db3
children	407684f806e4

comparison

equal deleted inserted replaced

-:39f0e1d7a7e5
+:a3fb231feeb9
 最低限5題をまとめてレポートで提出せよ
 <a href="agda/record1.agda"> record1</a> <!---  Exercise 2.2 --->
---Sum type
+--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 を使って一階述語論理を定義することもできる。

Mercurial > hg > Members > kono > Proof > automaton

comparison a02/lecture.ind @ 326:a3fb231feeb9