型理論 - mrsekut-p

型理論

type theory

階型理論とも言う

型に関する性質を論ずる形式的体系、またそれによる型付けの規則

数理論理学の一分野

計算機科学よりも歴史が古い

型理論の歴史

以下より構成される

型付け規則(推論規則)

predicativeな型理論

正しいとわかっている型から推論規則を繰り返し用いて得られる型のみを扱う型理論

ITT nなど

inpredicativeな型理論

超越的な型の構成も許す型理論

ex. 型上を動く変数の全称束縛を許す型

わからんmrsekut.icon

参考

龍田『型理論』

http://www.scholarpedia.org/article/Computational_type_theory

https://plato.stanford.edu/entries/type-theory/

Bertrand Russell

https://www.jstage.jst.go.jp/article/jssst/5/1/5_1_98/_article/-char/ja