論理とプログラム２００７年度

Moodelに進み具合いを記録しておきます。出席できない人は
参考にしてください。

講義要項

この科目は基礎から始めますが、理解を助けるのは、「集合と論理」の基本です。
上記HPの他に、集合と論理の基礎としては、「情報系の数学入門」（林・八杉著、 オーム社）
　 があり、図書館に入っています。科目「集合と論理」を履修した人は、その教科 書です。
論理の基礎がやさしく書いてある資料については、 「集合と論理２００７」を参照のこと。
また、なぜ論理が必要なの？についてもこれを参照してください。

ほかに参考になるページには、次のようなものがあります。

抽象化の技法（2002年度） および論理とプログラム2001

京都大学 高崎金久先生の論理学のページ
論理学一般についての講義内容が公開されています。高崎先生の
許可を得ていますので、参考にしてください。ただし無断引用
は厳禁です。あくまでも理解を助けるための参考です。

＜お話・数学基礎論＞論理や集合について楽しく学べる
図書館に入っています。
ここに説明あり

2003年度卒業研究
興味のある人は知らせてください。

レポートは、Moodleで行います。
その説明は後でします。
レポートを課する理由の一つは、皆さんの勉強の指針になることです。
課題をあわててするのでなく、関連することをゆっくり勉強してから
とりかかってください。答そのものでなければ関連する質問にも答えます。

(ii) こちらはそれぞれの人に対して、その人が好きな花があるので、
∀x:Human∃y: Flower・Likes(x,y)
となります。

この二つを比べて量記号の使い方の本質を学んでください。
(i)は∃が最初にあるので、∀xの x に依存しないで y がある、ということを表 しています。
(ii) は∀が先にあるので、それぞれの x に対して　y が存在する、したがって
y は x によって異なるかもしれません。

次の集合を定義してください。 （集合の名前は各自つけていいです。）

1. あなたの好きな食べ物の集合。

（個数は５以上、１０以下。表記は日本語でもローマ字でも英語でもいい。）

2. 関数　y=√(x^2 - 2) の関数値の集合。ただし、実数から実数への関数とす る。
（√(x^2 - 2) は(x^2 -2)のルート　を現す。なお、√は　るーと　と入力して 変換する。
また、関数の定義域に注意。）

解答：

1. 例：　{とうがらし、ねぎ、にんじん、とうふ、いわし、さんま}

2. 表記法の例：　{y:R|∃x:R(y=√(x^2 -2)}；　 {√(x^2-2), x:R | x^2 >=2}

前回の関数のグラフ（平面上の点集合） G_f を定義してください。
すなわち、 G_f は実数値関数　y=f(x)=√(x^2 - 2) のグラフ上の点
(x,y) の集合です。 （書き方はいろいろあります。）

解答：

G_f == {(x, √(x^2 - 2)), x:R|　x^2≧2・} 　または　 G_f == {z:RxR| ∃x:R∃y:R(y=√(x^2 - 2))∧z=(x,y))}

関数のグラフについて理解していない人が多かったです。
「集合と論理」（情報系の数学入門の第一章）に正確に書いてあるので
読み直してください。一般に関数 f のグラフは入力値と関数値の対で 表します。
とくに今は型を重視しているので、それらの値の型を明記します。
実数から実数への関数とすると
G_f == {x:R| "xについての制限" ・(x,f(x))}, G_f == {x:R, y:R| "xについ ての制限"・(x,y)}
などと表記します。ちなみにG_f の型はP(RxR)です。

　 daVinch== {Anna, Bianca, Leonardo}, Hobby == {painting, singing, dancing}
　　　[daVinch, Hobby] とする。すなわち、daVinch家の人々の名前の集合と趣 味の
　　　集合を基本型とする。daVinch家の人々はそれぞれHobbyの要素である趣味 を
　　　もち、しかも互いに重ならないとする。

問題： 上の条件のもとで、daVinch家の各人とHobbyの趣味の関係を作成し、
　　　　その型を示してください。（各自好きなように対応を考えてください。
　　　　また、名前等をすべて書かなくてもイニシャルだけでよい。）

解答：　問題の関係をたとえば　Shumi　とおくと、
Shumi == {A |->s, B |->d, L |->p}
Shumi: daVinch ←→　Hobby

注意：　 「A |-> s」は関係　Shumi をとくに写像とみなすときに　A に　s が対応する
ということを表す。「人々と趣味の対応が重ならない」という題意から、
Shumi は写像（実際には関数）とみなしている。Shumi の型は
P(daBinch x Hobby) であるが、とくに　この場合には関係と見なして
いるので、上のように書く。

例：「この箱の中のみかんはみんなおいしいよ」
この文を分析すると、「すべての物について、それがこの箱の中に入っていて、
それがみかんならば、それはおいしい」となる。三カ所に現れる
「それ」はべて同じ個体をさす。（ただし特定の個体ではない。）
この文を述語論理の論理式で書いてみよう。「x がこの箱に入っている」を
Box(x)、「x がみかんである」を Mikan(x)、
「x がおいしい」をDelicious(x)とおくと、
"turn A"x(Box(x) and Mikan(x)=>Delicious(x))

例：「この箱の中には大きいみかんがあるよ」
上の文と同様の定義をする。とくに 「x が大きい」をLarge(x)とおく。
この文を分析すると、
「ある物があって、それはこの箱に入っていて、それはみかんで、それは
おいしい」となる。したがって論理式は
"turn E"x(Box(x) and Mikan(x) and Delicious(x))

多少意味のはっきりしない文章もあります。自分ではっきりした文章に
解釈してください。また、論理式は一通りではありません。人によって ちがっていいのです。

お知らせ：6月22日（水）12号館で大学院の説明会が
あります。詳しくは掲示（貼紙もあり、POSTにもある）を見てください。
３年生も歓迎です。とくに大学院進学を決めていなくても
様子を見にきてください。

論理式に意味を与えるためには 1. 変数がとる値の集合、2. 述語記号が
表す関係（または性質）、の二点を決める。これを「論理式の解釈」という。
関数記号がある場合にはそれが表す関数を決める。
論理式の意味を考えることを「意味論」という。
どんな解釈でも真になる式を恒真、どんな解釈でも偽になる式を矛盾、適当に 解釈すれば真になる式を充足可能という。
命題論理の論理式の形をした恒真、充足可能、矛盾、は述語論理でも同じ 性質をもつ。
述語論理特有の恒真な式の例：(forall x)(P(x)=>(exists y)P(y))
矛盾の例：(exists x)(P(x) and (forall y) notP(y))

次の論理式　（A と呼ぶ）　について以下の問に答えてください。
∀x:X・P(x)⇒∃y:Y(Q(x,y)∧¬P(y)∧Q(z,y))
ただし z:Z が別途宣言されているものとする。

問題：　 １．　∃y　の有効範囲にある論理記号（命題結合子）と
　　　述語記号のそれぞれについて、出現回数を書いてください。
　（例：　P は１。　　解答ではP は不要）

２．　変数のうち、A　で束縛されているもの、自由なものは 　　　どれですか？
　（変数の名称、すなわち文字のみでよい。回数、出現場所、等は不要）

解答：　1. Q 　２回；　　∧　２回；　否定　１回
2. 束縛されているもの　x, y ；　　自由なもの　　z

そのニ：真と偽があるのに恒真と言いきれるもの（論理式）があるのか？
例　(forall x)(P(x)=>(exists y)P(y)); A or notA

その三：「人は誰でも誰かを愛するが、愛する相手が自分を愛しているとは 限らない」
これを表す論理式の成り立ちがわからない。
まずこの文章は二つの文章を「かつ」で結んでいる。
「人はだれでも誰かを愛する」（これをAとおく）
「愛する相手が自分を愛しているとは限らない」（これをBとおく）
A：ここで必要なのは「・・・は人である」と「・・・は＊＊＊を愛する」である
・・・や＊＊＊を変数x,yなどで表す。「x は人である」を H(x)、「x は y を愛する」\
をL(x,y)とおく。「人は誰でも」は 「どんな x についても x が人ならば」という
意味だから、(forall x)(H(x)=>...)。「x が誰かを愛する」は、誰か、とは人の
ことだから、(exists y)(H(y) and ***)となる。***は「x が y を愛する」だから
L(x,y)。...にこれ全体をいれると
(forall x)(H(x)=>(exists y)(H(y) and L(x,y)))
B：これは「愛する相手が自分を愛する」を否定している。それで最後に not を
つけることにして、「・・・」の部分を論理式にする。
自分と相手と２種類の人がいるので、前者を x 、後者を y とおく。
「・・・」は「x が y を愛するならば、y が x を愛する」（これをCとおく）
ということである。 x も y も人であることが要請されているので、C
の前提に「x が人で、y が人である」を加える。ここで x も y も誰でよいので
「すべての x とすべての y について」である。したがって全体は
(forall x)(forall y)(H(x) and H(y) and L(x,y)=>L(y,x))であり、これ全体の
前に not をつければできあがり！

その四：forall や exists の使い方がよくわからない。
このことに限りませんが、まずテキストをじっくり読んでください。
次にノートで該当するところをじっくり読んでください。
そうして理解したら同じことをテキストを見ないで自分で考え直してください。
なにごとも自分で時間をかけて、手を動かして（文字通り手間隙かけて）
勉強する以外に最終的に理解することはできないのです。
その上で、具体的な疑問があれば質問してください。

述語論理の論理式に意味を与える（解釈する）、とは
(1) 変数が値をとる範囲（変数が走る集合）を決める。
(2) 述語記号に、その集合上で意味を与える。
(3) 関数記号がある場合には、その集合上の関数を当てはめる。

例： ∀x∃yA(y,x)
解釈その1 (1) 「人々」の集合で考える。
(2) A(y,x) は、「祖先関係」とする、すなわち、A(x,y)は「y は x の祖先であ る」
を表すとする。このとき上の論理式は「だれにても祖先がいる」と読める。
解釈その2 (1) 「実数」の集合で考える。
(2) A(y,x) は y このとき上の論理式は「どの実数についても、それより大きい実数がある」 と解釈される。

次の論理式に各自意味を与えてください。

∀x:A・(P(x)⇒∃y:B・Q(x,y)∨R(y,x))

手順は、AとBに型としての意味を与える。
述語記号　P(x) ,Q(x,y), R(y,x)　にそれぞれ意味を与える。
全体を日本語で表現する。

解答例
A：Potters （Potter家の人々の集合）、B: 楽器
P(x)：xが女性である、 Q(x,y)：xはyを演奏できる
R(y,x)：　yはxの興味をそそる
論理式に意味を与える（解釈する）と：
Potter家の女性は（誰でも）ある楽器を演奏するか、（その）楽器が
その人の興味をそそる。

注：自然な表現にしようとしすぎて、もとの論理式とは全く
意味のちがう解釈をした人が多かったです。
それぞれの論理結合子と量記号の意味をよく考えて
それらに忠実に解釈すれば、自然に正しい表現になります。
大事なことなので、次回にもっと簡単な論理式の意味を問う
問題を出します。

　次の文章(a), (b) を、述語論理の論理式で表現せよ。

(a) 「この図書館の本はすべて貸し出し可能です。」
(b) 「この図書館の登録者ならば誰にでも
この図書館の本で面白いと思うものがありますよ。」

（「xが本である」をCopy(x)、「xがこの図書館にある」を
In(x)、「xは貸し出し可能である」をIssue(x)、「yはこの図書館の
登録者である」をRegis(y)、「yはxを面白いと思う」を
Int(y,x)として表現する。）

１．次の論理式に意味を与えてください。
　　∀x:A・(P(x)⇒∃y:B・Q(x,y))
２．　次の論理式の冠頭標準形を求めてください。 　　　 ∀xP(x)⇒∃yQ(y)∧¬∃zR(z)

解答

1. 解答例：　A: 猫（の集合）、　B: 魚（の集合）、　P(x): xはこどもである、 Q(x,y): x は y を好き
「子猫は（みんな）何か魚が好きである」

注：　今回は皆さんよくできていました。本質はわかっているのですね。
面白い解釈がいろいろあって、楽しませていただきました。
とくに、「情けは人（他人）のためならず」！格言も書けるのですね。
では「犬も歩けば棒に当たる」はどうでしょう？

2. 変形の順序はいろいろあっていいのです。以下は一例です。
∀xP(x)⇒∃yQ(y)∧¬∃zR(z)
∀xP(x)⇒∃yQ(y)∧∀z¬R(z)
∀xP(x)⇒∃y∀z(Q(y)∧¬R(z))
∃x(P(x)⇒∃y∀z(Q(y)∧¬R(z)))
∃x∃y∀z(P(x)⇒(Q(y)∧¬R(z)))

注：　途中のプロセスを少し省略しました。また、∃x∃y∀zの順序は自由です。
ただし、それは冠頭標準形を作るときに限ります。一般には∀と∃の順序は非常 に
大事です。このことを混同しないでください。

成績評価基準：課題/期末試験　の割合を　20/80 にします。

例：変形回文の再帰構造 ＜A＞::= aa|bb|a＜A＞a|b＜A＞b

再帰的定義 l(aa)=l(bb)=2; l(a＜A＞a)=l(b＜A＞b)=l(＜A＞)+2

構造帰納法 P(＜A＞): 「l(＜A＞)は偶数」とするとき、すべての＜A＞について
が成り立つことを示す。
1. l(aa)=l(bb)=2 は偶数。
2. l(＜A＞)が偶数とするとき、l(a＜A＞a)=l(b＜A＞b)=l(＜A＞)+2は偶数。
ゆえに、すべての＜A＞についてl(＜A＞)は偶数。

同様に、「すべての＜A＞が実際に回文である」を示せ。

重みをつける w(aa)=w(bb)=1; w(a＜A＞a)=w(b＜A＞b)=w(＜A＞)+1
w(＜A＞)=nとして、nに関する数学的帰納法で 「すべての＜A＞が実際に回文である」を示せ。

計算帰納法 m(x,2)=x*2 が偶数であることを示す。
m(x,2)=m(x-1,2)+2 = m(x-2,2)+2+2 =... m(0,2)+2+2...+2.
計算が進んで、最後にm(0,2)=0が直接計算できる。
上の等式から命題が示される。

今日の演習問題：(1) ¬と∧からつくられる論理式の再帰的構造を定義せよ。
この構造について、次のことを実行せよ。
(2) 各論理式 G に現れる論理結合子の個数 λ(G)を定義せよ。 （再帰的定義）
(3) 各論理式 G に対してその真理値 v(G) を定義せよ。 （再帰的定義）
(4) すべての論理式 G に対して、T,Fの丁度一つの真理値が決まることを 示せ。（構造帰納法、または、重みによる帰納法）

この課題について過去にあった質問と、その回答を書いておきます。
何をどう示すのか？（かっこの中のコメントの解説）
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
答え 構造帰納法を使うのは、Aの構造にしたがって、Bを定義
（構成）できることを示すことです。Aが変数の場合はそのまま、
Aが論理記号を使って作られている場合は、その論理記号と帰納法の
仮定からnotとandに書き換えられることを示します。
そのように書き換えても真理値が変わらないことは、テキ
ストや 講義にあった命題を使っていいのです。いちいち真理値の計算
を する必要はありません。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

論理式 A と B の X と Y は、命題変数を変えたほうがいいので しょうか？
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
答え いいえ、命題変数は同じにしてください。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

「A の構成における最後の論理結合子についての場合わけに よる。」とはどういう事なのか。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
答え 最初の質問の答えでも触れましたが、たとえばAが F and G の形
ならば、FとG に関する帰納法の仮定を使えばそのままですね。
もしAが F or G ならば、or はBの中に現れては困るので、and とnotで
書き換えなければなりません。
このように論理結合子によって扱いがちがう、ということです。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

（１）　再帰的構造を一つ述べて（定義して）ください。（２点）
解答：　例１　回文　例２　論理式　例３　数式　（a,b,...は式；
x,y が式ならば x+y, x*y は式）　例４　∧と∨から作られる論理式　　
これをP-論理式と呼ぼう。（命題変数　X, Y, ... はP-論理式；A, B が
P-論理式ならば、A∧B と　A∨B　もP-論理式）

関数の再帰的定義は、ちょっとちがう。それがある性質をもつ個体の
集合を定義していないからである。しかしたとえば
自然数の中で　f(0)=2; f(n+1)=f(n)*2+1 で定義される関数 f の
値を集めたものは再帰的構造といえる。それを　f-数とよぶと
２はf-数；　ｘ　がｆ−数ならば、ｘ＊２＋１はｆ−数

（２）　m(x,y)=x*y のとき、p(x,y)=y^x を再帰関数として定義してください。 （３点）
(x,y=1,2,3,...) p(1,y)=y; p(x+1,y)=m(p(x,y),y).（ここまでできていれば
とりあえず合格。できれば p(x,y)=if x=1 then y else m(p(x-1,y),y) fi
と書いてほしかった。

ちょっと失敗しても、点数は少ないのであまり心配しないでください。
でも、「塵もつもれば山」ですから、課題は必ず提出してください。
欠席と０点は意味がちがいます。
この解答をよく理解して、後に備えてください。

その一：再帰的関数の（５）と（６）がよくわからない。
定義の読み方を書きます。
(5) f[x_,y_] := If[x=0,h[x,y],g[f[x-1,y],x,y]]
x,y は入力値です。x=0のとき、h[0,y]を出力（つまりf[0,y]の値はh[0,y]）。
x>0のとき（つまりx=0でないとき）、f[x,y]の値は g[f[x-1,y],x,y]である。
すなわちf[x,y]の計算をf[x-1,y]の計算に「帰着」させる。こうしてx-1,x-2,...
とxの値を小さくしていってしまいに 0 のときに直接h[0,y]の値を得る。それを使って,\ br> 逆にf[1,y],f[2,y],...,f[x-1,y],を計算していき、最後にf[x,y]を得る。
これはMathematicaの再帰的定義(recursion)（計算）の一つの形と全く同じ。
(6) f[x_,y_] := If[g[x,y]=0,y,f[x,y+1]]
g[x,y]の値が0になる、y以上の最小のyの値を求める。g[x,y]=０ならば、出力はy、
そうでなければ次はゼロになるかもしれない、という期待でf[x,y+1]を計算しようとす\\ る。
(6)の定義をf[x,y+1]にあてはめると、
f[x,y+1]=If[g[x,y+1]=0, y+1,f[x,y+2]]となる。もしg[s,y+1]=0ならば答えはy+1,
そうでなければy+2を試す。こうしてどこかでg[x,z]=0となれば、その最初のzが答え。
実際にはg[x,z]が決してゼロにならなければ計算はいつまでも続くが答えは出ない。

第二回課題を出します。６月３日公開、６月１８日締め切り です。
出題範囲は、述語論理（３・６全体）です。

関数（プログラム）の停止性について
pp.136-138[5],[6]（述語論理の意味論とその例題）

プログラムに入力した場合、計算が進む（計算機が走って、 計算が続く）、すなわち文法的に正しいプログラムであり、 また入力も正しく、有限ステップ以内で計算が終り、答が 出力される。このときその関数（プログラム）は（正しく動き） 停止する、という。プログラムが正しく動くが、いつまでも止まらず 計算しつづけるとき、停止しない、という。プログラムに関して 計算が進むか、出力の答が期待したものであるか、という正当性と ともに、計算が停止するか（停止性）という問題はソフトウエア科学で 大きな課題である。

２００１年度のページの最後のほうに「レポートの解答はここ」 というのがある。この解答を参考にするとよい。

訂正

問題１の小問に（２）が二つあることを指摘されました。うっかりミスです。
最初の（２）は削除してください。したがって（１）には「論理式の再帰的定義」
（これを(a)とする）と、「真理値の定義と構造帰納法」（これを(b)とする）の
二つの問題があります。

命題論理の体系Pで証明可能な論理式は恒真である。（健全性）
証明可能な命題論理の論理式は体系Pで証明可能である。（完全性）

演習問題 p.118の各公理の恒真性を示せ。（真理値表を使うか、
和積標準形を使う）

本日の配布物：証明に関する補題（2枚）

λ計算系と命題論理の体系
資料はここ
抽象的なプログラム体系の定義。ただし「型」の入力ミスがある。
プログラムの定義の5)で、σとτが逆になってます。

解答　問題の項を t とおく。　項の変化を-->で表す。
1. t --> (fun x.snd＜e_1,x＞)(e_3) --> (fun x.x)(e_3) --> e_3
2. t --> x
3. t --> (fun v.((fun u.u)(x)))(e) --> (fun v.x)(e) --> x
計算順序は一意的ではないので、各自好きな順に計算してよい。最後の
正規形はどのようにしても同じところに行き着く。

1. 出題範囲：　述語論理の論理式（文章を論理式で表す）;　
述語論理の公理と推論（ある具体的な証明に使われる公理・推論）；
ラムダ計算系の項の計算
プログラム検証について１０行くらいで述べる。
注：　再帰的構造、いろいろな帰納法からは出題しない。

2. 配点：　課題/期末試験　=　20/80

3. 　持込物：　なし

4. 程度：課題や演習問題と大体同じ程度。課題の正解をよく理解したおくこと。
過去の問題のファイルがこのページにあるので、その中の、出題範囲に相当する 問題を
解いてみるとよい。基本的には、このページ、教科書、ノート、プリント、など をていねいに
読んでおけばできると思う。

参考書：「プログラム検証論」、林晋著共立出版）
（この本は図書館に入れてあります。）

7月17日（木） 3pm->3:40pm
この時間帯に都合つかない場合にはメールで連絡くささい。
yasugi@cc

(1) x:α, y:β　のとき、次の各項の型は何か？
　　＜x,y＞, snd＜x,y＞, fst＜snd＜x,y＞,y＞, λy.fst＜snd＜x,y＞,y＞
答えは、この順に：αx β, β, β, β→β

(2) 項　(λy.fst＜snd＜x,y＞,y＞)＜x,x＞ を計算せよ。（途中経過をすべて 記述せよ。)
例：　(λy.fst＜snd＜x,y>,y＞)＜x,x＞==> (λy.fst＜y,y＞)＜x,x＞==> (λ y. y)＜x,x＞ ==>＜x,x＞ 途中計算はいろいろな順序がある。しかし最終的に行き着くのは＜x,x＞である。