-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.tex
83 lines (61 loc) · 3.37 KB
/
main.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
\documentclass[book]{jlreq}
\usepackage{makeidx}
\usepackage{bussproofs}
\usepackage{color}
\usepackage[colorlinks]{hyperref}
\title{Intheo の型理論}
\author{Hexirp}
\makeindex
\def\——{—\kern-.5\zw—\kern-.5\zw—}
\newcommand{\bidash}{\——}
\newcommand{\CIC}{\textsf{CIC}}
\newcommand{\Type}{\mathrm{Type}}
\newcommand{\Level}{\mathrm{Level}}
\newcommand{\suc}{\mathrm{suc}}
\begin{document}
\frontmatter
\maketitle
Intheo は、純粋関数型プログラミング言語です。そして、カリー・ハワード対応を利用して定理を証明することも
可能です。となれば、どのような型理論に基づいているのかという疑問は当然です。この文書は、その疑問に答える
でしょう。
Intheo がベースとする型理論は、 Coq が基礎とする帰納的構造の計算~\cite{cic} と、方形的型理論~\cite{cutt} と、
数量的型理論~\cite{qtt} の三つを一まとめにしたものです。
Intheo の設計原理\bidash{}全てを、可能な限り明確に行う\bidash{}は、それが基礎とする型理論にも適用されます。
この型理論における型判定は、 \( Γ \vdash x : T \) の一つしかありません。そして、ある空から推論可能な
型判定 \( Γ \vdash x : T \) は、それを導く推論木と一対一対応します\bidash{}つまり、ある項は、それの
型が表す命題を証明する方法を一意に表しています。
\tableofcontents
\mainmatter
\part{帰納的構造の計算}
\index{きのうてきこうぞうのけいさん@帰納的構造の計算}帰納的構造の計算は、構造の計算に帰納型を追加した体系です。
かなり強力な表現力を持っていて、噂では \( \textsf{ZFC} + \textrm{``There are countably many inaccessible
cardinals.''} \) と同じ無矛盾性を持つとか言われています。
「帰納的構造の計算」は、 \index{Calculus of Inductive Constructions}``Calculus of Inductive Constructions'' を
日本語に直訳した言葉です。これは \index{CIC@\( \CIC \)}\( \CIC \) とも略されます。
帰納的構造の計算には、\index{うちゅうかいそう@宇宙階層}宇宙階層が必要になります。これは、確か帰納型を含むことへの
対価だったはずです。
\index{Type@\( \Type \)}\( \Type \) は、一般的な型を表す記号です。 \index{Level@\( \Level \)}\( \Level \) は
宇宙レベルの型を表す記号です。 \( i : \Level \) である時 \( \Type _ {i} \) と書き、これが一般的な形です。
\begin{figure}[h]
\centering
\begin{prooftree}
\AxiomC{\( \)}
\UnaryInfC{\( i : \Level \vdash \Type _ {i} : \Type _ {\suc ( i )} \)}
\end{prooftree}
\caption{\( \Type _ {i} \) の型}
\label{cic-type-type}
\end{figure}
\backmatter
\begin{thebibliography}{99}
\bibitem{cic}
Inria, CNRS, and contributors.
\href{https://coq.github.io/doc/v8.13/refman/language/cic.html}{\textit{Typing rules --- Coq 8.13.2 documentation}}.
\bibitem{cutt}
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg.
\textit{Cubical Type Theory: a constructive interpretation of the univalence axiom}.
\bibitem{qtt}
Robert Atkey.
\href{https://bentnib.org/quantitative-type-theory.html}{\textit{The Syntax and Semantics of Quantitative Type Theory}}.
\end{thebibliography}
\printindex
\end{document}