研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む
#TPP2014 高信頼な理論と実装のための定理証明および定理証明器
研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む
Software Foundations
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software. The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant. The exposition is intended for a broad range of readers, fro
Why: asoftware verification platform
Overview Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. (See the list of supported provers below.) Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, s
Isabelle Tutorial その11 - caeruiro
5.7 Interlude: the Basic Methods for Rules 次の規則を例として、メソッドの作用を詳しく見ていきます。 規則の名前をRとします。 メソッドruleはQとサブゴールを単一化し、P1からPnを新たなサブゴールとします。 メソッドeruleはQとサブゴールを単一化すると同時にP1を前提の何れかと単一化し、P2からPnをn - 1個の新たなサブゴールとします。単一化した前提は除去されます。(rule R, assumption)は似ていますが、前提は除去されません。 メソッドdruleはP1を前提の何れかと単一化し、これを除去します。得られるサブゴールはP2からPnのn - 1個と、元のゴールの前提からP1とマッチした項を取り除きQを加えた、計n個です。 メソッドfruleはdruleと似ていますが、マッチした仮定を除去しません。 各メソッドに_tacを付け
Isabelle Tutorial その10 - caeruiro
5. The Rules of the Game この章ではIsabelleを使った証明のコンセプトとテクニックを紹介します。 5.1 Natural Deducation Isabelleでは、証明は推論規則によって構成されます。もっとも有名な推論規則の一つがmodus ponensです。 Isabelleでは自然演繹を使用します。Isabelleは適用可能な規則を探索することで、自動的に証明しようとします。自動証明がうまくいかない場合は、後述する方法で推論規則を適用し証明を手動で進めます。 5.2 Introduction Rules ある論理記号について、導入規則はその記号が含まれた式を推論するのに使用します。例えば論理積の導入規則は、もしPとQが言えるならば、P ∧ Qが言えることを示しています。 結論に論理積が導入されているのがわかります。多くの場合、Isabelleの証明は後ろ
Isabelle Tutorial その9 - caeruiro
3.4 Advanced Datatype 3.4.1 Mutual Recursion 相互再帰するデータ型の例として、算術式とブール式を示します。算術式には条件文が含まれており、よってブール式が含まれています。またブール式には値の比較が含まれており、よって算術式が含まれています。相互再帰するデータ型の定義はandで繋げて記述します。 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" | Sum "'a aexp" "'a aexp" | Diff "'a aexp" "'a aexp" | Var 'a | Num nat and 'a bexp = Less "'a aexp" "'a aexp" | And "'a bexp" "'a bexp" | Neg "'a bexp" この式の評価関数は次のように定義します。 prim
Isabelle Tutorial その8 - caeruiro
3.3 Case Study: Compiling Expressions 今節では、変数、定数、そして二項演算子からなる式からスタックマシーンへのコンパイラを開発します。これは、2.5.6のブール式を一般化したものです。変数や値の型は特に定めず、型パラメータとして定義します。二項演算子も詳細は定めず、適当な演算子を持っているとします。 types 'v binop = "'v => 'v => 'v" datatype ('a, 'v) expr = Cex 'v | Vex 'a | Bex "'v binop" "('a, 'v) expr" "('a, 'v) expr" 三つの構成子は定数、変数、二項演算子の適用を表わします。式をある環境の下で評価する関数は次のように定義できます。 primrec "value" :: "('a, 'v) expr => ('a => 'v) =
Isabelle Tutorial その7 - caeruiro
3.2 Induction Heuristics この節では、帰納法を使った証明のヒューリスティクスを説明します。最初は既に出てきたヒューリスティクスです。 再帰関数に関する定理は帰納法で証明せよ。 次は二つ以上の引数を取る関数の証明についてです。 i番目の引数が再帰的に定義されている関数は、i番目の引数について帰納法を適用せよ。 このヒューリスティクスは例えば2.3節の証明で使いました。 ゴールが固有的な場合、帰納ケースの前提が弱すぎて証明できない場合があります。そこでキーとなるヒューリスティクスは、帰納法を使う前にゴールを一般化することです。例を使って見ていきます。 関数revは効率が悪いので、累積変数を導入し線形時間で計算可能な関数を作成します。 primrec itrev :: "'a list => 'a list => 'a list" where "itrev [] ys =
Isabelle Tutorial その6 - caeruiro
3. More Functional Programming 3.1 Simplification 単純化はIsabelle及び他の多くのシステムにおいて重要な定理証明ツールです。今節では単純化について述べていきます。 3.1.1 What is Simplification? 簡単に言うと、単純化とは等式の左辺から右辺への変換を繰り返すことです。例えば、@のルールを使った単純化のステップを示します。 (0#1#[]) @ [] → 0#((1#[]) @ []) → 0#(1#([] @ [])) → 0#1#[] これは項書換えと見ることもでき、その場合等式は書換規則と見ることができます。 既に見たように単純化を用いて算術式を証明することもできますが、この場合は項書換え以上のことが行われています。ただしこれについてこのチュートリアルでは取り上げません。 3.1.2 Simplifica
Isabelle Tutorial その5 - caeruiro
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" where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" lemma "sum n + sum n = n * (Suc n)" apply(induct_tac n) apply(auto) done +, -, *, div, mod, min, max, <=, <などが定義されています。最小値演算LEASTも定義されています。例えば(LEAST n. 0 < n) = Suc 0です。 定数0や1
Isabelle Tutorial その3 - caeruiro
2. Functional Programming in HOL ここからはHOLでどのように関数プログラムを書き、どのように検証するのか見ていきます。Isabelle/HOLを使う目的はシステムをモデル化し検証することなので、関数を実行可能なかたちで定義する必要はないのですが、まずは実行可能な定義を書くことにします。ただし、HOLでは必ず全域的でなければならないことに注意してください。 2.1 An Introductory Theory MLやHaskellと同じようにデータ型と関数を定義することができます。簡単なリストを定義しながら、方法を一つ一つ見ていきます。 theory ToyList imports Datatype begin HOLには既にリストが定義されています。多くの場合Mainをインポートしますが、定義済みのリストもインポートしてしまうため、ここではDatatype
Isabelle Tutorial その2 - caeruiro
1.4 Variables もちろんIsabelleは自由変数と束縛変数を区別しますし、束縛変数は名前の衝突が起こらないよう自動で改名されます。この2つに加えて、?で始まる変数があります。これをスキーマ変数(schematic variable)またはアンノウン(unknown)といいます。スキーマ変数は論理的には自由変数と同じですが、Isabelleの証明では自由変数とは異なり他の項に置き換えることができます。 証明を終えるとその定理に含まれる自由変数がスキーマ変数に置き換えられることがわかります。これにより、新たな定理を他の定理の証明に使うことができるのです。実際に証明をしてみると、なんとなくわかってくるかと思います。ただし、スキーマ変数を意識する必要はあまりないでしょう。 1.5 Interaction and Interfaces Isabelleとshellで直接対話することもで
Isabelle Tutorial その1 - caeruiro
1. The Basics 1.1 Introduction Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。 1.2 Theories Isabelleを使用して理論を構築していきます。理論とは、型、関数、定理の集まりです。理論Tを定義するには次のように書きます。 theory T imports B1, ..., Bn begin 宣言、定義、証明などなど end B1, ..., Bnは既存の理論で、Tをこれらの上に構築していきます。オブジェクト指向プログラムのクラスの継承みないなものです。名前が衝突する場合は、T.fやB.fなどと書いて回避します。ファイル名はT.thyとします。 既存の理論ファイルは次のページで探すことができますし、Isabelleをインストー
計算モデルと論理とゲーデルの不完全性定理 - Gemmaの日記
ゲーデルの不完全性定理は、数学を扱う数学、つまりメタ数学を考えるが、それだと理解が難しい。しかし、証明(数学)＝プログラムという悟りを開くと、プログラムを扱うプログラム、つまりメタプログラムを考えればよくなり、それならコンパイラ等でなじみがあるので理解が優しくなる。 話の流れは以下。 1. プログラムとは何か 2. 証明とは何か 3. 証明＝プログラム , （ {、 { ヽ.ｰ､､ ＼､__ぃ._ゝ⌒ヾ iヾ）}､_ ﾝ_ｰ-_二ｰ-, 〉 {厶 _､ヽ _ ヽ._＞'´ ／ /,ィ／ / ハYﾍい ,. -- 〃⌒ r−-､ ィ´ 〃 ,ｲ/7' ,ｲイ/ 小ヽ 丶、 ,. ‐ '´ﾊ i ″｀ヽ、 、ヽ、 ／幺ィ {从{小込v' jｩ仏厶川ﾘ} YV, 小 Vj. |丶 ヽ ｀ ｰ-ミー--'_,辷三彡
日本語の Coq 情報 - まめめも
ついでに、主に日本語の Coq 情報を (10 分で思い出せる範囲で) まとめてみます。順不同。 公式に近い情報 本家 Coq'Art (Coq の教科書) Cocorico! (本家 Coq wiki) CiteSeer (笑) Coq のことをまとめようとしている wiki 菊さんの Coq wiki Tossy-2 の Coq wiki たまに Coq のことが書いてあるブログ yoshihiro503 さんのブログ (LL 魂で Coq の発表をされた方、Coq の話ばっかり) いまいけいごさんのブログ 菊さんのブログ Tossy-2 のブログ あろはさんのブログ (2006/04 〜 05 頃) 他にもちらほら見かけるはずなのですが、ちゃんとメモしてなかったので思い出せません。見つけたら自発的に適宜追加するかもしれませんが、教えてもらえると助かります。
The Agda Wiki
Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Agda is a proof assistant. It is an interactive system for wr
産総研：システム検証研究センター：CVS研修コース「Agdaによる仕様記述」
研修コース「 Agda による仕様記述」開催のお知らせ ■コース概要 近年、体系的にシステムを開発する手段の一つとして数理的技法(形式手法)が注目を集めています。例えば形式仕様記述の枠組みを使うと、仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。結果として設計書や実装に不具合の種が入り込むことを防ぐことができます。 本コースでは、形式仕様記述の概要とその実際を講義と演習を通して実感して頂きます。演習環境として用いるツール Agda は(１)関数型プログラミング言語(２)形式仕様の処理系(３)定理証明支援系の側面を持つツールです。本コースでは(１)(２)の側面を使い、抽象的なデータの定義と関数を用いてシステムを記述すること、記述を支援する Agda の機能と操作法を扱います。演習の時間を多くとり、実例と経験から形式仕様記述を理解できるコースとなっています。 ■目標 (１
はじめての Coq - zyxwvの日記
Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明するためにどうしたらいいかが書いてあるわけじゃないし。 だって「(a -> b -> c) -> (a -> b) -> a -> c" を証明してみましょう」とか言われても全然やる気にならないじゃん。そんなことを証明するために Coq を使いたいわけじゃない！ そんなわけで、ocaml-nagoya の合宿の機会を利用して id:yoshihiro503 さんと id:suer さんに、Coq をプログラミング言語として使う場合の基本を教えてもらってきました。特に id:yoshihiro503 さんは少なくとも僕から見ると Coq M
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/CoPL/
関数型プログラミング言語「Agda」の研修コースを産総研が開催 | スラド デベロッパー