狠狠撸

証明プログラミング超入门
～述語論理を添えて～
2015/03/27
門脇香子(@kdxu)
1

自己紹介
? 門脇香子 (@kdxu)
? お茶の水女子大学浅井研(M1)
? 研究はコンパイラの定式化
? 趣味でゲーム開発

みなさん証明は好きですか？

概要
? 証明プログラミングとは？
? Agda による例?
1. ふつうの証明?
2. 命題論理と述語論理

証明プログラミングとは？
? ある種の性質を保障したプログラムが書ける?
数学の定理を証明したり，停止性などの性質が保障された
コンパイラなどを実装できる
? コードの停止性，正当性などを証明できる?
活用例 : OpenSSLの脆弱性の発見 ?
??? CompCert(安全性が保証されたCコンパイラ)
? テストではなく証明で正しさを保証する
? TDDからPDDへ(Proof-Driven-Development!)

Agda について
? もっとも有名な定理証明支援系の1つ
? 依存型という型を使用できる
? Syntax としては Haskell に近い
? 証明を項として表し直接操作する

インストール&セットアップ
? 適当にググる?
$ cabal install agda?
$ agda-mode setup
? AgdaWikiを見ましょう

まずは型定義
? data で新しい型を定義できる
? indent に注意
? Set の部分集合としてのBool型という意味

まずは型定義
? 自然数の型
? ペアノの公理による定義
? zeroがNat型ということと，xがNat型ならsuc x
もNat型だということを示している

関数定义
? 普通の足し算の定義
? (suc m) + n = (suc (m + n))
? C-c C-n で関数を評価できます

関数定义
? 中値記法もできます

何か証明してみよう
? Nat 型と Bool 型の簡単な定義はできた
? ここでなにか簡単な定理を証明する
? 同値性の証明をするならば同値関係のデータ型が必
要(equality)?
-> どのように定義するのか？

同値性
? 2つのものが同じということは，以下のように定義できる
? 例 : zero (suc zero) はダメ?
x x の形をしていない．型はあるが，値が存在しない?
なので，re?という型にならない
? re?になりうる値が存在するかで同値性が定義できる

定理は関数
? 例えば 0 + n n を示したい?
-> 返り値がre?となるように関数を書ければよい
? 関数の型は?
(n : Nat) → (0 + n n)?
となる
? ここで suc 関数に対する再帰的処理が必要になる

定理 = 関数
? これを Agda は型が等しいと判断してくれない
? ここで suc 関数に対する再帰的処理が必要になる
? 一般的に定理を再帰的に示す関数 cong
(congruence : 合同の意)を定義?

証明完了！
? zero と suc nで場合分けしている (C-c C-c n)?
zero の場合は zero + zero は zeroなので直ちにre??
suc n の場合は n に関して再帰的に証明をする

Tips : 依存型
? Agda では依存型(Dependent Types)という型が使えます
? 「値に依存する型」を作ることができる型
? 例 Vec N 型 - 長さを型レベルで保持しているリスト
? 型の段階で長さの比較や空リスト判定を保証できる

今日の目的
? 一階述語論理をAgdaで表現し，何かを証明する
? 一階述語論理って？そもそも述語論理って？

命題論理
? 述語論理は命題論理の拡張
? 命題論理 : P → Q ，? P Q みたいなやつ?
命題変数(P，Qなど)を原子式(それ以上分解できな
い命題）とした推論体系
? 推論の性質によりさまざまな論理体系がある

命題論理の構文要素
? 原子式 : P，Q，R …
? 真理値真（?）または偽（）
? 結合子 : ?，，など
? これらを組み合わせてさまざまな論理式をつくる

一階述語論理
? 個体の量化のみを許す述語論理?
具体的には，古典論理に?
- 原子論理式?
- 量化?
が加わっている．

一階述語論理
? 量子論理式?
例 : P x y z …
? 項を関係として表す

量化
? 「すべての x において～である」「～を満たす x
が存在する」
? 全称量化( )，存在量化( )

一階述語論理 at Agda
https://gist.github.com/KDXU/3ecf21603abe9e9a409e

一階述語論理式の例
? 例 : y x Loves(x,y)?
? Everyone in the world is loved by at least
one person
? 例2 : x y Loves(x,y)?
? There is a person who loves everyone in the
world

おすすめ教材
? Ulf Norell 氏の Dependently Typed Programming in
Agda ?
(http://www.cse.chalmers.se/ ulfn/darcs/AFP08/
LectureNotes/AgdaIntro.pdf)
? Brutal [Meta]Introduction to Dependent Types in
Agda ?
(http://oxij.org/note/BrutalDepTypes/)
? お茶大製「みんなのAgda wiki」?
(http://agda.wiki.fc2.com/)

? 私は今日紹介した Agda という言語を用いて証明
付きの型推論器を構成しています
? 実装 : https://github.com/kdxu/InferAgda

おわり
証明プログラミングを楽しみましょう！

狠狠撸

証明フ?ロク?ラミンク?入门2

Recommended

More Related Content

What's hot (20)

Viewers also liked (8)

Similar to 証明フ?ロク?ラミンク?入门2 (13)

証明フ?ロク?ラミンク?入门2