-title:  Agda での Programming 技術

-author: 河野真治

--なんで、今、証明支援系なのか?

証明支援系の歴史は古い ( HOL, Coq, Agda も新しくない )

Monadって何?

Monad を解説しているサイトは多いが、多くは皮相的

元は圏論の概念

→　だったら、Monad を証明支援系を使って理解すれば良いんじゃないの?

--プログラムの検証の二つの方法

    モデル検証
    証明

-- モデル検証

    可能な実行をすべて試す 
　　論理の言葉で言えば、充足可能性を調べる
    バグを探す、検索空間が膨大、比較的大きなものに対処できる
    扱う問題の規模に探索時間が依存する

--証明

    プログラムがどういう性質を満たすかを論理式で記述する
    推論規則を使って、公理と仮定から性質を導く
    非常に難しく、証明の長さも長い
    扱う問題の規模に証明時間が依存する

--Curry Howard 対応

証明とλ計算式が対応する。対応は、扱う論理に寄って異なる

論理が複雑になる分、λ計算を拡張する必要がある

　　→　ラムダ計算の拡張の指針になる

証明する論理式は型に対応する

証明するべき式の型になるλ式を作れれば証明されたことになる

--Agda とは何か

Haskell実装、Haskellに似た構文

   indent による scope の生成

型と値

   : で型を定義
   = で値を定義

集合
    すべての値は集合

集合のレベル
    集合の集合はレベルが上がる

暗黙の引数

    {} で省略可能な引数を作れる

--λ

    module proposition where
    postulate A : Set
    postulate B : Set

集合であるA,Bを命題変数として使う。

    Lemma1 : Set
    Lemma1 = A -> ( A -> B ) -> B

これが証明すべき命題論理式になる。実際には式に対応する型。
    lemma1 : Lemma1

として、この型を持つ lambda 式を使えば証明したことになる。
以下のどれもが証明となり得る。

    -- lemma1 a a-b = a-b a
    -- lemma1 = \a a-b -> a-b a
    -- lemma1 = \a b -> b a
    -- lemma1  a b = b a


--data 

Haskell の data と同じ。

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


論理式の排他的論理和を表すのにも使える。

    data _∨_  (A B : Set) : Set where
      or1 : A -> A ∨ B
      or2 : B -> A ∨ B

or1 と or2 が Constructor である。

    Lemma6  : Set
    Lemma6 = B -> ( A ∨ B )
    lemma6 : Lemma6
    lemma6 = \b -> or2 b

これは、∨ の導入になっている。削除は、

    lemma7: ( A ∨ B ) -> A
    lemma7 = ?


--equality

さらに、data は等式を表すのにも使う。

    data _==_  {A : Set } :  List A → List A → Set  where
          reflection  : {x : List A} → x == x

直観主義論理には命題自体に真偽はない。なので、返すのは Set になっている。なので、二重否定は自明には成立しない。

--record

record は、論理積を作るのに使う。

    record _∧_ (A B : Set) : Set where
       field
          and1 : A
          and2 : B

∧の導入

    lemma2 : A → B → A ∧ B
    lemma2 a b =  record { and1 = a ; and2 = b }

∧の削除 ( open _∧_  が必要 )

    lemma3 : A ∧ B → A
    lemma3 a =  and1 a

record は、ある性質を満たす数学的構造を表すのに使う。

--Append の例

    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)


-- Append の実行

 　Agda の実行は正規化
   Haskell と同じ

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

    l3 = l1 ++ l2


--Append の結合則の証明

証明するべき式 

    list-assoc : {A : Set } → ( xs ys zs : List A ) →
         ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )


List の持つ性質を表す式

    data _==_  {A : Set } :  List A → List A → Set  where
          reflection  : {x : List A} → x == x

    cong1 :  {A : Set  }  { B : Set  } →
       ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y

    eq-cons :   {A : Set } {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )

--Agda での証明手順

(1) 証明するべき式を型として記述する

(2) 値を = ? と取り敢えず書く

(3) ? をλ式で埋めていく

(4) C-N で正しいかどうかをチェックする

    赤   ... 型エラー
    黄色 ... 具象化が足りない
    停止性を満たさなない

(5) data  は patern match で場合分けする

(6) 必要なら式変形を使う


--Haskell と Agda の違い

Haskell で結合則を証明できる?

Haskell は型に関数やデータ型の constructor を書けない

Haskell のプログラムは Agda のプログラムになる?

   float とかはない
   integer は、succesor で書く必要がある

--式変形

λ式では、人間に読める証明にならない

    ++-assoc A (x :: xs) ys zs = let open  ==-Reasoning A in
      begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)                                                                                       
        ((x :: xs) ++ ys) ++ zs
      ==⟨ reflection ⟩
         (x :: (xs ++ ys)) ++ zs
      ==⟨ reflection ⟩
        x :: ((xs ++ ys) ++ zs)
      ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
        x :: (xs ++ (ys ++ zs))
      ==⟨ reflection ⟩
        (x :: xs) ++ (ys ++ zs)
      ∎




--いくつかの技術

等号

?

Unicode の記号

module

暗黙の引数が多すぎる

--Agda で証明できないこと

a ≡ b は証明できない

functional extensionarty

    -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → 
          (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )

実際には、

    postulate extensionality : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } 
       → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂


部分集合

    異なる集合の要素は異なるので、部分集合を作れない
    →　　x ∈ P 　を自分で定義する

合同性   x ≡  y ならば f x ≡  f y 。これは、_≡_  に付いてしか言えない。
Relation などで定義すると、合同性は自分で仮定あるいは証明する必要がある。


直観主義論理の限界

   あんまり良くわかりません

--圏論の定理の証明

  Monad の結合性
  Monad から作る Kleisli 圏
  Kleisli 圏から作る随伴関手
  随伴関手での Limit の保存
  米田のレンマ

--本の証明とAgdaの証明

    本の証明は、山登りの道標しか示さない

    Agdaの証明は、全部繋がっている

    Agda の証明は式なので対称性が目で見える

--定理を理解することと証明を理解すること

定理を理解するということは使い方を理解すること

定理は証明のショートカットでもある

証明を理解しても使いこなせない

--結局、Monad は役に立つのか?


--結局、証明 は役に立つのか?

--Agda は面白い

詰将棋みたいなもの

学会でノートPCで内職しているのは Coq 

Agda は Coq よりもマイナー