言語モデル論

東大 小林研究室

プログラミング言語の基礎となる計算モデル、および意味論について学び、プログラムの挙動に関する厳密な推論やプログラミング言語およびその処理系の正しい設計を行えるようにする。

講義の前半はプログラミング言語の基本的な意味論を学び、後半ではλ計算を代表とする計算モデルおよび型システム等について学ぶ。

第1回：導入

第2回～6回：プログラミング言語の意味論（操作的意味論、表示的意味論、公理的意味論）

第7回～11回: λ計算と型システム

第12回～13回：その他の計算モデルとプログラミングパラダイム

途中で中間試験を行う場合もある。

第1,2講

c言語では代入文の値は左の値である。

人命に関わるソフトウェアがあるので性質を理解することが大事

構文と意味

・構文

正しいプログラムの構造を規定

・意味

文やプログラムが意味するものを規定

構文的に間違い

he ball a threw

意味的に間違い

a := n | X | a+a | a×a

ただし、a,n,Xはそれぞれ算術式、整数、変数を表すメタ変数

これは、aとは整数または変数または算術式の足し算または算術式の掛け算と読む

言語を定義するたために使う変数をメタ変数という

というのもその言語にも変数があるはずだから

文の導出過程を表す木構造を構文解析木という

+や×を木構造と考えると曖昧性は除かれる

ここからは抽象構文として進める

Ind(F)「F(S)がSに含まれるヲ満たす最小のS」

s :~ 0|1|0s|1s

F(S) = {0,1} U {0s|s含まれるS}U{1s|s含まれるS}

照明手法としての帰納法

定義から自動的に帰納法の原理が出てくる

木構造の性質を構造的帰納法を使って証明してみる

プログラミング言語の構文

-構文論と意味論

-構文の定義方法(BNF)

-構文解析木

-構文の抽象性

-抽象構文と具象構文

-構文定義の厳密な解釈(機能的定義)

構文論とは正しいプログラムの構造を規定し、意味論とは分野プログラムが意味するものを規定する

構文はBNFによって定義される

a::= n | X | a+a | a*a

a,n,Xはそれぞれ算術式、整数、変数を表すメタ変数

構文解析器は文の導出過程を表す木構造

同じ文に対して複数の構文木が存在する時を、構文の曖昧性という

具象構文：実際のプログラムの文面を定義、曖昧性のないように定義、構文解析や言語の構文定義にしよう

抽象構文：文がどのように構成されるかを定義、曖昧性があっても良い、プログラムの意味の定義にしよう

a1,a2,a3がSに含まれる「

第3講

・プログラミング言語の代表的な意味論

・言語IMPの操作的意味論

-算術式の操作的意味論

-ブール式、コマンド式の操作的意味

・操作的意味論の基づくプログラムの性質の推論の例

プログラミング言語の意味論の必要性

・プログラムが正しく動作することを証明するには？

・もしインタプリタやコンパイラによってプログラムの動作が違ったら？

・プログラムXの改良版Yを作った、XをYで置き換えても大丈夫？

プログラミング言語の代表的な意味論

・操作的意味論

プログラムがどのように評価されるべきかを定義

・表示的意味論

プログラムを入力から出力への数学的関数と捉え、意味を定義

・公理的意味論

プログラムがどのような性質を満たすべきかを定義

現在では、意味定義よりはプログラム検証への応用が中心

プログラミング言語Wの構文

算術式、ブール式、プログラム

算術式の評価

評価文脈のインストラクション（命令）

・評価文脈

穴の空いた算術式

穴が評価する場所を表す

・インストラクション

評価対象の算術式

評価文脈と命令の構文

評価規則

ブール式の評価文脈と命令

第4講

・前回の復習

・操作的意味に基づくプログラムの仕様の形式的記述

・プログラムの性質に関する推論

算術式の操作的意味

a::= n | X | a0+a1 | a0*a1

E::= [] | []+a | n+[] | []*a | n*[]

I::= X | n1+n2 | n1*n2

ブール式の評価文脈と命令

プログラムの評価規則

プログラムの評価例

ーーここまで復習ーー

プログラムと仕様

第5講

・前回までの復習

・ホーア理論（公理的意味論）

-プログラムの正しさの証明をより機械的に行えるように

つまり、コンピュータによる自動または半自動検証

プログラム言語IMPの構文

算術式

ブール式

プログラム

プログラムの評価文脈と命令

プログラムの評価規則

プログラムの仕様の典型的な形

完全正統性 ＝　部分正当性 + 停止性

プログラムの正しさの証明技法

・ループの不変条件

・ループ変動式

プログラムの正しさの推論例

ホーア理論

ホーア理論とは？

・プログラムが満たすべき性質を推論規則の形で表したもの

・プログラムの正しさの機械的検証の有効

部分正当性と完全正当性

・部分正当性

「Aを満たす状態の下でcを実行するとプログラムが停止するならば終了状態はBを満たす」

・完全正当性

「Aを満たす条件のもとでcを実行すると、プログラムが停止し、終了状態はBを満たす」

例：部分正当性と完全正当性

Exercise

以下の性質を部分紫衣統制または完全正統性の表明を用いて表せ

部分正統性の推論規則(1)~(5)

プログラム全体の規則はプログラム個々の規則から導かれる

これらの推論規則はフローチャートを思い浮かべれば余裕で思いつける

推論例

完全正当性のための規則

while分だけが停止しない可能性があるので、while文の規則を少し変えればok

ホーア論理の健全性と完全性

ホーア理論は本当に正しいのか？

|-は、ホーア論理の規則から導けるということ

|=は、意味的に正しい（Aを満たす初期状態のもとでcを実行すると終了状態が存在するならばBを満たす）

健全性：|-{A}c{B}ならば|={A}c{B}

（相対）完全性 |={A}c{B}ならば|-{A}c{B}

結論から言うと、この２つはどちらも成り立つ

議論は次回に回す

第6講

・前回の復習

ーホーア理論

ー健全性と相対完全性

・ホーア理論の相対完全性の証明の概略

・ホーア理論に基づく半自動プログラム検証

{A}c{B}の完全な公理化は可能か？

答えNo

ホーア理論の健全性

証明は黒板で

ホーア理論の相対完全性の証明の概略

最弱事前条件が証明で活躍する

第７講

相対完全性の鍵となるのが最弱事前条件

最弱事前条件に基づく全自動プログラム検証？

自動定理証明器さえあれば、プログラムの全自動検証が可能！

現実には線形可能性の壁

完全な全自動定理証明器は原理的に存在しない（ゲーデルの不完全性定理）

ホーア論理に基づくプログラムの半自動検証

注釈付きプログラム⇨Verification Condition generator⇨検証条件⇨定理証明器

表示的意味論

・プログラムを数学的な関数とみなす

-while言語の場合

算術式：状態を整数に対応づける関数

ブール式：状態をブール値に対応づける関数

プログラム：初期状態を終了状態に対応づける部分関数

・各式の意味は、部分式の意味から定まる

関数のラムダ記法

f(x) = e

によって定義される関数fを

λx.e

と書く

表示的意味論まとめ

・プログラムの意味は数学的な関数

・意味を合成的に定義

・ループや再帰の意味はそれに付随する再帰方程式の最小解として定まる

・言語によってプログラムの意味を解釈する領域自体が再帰的に定まる

第8回

while文の意味再考

nまでとして、nを無限大にすることで元のwhile文の意味になる

表示的意味論

・プログラムの意味は数学的な関数

・各式の意味は部分式の意味から定める

・ループや再帰のの意味は、それに付随する再帰方程式の最小解として定まる

おまけ

cpo(complete partial order)

・表示的意味論の意味領域としてよく用いられる

・半獣じょ集合のうち、以下の条件を満たすもの

ー最小元が存在

ー任意の無限単調増加列が最小上界を持つ

cpo上の函数の単調性と連続性

cpoと表示的意味

・表示的意味論では、「」は通常止まらないプログラムの一身を表す

・プログラムとしての関数の意味は、cpo状の連続函数として与えられる

・再帰函数 f=F(f)の意味は、連続函数Fの最小不動店として与えられる

ラムダ計算とは？

・関数だけからなる計算モデル

（計算可能な関数を全て表現可能 cf. チャーチ-チューリングの提唱）

・チューリング機械と同等の表現力

・近代的プログラミング言語の基礎（特に関数型プログラミング言語）

・型の概念を加えると、論理学とも密接な対応

(cf. カリー-ハワード同型対応)

ラムダ式の構文

M := x | λx.M | M1M2

変数、λ抽象、適用

記法状の約束

・関数適用は左結合

・λ中小の範囲はなるべく広くとる

計算（β簡約）規則

代入について

λxのxは、外から来た変数のメタ変数なので、代入は施さない

自分にとって一番左側のラムダの参照する

携帯の写メ参照

代入するときは、必要に応じて変数名を付け替える

これをα変換という

第9講

ラムダ計算とは

関数だけからなる計算モデル

チューリング機械と同等の表現力

近代的プログラミング言語の基礎

型の概念を加えると論理学とも密接な対応

計算（β簡約）規則

代入のようなもの

η簡約

同じ関数について

ブール値の演算の表現

自然数の表現

足し算、掛け算、冪乗

mult = λmλn.λs.n(m s)

exp = λm.λn.n m

plus = λm.λn.λs.λz n s(m s z)

ゼロ判定

組

基本データを組み合わせた複雑なデータを表現するのに使用

複素数は実部と虚部を表す実数の組として表現可能

整数は自然数と符号の組として表現可能

組みを使って前者関数を作る→引き算を定義する

schemeという関数型言語を使ってエンコードしてみる

再帰関数と不動点

第10講

ラムダ計算は代入と関数だけでチューリングマシン

チャーチ・ロッサーの定理

正規系の一意性

ダイヤモンド性→チャーチロッサー→弱合流性

ただしこれは必要条件である

授業めも２

第１章 はじめに

コンピュータの指令書がプログラムであり、その誤動作は、人命や財産、機密情報の流出などの重大な事態に直結する。本書では、プログラムに対して数学的な意味を与えることによりプログラムの動作についての厳密な議論を可能にする

構成的プログラミングと呼ばれるプログラム構成手法では、プログラミングは数学の定理を厳密に書き下す作業と等価である

第2章 数学の予備知識

集合や論理の基本概念の理解は必須である。

2.1 論理式

2.2 集合

コラム：集合の濃度と計算可能性

コンピュータのプログラムによって計算できるものに限界はないのか、というのはコンピュータサイエンスの根幹に関わる重要な問題であるが、答えは限界はある。

これは集合の濃度の議論からでも知ることができる

計算不可能な問題には、コンピュータサイエンスや数学にとって重要な問題が含まれていることが知られている

・停止性問題：プログラムpとその入力xが与えられたときp(x)が停止するか否か

・ディオファンティん方程式の可解問題：整数係数の多変数多項式からなる方程式が与えられた時にその整数解が存在するか否か

第3章 プログラミング言語の構文

プログラミング言語においては、構文をを解釈するフェーズと意味を解釈するフェーズがある。

3.1 BNFによる構文の定義

3.2 構文解析木と文法の曖昧性

文の構造は構文定義に従って構成される構文解析木によって表現することができる

3.3 具象構文と抽象構文

プログラミング言語の構文と意味論を定義する際には二種類の構文を使い分ける。

具象構文は、曖昧性がなく、かっこや演算子間の優先順位などを明確にした構文である

一方、本質的でない部分を省略して単純化した抽象構文も存在する

3.4 構文解析

インタプリタやコンパイラなどのプログラム評価器、プログラム変換器では、まず文字列としてプログラムを受けとり、構文解析器を内部で生成する。この処理を構文解析という。さらに、構文解析の処理は、字句解析と構文解析の２つに細分される

3.5 言語Wの構文

言語WはC言語などの命令型プログラミング言語を単純化したもので、プログラムは有限個の変数に値を保持しながら条件分岐やwhile文による繰り返しにより計算を行う

3.6 帰納的定義

前節でBNFを用いて定義したプログラムの集合は無限集合である。無限集合を定義する際に頻繁に用いられる定義の仕方として帰納的定義があり、実はBNFによる定義は帰納的定義の一種と考えることができる

本節では、集合の帰納的定義とそれに付随する帰納法による証明原理について解説する

第4章 操作的意味論

プログラムの動作について数学的に厳密な議論を行うためには、プログラムの意味が明確に定義されていなければならない

プログラムの意味を定義する代表的な流儀として、操作的意味論、表示的意味論、公理的意味論がある

4.1 算術式の評価規則

4.2 ブール式の評価規則

4.3 プログラムの評価規則

第5章 プログラムの性質に関する推論

4章で用いた意味論に基づき、実際にプログラムの仕様を論理式を用いて記述し、プログラムがその仕様を満たすことを証明できることを確認する

5.1 プログラムの仕様に関する説明

5.2 プログラムの正当性の証明

前節のように、仕様を論理式として記述すれば、プログラムが仕様を満たすことを数学的に証明することができる

5.3 ループ不変条件とループ変動式

while文のような繰り返し構造を持つプログラムの部分正当性や低姿勢を議論する際には以下で述べるようなループ不変条件やループ変動式に着目すると便利である

第6章 ホーア理論

5章において、プログラムが期待通りの動作をすることを操作的意味に基づいて厳密に検証する方法を学んだ

本章では、プログラムが与えられた性質を満たすことを機械的に導くための推論体系を与える

この推論体系のことを、フロイト・ホーア理論という

このホーア理論を用いると、プログラムの正しさをコンピュータを用いて半自動的に検証することができる

推論規則群がプログラムが満たすべき性質を定めていると考えることもできることから、公理的意味論とも呼ばれる

6.1 ホーア理論の表明

6.2 部分正当性の推論規則

6.3 ホーア理論の健全性と相対完全性

6.4 プログラムの半自動検証へのホーア論理の応用

6.5 完全正当性のための推論規則

第7章 表示的意味論

本章では、言語Wの表示的意味論を与える。表示的意味論では、プログラムの各構成要素を数学的な関数とみなす。

7.1 算術式の表示的意味

7.2 ブール式の表示的意味

7.3 プログラムの意味

第8章 ラムダ計算

前章までは、制御構造がif文とwhile文だけからなる単純なプログラミング言語を考えてきたが、実際のプログラミング言語には再帰関数、高階関数、オブジェクトなど、より高レベルな機能が備わっている

本章では、そのような高レベルプログラミング言語の基本モデルとして使われることの多いλ計算を取り上げる

現在では、コンピュータサイエンスにおいて計算可能性の議論やプログラミング言語の基本モデルなどとして極めて重要な役割を果たしている

8.1 構文

λ計算の特徴は、関数のみからなる極めて簡潔な計算系を記述しながらも豊かな表現力を持つことにある

記法に関する約束事

適用は左結合である

λ抽象よりも適用の方が結合力が強い

8.2 代入と簡約

λ計算における計算を表す簡約の概念を定義する

λ計算は関数のみから成っている体系なのでm計算は関数呼び出し、すなわち関数適用が与えられたときに、関数の本体M中の仮引数xを実引数Nで置き換える操作、が基本となる計算ステップでありこれをβ簡約という

代入の対象となるのは自由変数のみ

N中に自由変数がある時にはそれがM中の束縛変数と混同されないようにしなければならない

η簡約

8.3 ラムダ計算の表現力

本節では、変数、λ抽象、適用というたった３つのプリミティブしか持たないλ計算がプログラミング言語として十分な表現能力を持つことを確認する

基本データの表現

ブール値や自然数などの基本データは関数として表現することができる

集合や自然数の集合の要素は有限個の構成子から構築することができるので、各値をそれらの構成子供を受け取って対応する値を返す関数として表現することである

8.4 簡約戦略と関数型言語

純粋なλ計算では任意のβ簡約基の簡約を許すため、簡約の仕方に非決定性があるが、逐次プログラミング言語では、通常一定の簡約戦略に従って決定的な簡約が行われる

幸いなことに、正規系が存在すれば必ずそれに辿りつけるような簡約戦略が知られており、それを最左戦略という