-
Notifications
You must be signed in to change notification settings - Fork 11
/
Copy pathindex.html
233 lines (227 loc) · 9.13 KB
/
index.html
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
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
<html>
<head>
<meta charset="utf-8" />
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<meta name="description" content="" />
<meta name="author" content="Maxim Sokhatsky" />
<link href="https://fonts.googleapis.com/css?family=Montserrat:900" rel="stylesheet">
<title>AXIO/8.0</title>
<link rel="stylesheet" href="https://n2o.dev/blank.css" />
</head>
<body>
<nav>
<a style="background-color:#00C2E7;color:white;" href='https://groupoid.space/institute/index.htm'>Groupoїd Infinity</a>
</nav>
<header>
<h1 style="border:0;color:#01C2E7;margin-right:20px;">AXIO</h1> <h1 style="color:PaleVioletRed;">8.0</h1>
</header>
<aside>
<article>
<section>
<h3>SYNOPSIS</h3>
<div>Groupoїd Infinity fibrational type systems for
mathematical representation, certification (theorem proving),
with extraction to verified interpreter and its runtime.<br><br></div>
<div>2016—2024 © <a href="https://5ht.co/license/">ISC</a>
<br><br></div>
</section>
<section>
<h3>NOTES</h3>
<div>The main research product is an AXIO/1 formal runtime that is
able to run simple typed lambda programs on verifiable interpreter Joe.
But nobody can limit one developing their own higher languages with
extraction to that interpreter. In order to keep that process in one place
under cathedral type of open source software management proceess — the AXIO/1 appears.<br><br>
AXIO/1 consists of runtime and its languages Joe, Alice, Bob for software constructions that are using Standard ML like syntax;
and higher languages and its extractors to runtime Alonzo, Henk, Per, Anders for theorem proving
that are using Lean like syntax.
</div>
</section>
</article>
</aside>
<main>
<section>
<p></p>
</section>
<section>
<hr>
</section>
<section>
<p>Verified Lambda Interpreter and Concurrent Parallel Matrix Runtime.
Joe, Bob, and Alice languages share the same Standard ML like BNF grammar.</p>
</section>
<section>
<a name=Joe></a>
<h3><a href="https://github.com/groupoid/joe">Joe</a></h3>
<p><b style="sel">Joe</b> is a certified bytecode stack interpreter and Intel/ARM code compiler.</p>
<P>[1] — MinCaml<br>
[2] — CoqASM<br>
[3] — Verified LISP Interpreter<br>
[4] — Kind<br>
</p>
<figure><code>
fun a (0, n) = n + 1
| a (m, 0) = a (m - 1, 1)
| a (m, n) = a (m - 1, a (m, n - 1))
</code></figure>
</section>
<section>
<a name=Bob></a>
<h3><a href="https://github.com/o83/n2o">Bob</a></h3>
<p><b style="sel">Bob</b> is a parallel concurrent non-blocking
zero-copy run-time with CAS cursors [4,5].</p>
<P>[5] — Kernel<br>
[6] — Pony<br>
[7] — Erlang<br></p>
<figure><code>
fun proc =
let val p0 = pub(0,8)
val s1 = sub(0,p0)
val s2 = sub(0,p0)
in send(p0,11);
send(p0,12);
[ receive(s1);
receive(s2);
receive(s1);
receive(s2)
]
end
</code></figure>
</section>
<section>
<a name=Alice></a>
<h3><a href="https://tonpa.guru/stream/2023/2023-09-25%20Formal%20Tensor.htm">Alice</a></h3>
<p><b style="sel">Alice</b> is a linear types calculus
with partial fractions [6] for BLAS level 3 programming.</p>
<P>[8] — NumLin<br> </p>
<figure><code>
fun simpleConvolution (i n: int) (x0: float) (write w: vector float)
: vector float
= begin
if n = i then result.emit(write),
a = [w0,w1,w2] = w.get(0,3),
b = [x0,x1,x2] = [ x0 | write.get(i,2) ],
write.set(i, Dotp(a,b)),
simpleConvolution((i + 1),n,x1,write,w)
end
</code></figure>
</section>
<section>
<hr>
</section>
<section>
<p>Sound and Consistent Predicative Formal Languages.
Alonzo, Henk, Per, Anders languages share the same Lean like BNF grammar.</p>
</section>
<section>
<a name=Alonzo></a>
<h3><a href="https://github.com/groupoid/alonzo">Alonzo</a></h3>
<p><b style="sel">Alonzo</b> is an STLC-40 type system as example of core
calculus discovered before fibrational ΠΣ provers.</p>
<p>
STLC-40 — Simple Theory of Types<br>
</p>
<figure><code>
def zero : (T → T) → T → T := λ (s: T → T) (z: T), z
def succ : ((T → T) → T → T) → ((T → T) → T → T)
:= λ (w: (T → T) → T → T) (y: T → T) (x: T), y (w y x)
</code></figure>
</section>
<section>
<a name=Henk></a>
<h3><a href="https://github.com/groupoid/henk">Henk</a></h3>
<p><b style="sel">Henk</b> is a Pure Type System (PTS-91) in
the style of Coquand/Huet Calculus of Inductive Constructions (CoC-88)
with infinite numbere of universes. Henk also supports AUTOMATH syntax (AUT-68).</p>
<p>
AUT-68 — AUTOMATH<br>
CoC-88 — Calculus of Constructions<br>
PTS-91 — Pure Type System (Π)<br>
</p>
<figure><code>
def N := Π (A : U), (A → A) → A → A
def zero : N := λ (A : U) (S : A → A) (Z : A), Z
def succ : N -> N := λ (n : N) (A : U) (S : A → A) (Z : A), S (n A S Z)
def plus (m n : N) : N := λ (A : U) (S : A → A) (Z : A), m A S (n A S Z)
def mult (m n : N) : N := λ (A : U) (S : A → A) (Z : A), m A (n A S) Z
def pow (m n : N) : N := λ (A : U) (S : A → A) (Z : A), n (A → A) (m A) S Z
</code></figure>
</section>
<section>
<a name=Per></a>
<h3><a href="https://github.com/groupoid/per">Per</a></h3>
<p><b style="sel">Per</b> is a ΠΣ (MLTT-72) prover with Calculus of
Inductive Constructions and idenitity types (MLTT-75). The natural
extension of CoC to CIC was done by Frank Pfenning and Christine Paulin (IND-89).</p>
<p>
Mini-TT — OCaml implementation<br>
MLTT-72 — Pi, Sigma<br>
MLTT-75 — Pi, Sigma, Id<br>
MLTT-80 — 0, 1, 2, W, Pi, Sigma, Id<br>
PP-89 — Inductively Defined Types<br>
CIC-2015 — Calculus of Inductive Constructiions<br>
</p>
<figure><code>
def empty : U := inductive { }
def L¹ (A : U) : U := inductive { nil | cons (head: A) (tail: L¹ A) }
def S¹ : U := inductive { base | loop : Equ S¹ base base }
def quot (A: U) (R : A -> A -> U) : U
:= inductive { quotient (a: A)
| identification (a b: A) (r: R a b)
: Equ (quot A R) (quotient a) (quotient b)
}
</code></figure>
</section>
<section>
<a name=Anders></a>
<h3><a href="https://github.com/groupoid/anders">Anders</a></h3>
<p><b style="sel">Anders</b> is a Homotopy Type System (HTS-2013)
with Strict Equality and Cubical Agda (CCHM-2016) primitives.</p>
<p>
HTS-2013 — Homotopy Type System<br>
BCH-2014 — Cubical Sets<br>
CCHM-2015 — Cubical Type System<br>
OP-2016 — Topos Axioms<br>
CHM-2017 — Huber Equations<br>
VMA-2017 — Cubical Agda<br>
</p>
<figure><code>
def idfun (A : U) : A → A := λ (a : A), a
def idfun′ (A : U) : A → A := transp (<i> A) 0
def idfun″ (A : U) : A → A := λ (a : A), hcomp A 0 (λ (i : I), []) a
def isFiberBundle (B: U) (p: B → U) (F: U): U
:= Σ (v: U) (w: surjective v B), (Π (x: v), PathP (<_>U) (p (w.1 x)) F)
def ~~ (X : U) (a x′ : X) : U := Path (ℑ X) (ι X a) (ι X x′)
def 𝔻 (X : U) (a : X) : U := Σ (x′ : X), ~~ X a x′
def unitDisc (X : U) (x : ℑ X) : U := Σ (x′ : X), Path (ℑ X) x (ι X x′)
def starDisc (X : U) (x : X) : 𝔻 X x := (x, idp (ℑ X) (ι X x))
def T∞ (A : U) : U := Σ (a : A), 𝔻 A a
def inf-prox-ap (X Y : U) (f : X → Y) (x x′ : X) (p : ~~ X x x′)
: ~~ Y (f x) (f x′) := <i> ℑ-app X Y f (p @ i)
def d (X Y : U) (f : X → Y) (x : X) (ε : 𝔻 X x) : 𝔻 Y (f x)
:= (f ε.1, inf-prox-ap X Y f x ε.1 ε.2)
def T∞-map (X Y : U) (f : X → Y) (τ : T∞ X) : T∞ Y
:= (f τ.1, d X Y f τ.1 τ.2)
def is-homogeneous (A : U)
:= Σ (e : A) (t : A → equiv A A),
Π (x : A), Path A ((t x).1 e) x
</code></figure>
</section>
<section>
<a name=Urs></a>
<h3><a href="https://github.com/groupoid/CCHM">Urs</a></h3>
<p><b style="sel">Urs</b> is an equivariant superhomotopy type system
with fermion and boson modalities built-in into type checker.
</p>
<p>
R-HoTT — Rezk Infinity Categories<br>
G-HoTT — Guarded Cubical<br>
L-HoTT — Linear HoTT<br>
ES-HoTT — Equivariant Super HoTT<br>
</p>
</section>
</main>
<footer> <br><br> Groupoїd Infinity <span class=red> ❤ </span> 2016—2024</footer>
</body>
</html>