勉強会:【マルレク】型の理論入門
【マルレク】型の理論入門
■ 日時:2019/9/03 19:00ー22:00
■ 感想
→ 数年前では、全くわからなかった内容が
大分、わかるようになってきた → 継続は力
→ まだ、論理や整数論について
人に説明できるぐらいにわかるよう勉強が必要である
→ まずは、今、始めている形式理論、Haskell、Coqについて
最後までやりきる事が必要だと思っている
年末までの進捗を見て、今後の対策を考えたい
■ 開催・資料
(セミナ・メモ)
● 集合論の成立
・カントール
→ 順序数 → 無限の順序数ω
→ ω^ω → 可算回で辿り着く
→ ε0 → Cantor Nomal Form → ゲンツェンの数論の無矛盾性証明
→ 無限集合の要素の個数
→ 部分は全体と同じ数の要素を持つ → 1対1対応
→ 実数の個数は自然数の個数より大きい
→ 連続体仮説
→ 可算無限集合の濃度 → χ0
・集合論の矛盾
→ Cantorの集合概念とFregeの公理
→ Russellのパラドック
→ 自己参照的な定義
→ Russellの型理論
→ 直観主義・構成主義
● 証明可能性と計算可能性
・ヒルベルト・プログラム:数学の形式化と無矛盾性の試み
→ ゲーデルの不完全性定理
→ 計算可能性、証明可能性
→ 帰納関数論、ラムダ・カリキュラス、チューリング・マシン
→ チャーチ=チューリングのテーゼ
→ 証明可能性と計算可能性の同一性
● 新しい「型の理論」
・Curry-Howard対応
→ Curry → 型付ラムダ計算:直観主義論理
→ Howard → 論理式はラムダ計算の型
→ 「型」と「命題」、「要素」と「証明」 → 相対性
→ Propositions as Type → Proofs as Terms
→ 型の理論の記述
→ Martin-Löfの型理論
→ Dependent Type
→ Polymorpic関数
→ Inductive Type:帰納的型
● Univalent Foundation
・論理=数学的 a:Aの解釈
→ 集合論、構成主義、PAT、HoTT
→ 同一性の解釈
Path → 反射律、逆の道、道の結合
・Univalence Axiom
→ 構造主義の原理、統価原理、ライプニッツの原理
・UniMath
→ 数学の証明はコンピュータでチェックできるプログラム
→ プログラム停止問題
----+----+---
●「型の理論」入門
・型のないラムダ計算
→ 関数表記 → λ記法 → 抽象化
→ 関数の値の計算
→ 変数への値の代入、適用と代入、自由変数と束縛変数
・λ計算
→ α-conversion, β-reduction, η-conversion
・ラムダ計算への型の導入 → 型を持つラムダ計算は停止する → 正規オブジェクト → 型の計算ルールで値が決まる
・判断と論理式
→ 論理式と論理式の意味
→ 論理式の意味 → 判断
→ 証明 → 判断を明証なものにする → 直観主義
→ 知識と証明は同じ
・推論ルール Natural Deduction
・Curry-Howard対応
→ 「型」と「命題」、「要素」と「証明」との「双対性」
→ PAT:”Propositions as Types”, “Proofs as Terms”
→ ”Proof as Program”
・型の理論と証明の理論
・Calculus of Inductive Constructions
→ 数学的帰納法
→ Coq → Type と Prop と Set
以上