抽象化の技法


注意 講義要項を読んでおくこと。
小林先生のプログラミング言語学および鴨先生の先端科学特論と 関連があります。三つで計算機科学の基本的な理論のワンセットと 考えてください。

第一回 4月14日 いろいろな帰納法 情報系の数学入門 2章 
         数学的帰納法の復習、累積帰納法  構造帰納法 2.6[1] 

第二回 4月21日 重みをつけた帰納法2.6[5]、計算帰納法2.6[6]、 述語 (第3章 3.6[1])

第三回 4月28日 述語論理の式、文章の記号化、出現、有効範囲、束縛、自由 (3.6[2], [3], [4])


演習問題:次の文章を述語論理の論理式として表現せよ。
(1)馬の耳は動物の耳
(2)だれにでも愛する相手がいる。
(3)任意の正の実数xについて、y^2=xとなる正の実数yがある。

第四回 5月12日 述語論理の意味論、例(3.6[5],[6])
命題論理の体系--公理、推論規則、証明、定理、健全性(無矛盾性)
完全性 (3.4[1],[2],[3])

レポート!


提出日:6月15日、16日 提出場所:理学部事務室(表紙をつける)
十分時間がありますね。よく考えて答えてください。
レポート作成フォーマット:LaTex
講義要項に書いてあるとおりです。LaTexによるレポート作成は
この科目の教育の一環です。

課題 1 任意の(命題論理の)論理式 A について、"not"と"and"だけから作られる
論理式 B で恒に v(A)=v(B) となるものがあることを示せ。
(論理式の構成に関する構造帰納法を適用する。A の構成における
最後の論理結合子についての場合わけによる。 情報系の数学入門・第2章、2.6[1] 82ページ参照)
課題 2 「皆が何か動物を好きなわけではない」を、述語論理の記号で表せ。
(述語記号は自分で適当に設定してよい。)
課題 3 (exists x)(forall y)leq(x,y)
(ただし、leq(x,y)は"x は y 以下である"を表す。)
    この論理式が正しい数学の集合と正しくない集合をそれぞれ与えよ。
   正しくないほうは、反例をあげよ。
課題 4 命題論理の体系Pの公理(Ax7)(A=>B)=>((A=>notB)=>notA) が恒真である
ことを示せ。(情報系の数学入門・第3章 3.4[1])

4年生以上で、就職活動で出席困難な人は、申し出てください。(具体的に
欠席理由を求めます。)
以上


レポートの課題についての質問と答え 課題1について

何をどう示すのか?(かっこの中のコメントの解説)
****************************
答え 構造帰納法を使うのは、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で
書き換えなければなりません。
このように論理結合子によって扱いがちがう、ということです。
*****************************


第五回 5月19日 述語論理の論理式についての補足(メタ変数、アルファ同値、
代入)自然演繹の証明(初めのみ)(数理論理学 1章1.1--1.2.6の初め)

*休講、補講のお知らせ
休講:6月9日 一回あいた分、レポートの勉強しておいてくださいね。
補講:7月10日(土)3時間目 512教室
不便な時間でごめんなさい。皆さんの都合のよい時間はこれくらいなのです。
なるべく質問と演習の時間にします。質問をもってきてください。


第六回 5月26日 自然演繹の証明:命題結合子の場合 (「数理論理学」 1.2.6 pp.17-23)
演習問題 "and"と"or"の交換律、結合律、A and A <==> A, A or A <==> A


第七回 6月2日 自然演繹の証明:限量記号の場合(「数理論理学」1.2.6)
証明の例 (A=>B)=>(notA or B)など


第八回6月16日、第九回 6月23日 自然演繹の証明もっともっと
 自然演繹の体系NKおよびNJの証明図・続き
シークエントの証明可能性(p1.2.8 34ページ)
健全性(証明可能ならば恒真)(2.2.3 54ページ)
および(健全性を仮定した上での)完全性
(恒真な述語論理の式は証明可能)(証明は略)(参照:4.5 118ページ)
完全性はゲーデルの定理。恒真性を証明という形式で表現できることを示す重要な定理。
等号をもつ論理体系(1.2.12 41ページ)


*レポートの結果について : 4年生に提出猶予しているので、9月まで解答を書けません。
レポートは一度返しますので、講義の後にとりにきてください。
なお、評価は、レポート(前期、後期各一回)40点、期末試験
(各一回)60点、合計/2 が成績となります。


第十回 6月30日: 自然数の特徴づけ、PA(Peano算術)の公理
PAは述語論理(NK)を基礎に、自然数の性質をあらわす公理を加えたもの。
教科書 1.3 応用述語計算 (42-45ページ)
演習(課題ではない!):「素数が無限にある」をPAの論理式として書け。
ただし「nは素数」は Prime(n)と書く。


第十一回:7月7日 PAで書ける数学の命題、証明図とプログラム


*前期期末試験について:NKの証明図作成(ごく簡単なもの)、PAの言語で
数学の命題を表す、数学的帰納法の使い方


*期末試験はどうでしたか?秋までには解答を載せますので、参考にしてください。 ざっと見たところ、1の(1)は、これほどやさしい証明図はないのに、皆さんやさしいことを 無理に難しくして失敗しています。もっとも正解も多かったですが。
(2)はちょっと考える問題ですが、例題をいくつかていねいに見ておけばできるはずです。
2は日本語をそのまま論理記号に書き直す問題です。条件がいくつかあるときにはそれらを "and"でつなげばいいのです。「無数に」は素数のときと同じ要領で表現します。
3はだいたいできています。やはり慣れていることには強い?
では後の試験の成功と、良い夏休みを!


*前期期末試験と今後の方針について

良く理解している人もいましたが、全体として、論理式という一番
基本的なことが理解できていなかった。解答を
ここ におきますから、よく読んで理解してください。
レポートや試験は、成績をつける目的だけではありません。その勉強をする
ことによって、理解を深めまた理解できていないことは何か、を自覚できる
ように、という目的もあります。そこで理解を深めるために、次の方針をとります。

**後期のレポート(1月初めに提出、詳細は後で)では前期の内容も含めて、
総合報告を書いてもらいます。(ほかに技術的な問題もだします。)そのために
40点満点ではなく60点満点にして、前期との調節をします。(後期の期末試験は
予定通り60点)総合点が満点を越える人は満点で打ちきります。
なお、LaTexで証明図を書くには次のファイルを自分のところにコピーすればできます。
/NF/local/Solaris2J/lib/tex/macros/proof.sty
とても便利なマクロです。


10月20日:命題論理の自動証明(ワンのアルゴリズムの応用)

*休講と補講のお知らせ:休講は11月17日、補講は12月8日4限め(3限でなくてごめんなさい。)
11月:Curry-Howard 対応、述語論理の自動証明、冠頭標準形、Herbrand標準形


第2回レポート
提出日 2000年(そうです、最高位の数字が2になるのです!)1月11日、12日
提出場所 理学部事務室 (表紙をつけて綴じること)

1 述語論理の体系 NK および NJ について論述せよ。(A4約3枚)

2 自然数論 PA について論述せよ。(A4約1枚)

注 (以上1と2について、書き方は自由です。主張したいことが読者に伝わるように書いてください。
提出する前に友人などに読んでもらうことを勧めます。

3 〔1〕論理式 (A==>(B==>A and B)) の(NJにおける)証明 Q を作成せよ。
  〔2〕証明 Q にCurry-Howard 対応する F_0 のプログラム e を書け。
〔3〕P が論理式 A の証明のとき、Q と P を使って B==>(A and B) の証明 R を書け。
〔4〕R に対応するプログラム p を書け。

4 次の論理式の証明を、分解の木を参考にして、作成せよ:
(*) (forall)xP(x) or (exists)y(notP(y))


*しばらくごぶさたしました。忙しくて講義進行状況を かけませんでした。
12月3日現在の状況を書きます。「論理式と型」、「証明とプログラム」 (テキスト6章:Curry-Howardの対応)、
なお、証明をプログラムとみなすことについては、次の解説が参考になります。
数理科学(サイエンス社)99年11月号、「証明とプログラムの統一」佐藤雅彦著
「述語論理の自動証明」 (テキスト5章:5.1--5.4)を終わりました。
今後まず「形式的技法:ソフトウエア仕様記述言語Z」の解説をします。 参考書として
ソフトウエア仕様記述の先進技法ーZ言語、ポター・シンクレア・ティル著、 田中訳、プレンティスホール・トッパン

12月8日、15日:形式的技法」のスキーマの例による説明をしている。

*注: レポートは前回と同じくLaTexで書いてください。ただし証明の作成は
手書きでもいいです。前にお知らせしたproof.styを使うときれいに書けます。 興味があったら試してみてください。


*後期期末試験のヒント
問題は3題です。
1は文章を述語論理の式で書くこと。ただし言語Zの記法による。 したがって型を使う。
例 「偶数は3で割り切れない」: forall n:N・not divides(3,2n)
「花子がきらいな花がある」: exists f:Flowers・not likes(Hanako,f)

2はかんたんなスキーマを書くこと。
例  「二つの入力値の最初の要素を取り出す写像の定義を書け」:
  project1(x,y)=xとなる写像projectの定義。任意の集合XとYからXへの 写像の型をもつ。

3は、一年間の講義の中で、あなたが得意とする事柄について、数行で書く。
内容は何でもいいですが、読む人が理解しやすくて納得するように書いてください。
あらかじめ書いてみて、覚えてきてください。

試験終了後に1と2の解答を載せます。

では
I enjoyed having you in my class and Good Luck on the finals!


試験はどうでしたか?ごく基本的な問題だったのですが、2の出来がよく
なかったです。3はあらかじめ準備したものを書けばよいのですが、
求められているのはひとつのテーマをきちんと表現することで、
感想やエッセーではありません。(計算機科学の科目です。)
要求されていることは何か、を見極めるのも能力のうちです。
それからいくつかの式だけ並べたような答案がありましたが、
これでは意味をなしません。そのテーマが何を意味するのか、
それに関して何が成り立つのか、をきちんとした文章で
記述しなければ、主張が相手に伝わりません。これはどの科目、
いや、毎日のどんな場面においても同じことが言えます。
成績は一年間のレポート、最後の講義中の解答および
期末試験の総合点によりつけました。
二回目のレポートを60点(本来は40点)満点にしてあるので、
これ以上考慮することはしません。
なお、卒業予定者に限り、20日すぎに合否をここに書きます。
メールによる問い合わせはご遠慮ください。

参考書 *は教科書
* 情報系の数学入門 林・八杉著 オーム社  (集合・写像・論理・計算・
帰納法・命題論理の式、真理値、恒真性の判定アルゴリズム、述語論理の式)
*数理論理学 林著 コロナ社 (述語論理の証明論)
証明論入門 竹内・八杉著 共立出版 (述語論理と算術体系の証明論)
論理パズルとパズルの論理 八杉・林著 (論理パズルの解き方)
ゲーデルの謎を解く 林著 (不完全性定理解説)
ソフトウエア仕様記述の先進技法-Z言語、内山光一他訳 トッパン

../
/
Last modified: Tue May 6 17:38:29 JST 2003