勉強会【マルレク】プログラムと論理
【マルレク】プログラムと論理
■ 日時:2019/10/10 19:00ー22:00
■ 感想
→ 今、興味を持って一番勉強している論理学とプログラムの話
Coqを始めに「マルレク」の中心テーマに成るらしい
→ Coqや論理学、型付関数論の基本を勉強しながら
他の勉強会と併せて学習を進めていきたい
■ 開催・資料
- 講演資料
(セミナ・メモ)
● 第一部 計算と論理 20世紀
・型付ラムダ計算と論理
→ Curry-Howard 対応
→ ラムダ計算の関数型 論理式の合意
→ 型付λ式の型の定義:論理式の三段論法
→ 「型」と「命題」、「要素」と「証明」
→ 証明は型を持つ
・Dependent Type と論理
→ Martine-Los 論理的な命題も型である
→ Polymorphic 型に依存して型が決まる → vec(ベクトル)
→ Indutive Type 帰納的型 → nat(自然数)
→ 同一性の型
・証明とは何か?
→ 命題 a → b の証明
→ 命題:aの証明から命題:bに変換する方法
→ a:A の解釈
→ 集合論、構成主義、PAT、型の理論、HoTT
・PAT:"Propsitions as Types" "Proofs as Terms"
・証明支援システム Coq
→ ソフトウェア基礎科学の普遍言語(Ligua Franca)
● 第二部 プログラムと論理 20世紀
・形式手法
→ Hoare - Hoare Logic
→ P {Q} R → 事前状態{プログラム}事後状態
→ Dikstra - Nondeterminacy
→ Pで必要である条件 → wp(S,R) → guard
→ Lamport - Temporal Logic
→ 時性理論
・証明の性質をめるる論争
→ 数学者 →
→ 社会的プロセス
・形式手法の後退
→ Hoare
→ Lamport
● 第三部 21世紀の形式手法
・Deep Specification と証明システム Coq
-- 形式手法の’Lingua Franca
→ Deep Specification → rich, two-side, formal, live
・形式的推論・証明サンプル
-- Hoare Logic の三組の証明
・Deep Specification における仕様と実装例
-- Kami プロジェクトを例に
・Software Foundation
以上