抽象化の技法２００２

数理論理学（林晋著、コロナ社）

２ 冠頭標準形と恒真性判定

まとめ

３ ９８年度八杉特研卒業研究論文 （布施田敏樹）

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

講義要項にそって講義を進めます。
テーマはいくつかあります。どれもプログラミング科学の基礎に
なるものであり、できるだけ「使える」技術を目標にします。
つまり観念論ではありません。
要点は印刷して配布しますが、詳しい説明は授業中にしっかり聞いておいて ください。
配布物はこのページも貼ってあるので、無くしたりもらい損ねたときに みてください。

１０月１日：まずは冠頭標準形から。 その１

述語論理の任意の論理式 A について、 A と同等な（意味が同じな）
論理式 A^p を構成する規則が与えられる。A^p は限量子がすべて
一番外に並んでいて、それらの中は命題論理の論理式になっている。
変形規則は各論理結合子について定義される。
今日は変形規則と標準形作成の演習。
問題 1. の３番目の式の変形を来週までに書いて提出すれば
みてあげます。（最後に多少成績に加算できます。）

質問用紙を渡すので、随時質問を書いてもってきてください。
用紙が必要になったら申し出てください。
もちろん講義の最中や後やほかのときにも質問してください。

Education Support System （課題出題・提出システム）というのがあります。
これを使って課題提出、評価をしてみたいと思います。
初めてなのでうまく使いこなせるかどうか分かりませんが、
慣れると便利なようです。皆さんの協力をお願いします。
とりあえず１０月２３日に課題が公開されるようにしてあります。
（受講登録終了しないと皆さんがログインできません。23日にもし
ログインできなかったら、２ー３日待ってください。
上のURLに入って、左下のHELPボタンをクリックすると使い方が書いてあります。
それを参考に課題の解答をしてください。
念のために自分の手元に解答を保存しておいてください：
もしうまくいかなかったら、ハードコピーで提出できるように！

「抽象化の技法　そのII」の１ページ目
冠頭標準形をSkolem標準形に変形する。（∀の記号の除去）
「その II」は ここ

A^pと、そのSkolem標準形A^sの同値性は、上とちがって、「恒真性について
同値である」ということである。詳しくは次回。

冠頭標準形 A^p と、そのSkolem標準形 A^s は「恒真性において同値」である。
これは、ある論理式と A と、そのSkolem標準形 A^s が「意味が同じ」という
意味での同値性とは異なることに注意。（証明は、簡単な例で。
十分条件の証明は終了。必要条件は来週。これは背理法による。肯定的に
証明しようと思って、この日は失敗！）

「そのIII」は は、ここ

レポートシステムが稼働始めました。試してみてください。
具合い悪ければ、知らせてください。

次回からは「計算」についてのいくつかの考え方を始めます。

∀xP(x)⇒¬∀y∃z(A(y,z)∨∀uR(z,u)) の冠頭標準形

∀xP(x)⇒¬∀y∃z∀u(A(y,z)∨R(z,u))
∀xP(x)⇒∃y∀z∃u¬(A(y,z)∨R(z,u))
∃x(P(x)⇒∃y∀z∃u¬(A(y,z)∨R(z,u)))
∃x∃y∀z∃u(P(x)⇒¬(A(y,z)∨R(z,u)))

注：∃xの位置は自由；∃y∀z∃uの順序は変えてはいけない。

今回は試運転で、協力をお願いしましたが、協力度はあまり高く
ありませんでした。協力者には協力点を２−５点配分しました。
次回からは正式にレポートにします。
このページの掲示を注意していｋてください。

解答　１．　A＝∃x(P(x)∧∀yQ(y))⇒¬∃xR(x)
A^p = ∀x∃y∀z(P(x)∧Q(y)⇒¬R(z))
A^s = ∃y(P(c)∧Q(y)⇒¬R(f(y))
A^m = P(c)∧Q(α)⇒¬R(f(α)) すなわち、
¬P(c)∨¬Q(α)∨¬R(f(α))

2. B = ∃x(¬P(x)⇒¬∃yP(y))が恒真であること
B^m = P(α_i)∨¬P(f(α_i))
P(α_1)∨¬P(f(α_1))∨P(α_2)∨¬P(f(α_2))　　
として、　α_1 = f(c), α_2 = c とおけば,
P(f(c))∨P(c)∨¬P(f(f(c)))∨¬P(f(c)).

P(f(c)) は正、負それぞれに出現。

注：１の限量記号の順序は、∀x∃yの順序は変えられません。
∀zは、上の位置でも、最初でもいいです。
もし、∀z を最初に置くのならば、A^m は
P(c)∧Q(α)⇒¬R(d) の形になります。

基本的には皆さん理解していたようですが、否定¬が
抜けている答案がいくつかありました。それでは意味が変わって
しまいます。もし¬記号が出せなかったらnotとか、〜とか、
で代用してもいいですから、無視しないこと。（？で代用した
人もいました。それでもいいです。）

なお、評価は、１、２それぞれ５点、合計１０点です。
解答をみて、大体自分の評価をみつもってください。
成績は開示します。それを見て、答案を見たければ、
申し出てください。

1. 69ページ、問１のTuring計算機で、第二、第三の計算をしてみる。
解答は来週教室で。

2. (1) 次の初期状況から出発して、71-72ページの各計算機で、
（一回の）計算を実効せよ。ただし、K_n は K_2 で。
BB11B111q_0B11BB

(2) 74ページ、例5で、S(2)をM_2で計算せよ。

(3) 74ページ、例6で、+(2,3)をM_3で計算せよ。

注：(2)は最終的に B111B1111q_HB となる。
(3)は最終的に B111B1111B111111q_HB となる。
こうならなければ、相談にきてください。

参考文献は次の二つです。
ソフトウエア仕様記述の先進技法ーＺ言語（ポター等著、田中訳、トッパン）
９９年度八杉特研卒業研究論文 （岩瀬、大西、平井、平田）
この論文は多少の誤字、ミス記述などありますが、言語Zについて要領よく まとめてあります。
ZはOxford大学で開発された仕様記述言語です。インターネットで
Formal Methods, Z, などで検索すると、いろいろ情報が得られます。
とくに Oxfordのサイト
を探してください。

inEurope(Paris)∧∀cap:Capitals・(inEurope(cap)⇒romantic(Paris)>=romantic(cap))

ただし「以上」を>=と表している。あるいは、「ヨーロッパの首都の集合」をECとして、
inEuropeを略すこともできる。また、romantic(x)を「x はロマンチックである」という
述語とすることもできる。たとえば

Paris:EC・∀cap:EC・(romantic(cap)⇒romantic(Paris))

「ほかの都市がロマンチックならば、もちろんパリはロマンチック」によって
パリが最もロマンチックであることを表現している。
ただし、これではどの首都もロマンチックでないかもしれない。パリが実際に
ロマンチックであることを表すには、∃cap:EC・romantic(cap)を加えればよい。

(vi) 私のスペイン語の夜のクラスでは、最年長の学生は最年少の学生の４倍以上の年齢である
age(x) を、x の年齢、SEを「スペイン語の夜のクラス（の学生全体）」とおく。

∃x:SE・∃y:SE・(∀z:SE・age(x)>=age(z)>=age(y)∧age(x)>=4*age(y))

または、数学的に同値な式として

∃x:SE・∃y:SE・age(x)>=age(y)

今後の予定：型の簡単な説明とスキーマの説明

1. B11q_01B→B111q_61B→B1111q_6B→B11111q_6B→・・・　↑

2. B11q_01B→B1q_11B1B→Bq_111B1B→q_1B11B1B→q_2BB11B1B→
q_21B11B1B→q_H1B11B1B↓

大きい問題が３題
１．　(1) 与えられた述語論理の論理式 A の冠頭標準形、スコーレム標準形、
マトリックスの一つ、その和積標準形、を求める。（穴埋め問題）
(2) (1) の結果を使って、 A が恒真であることを示せ。

２．　(1) ある Turing 機械　M の初期時点表示が与えられているとき、
M の動きの各時点における時点表示を表せ。
(2) (1) を参考にして、機械 M の働きを、ことばで記述せよ。

３．　簡単なスキーマの作成。（穴埋め問題）

以上、学期の間に学んだ事柄の基本がわかっていれば、できる問題です。

問題4.25(ii) bignumbers == {n:N|n>1000000}

問題4.27initialstock に属し、その在庫レベルが１０より少ない在庫品すべての集合
initiallowlines の公理的記述。（簡単のため、縦線は省略）
initialstock: Stock
initiallowlines: Stock
---------------------------------- initiallowlines \subset initialstock
∀i:Item∀m:N・(i,m)εinitiallowlines <=> (i,m)εinitialstock ∧m=< 10
注：「A \subset B」は、A が B の部分集合（含まれる）を表す。
Item は品目を表す型、εは「要素」関係、<=>は両方向きの「ならば」
すなわち、同値性、=< は「以下」を表す。

(ii) 双子素数の集合　TwinPrimes の略記的定義をあたえよ。
ただし、双子素数とは、二つの整数n,n+2の対で、両方とも素数であるもの。
Prime(x) （x は素数）：x>1∧¬∃y,z:N・1 TwinPrimes == {a: N x N| ∃n:N・a=(n,n+2)∧Prime(n)∧Prime(n+2)

(iii) singleton （要素を１個だけもつ集合）の総称的定義
====[X]==============
singleton:PX
----------------------
∃x:X(xεsingleton)∧∀y:X・yεsingleton ⇒y=x
ただし　xεy　は「x が y の要素である」を表す。

試験前の質問について：　私の予定が未定の部分が多いので、
確定した時間があまりとれませんが、
２１日（火曜日）、２時過ぎから２：５０まで、
２２日４時前から４：３０まで、C2教室で、待機しています。
用事があったらきてください。

２．「みんなが好きな花がある」→「ある花があって、人はすべて
その花が好きだ」
∃f:Flower・∀p:Person・Likes(p,f)

注意：１はほとんどの人ができていました。２の典型的なまちがいは
∃p:Person・∀f:Flower・Likes(p,f)
「花がある」といっているのに、なぜ「人がある（いる）」となるのですか？
仕様記述でも、プログラミングでも、日本語の正確な理解が不可欠なのです。
このことをよく覚えていてください。
なお、少数ですが、p:Person を、Person:p と書いていました。これはZの文法の
問題です。Zに限らず、型の理論では　変数：型　という記法が基本です。

スキーマについて：図書館管理システムの例に基づく説明
プリントのp.130の、図書館の業務についての説明を読んでおく。
p.131 6.3 抽象的状態を規定するスキーマ
このページはざっと読んでおく。
p.132 スキーマ　Library の解説。
初めに用意する記号は、基本データ型と変数である。
１．　基本データ型（状況に応じて自分で決める。Z言語で指定して
あり、とくに明記しなくても使えるものもある。（例　整数型 Z、自然数型　Nなど
ここでは、型として、 Book（著書） Copy（著書の現物；コピーと呼ぶ）,
Reader（登録可能者、人々、と考えてもよい） を設定。
２．　変数　stock（蔵書の集合）、issued（貸し出中のコピーの集合）、
shelved（貸し出していない、すなわち、棚にある、コピーの集合）、
readers（実際に登録している利用者）
また、大域変数　maxloans （貸し出し可能冊数）を用意する。
これはスキーマLibrary以前に宣言しておくｒ。
Libraryの中の変数との違いは、普通のプログラム言語における
大域変数と局所変数の違いと同じである。maxloansは、スキーマの中で
値が変化しない。スキーマの中では、定数とみなされる。
以下、"Library"の説明をしていく。p.132 の説明と照らし合わせて
読むこと。
まず、スキーマの形式は（簡単のために左端の縦線は略）

---スキーマの名称--------------
宣言部

-----------------------------
述語部

-----------------------------

宣言部について

-|-> は、部分写像（関数）の型（集合）を表す。写像は「写像のグラフ」で
表される（「集合と論理」の「写像」参照）。すなわち
f(x)=y を f のグラフ G_f によって、(x,y) ε G_f と表したのと同じ
考え方である。

stock: Copy -|-> Book は、stock が蔵書の一冊でり、(x,y) という対の
形をしていて、x は型 Copy で、ある図書館で使えるコピーの識別子（記号や番号）、
y は型 Book で、その識別子を割り当てられた著書（の名前）である。
使える識別子でも、実際には使っていないものもあるから、stock は部分写像である。

issue: Copy -|-> Reader は、issue が貸し出し中のコピーであり、
(x,z) という対の形をしている。x の型は上と同じく Copy で、
z は型 Reader で、識別子 x の コピーを借りている登録者を表す。
これが部分写像であることは、内容から明らかであろう。
shelved: F Copy は、shelved が貸し出していない、図書館の棚に残っている
コピーの集合であることを示す。　F X は、X の有限部分集合全体を表す。
ここでは、 X 自体が有限集合で、したがって F X は、P X （X の部分集合全体）
と同じ、と考えてよい。

readers: F Reader は、reader が、登録可能な人々（Reader）　の有限部分集合
であることを示す。内容としては、実際に登録している利用者の集合である。

述語部について

dom f は、 f が写像（のグラフ）、すなわち、 (x,z) という対の集合ときに、f の定義域、
すなわち、(x,z) が f の要素になるような x の集合
したがって、dom issued は、貸し出し中のコピーの識別子の集合、dom stock は、
蔵書の識別子の集合を表す。これにより、第一行目は、「棚に残っている
コピー（の識別子）全体と、貸し出し中のコピー（の識別子）全体の和集合は
蔵書（の識別子）全体に等しい。第二行目はその二つの集合が共通部分を
もたない（同時に貸し出し中で棚になる、ということはない！）ことを表す。
ran f は、f が写像（のグラフ）であるとき、f の値の集合を表す。
上にならえば、(x,z) が f の要素になるような z の集合である。
第三行目は、「借り出している人々は実際の登録者の部分集合である」
すなわち、借りる権利のある人にだけ貸し出している、ということを表す。
#S は、集合 S の要素の個数、issued　|> {r} は、issued という、対(x,z)の集合の
要素のうち、z が r であるものの集合。つまり issued |> {r} の要素は
それぞれ (x,r) の形をしている。
最後の行は、「各登録者 r について、r に貸し出し中のコピーの冊数は
maxloans 以下である」を表す。すなわち、貸し出し可能最大冊数を
越えてはならない、ということである。
以上が、蔵書や登録者の出入りのない、図書館のデータとして基本的な
最低限の条件を表現している。

この説明と照らし合わせて、プリントのLibraryのスキーマをゆっくり眺めて
ください。図書館の機能をちょっと考えれば、意味がわかると思います。
期末試験は、たとえば、こういうスキーマの一部分の空白を埋める問題です。

24日には、４回目の課題の解答を書きます。

あと、英語のクイズをおまけの課題として出します。 ここに大体のことを書いて、解答はレポートシステムで出すようにします。
このページを注意していてください。

*B,1もよくわかりません。
答え：B や　1　（または | ）は、プリントにもあるし、講義でも説明したはずですが、
テープに印刷する文字です。実際には印刷されるのは１だけで、B は、その
ます目が空（から）であることを表します。（Bはblank のB）

*チューリング計算機の問題がよくわかりません。
答え：機械の表または、関数δの指示どおりヘッドを動かしてゆくだけです。
その様子をテープの状態で表すのは大変なので、時点表示という様式で
表します。プリントは短いものですから、ゆっくり読んでください。
また、上に模擬試験をおいておきましたので、それをぜひ参考にしてください。

*Zの論理式を表す問題で ∀x:X・..... と
∀x:X (.....) の使い方の違いがわかりません。
答え：・は「かっこ」だと考えていいのです。しかしときには両方使うことがあるので
まぎらわしいかもしれませんが、・は言語Zの記法です。
∀x:X・x=2∨x < 0 と、 ∀x:X(x=2∨x < 0) は同じことを表します。
しかし長い式の場合 ∀x:X・(x=2∨x < 0.......) のように書くこともあります。
この場合は本当は・か（　　）か、どちらかでいいのです。

*Turing機械Ｍの働き」とはどういう意味ですか？
「模擬試験」の第２問のことですか？
そこの答えを見ればわかると思うのですが、一般にたとえば
「Mは二つの数の足し算をする」とか、「Mは、１が並んでいるときに、その
一番左の１を消す」などというように、記述することです。

３人の会話（それぞれは意味をもつ）を聞いて、Bill は何か不審な気がします。

それはどういうことなのでしょう？答えは日本語で書いてください。
考えるヒントをここに書いておきます。（レポートシステムには、ヒントは書きません。）
答えがまちがっていても、解答者が自分にとっては筋が通っている、と
分かれば、５点の加算です。全然関係ないこと書いてあったらだめですが。
ともかく自分なりに考えて、答えてください。
これはいつも英語のクイズを教室で出すことの代わりです。
締め切りは２月15日です。ゆっくり楽しんでから答えてください。

Friendly conversation
Mary : "I am a liar."
John : "Mary is telling the truth."
Caryn : "Mary is not telling the truth."

Bill : "Neither John nor Caryn is correct. There is something strange about the whole thing."

Question : Why does Bill say so?

Hint: Suppose John is correct. Then Mary is telling the truth. So Mary is a liar.
This means that Mary is not teling the truth.
Suppose Caryn is correct. Then Mary is not telling the truth. So Mary is not a liar.
This means that Mary is telling the truth.

これを読むと、「型X の二つの要素 x,yがあって、それらは等しくなく、
両方ともtwos の要素であり、任意の型Xの要素 z について、z が twos の
要素ならば、z は x,y のどちらかに等しい。」
これが「twos がちょうど要素２個をもつXの部分集合である」ことを示すことは
分かるでしょう。
・の代わりに括弧を使ってもかまいません。
なお、述語部が　「#twos = 2」というのがありました。# を知っていればこれでも
いいわけです。授業中にも#は使いましたし。私の意図は、singleton の例に倣って
上のように論理式で書いてほしかったのではありますが、まちがいではないので
これでけっこうです。ただし、論理式で書こうとしてちょっとまちがった、という
人に不利にならないように配慮しました。
スキーマの形式が分かっていれば、かなりの配点をし、論理式の細かいことは
あまり厳密に区別しませんでした。もちろん全体が「明後日」の方向では困りますが。
今回課題提出しない人が多かったのは、残念です。その埋め合わせのためにも
クイズにはぜひ答えてください。

初めてのテーマをトピック風に解説したので、まだ完全には
自信ないな、と思うかもしれません。それはそれでいいのです。
将来こういうことに出会ったときに、勉強するための基礎は できているはずです。
では、卒業生は、元気で社会にでてください。
３年生は、卒業と就職に向けて有益な一年を送ってください。