言語組：講義資料
いまどきの！？
プログラミング言語理論
いなば かずひろ
稲葉 一浩http://www.kmonos.net/
http://twitter.com/kinaba
2/39
お話しする内容
• 時は2009年
• 「プログラミング言語」の
「理論」の
「研究者」のあいだで
• 今なにがアツい？
3/39
理論系のトップレベルの学会
• POPL 2009
–Symposium on Principles of
Programming Languages
»“プログラミング言語の本質”
• ESOP 2009
–European Symposium on
Programming
4/39
今年の時間割:POPL 2009
•
•
•
•
並行性 (Concurrency)
型１(Types)
その他１ (Medley)
静的解析１
(Static analysis)
• 関数型ﾌﾟﾛｸﾞﾗﾐﾝｸﾞ
(Functional programming)
• その他２ (Medley)
• 静的解析２
(Static analysis)
• 静的解析３
(Static analysis)
• プログラム論理学
(Program Logics)
• 型２ (Types)
• マルチコア (Multicore)
• 検証 (Verification)
5/39
今年の時間割:ESOP 2009
• 型付き関数型言語
(Typed Functional
Programming)
• 計算の(副)作用
(Computational Effects)
• オブジェクト指向
言語の型
(Types for Object-Oriented
Languages)
• 検証 (Verification)
• セキュリティ
(Security)
• 並行性 (Concurrency)
• サービス指向
(Service-Oriented Computing)
• 並列・並行プログ
ラミング (Parallel and
Concurrent Programming)
6/39
わかること
• 静的解析・検証・型
–古くから理論屋さんの主な話題
• 並行・並列・マルチコア
–当たり前ですが流行ってます
7/39
静的解析・検証・型
• 例
– 「このポインタがこの変数を指す可能性はあ
るか無いか？」の解析 → 無いと証明できれ
ばできる最適化がある（参考: C99のrestricted）
– 「このint型の変数はどのくらいの範囲の値に
なる可能性があるか？」の解析 → 配列の
オーバーランが絶対起きないことの保証
– Rubyのような動的型付け言語で
静的に型検査する研究
–…
8/39
並行・並列・マルチコア
•例
– 並列/分散プログラムの数学的に
扱いやすいモデルを考える
– デッドロックしないことの
自動/手動証明手法
– ロックフリーデータ構造の
正しさの証明手法
– STM(トランザクショナルメモリ)が
正しく動いていることの保証…
9/39
わかること：結論
• プログラム理論の学者さんは
「保証」「証明」がお好き
–(※脇道：
なんで？なんのため?）
10/39
ここでニュース！！
•速報！！
•いま
「証明」界に異変！？
11/39
最近の論文からの引用
machine-checked
construction and verification of code-based proofs… [G. Barthe et al. ,
1. …Certicrypt, a framework that enables the
POPL 2009]
proof
assistant both for programming the compiler and for proving…
2. …a compiler from Cminor to PowerPC assembly code, using the Coq
[X. Leroy, POPL 2006]
3. … accurate semantics for x86 …
mechanised in HOL.
…For programs
prove
…we
in HOL that their behaviour is sequentially consistent. [S. Sarkar et
al., POPL 2009]
4. … formal verification of an SLR parser generator…. This conversion also illustrated
the gap between simple textbook definitions and a
verifiable
executable implementation in a theorem prover.[M. Schäfer
al., ESOP 2009]
et
12/39
異変：急増しているキーワード
• Mechanized
機械化
機械的
• Machine-checked チェック済
• Proof
証明
• Assistant
支援
• Executable
実行可能
プログラミング
• Programming
13/39
証明のニューウェーブ
• 紙とペンでの証明
• コンピュータでの全自動証明
• 証明が書けるプログラミング
言語を使う (←New!!)
(※注: このアイデア自体はNewというほ
どでもなく30年以上前のものです。が、
ここ数年で爆発的に使われ始めてます)
14/39
発想：計算したい問題がある
• 紙とペンで計算
↓ (大きな計算はできない)
• 問題を書いたら全自動で
解いてくれる夢の計算機
↓ (一部の問題に限れば可能。でも一般には無理)
• 人間がアルゴリズムを
プログラミング！ (大成功！)
15/39
発想：証明したい問題がある
• 紙とペンで証明
↓ (大きな証明はできない/間違うかも)
• 問題を書いたら全自動で
証明してくれる夢の計算機
↓ (一部の問題なら可能。でも一般には無理)
• 人間が証明を
プログラミング！ (大成功！？)
証明をプログラミングする！
～Proof meets Programming
～
17/39
証明が書ける言語の雰囲気
int[] qsort( int[] xs ) {
if( xs.size <= 1 )
return xs
else {
int[] ls = xs[1..-1].select{|x|x<xs[0]}
int[] gs = xs[1..-1].select{|x|x>=xs[0]}
return qsort(ls) + [xs[0]] + qsort(gs)
}
※コードはイメージです ： (Ruby+C)÷2 くらいの仮想言語
}
“qsort の返値は必ずソート済み(小さい順
に並んでる)” を「証明」してみる
18/39
証明が書ける言語の雰囲気
(int[],sorted(.)) qsort( int[] xs ) {
if( xs.size <= 1 )
return xs
else {
int[] ls = xs[1..-1].select{|x|x<xs[0]}
int[] gs = xs[1..-1].select{|x|x>=xs[0]}
return qsort(ls) + [xs[0]] + qsort(gs)
}
関数の型を、「配列を返す」から
}
「配列と、その配列がソート済みなことの証明」
のペアを返すように変更
19/39
証明が書ける言語の雰囲気
(int[],sorted(.)) qsort( int[] xs ) {
if( xs.size <= 1 )
return (xs, “個数が1個以下なら当然sorted”)
else {
int[] ls = xs[1..-1].select{|x|x<xs[0]}
int[] gs = xs[1..-1].select{|x|x>=xs[0]}
return qsort(ls) + [xs[0]] + qsort(gs)
}
サイズが 1 以下の場合
}
配列と、sortedなことの証明を返すようにする。
20/39
証明が書ける言語の雰囲気
(int[],sorted(.)) qsort( int[] xs ) {
if( xs.size <= 1 )
return (xs, “個数が1個以下なら当然sorted”)
else {
int[] ls = xs[1..-1].select{|x|x<xs[0]}
int[] gs = xs[1..-1].select{|x|x>=xs[0]}
(int[] lss, sorted(.) lsp) = qsort(ls)
(int[] gss, sorted(.) lsp) = qsort(gs)
return (lss + [xs[0]] + gss, ???)
}
qsort の再帰呼びは配列と証明のペアを返します
}
あとはこれを使って全体がsortedな証明を作る！
21/39
証明が書ける言語の雰囲気
あとはこれを使って全体がsortedな証明を作る！
(int[] lss, sorted(.) lsp) = qsort(ls)
(int[] gss, sorted(.) lsp) = qsort(gs)
return (lss + [xs[0]] + gss,
???)
どうやって？
今作ってある証明は
- 「lssはソート済み」と「gssはソート済み」
だけ
22/39
証明が書ける言語の雰囲気
あとはこれを使って全体がsortedな証明を作る！
(int[] lss, sorted(.) lsp) = qsort(ls);
(int[] gss, sorted(.) lsp) = qsort(gs);
return (lss + [xs[0]] + gss, “ソート済みな
配列とソート済みな配列をつなげたらソート済みに
決まってるじゃん。根拠→”(lsp,gsp) )
↑ …
23/39
証明が書ける言語の雰囲気
あとはこれを使って全体がsortedな証明を作る！
(int[] lss, sorted(.) lsp) = qsort(ls)
(int[] gss, sorted(.) lsp) = qsort(gs)
return (lss + [xs[0]] + gss, “ソート済みな
配列とソート済みな配列をつなげたらソート済みに
決まってるじゃん。根拠→”(lsp,gsp) )
↑ 残念、間違いです！！！
例： [4,5,6] + [1,2,3] == [4,5,6,1,2,3]
24/39
証明が書ける言語の雰囲気
lss は xs[0] より小さくて、gss は xs[0] 以上
なんだから、そんなことにはならないよ！
(int[] ls, small(..) lsSmall) =
矢印は
xs[1..-1].select{|x|x<xs[0]}
一部
省略…
(int[] gs, big(..) gsBig) =
xs[1..-1].select{|x|x>=xs[0]}
(int[] lss, sorted(.) lsp) = qsort(ls)
(int[] gss, sorted(.) gsp) = qsort(gs)
return (lss + [xs[0]] + gss, “xs[0]より
小さいソート済みの配列とxs[0]以上の
ソート済み配列を繋げたらソート済みに決まってる
じゃん。根拠→”(lsSmall,gsBig,lsp,gsp))
25/39
証明が書ける言語の雰囲気
(int[] ls, small(..) lsSmall) =
xs[1..-1].select{|x|x<xs[0]}
(int[] gs, big(..) gsBig) =
xs[1..-1].select{|x|x>=xs[0]}
(int[] lss, sorted(.) lsp) = qsort(ls)
(int[] gss, sorted(.) gsp) = qsort(gs)
return (lss + [xs[0]] + gss, “xs[0]より
小さいソート済みの配列とxs[0]以上の
ソート済み配列を繋げたらソート済みに決まってる
じゃん。根拠→”(lsSmall,gsBig,lsp,gsp))
↑ 残念、まだ不完全です！！！lsがxs[0] より
小さいからって、lssがxs[0]より小さいとは限らないよね？
26/39
証明が書ける言語の雰囲気
qsort したって値の範囲が変わるわけないじゃん！！
「証明」しないとわかんない！
(int[],sorted(.),sameRange(..)) qsort(int[] xs) {
if( xs.size <= 1 )
return xs
else {
int[] ls = xs[1..-1].select{|x|x<xs[0]}
int[] gs = xs[1..-1].select{|x|x>=xs[0]}
return qsort(ls) + [xs[0]] + qsort(gs)
}
}
27/39
できました！
(int[],sorted(.),sameRange(..)) qsort(int[] xs) {
if( xs.size <= 1 )
return (xs,”1個以下なら当然ソート済み”,
”引数そのまま返してるんだから値の範囲は当然同じ”)
else {
(int[] ls, range(.,min(.)～.) lsSmall)
= xs[1..-1].select{|x|x<xs[0]}
(int[] gs, range(.,.～max(.)) gsBig)
= xs[1..-1].select{|x|x>=xs[0]}
(int[] lss, sorted lsp, sameRange sl) = qsort(ls)
(int[] gss, sorted gsp, sameRange sg) = qsort(gs)
return (lss + [xs[0]] + gss, “ちっちゃいソート済みと
大きいソート済みを繋げたらソート済み。証拠
→”(lsp,gsp,lsSmall,gsBig,sl,sg),
”元の範囲に収まってる配列をくっつけてもやっぱり
元の範囲に収まる”(lsSmall, gsBig, sl, sg))
}}
28/39
Good:「紙とペン」より確実
• 「証明が正しい」ことの
チェックは全自動でできる！
–間違った証明を書いたら
コンパイラが教えてくれる
• C言語等の型チェックが
全自動なのと同じ原理
29/39
Good: 人間の直感
(int[],sorted(.),sameRange(..)) qsort(int[] xs)
• 「sortedの証明には値の範囲が変わ
らないことの証明も同時に要る！」
– のような発想は、コンピュータに全自
動でやらせるのはなかなか難しい
(※これくらいならできるかもですが)
– こういうところをプログラマの発想で
補いつつ「正しい」証明を書ける
30/39
Good: 大規模証明開発！
• 証明支援環境
– 「あとこれとこれとこれを証明すれば全部証
明終わるよ」と教えてくれる
– 簡単な証明は補完機能で勝手に書いてくれる
– 使えそうな定理のリストアップ機能
• プログラミングといっしょ
– 「証明」も普通のプログラムなので
関数に分けたりモジュール化したり…
31/39
Good: 証明もオブジェクト
• int* bsearch(int[] xs, int key)
↓ 二分探索する関数：
↓
コメントに”ソート済み配列にしか
↓
使えないよ”と書いておく
↓
• int*
bsearch
(int[] xs, sorted(.) prf, int key)
↑ ソート済みしか受け取らん！とコードで語る
32/39
Bad: 書きにくい
• それでもまだ凄くプログラミングが
めんどくさい
研究者自身にとっても大変
今までサラッと流してた部分が
厳密にプログラム化すると
実は面倒だったり
• 画期的な証明記述言語/ライブラリが
求められています！
33/39
利用例:
プログラム powered by 証明
• コンパイル結果が正しいこと
の証明つきコンパイラ
• 暗号プロトコルがアタックさ
れにくいことの証明付き暗号
エンコーダ
•…
34/39
さっきtwitterに貼られてた
• http://ertos.nicta.com.au/research/l4.verified/
35/39
利用例:
証明 powered by プログラム
• wikipedia「四色問題」
– いかなる地図も、隣接する領域が異なる色に
なるように塗るには4色あれば十分だという
定理
– 1976年に ケネス・アッペル (Kenneth Appel) とヴォ
ルフガング・ハーケン (Wolfgang Haken) はコン
ピュータを利用して、本定理を証明した。しかし、
あまりに複雑なプログラムのため他人による検証が
困難であることや、プログラム自体の誤りの可能性
を考慮して、この証明を疑問視する声があった。
36/39
利用例:
証明 powered by プログラム
• G. Gonthier,“A ComputerChecked Proof of the Four Color
Theorem”
–四色定理のコンピュータプログラ
ムを使った証明を、証明が書ける
言語「Coq」で全部書いた
–（Coqの型チェックが正しいと信頼
できるなら）確実に正しい証明
38/39
参考資料：証明支援言語の例
（検索用キーワード）
• 実装
– Agda
– Epigram
– Ωmega (Omega)
– Coq
– Isabelle/HOL
証明プログラムを
直接書く系
証明スクリプト系
• 理論
– Dependent Type
– Calculus of (Inductive) Construction
39/39
まとめ
• 「証明できる
プログラミング言語」
を使って、
今までは正しさを「証明」
できなかったような
巨大プログラムの正しさを
証明するのがブームです
© Copyright 2024 ExpyDoc
