ついに最終章です。10. Case Study: Verifying a Security Protocol最後の章は、セキュリティプロトコルをモデル化し、その正しさを証明します。Needham-Schroeder公開鍵プロトコルを例として、Isabelleを使ったプロトコルの検証方法を見ていきます。 10.1 T…

9.2 Advanced Induction Techniques この節では、証明したい式が帰納法に適した形になっていない場合にどうすべきか、そして帰納法のための新たな定理をどのように導出し使うかということを見ていきます。 9.2.1 Massaging the Proposition 証明したい式が帰…

9. Advanced Simplification and Induction 9.1 Simplification この節では、単純化に関してこれまで述べてこなかった部分を補足します。 9.1.1 Advanced Features Congruence Rules.P ==> QのQを単純化するのに前提Pを利用できます。==>ならば当然のように…

8.5 Introducing New Types 多くの場合は定義済みの型boolや=>とそれらの組み合わせで事が足りますが、稀にこれらでは表わせない高度な型が必要になる場合があります。そのような場合に必要となる型の導入方法を紹介します。 8.5.1 Declaring New Types type…

8.3 Type Classes 型クラスの概念はHaskellによって広まりました。型クラスは型とインタフェースの集合を定義し、そのクラスに属する型はインタフェースを実装しなければなりません。Isabelleが提供する型クラスも同様ですが、さらにプロパティ(型公理)を定…

8. More about Typesこの章ではより高度な型の扱い方を紹介します。 8.1 Pairs and Tuples ペアやタプルは既に登場しましたが、ここではパターンマッチついて見てみます。 8.1.1 Pattern Matching with Tuples 変数を束縛するためのパターンとしてペアやタプ…

7.4 Case Study: A Context Free Grammer ここでは、HopcroftとUllmanによる文脈自由文法の例*1を取り上げます。生成規則は次のようになっており、これはaとbの数が同じ文字列を生成します。 まず、アルファベットを定義します。 datatype alpha = a | b 便…

7.2 The Reflexive Transitive Closure 帰納的定義はパラメータを取り、集合を作るための関数とすることができます。また関係はペアの集合であることから、これも帰納的に定義できます。例として関係から反射推移閉包への写像関数を考えます。 inductive_set…

7. Inductively Defined Setsこの章では集合の帰納的定義を紹介します。 7.1 The Set of Even Numbers 偶数の集合は、定数0と演算子+2からなる最小の集合として帰納的に定義できます。もちろん、整除関係(dvd)を使用しても定義できます。それぞれの方法で定…

6.6 Case Study: Verified Model Checking ケーススタディとしてComputation Tree Logic(CTL)を使ったモデル検査を取り上げます。モデル検査の基礎は集合論であり、これをHOLを使って見てみます。まずpropositional dynamic logic(PDL)と呼ばれる単純な様相…

6.4 Well-Founded Relations and Induction 整礎性は手続きの停止性と関係します。例えば複雑な再帰関数の定義にはその停止性を保証するための整礎関係を示す必要があり、また多くの数学的帰納法は整礎帰納法の特別な場合です。関係が整礎であるとは、関係が…

6. Sets, Functions and Relationsこの章では集合、関数、関係を見ていきます。集合は、例えば言語理論や計算理論、状態遷移機械など計算機科学における形式化にも有用です。Isabelleは、集合計算が含まれる多くの式も自動証明します。このドキュメントで全…

5.17 Managing Large Proof 長くなりがちな証明のステップを短くする方法を見ていきます。 5.17.1 Tacticals, or Control Structures 長い証明の中には、規則性が現れることがあります。プラス記号(+)を使用して、ステップを繰り返すことができます。例えば…

5.15 Forward Proof: Transforming Theorems ここまでは後ろ向きの証明を扱ってきましたが、前向きに証明を行うこともできます。前向きの証明は、一般的な定理から固有の定理を導くのに便利です。例えば最大公約数の分配法則を考えます。 k * gcd(m, n) = gc…

5.12 Proving Theorems Using the blast Method Isabelleのclassical reasonerは自動証明のためのツールの一つであり、その中でも最も重要なメソッドがblastです。述語論理の例から見ていきます。次の例はAndrew's challengeと呼ばれ、自動証明が難しいとさ…

5.10 Description Operators HOLには二つの記述演算子があります。確定記述はその式を満たす唯一の値を表わします。不確定記述はその式を満たす任意の値を表わします。 5.10.1 Definite Description 確定記述は伝統的にιx. P(x)と書きます。これは、P(x)を満…

5.7 Interlude: the Basic Methods for Rules 次の規則を例として、メソッドの作用を詳しく見ていきます。 規則の名前をRとします。メソッドruleはQとサブゴールを単一化し、P1からPnを新たなサブゴールとします。メソッドeruleはQとサブゴールを単一化する…

5. The Rules of the Gameこの章ではIsabelleを使った証明のコンセプトとテクニックを紹介します。 5.1 Natural Deducation Isabelleでは、証明は推論規則によって構成されます。もっとも有名な推論規則の一つがmodus ponensです。 Isabelleでは自然演繹を使…

3.4 Advanced Datatype 3.4.1 Mutual Recursion 相互再帰するデータ型の例として、算術式とブール式を示します。算術式には条件文が含まれており、よってブール式が含まれています。またブール式には値の比較が含まれており、よって算術式が含まれています。…

3.3 Case Study: Compiling Expressions 今節では、変数、定数、そして二項演算子からなる式からスタックマシーンへのコンパイラを開発します。これは、2.5.6のブール式を一般化したものです。変数や値の型は特に定めず、型パラメータとして定義します。二項…

3.2 Induction Heuristics この節では、帰納法を使った証明のヒューリスティクスを説明します。最初は既に出てきたヒューリスティクスです。 再帰関数に関する定理は帰納法で証明せよ。 次は二つ以上の引数を取る関数の証明についてです。 i番目の引数が再帰…

3. More Functional Programming 3.1 Simplification 単純化はIsabelle及び他の多くのシステムにおいて重要な定理証明ツールです。今節では単純化について述べていきます。 3.1.1 What is Simplification? 簡単に言うと、単純化とは等式の左辺から右辺への変…

2.6 Some Basic Types 2.6.1 Natural Numbers 自然数を表す型natは構成子0とSucで定義されています。case式を使った例を示します。 case n of 0 => 0 | Suc m => m 原始再帰関数の定義と、帰納法による証明の例も示します。 primrec sum :: "nat => nat" whe…

やっと証明に入りました。 2.3 An Introductory Proof 証明の大まかな流れを追ってみます。Main Goal.リストにrevを二回適用すると元に戻ることを証明します。 theorem rev_rev [simp]: "rev (rev xs) = xs" theoremは新しい定理"rev (rev xs) = xs"を証明し…

2. Functional Programming in HOLここからはHOLでどのように関数プログラムを書き、どのように検証するのか見ていきます。Isabelle/HOLを使う目的はシステムをモデル化し検証することなので、関数を実行可能なかたちで定義する必要はないのですが、まずは実…

1.4 Variables もちろんIsabelleは自由変数と束縛変数を区別しますし、束縛変数は名前の衝突が起こらないよう自動で改名されます。この2つに加えて、?で始まる変数があります。これをスキーマ変数(schematic variable)またはアンノウン(unknown)といいます。…

Isabelleのチュートリアルを読みながらまとめていきたいと思います。http://www.cl.cam.ac.uk/research/hvg/Isabelle/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf最新バージョンはIsabelle2009-1。バージョンが変わる前…

1. The Basics 1.1 Introduction Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。 1.2 Theories Isabelleを使用して理論を構築していきます。理…