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 節を終わらせる予定。

文献

コメント



トップ   編集 凍結 差分 履歴 添付 複製 名前変更 リロード   新規 一覧 検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2015-05-21 (木) 18:31:37