-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.pug
163 lines (145 loc) · 8.99 KB
/
index.pug
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
include header
html
head
meta(property='og:title' content='LAURENT')
meta(property='og:description' content='Analytical Type Theory')
meta(property='og:url' content='https://laurent.groupoid.space/')
block title
title LAURENT
block content
nav
<a href='#'>LAURENT</a>
<a href='https://laurent.groupoid.space/mathematics/tutorial/'>TUTORIAL</a>
article.main
.exe
section
h1 ANALYTICAL TYPE SYSTEM
aside
time Published: 28 FEB 2025 LOSAR
+tex.
MLTT-72 based Type Theory for mechanical formalization
of Théorie des Distributions and Analyse Mathematique
by Laurent Schwartz and Foundation of Constructive Analysis by Errett Bishop.
+tex.
We omit identity types Id, idp, J (HoTT, MLTT-80, MLTT-75) to keep
the system lean with Pi and Set truncated Sigma relying instead on
Prop predicates. Also we have explicitly built in set theory with
open sets and topology to have more classical core.
Built-in inequalities propositional resolution by reduction
is handled by external Z3 SMT solver.
section
.macro
.macro__col
h3#hts <b>MLTT</b>
ol
li: a(href='https://laurent.groupoid.space/foundations/prop/') PROP
li: a(href='https://laurent.groupoid.space/foundations/universe/') U<sub>0</sub> : U<sub>1</sub>
li: a(href='https://laurent.groupoid.space/foundations/forall/') FORALL
li: a(href='https://laurent.groupoid.space/foundations/exists/') EXISTS
li: a(href='https://laurent.groupoid.space/foundations/and/') AND
li: a(href='https://laurent.groupoid.space/foundations/or/') OR
li: a(href='https://laurent.groupoid.space/foundations/real/') REAL
.macro__col
h3#mltt <b>SET</b>
ol
li: a(href='https://laurent.groupoid.space/foundations/set/') SET
li: a(href='https://laurent.groupoid.space/foundations/seteq/') EQ<sub><b>Z3</b></sub>
li: a(href='https://laurent.groupoid.space/foundations/complement/') \
li: a(href='https://laurent.groupoid.space/foundations/intersect/') INTERSECT
li: a(href='https://laurent.groupoid.space/foundations/closure/') CLOSURE
li: a(href='https://laurent.groupoid.space/foundations/power/') POWER
li: a(href='https://laurent.groupoid.space/foundations/quotient/') QUOTIENT
.macro__col
h3#mltt <b>CALC</b>
ol
li: a(href='https://laurent.groupoid.space/foundations/seq/') SEQ
li: a(href='https://laurent.groupoid.space/foundations/inf/') INF
li: a(href='https://laurent.groupoid.space/foundations/sup/') SUP
li: a(href='https://laurent.groupoid.space/foundations/limit/') LIMIT
li: a(href='https://laurent.groupoid.space/foundations/sum/') SUM
li: a(href='https://laurent.groupoid.space/foundations/union/') UNION
li: a(href='https://laurent.groupoid.space/foundations/measure/') MEASURE
li: a(href='https://laurent.groupoid.space/foundations/lebesgue/') LEBESGUE
li: a(href='https://laurent.groupoid.space/foundations/bochner/') BOCHER
br
br
+tex.
$\mathbf{Installation}$.
+tex.
The $\text{Laurent}$ doesn't have proper syntax yet,
that's said you use it as OCaml framework
working in pure AST as you would do in Lisp.
+code.
$ git clone \
[email protected]:groupoid/laurent
$ opam install z3
$ ocamlfind ocamlc -o laurent \
-package z3 -linkpkg src/laurent.ml
section
h1 SYNTAX
+tex(true).
$$
\begin{array}{c} \\
\mathrm{Laurent} := \mathrm{MLTT}\ |\ \mathrm{Base}\ |\ \mathrm{Set}\ |\ \mathrm{Q}\ |\ \mathrm{Mu}\ |\ \mathrm{Lim} \\
\mathrm{MLTT} := \mathrm{cosmos}\ |\ \mathrm{var}\ |\ \mathrm{forall}\ |\ \mathrm{exists}\ \\
\\
\mathrm{cosmos} := \mathbf{Prop}\ :\ \mathbf{U_0}\ :\ \mathbf{U_1} \\
\mathrm{var} := \mathbf{var}\ \mathrm{ident}\ |\ \mathbf{hole} \\
\mathrm{forall} := \forall\ \mathrm{ident}\ \mathrm{E}\ \mathrm{E}\ |\ \lambda\ \mathrm{ident}\ \mathrm{E}\ \mathrm{E}\ |\ \mathrm{E}\ \mathrm{E} \\
\mathrm{exists} := \exists\ \mathrm{ident}\ \mathrm{E}\ \mathrm{E}\ |\ (\mathrm{E}, \mathrm{E})\ |\ \mathrm{E}\mathbf{.1}\ |\ \mathrm{E}\mathbf{.2} \\
\mathrm{Base} := \mathbf{ℕ}\ |\ \mathrm{ℤ}\ |\ \mathrm{ℚ}\ |\ \mathrm{ℝ}\ |\ \mathrm{ℂ}\ |\ \mathrm{ℍ}\ |\ \mathrm{𝕆}\ |\ \mathrm{𝕍}\ \\
\mathrm{Set} := \mathbf{Set}\ |\ \mathbf{SeqEq}\ |\ \mathbf{And}\ |\ \mathbf{Or}\ \\
|\ \mathbf{Complement}\ |\ \mathbf{Intersect}\ \\
|\ \mathbf{Power}\ |\ \mathbf{Closure}\ |\ \mathbf{Cardinal}\ \\
\mathrm{Q} := \mathbf{-/\hspace{-1mm}\sim}\ |\ \mathbf{Quot}\ |\ \mathbf{Lift_Q}\ |\ \mathbf{Ind_Q} \\
\mathrm{Mu} := \mathbf{Mu}\ |\ \mathbf{Measure}\ \\
|\ \mathbf{Lebesgue}\ |\ \mathbf{Bochner}\ \\
\mathrm{Lim} := \mathbf{Seq}\ |\ \mathbf{Sup}\ |\ \mathbf{Inf}\ \\
|\ \mathbf{Limit}\ |\ \mathbf{Sum}\ |\ \mathbf{Union}\ \\
\\
\end{array}
$$
h1 SEMANTICS
br
h2 MLTT
+tex.
$\mathbf{Definition\ 1.3.1}$ ($\forall$-Formation, Dependent Product).
$\forall$-types represents the way we create the spaces of dependent functions $f: \forall\ (x:A), B(x)$
with domain in $A$ and codomain in type family $B : A \rightarrow U$ over $A$.
+tex(true).
$$
\forall : U_0 =_{def} \prod_{A:U}\prod_{x:A}B(x).
$$
+tex.
$\mathbf{Definition\ 1.4.1}$ ($\exists$-Formation, Dependent Sum). The dependent sum
type is indexed over type $A$ in the sense of coproduct or disjoint union,
where only one fiber codomain $B(x)$ is present in pair.
+tex(true).
$$
\exists : Prop =_{def} || \prod_{A:U}\sum_{x:A} B(x) ||_0.
$$
section
h1 Bibliography
br.
section
h2 ANALYSIS
p.
[1]. L.Schwartz. Analyse Mathematique (1967)<br>
[2]. E.Bishop. <a href="https://archive.org/details/foundationsofcon0000bish">Foundations of Constructive Analysis</a> (1967)<br>
[3]. D.Bridges. <a href="https://core.ac.uk/download/pdf/82492373.pdf">Constructive mathematics: a foundation for computable analysis </a> (1999)<br>
[4]. W.Ziemer, M.Torres. <a href="https://www.math.purdue.edu/~torresm/pubs/Modern-real-analysis.pdf">Modern Real Analysis </a> (2017)<br>
[5]. A.Booij. <a href="https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf">Analysis in Univalent Type Theory</a> (2020)<br>
[6]. Z.Murray. <a href="https://arxiv.org/pdf/2205.08354">Constructive Real Numbers in the Agda</a> (2023)<br>
+tex(true).
<br>
$$
\int
$$
<br><br>
+tex.
Присвячується Володимиру Олександровичу Клименку.
Механізована верифікація теорем функціонального аналізу
і теорії розподілів Лорана Шварца
у власній теорії типів на основі MLTT-72.
Повторна магістерська робота.
include footer