プログラム理論特論 第２回 亀山幸義 kam@is.tsukuba.ac.jp http://logic.is.tsukuba.ac.jp/~kam/progtheory

この授業の目的 プログラム言語の難しい理屈を知ること？ プログラムの「正しさ」を保証する技術の基礎を理解すること No 自動的な方法 型に基づく方法 モデル検査に基づく方法 対話的な方法（人間の手助けが必要） 記号論理による演繹的方法

「現実」のプログラム言語 C: Java: ML: オーソドックスな言語 「細かい操作が何でもできる」が、かえって危ない（ポインタ操作など） オブジェクト指向 細かい操作（危ない）操作はあまりできない 機械語レベルでの安全性検証つき 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　が　ｘ、ｙ　に依存する変数だったら？ ∫f(x)dx　と ∫f(y)dy　は「関数として」同じ 本当にそうか？ 「関数」と呼ぶ以上、出力結果だけでなく、どの変数が入力かを明示しなければおかしい。

λ記法 入力となる変数を 「λ変数.」 と記述する。 λ記法を使うと、高階関数が簡単に書ける λx.x3+5x+2 入力となる変数を　「λ変数.」　と記述する。 λx.x3+5x+2 「微分する」という操作をD　であらわすと D(λx.x3+5x+2) = λx. 3x2+5 λx.x+1 と　λy.y+1　という関数は同じ 一方、λx. x-y　と λy. x-y　は違う 「積分する」という操作を Int であらわすと Int (λx.f(x)）　と Int(λy.f(y))　は同じ λ記法を使うと、高階関数が簡単に書ける 引数や返り値として関数をとる関数 例：　上のDやInt

λ記法（つづき） 関数に引数を食わせる 関数「λx.x3+5x+2」に、引数「３」を適用すると答えとして４４が返ってくる D(λx.x3+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, … がある（無限個の変数がある） 変数の有限集合を文脈と呼び、Γ、Δ等であらわす Γ|- M:Λ　と言う形の表現 Γという文脈のもとで、項Mはλ式である 項Mはλ式であり、その自由変数はΓである。

構文 項の構成規則 Γ|- M: Λ Γ|- M: Λ Γ|- N: Λ Δ|- λx.M: Λ Γ|- MN: Λ Γ|-x : Λ

例題 Δ|- f : Λ Δ|- x : Λ Δ|- f : Λ Δ|- f x : Λ Γ={f} Δ={f, x}

自由変数 同じ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.(x+5)+5 (λf. λx. f (f x))(λy. y+x) ⇒λx.(λy.y+x)((λy.y+x)x) ⇒λx. (x+x)+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　の（表面に現れない）構造が見えてくる

記号論理における形式と意味 記号論理の形式的体系 意味論 「論理式」「証明」などの概念を、記号列の集合として帰納的に定義したもの、あるいは 論理式や証明を導きだすゲームのルールを決めたもの 「A⊃A」という論理式がゲームのルールに従って導きだせるかどうか？（証明可能かどうか？）という議論。 正しいとか誤っている、という議論ではない。 証明論：形式的証明の構造に関する理論 意味論 単なる記号列としての論理式等に、他の数学的対象を対応つけたもの　（e.g. 集合論、Turing機械）

参考書 以下の本の第１章 佐藤雅彦，桜井貴文「プログラムの基礎理論」，岩波講座ソフトウェア科学１３，岩波書店