-
Notifications
You must be signed in to change notification settings - Fork 8
/
Copy pathType2Logic.tex
executable file
·122 lines (81 loc) · 5.31 KB
/
Type2Logic.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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
\section{从类型到逻辑}
本文只介绍简单类型$\lambda$演算(STLC)的Curry-Howard同构。在后续发展中，研究人员陆续提出了System F，构造演算等
\subsection{回顾}
我们重新梳理一下$\lambda$演算相关内容，首先是无类型$\lambda$演算。
$$E, F ::= x \ | \ \lambda x.E \ | \ (E F) \ | \ ...$$
然后是简单类型$\lambda$演算。注意，为了表述方便，本节采用和前文略有不同的记法
$$\sigma, \tau ::= \beta \ | \ \sigma \to \tau$$
$$E, F ::= x \ | \ \lambda x : \sigma . E \ | \ E F \ | \ ...$$
定型规则如下：
\begin{prooftree}
\AxiomC{$x : \sigma \in \Gamma$}
\LeftLabel{VAR}
\UnaryInfC{$\Gamma \vdash x : \sigma$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Gamma, x : \sigma \vdash E : \tau$}
\LeftLabel{ABS}
\UnaryInfC{$\Gamma \vdash (x : \sigma . E) : (\sigma \to \tau)$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\Gamma \vdash E : \sigma \to \tau$}
\AxiomC{$\Gamma \vdash F : \tau$}
\LeftLabel{APP}
\BinaryInfC{$\Gamma \vdash E F : \tau$}
\end{prooftree}
\subsection{$\lambda$ Cube概述}
\begin{center}
\xymatrix@!0{
& \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
& & \lambda P\omega \ar@{-}[dd]
\\
\lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
& & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
\\
& \lambda\underline\omega \ar@{-}'[r][rr]
& & \lambda P\underline\omega
\\
\lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
& & \lambda P \ar@{-}[ur]
}
\end{center}
$$K ::= \star \ | \ \Box \ | \ K \to K$$
$$T, U ::= V \ | \ S \ | \ T U \ | \ \lambda V : T.U \ | \ \Pi V : T.U$$
\begin{itemize}
\item Type polymorphism（项依赖于与类型，$\Box \to \star$），如System F，由Girard和Reynolds提出。
\item Type constructors（类型依赖于类型，$\Box \to \Box$）
\item Dependent types（类型依赖于项，$\star \to \Box$）
\end{itemize}
\begin{table}[!htb]
\centering
\caption{Eight systems}
\begin{tabular}{|c|c|c|}
\hline
类型系统 & 关系 & 例 \\ \hline
$\lambda_{\to}$ & $\star \to \star$ & STLC \\ \hline
$\lambda_2$ & $\star \to \star, \Box \to \star$ & System F \\ \hline
$\lambda _{\underline \omega}$ & $\star \to \star, \Box \to \Box$ & Weak $\lambda_{\omega}$ \\ \hline
$\lambda_{\omega}$ & $\star \to \star, \Box \to \star, \Box \to \Box$ & System $\text{F}_{\omega}$ \\ \hline
$\lambda P$ & $\star \to \star, \star \to \Box$ & LF \\ \hline
$\lambda P_2$ & $\star \to \star, \star \to \Box, \Box \to \star$ & $\lambda P_2$ \\ \hline
$\lambda P_{\underline \omega}$ & $\star \to \star, \star \to \Box, \Box \to \Box$ & Weak $\lambda P_{\omega}$ \\ \hline
$\lambda P_{\omega}$ & $\star \to \star, \Box \to \star, \star \to \Box, \Box \to \Box$ & CoC \\ \hline
\end{tabular}
\end{table}
\subsection{依赖类型}
\subsection{归纳构造演算和Coq}
\subsection{语义意义下的同构}
\begin{table}[!htb]
\centering
\caption{My caption}
\begin{tabular}{|l|l|l|}
\hline
\textbf{Logic} & \textbf{Type System} & \textbf{Category Theory} \\ \hline
\begin{tabular}[c]{@{}l@{}}Intuitionistic \\ Propositional Logic\end{tabular} & \begin{tabular}[c]{@{}l@{}}Simple Types\\ Lambda Calculus\end{tabular} & Cartesian Closed Category \\ \hline
\begin{tabular}[c]{@{}l@{}}Second order \\ Intuitionistic Logic\end{tabular} & System F & \\ \hline
Classic Linear Logic & Linear Type System & Star-autonomous Category \\ \hline
& \begin{tabular}[c]{@{}l@{}}Extensional Dependent \\ Type Theory\end{tabular} & \begin{tabular}[c]{@{}l@{}}Locally Cartesian \\ Closed Category\end{tabular} \\ \hline
& \begin{tabular}[c]{@{}l@{}}Homotopy Type Theory \\ without Univalence\end{tabular} & \begin{tabular}[c]{@{}l@{}}Locally Cartesian Closed\\ $(\infty, 1)$-Category\end{tabular} \\ \hline
... & ... & ... \\ \hline
\end{tabular}
\end{table}