2011/自主ゼミ/計算機科学ゼミ の変更点

• 追加された行はこの色です。
• 削除された行はこの色です。
• 2011/自主ゼミ/計算機科学ゼミ へ行く。
• 2011/自主ゼミ/計算機科学ゼミ の差分を削除

[[2011/自主ゼミ]]
#contents

* 概要 [#o394e7ee]

:代表者   | [[t_uda]]
:分類     | 数学
:形式     | 輪講
:内容     | 型理論 (System T, System F, ...etc)
:日程     | 火6
:教室     | 理6-207
:参加人数 | (3+α)人

* 報告 [#t1954591]

**第 1+i 回 2011/05/10 (火) [#j3c6d237]
>[[t_uda]] (2011-05-12 (木) 13:24:31)~
~
第 6 章「強正規化定理」を一応終えた。次回は第 7 章から。~

//
**第 1+2i 回 2011/05/17 (火) [#h0d5fd78]
>[[t_uda]] (2011-05-17 (火) 20:44:04)~
~
第 7 章「Goedel's System T」を半分までやった。証明の場合分けの細かい部分をチェックした。~
~
課題. 自然数上の加法 x+y に相当するλ項 t[x,y] について、可換性（t[x,y] = t[y,x]）や x についての帰納性（ t[0,y] = y, t[Sx,y] = St[x,y]）が成り立つかどうかは直ちには分からないので次回までに考察しておいて下さい。~

//
**第 1+3i 回 2011/05/24 (火) [#z1fa1a09]
>[[t_uda]] (2011-05-25 (水) 23:19:03)~
~
第 7 章の残りを終わらせた。足し算・掛け算・べき乗・前者関数・引き算を再帰演算子 R を使って実際に定義し、R の性質を理解した。~

//
**第 1+4i 回 2011/06/03 (金) [#m2ff6609]
>[[t_uda]] (2011-05-30 (月) 14:58:10)~
~
※今週の 5/31(火) は休み。代わりに 6/03(金) にやります。~
8.4 の、 direct product of 2 coherence spaces までやった。次回 8.5 から。

//
**第 1+5i 回 2011/06/07 (火) [#t67e80a1]
>[[t_uda]] (2011-06-07 (火) 18:00:52)~
~
8.5.1 をやった。F と Tr(F) の対応について詳しく検証した。~

//

* 文献 / 関連項目 [#jfe30e1a]
- [[2010/自主ゼミ/計算機科学ゼミ]]
- "[[Proofs and Types>http://www.paultaylor.eu/stable/Proofs+Types.html]]" / J.-Y.Girard, Y.Lafont and P.Taylor / Cambridge Univ. Press, 1989

//#comment