【数学】 Proofs and Typesを読んだ記録
ゼミ(2022/10/21~)をするなかであったらよかったなという情報をまとめていきます
役に立つ文献
Chapter 1 10/21
頑張って英語を読みましょう これを機に数学英語以外も読めるようになろう
Chapter 2 10/21
λ-calculusの諸原則などはふつうに目を通しておいた方がよい. Left-associativeだとか, λx.の後は可能な限り関数と見るとか
つまり λx.tx = λx.(t x) はinput : yを t にapplyするから, yをinputしたら t y と同じってこと.
Chapter 3 10/21
急に free variableとかいう言葉が出てくるが, これもwikiに定義が乗っているので見ましょう.
Lemmaは, 対< - , - >が含まれている時がなんとなく微妙.
Corは一瞬意味が不明だが, tのtypeを帰納的に導き出してそこに出てくるatomic typeを洗い出したものの全体と, free valの属するatomic typeの全体がstrictな包含関係にあるとき, みたいな仮定である. これも対< - , - >が微妙.
ところでvariableのtypeは別になんでもありうる. たとえば当たり前だが関数を引数にとる関数のvariableのtypeは$ U \to Vみたいな形になっている.
Chapter 4 10/28
Church-Rosser Propertyは別にそこまでめんどくさい証明ではないのでwikiでも見ると良いと思う
ケーニヒの補題 : Gを無限個の点からなる連結グラフで全ての点の次数は有限(すなわちどの点も他の有限個の点としか接続していない)とする. このとき, Gは無限長の単純道(同じ点を2度通らない道)を持つ.
最後のはこれの対偶で明らか.
Chapter 5 11/1
とにかく丁寧に読めば問題ないはず. 流し読みとか横着しないで読みましょう.
左より右のが強いとはつまり、左のAで右のAをまかなえるという意味.
逆にCut Ruleは右にAがあれば左のAの役割を実質的にこなせるという意味で右の方が強いことをimplyしている
右Aと左Aを作る~~みたいな部分は、本当に丁寧に読めば既存のものに操作をして新しいものの全体をつくっているのだということがわかるはず
それより後は素直に書いてある通り. Cut-freeならnormalな演繹へとconvertできるが, べつにCutが入っててもnormalになることはある.
Chapter 6 11/8
$ \nu(t)についてのinductionを回すとき, strong-normalisation-theoremをまだ示していないから, ”下から”証明を回さないといけないことに注意. 横着して"減らしていくといつか正規形になります"みたいなことはできない
一番最後の証明は逐次代入と同時代入が一緒かどうかかなり怪しい. けれど実はpropositionの"XにXを代入する"場合だけならば逐次代入は同時代入と変わらないことがわかって, なのですべてのtermはreducibleがいえる. これでヤバそうな場合でも上からぶん殴る形で$ \lambda y.wのreducibilityが言えていることになる
Chapter 7 11/29
面白い まあそうなってるよね 構築がえらい
ペアノの公理系もえらい
Chapter 8 12/6 12/13
圏論を知っておこう! 身も蓋もなさすぎる わたしは圏論がわからないです
8.1/8.5はへーそうなんだ~(?)といって飛ばすとして、他の内容はべつに難しいものではないのでふつうに理解するだけ
Chapter 9 12/20
構成が、えらい!
えらいです
Chapter 10 12/27
また未定義の単語が出てくる Principal premise はEliminationでEliminateされた論理記号が使われている仮定のことです
で、"BAD"だと言われているルールはこのPrincipal premiseが結論と何の関係ももたない(つまり、Subformulaじゃない)から
10.3.1 Subformula property は仮定に"normal"が入っていることに注意 つまり"reduce"されうる部分がないので, 0回以上のIntroductionが行われたあと0回以上のEliminationが行われるという形でしかありえない(たぶん)。 EliminationのあとにIntroductionは入れないから
何回でもいうが、数学的には10.6.3のRuleを追加してはじめて「実質的に同じものとみなせる」。まあここら辺は構成よりも気持ちが先行しているので成立しろビームを撃ってもいいんだけど、ちゃんと詰めようと思ったらそこの気持ちと成立の可否は分けておいた方がいい気がする
Chapter 11 1/10 1/17
すげえ!!!!!!!!!!!!!!!!!! これ考え付いたやつ、天才らしいです
11.4とか死ぬほど大事なので、ちゃんと頭に叩き込んでください 手動かして計算して「マジじゃん」みたいになろう あるいはあなたが天才なら自明なのでやらなくていいです
typo発見した:ListWではなくWの場所がひとつある
Chapter12 2/9
Linearlisationの発想は自然で、Linearなやつの都合がいいならTraceの$ (a_0,\ \beta)の$ a_0の部分を集合一要素の集合だと思えばいーじゃん! みたいなね
それでうまくいってんだから何も言うことは無い……
Chapter 13 2/18
やったなこれ なんかこんな証明やった記憶ありませんか?
まあやっていることはかなり素直で、上へ上へ持っていけばいつか最上段にぶちあたってvanishするよねって話
最後らへんで言ってることは、Vanishするまえに公理-公理のpairにぶち当たると困るよねという話 だと思うんだが
Chapter 14 2/23
まあ 結論だけ飲んでも問題ないっちゃあない
結局この章のほとんどの内容は「Reducibility Candidatesについて当たり前に成り立って欲しい内容が成り立っているよね!」っていうことを、Reducibility Candidateの帰納的構成での特徴づけを介すことで証明して、そうすれば同様の議論が回りますよねと言っているにすぎない(証明じたいもぜんぶ簡単 実際にやってみるといいです)
Chapter 15 3/2
すべてを忘れた すまんが力尽きたので皆さん自力で読んでください
終わり!!!
総評
ある程度この分野(Type System /Type Theory)の知識があるといいですね ない場合は他の本を先に読もう!