2010/自主ゼミ/計算機科学ゼミ

2010/自主ゼミ

内容 †

代表者

t_uda

分類

数学/計算機科学

内容

型理論(型付きλ計算)をやる予定。

形式

輪読

日程

• 【後期】 水曜 6 限; 10/20(水)～
• 【春休み】 水曜 4・5 限; 2011/02/23(水)～

教室

• 【後期】 理6-303
• 【春休み】 理6-302

知識

簡単な論理学の知識（特に記号操作に対する慣れ）さえあれば前提知識は全く不要。

報告 †

第 0 回 2010/10/20 (水) †

t_uda (2010-10-23 (土) 20:51:29)

関連する第 5 章の導入部分と、第 6 章「自然演繹の体系」の 1, 2 節をやった。残りは問 6.1 の演習時間。(5) 以外は解答済み。

→ (5) の証明図: http://twitpic.com/307lub

第 1 回 2010/10/27 (水) †

t_uda (2010-10-28 (木) 00:13:10)

関連する LJ についてサラっと流した後、NJ と LJ の証明可能性同値の証明。Rem. NJ は直観主義論理の体系。

述語論理を含む NJ と、その問題演習をした。問題演習の過程で公理(∀I)と(∃E)を使えば ∃xA⊃∀xA が示せるのではないかと言う疑問が出た。

→ t_uda: 疑問解消。仮定の固有変数条件のため、そのような証明はできない。

第 2 回 2010/11/10 (水) †

t_uda (2010-11-10 (水) 21:25:46)

先週は文化の日で休み。2週間ぶり。

背理法を公理につけくわえた論理体系 NK について。問題演習は、3問未消化: 6.4 (3), 6.5 (1)-(2)

第 3 回 2010/11/17 (水) †

t_uda (2010-11-18 (木) 00:40:44)

NK での論理式の正規化（証明図の簡約）と関連定理について。

4問未消化: 問 6.4 (3), 章末 6.2 (2)-(3)

問 6.2 (2)「∃x∀y(P(x)⊃P(y))」の証明図

第 4 回 2010/12/01 (水) †

t_uda (2010-12-04 (土) 03:17:40)

λ計算の初歩の辺り。主に定義の確認。ちゃんと準備されていたので良い感じに進んだ。

後は関連する演習問題（今回は全て消化）。この手の証明問題は構造的帰納法を使います。

第 5 回 2010/12/08 (水) †

t_uda (2010-12-08 (水) 22:09:34)

私が担当。目標だった型付きλ計算を一気に終わらせた（本の最後まで終わらせた）。
今回は演習問題はやっていない（少ないし）。

次回から、次のテキスト "Proofs and Types" を使って型理論をもっと厳密にやる。

第 6 回 2010/12/15 (水) †

t_uda (2010-12-15 (水) 22:04:41)

2, 3 章を一応終わらせた。「正規＝冠頭標準形」の定理の系についての理解や、説明文の理解（日本語訳）などが不十分だった。

次回は 4 章。

第 7 回 2011/01/12 (水) †

t_uda (2011-01-12 (水) 22:58:48)

第 4 章で使う Church-Rosser の定理の証明をしてもらった（途中まで）。

次回は証明の修正の後、第 4 章に入る。

第 8 回 2011/01/19 (水) †

t_uda (2011-01-20 (木) 21:04:38)

Church-Rosser の定理を証明した。第 4 章は少し入った。

第 9 回 2011/02/23 (水) †

t_uda (2011-02-24 (木) 02:31:25)

第 4 章の 2 節までやった。次回、3 節 と 4 節を終わらせる予定。

文献 †

• 『情報科学における論理 - Amazon』 - 情報数学セミナー (小野 寛晰)
  • 前期使った本の続き。後期は、独立している第 6 章だけやる。
• 『型理論I-IV - CiNii』 (龍田 真)
  • I から IV まで全て PDF で入手できるので、後半はこれを使う。…かも。
  • 多分ペーパー誌に連載されていた記事だと思う。論文程堅くはないが、そこそこ専門的な感じ。
• "Proofs and Types" / J.-Y.Girard, Y.Lafont and P.Taylor / Cambridge Univ. Press, 1989
  • 絶版。PDF ファイルとして無償配布されている。
  • 来年度の数学講究の計算機分野で長谷川先生が副読本として挙げている本。
  • 後半はこのテキストでゼミをすることにした。(第 6 回～）

コメント †