2010/自主ゼミ/計算機科学ゼミ
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
|
ログイン
]
開始行:
[[2010/自主ゼミ]]
#contents
* 内容 [#w7ab642f]
:代表者 | [[t_uda]]
:分類 | 数学/計算機科学
:内容 | 型理論(型付きλ計算)をやる予定。
:形式 | 輪読
:日程 |
--【後期】 水曜 6 限; 10/20(水)~
--【春休み】 水曜 4・5 限; 2011/02/23(水)~
:教室 |
--【後期】 理6-303
--【春休み】 理6-302
:知識 | 簡単な論理学の知識(特に記号操作に対する慣れ)...
* 報告 [#rfe0b3f9]
**第 0 回 2010/10/20 (水) [#v02177d7]
>[[t_uda]] (2010-10-23 (土) 20:51:29)~
~
関連する第 5 章の導入部分と、第 6 章「自然演繹の体系」の ...
→ (5) の証明図: http://twitpic.com/307lub
**第 1 回 2010/10/27 (水) [#cc577ff5]
>[[t_uda]] (2010-10-28 (木) 00:13:10)~
~
関連する LJ についてサラっと流した後、NJ と LJ の証明可能...
~
述語論理を含む NJ と、その問題演習をした。問題演習の過程...
→ [[t_uda]]: 疑問解消。仮定の固有変数条件のため、そのよう...
//
**第 2 回 2010/11/10 (水) [#z9105958]
>[[t_uda]] (2010-11-10 (水) 21:25:46)~
~
先週は文化の日で休み。2週間ぶり。~
~
背理法を公理につけくわえた論理体系 NK について。問題演習...
//
**第 3 回 2010/11/17 (水) [#ob075ceb]
>[[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))」の証明図>http://twitpic.co...
//
**第 4 回 2010/12/01 (水) [#fe588e40]
>[[t_uda]] (2010-12-04 (土) 03:17:40)~
~
λ計算の初歩の辺り。主に定義の確認。ちゃんと準備されていた...
~
後は関連する演習問題(今回は全て消化)。この手の証明問題...
//
**第 5 回 2010/12/08 (水) [#vb247945]
>[[t_uda]] (2010-12-08 (水) 22:09:34)~
~
私が担当。目標だった型付きλ計算を一気に終わらせた(本の最...
今回は演習問題はやっていない(少ないし)。~
~
次回から、次のテキスト "Proofs and Types" を使って型理論...
//
**第 6 回 2010/12/15 (水) [#a66d0f6f]
>[[t_uda]] (2010-12-15 (水) 22:04:41)~
~
2, 3 章を一応終わらせた。「正規=冠頭標準形」の定理の系に...
~
次回は 4 章。~
//
**第 7 回 2011/01/12 (水) [#ha03e184]
>[[t_uda]] (2011-01-12 (水) 22:58:48)~
~
第 4 章で使う Church-Rosser の定理の証明をしてもらった(...
~
次回は証明の修正の後、第 4 章に入る。~
//
**第 8 回 2011/01/19 (水) [#m8089db7]
>[[t_uda]] (2011-01-20 (木) 21:04:38)~
~
Church-Rosser の定理を証明した。第 4 章は少し入った。~
//
**第 9 回 2011/02/23 (水) [#v851f7eb]
>[[t_uda]] (2011-02-24 (木) 02:31:25)~
~
第 4 章の 2 節までやった。次回、3 節 と 4 節を終わらせる...
//
* 文献 [#j38d5ba6]
- 『[[情報科学における論理 - Amazon>http://www.amazon.co....
-- 前期使った本の続き。後期は、独立している第 6 章だけや...
- 『[[型理論I-IV - CiNii>http://ci.nii.ac.jp/naid/1000006...
-- I から IV まで全て PDF で入手できるので、後半はこれを...
-- 多分ペーパー誌に連載されていた記事だと思う。論文程堅く...
- "[[Proofs and Types>http://www.paultaylor.eu/stable/Pro...
-- 絶版。PDF ファイルとして無償配布されている。
-- 来年度の数学講究の計算機分野で長谷川先生が副読本として...
-- 後半はこのテキストでゼミをすることにした。(第 6 回~)
* コメント [#v7615472]
#comment
終了行:
[[2010/自主ゼミ]]
#contents
* 内容 [#w7ab642f]
:代表者 | [[t_uda]]
:分類 | 数学/計算機科学
:内容 | 型理論(型付きλ計算)をやる予定。
:形式 | 輪読
:日程 |
--【後期】 水曜 6 限; 10/20(水)~
--【春休み】 水曜 4・5 限; 2011/02/23(水)~
:教室 |
--【後期】 理6-303
--【春休み】 理6-302
:知識 | 簡単な論理学の知識(特に記号操作に対する慣れ)...
* 報告 [#rfe0b3f9]
**第 0 回 2010/10/20 (水) [#v02177d7]
>[[t_uda]] (2010-10-23 (土) 20:51:29)~
~
関連する第 5 章の導入部分と、第 6 章「自然演繹の体系」の ...
→ (5) の証明図: http://twitpic.com/307lub
**第 1 回 2010/10/27 (水) [#cc577ff5]
>[[t_uda]] (2010-10-28 (木) 00:13:10)~
~
関連する LJ についてサラっと流した後、NJ と LJ の証明可能...
~
述語論理を含む NJ と、その問題演習をした。問題演習の過程...
→ [[t_uda]]: 疑問解消。仮定の固有変数条件のため、そのよう...
//
**第 2 回 2010/11/10 (水) [#z9105958]
>[[t_uda]] (2010-11-10 (水) 21:25:46)~
~
先週は文化の日で休み。2週間ぶり。~
~
背理法を公理につけくわえた論理体系 NK について。問題演習...
//
**第 3 回 2010/11/17 (水) [#ob075ceb]
>[[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))」の証明図>http://twitpic.co...
//
**第 4 回 2010/12/01 (水) [#fe588e40]
>[[t_uda]] (2010-12-04 (土) 03:17:40)~
~
λ計算の初歩の辺り。主に定義の確認。ちゃんと準備されていた...
~
後は関連する演習問題(今回は全て消化)。この手の証明問題...
//
**第 5 回 2010/12/08 (水) [#vb247945]
>[[t_uda]] (2010-12-08 (水) 22:09:34)~
~
私が担当。目標だった型付きλ計算を一気に終わらせた(本の最...
今回は演習問題はやっていない(少ないし)。~
~
次回から、次のテキスト "Proofs and Types" を使って型理論...
//
**第 6 回 2010/12/15 (水) [#a66d0f6f]
>[[t_uda]] (2010-12-15 (水) 22:04:41)~
~
2, 3 章を一応終わらせた。「正規=冠頭標準形」の定理の系に...
~
次回は 4 章。~
//
**第 7 回 2011/01/12 (水) [#ha03e184]
>[[t_uda]] (2011-01-12 (水) 22:58:48)~
~
第 4 章で使う Church-Rosser の定理の証明をしてもらった(...
~
次回は証明の修正の後、第 4 章に入る。~
//
**第 8 回 2011/01/19 (水) [#m8089db7]
>[[t_uda]] (2011-01-20 (木) 21:04:38)~
~
Church-Rosser の定理を証明した。第 4 章は少し入った。~
//
**第 9 回 2011/02/23 (水) [#v851f7eb]
>[[t_uda]] (2011-02-24 (木) 02:31:25)~
~
第 4 章の 2 節までやった。次回、3 節 と 4 節を終わらせる...
//
* 文献 [#j38d5ba6]
- 『[[情報科学における論理 - Amazon>http://www.amazon.co....
-- 前期使った本の続き。後期は、独立している第 6 章だけや...
- 『[[型理論I-IV - CiNii>http://ci.nii.ac.jp/naid/1000006...
-- I から IV まで全て PDF で入手できるので、後半はこれを...
-- 多分ペーパー誌に連載されていた記事だと思う。論文程堅く...
- "[[Proofs and Types>http://www.paultaylor.eu/stable/Pro...
-- 絶版。PDF ファイルとして無償配布されている。
-- 来年度の数学講究の計算機分野で長谷川先生が副読本として...
-- 後半はこのテキストでゼミをすることにした。(第 6 回~)
* コメント [#v7615472]
#comment
ページ名: