曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。アマゾンアソシエイトやってまっせ。更新のお知らせはTwitter@cut_eliminationで

直観主義型理論

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ七「複数の仮定付の判断とコンテクスト」「集合とカテゴリー」(予習編)

他の直観主義型理論勉強会シリーズはこちらから。 複数の仮定付の判断とコンテクスト 複数の仮定付の判断の解釈 コンテクスト 代入 その他の判断 集合とカテゴリー カテゴリーとは(集合との違い) 単純型理論と分岐型理論と可述性 関数はプリミティブ デー…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ六「等号の規則」「仮定付判断と代入規則」(復習編)

お休みを挟んでこれの復習編。 等号の規則 これは導出可能規則と言ってもよさそうだけど、どうも導出体系ではないという点が重要そうなのでそうは言えない。特にカノニカルな要素を得る計算というのはあまりフォーマルに導入されていない。 が集合だと言って…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ伍「等号の規則」「仮定付判断と代入規則」(予習編)

今回は私の担当ではないのでゆるく。 等号の規則 前回は"equality"を「同等性」とか「等しさ」と訳していたけど、今回は「等号」という訳も使う。記号と考えたほうが「規則」という概念と相性がいいかと思い。「判断の形式の解釈」の節では「カノニカルナ要…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ四「判断の形式の解釈」「命題」(復習編)

予習編はこちら 「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ参「判断の形式の解釈」「命題」(予習編) - 曇りなき眼で見定めブログ 集合は型だと思ったほうがいいかも 3つの哲学 何がカノニカルな要素か? equality カノニカル…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ参「判断の形式の解釈」「命題」(予習編)

Per Martin-Löf, "Intuitionistic Type Theory", 1984の「判断の形式の解釈」「命題」の章を読んで訳したり考えたりしています。 判断の形式の解釈(Explanations of the forms of judgements) canonical、equality、computation 解釈とは 解釈と訳したのは…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弍「緒言」「命題と判断」(復習編)

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ壱「緒言」「命題と判断」(予習編) - 曇りなき眼で見定めブログ これの復習編です。 緒言 It is free from the deficiency of Russell's ramified theory of types, as regards the…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ壱「緒言」「命題と判断」(予習編)

Per Martin-Löfの"Intuitionistic Type Theory"(1984)、通称ITT84*1の勉強会の記録でござる。今回はとりあえず、最初の2節で読んでもわからなかったところをメモっときます。 個人的な動機 緒言(Introductory remarks) ロジックと数学の関係 ラッセルの型…