みぞメモ

ブログ作成用のメモ登録

勉強会:【マルレク】型の理論入門

【マルレク】型の理論入門

■ 日時:2019/9/03 19:00ー22:00
■ 感想

 → 数年前では、全くわからなかった内容が
   大分、わかるようになってきた → 継続は力
 → まだ、論理や整数論について
   人に説明できるぐらいにわかるよう勉強が必要である
 → まずは、今、始めている形式理論、Haskell、Coqについて
   最後までやりきる事が必要だと思っている
   年末までの進捗を見て、今後の対策を考えたい

■ 開催・資料

type-theory.peatix.com

www.marulabo.net


セミナ・メモ)

集合論の成立

カントール
 → 順序数 → 無限の順序数ω
   → ω^ω → 可算回で辿り着く
   → ε0 → Cantor Nomal Form → ゲンツェンの数論の無矛盾性証明
 → 無限集合の要素の個数
   → 部分は全体と同じ数の要素を持つ → 1対1対応
 → 実数の個数は自然数の個数より大きい
 → 連続体仮説
   → 可算無限集合の濃度 → χ0

集合論の矛盾
 → Cantorの集合概念とFregeの公理
 → Russellのパラドック
   → 自己参照的な定義
   → Russellの型理論
 → 直観主義構成主義

● 証明可能性と計算可能性

ヒルベルト・プログラム:数学の形式化と無矛盾性の試み
 → ゲーデル不完全性定理
   → 計算可能性、証明可能性
     → 帰納関数論、ラムダ・カリキュラス、チューリング・マシン
     → チャーチ=チューリングのテーゼ
     → 証明可能性と計算可能性の同一性

● 非カントール集合論の発見

連続体仮説集合論の独立性

・非カントール集合論
 → Tops Teory

● 新しい「型の理論」

・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

以上