PowerPoint

プログラム理論特論
第２回
亀山幸義
[email protected]
http://logic.is.tsukuba.ac.jp/~kam/progtheory
この授業の目的

プログラム言語の難しい理屈を知ること？


No
プログラムの「正しさ」を保証する技術の基礎
を理解すること

自動的な方法



型に基づく方法
モデル検査に基づく方法
対話的な方法（人間の手助けが必要）

記号論理による演繹的方法
「現実」のプログラム言語

C:



Java:




オーソドックスな言語
「細かい操作が何でもできる」が、かえって危ない（ポインタ操作など）
オブジェクト指向
細かい操作（危ない）操作はあまりできない
機械語レベルでの安全性検証つき
ML:



関数型
高度な「型」定義機構あり
関数型とはいえ通常の言語と同様な代入文等も書ける
プログラム言語の抽象化（理想化）


この授業での考察対象は、現実のプログラム言語
ではなく、抽象化したプログラム言語
利点


欠点


個別のプログラム言語の些細な違いにこだわることなく、
本質的な点のみに集中することができる
抽象化したプログラム言語での理屈（理論）を現実のプロ
グラム言語にそのまま適用することはできない
この授業では、「型付きλ計算」を採用
計算モデル：計算とはなにか？

計算機による操作である
Turing Machine
 Random Access Machine、多くのプログラム言語


関数である
ラムダ計算、Lisp/Scheme
 帰納的関数


推論（論理的思考）である


通信・コミュニケーションである


定理証明手続き、Prolog
並列計算モデル
DNA計算・自然計算、量子計算
ラムダ計算 (Lambda Calculus)

型のないラムダ計算と型付ラムダ計算がある

まず、型のないラムダ計算をとりあげる
Church, Curry 等がはじめた
 「関数」の概念を定式化したもの

関数呼び出しを表現する
 それ以外の概念は一切捨てる


変数への値の代入、制御構造、等
λ計算
ーInformal Introductionー
関数とは？

性質
いくつかの入力（引数）をもらって、出力（返り
値）を１つ返すもの：プログラムと共通する点
 同じ入力を与えれば、いつでも同じ出力が
返ってくる：プログラムとは必ずしも一致しない
点

関数とは？

次の関数を微分すると何になるか？






∫f(x)dx と ∫f(y)dy は「関数として」同じ


x3+5x+2
x3+ax+b
x3+yx+2
どの変数に着目するかによって結果が異なる
a, b がｘ、ｙに依存する変数だったら？
本当にそうか？
「関数」と呼ぶ以上、出力結果だけでなく、どの変
数が入力かを明示しなければおかしい。
λ記法

入力となる変数を「λ変数.」と記述する。


λx.x3+5x+2
「微分する」という操作をD であらわすと




λx.x+1 と λy.y+1 という関数は同じ
一方、λx. x-y と λy. x-y は違う
「積分する」という操作を Int であらわすと


D(λx.x3+5x+2) = λx. 3x2+5
Int (λx.f(x)）と Int(λy.f(y)) は同じ
λ記法を使うと、高階関数が簡単に書ける


引数や返り値として関数をとる関数
例：上のDやInt
λ記法（つづき）

関数に引数を食わせる
関数「λx.x3+5x+2」に、引数「３」を適用すると
答えとして４４が返ってくる
3
 (λx.x +5x+2)(3) を計算すると 44 になる。
 (λx.x3+5x+2)(3)
⇒ 44
3
 D(λx.x +5x+2)
⇒ λx. 3x2+5
 ((λx.(λy.x3+5x+y))(3))(5)
⇒ 47
 (λf.(λx. (f(x)+1))) (λy.y*2) ⇒
λx.(λy.y*2)(x)+1 ⇒ λx. x*2+1
 ((λf.(λx. (f(x)+1))) (λy.y*2)) (4)⇒ 9

形式的な記述

非形式的記述




構文や意味を厳密に定めない
われわれが通常とっている方法
厳密な議論には適さない（とくに、「○○を示すことができ
ない」ことを示すためには、議論の対象となっている仮定
や推論方法を厳密に決める必要がある）
形式化、形式的記述



誰が見てもただしさが納得できるように、使っている規則
や仮定を明示する
客観的に正しいかどうか判断できる
機械（コンピュータ）でも！
λ計算
ーFormal Introductionー
構文

変数


変数 x, y, … がある（無限個の変数がある）
文脈
変数の有限集合を文脈と呼び、Γ、Δ等であら
わす
 例： Γ＝｛x, y}


判断
Γ|- M:Λ と言う形の表現
 Γという文脈のもとで、項Mはλ式である
 項Mはλ式であり、その自由変数はΓである。

構文

項の構成規則
Γ|- M: Λ
Γ|-x : Λ
(x∈Γ)
Δ|- λx.M: Λ
Δ=Γ－{x}
Γ|- M: Λ Γ|- N: Λ
Γ|- MN: Λ
例題
Δ|- f : Λ Δ|- x : Λ
Δ|- f : Λ
Δ|- f x : Λ
Δ|- f (f x) : Λ
Γ|- λx. f (f x) : Λ
{}|- λf. λx. f (f x) : Λ
Γ={f}
Δ={f, x}
自由変数
同じMに対して、何通りものΓに対して、 Γ|M:Λ が証明できることがある
 そのような最小のΓを、「Mの自由変数の集
合」という。

例： λx. x+y の自由変数は y だけ
 例：（λx.x+y) + x の自由変数は x と y


自由でない変数（束縛変数）は、一斉に名前
をかえても「同じ」λ式である

例： λf. f(λy.fy) と λg. g(λx.gx) は同じ
意味論
構文を決める＝日本語の場合、どういう文字
列が「日本語の文」であるかを決める
 意味を決める＝それぞれの文がどう振舞うか
を決める
 意味論

操作的意味論 ←今回の講義で扱う
 公理的意味論 Hoare論理
 表示的意味論 Scott理論

操作的意味
計算規則を決めること
 計算規則

(λx. M) N ⇒ M [N/x]
 M⇒Nならば、C[M]⇒C[N]

操作的意味

代入
x[M/x] ≡ M
 y[M/x] ≡ y
 （λy.L)[M/x]
≡ λy. L[M/x] ではない！


(λy.L)[M/x]≡λz. (L[z/y][M/x])
ただし、z は x とは異なる変数で、かつ、
Mの自由変数でないもの
計算:例題
(λf. λx. f (f x))(λy. y+5)
⇒λx.(λy.y+5)((λy.y+5)x)
⇒λx.(λy.y+5)(x+5)
⇒λx.(x+5)+5
 (λf. λx. f (f x))(λy. y+x)
⇒λx.(λy.y+x)((λy.y+x)x)
⇒λx. (x+x)+x ???
 (λf. λx. f (f x))(λy. y+x)
⇒λz.(λy.y+x)((λy.y+x)z)
⇒λx. (x+z)+z

λ計算

特徴
Lisp, ML における関数呼び出しをsimulateす
ることができる
(define (foo x) (+ x 1)
foo≡λx. x+1
(foo (foo 3)) ⇒ 5
foo (foo 3)) ⇒5
(define (double f x) (f (f x)))
double≡λf.λx.f(fx)
(double foo 3) ⇒ 5
(double foo) 3 ⇒5
 非決定的な計算である

形式と意味
形式と意味

形式的 vs 意味的/内容的/実質的



前者：形だけ、目に見えるが内容を伴わない
後者：本質、目に見えない（ことが多い）が大事なもの
本当にそうか？




数学における「形式主義」（Hilbertのプログラム)
自然科学＝何らかの対象のモデル化、定式化から始ま
る学問
体系化された知識は何らかの形式をもって蓄えられるは
ず
計算機は形式的なデータを対象にしているが、意味は
扱えないのか？
形式的体系 (Formal System)

記号列の集合として定義


種々の概念を厳密に(客観的に、計算機により操
作可能な形で）定義する
帰納的定義
無限個の「もの」を有限的手段で定義
 例：自然数、リスト、二分木
 帰納法（例：自然数に対する数学的帰納法）

意味論 (Semantics)

形式的体系Fの(形式的）意味論とは、



数学的対象とは？



F から（別の）数学的対象への対応付け（写像）
ただし、F の構造を保つもの
特に定義はないが、「既に性質がよくわかっている数学的
対象」を選ぶことがおおい
例：プログラムの意味を、集合や関数で記述する
意味論は何の役に立つのか？


２つの（文面は異なる）計算機プログラムが同じであること
を示す
F の（表面に現れない）構造が見えてくる
記号論理における形式と意味

記号論理の形式的体系


「論理式」「証明」などの概念を、記号列の集合として帰納
的に定義したもの、あるいは
論理式や証明を導きだすゲームのルールを決めたもの




「A⊃A」という論理式がゲームのルールに従って導きだせるかど
うか？（証明可能かどうか？）という議論。
正しいとか誤っている、という議論ではない。
証明論：形式的証明の構造に関する理論
意味論

単なる記号列としての論理式等に、他の数学的対象を対
応つけたもの（e.g. 集合論、Turing機械）
参考書

以下の本の第１章

佐藤雅彦，桜井貴文「プログラムの基礎理
論」，岩波講座ソフトウェア科学１３，岩波
書店

Download Report