-
Notifications
You must be signed in to change notification settings - Fork 11
/
Copy pathindex.pug
160 lines (146 loc) · 12.6 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
include header
html
head
meta(property='og:title' content='FORMAL/1')
meta(property='og:description' content='Formal One')
meta(property='og:url' content='https://groupoid.github.io/formal.one/')
block title
title AXIO/1
block content
+header('', 'AXIO/1', 'Формальне середовище виконання, система вищих мов та базові бібліотеки для програмування, доведення теорем і формальної філософії')
article.main
.om
section
h1 Анотація
aside <a href="https://tonpa.guru">Максим Сохацький</a>
time 9 SEP 2021
p.
Перша формальна система AXIO/1 визначає формальний підхід до математичної
верифікації та описує спробу автора у цій парадигмі побудувати
замкнену уніфіковану систему формальних мов для програмування,
математики та філософії. В процесі розробки моделі такої
системи автору довелося апробувати частини її імплементації
для головних SML-подібних формальних академічних мов, мови
Erlang та інших (загалом 7 мов). За 10 років автором було
проаналізовані синтаксис та семантика основних мов програмування
(більше 50 мов) з різних промислових та академічних доменів,
8 мов з яких були особисто реалізовані автором. В роботі описані
8 мов уніфікованої мовної системи (концептуальна модель)
та представлені 2 їх імплементації.
p.
Головним чином, натхнення було почерпнуте з LISP-машин
минулого, APL-систем, перших систем доведення теорем таких
як AUTOMATH, віртуальних маших паралельної та узгодженої
обробки нескінченних процесів, таких як BEAM, та кубічних MLTT-пруверів.
section
h1 СТРУКТУРА
p.
Суть роботи полягає в побудові унікальної замкненої си-
стеми яка складається з:
1) системного програмного забезпечення – модального середовища
виконання разом з інтерпретатором написаним на формальній мові;
2) бібліотека та архітектура прикладного програмування N2O.TECH для середовищ виконання;
3) прикладного програмного забезпечення — системи вищих формальних мов,
для яких надано моделі, імплементації;
4) базова бібліотека разом з математичними компонентами (програми на вищих мовах).
h2 Середовище виконання
.index
.index__col
h2 Ядро
ul
li: a(href='https://groupoid.space/runtime/cps/') Інтерпретатор
li: a(href='https://groupoid.space/runtime/apl/') Тензори
li: a(href='https://groupoid.space/runtime/intercore/') Планувальник
li: a(href='https://anders.groupoid.space/foundations/modal/process/') Процеси
.index__col
h2 Бібліотека
ul
li: a(href='https://groupoid.space/runtime/effects/') Протоколи
li: a(href='https://anders.groupoid.space/foundations/mltt/io/') IO
li: a(href='https://anders.groupoid.space/foundations/mltt/ioi/') IOI
h2 Вищі мови програмування
.index
.index__col
h2 Ядро PTS/PTS/MLTT
ul
li: a(href='https://henk.groupoid.space') Чисте-ядро
li: a(href='https://groupoid.space/misc/semantics/') Фібраційне-ядро
.index__col
h2 HTS/CCHM і Бібліотека
ul
li: a(href='https://anders.groupoid.space/') Гомотопічне ядро
li: a(href='https://groupoid.space/misc/library/') Математичні компоненти
li: a(href='https://groupoid.space/misc/course/') Курс по теорії типів
li: a(href='https://anders.groupoid.space/mathematics/homotopy/hopf/') Розшарування хопфа
.om
section
h1 Середовище виконання
p.
Синтансичне дерево мови інтерпретатора містить модуль лінивих
відкладених обчислень (CPS), та розширення синтаксичного
дерева спеціальними командами пов’язаними з середовищем
виконання (управління процесами виконання).
Програми таких інтерпретаторів виконуються у певній пам’яті,
яка використовується як контекст виконання. Кожна така програма
виконується як атомарний поток інструкцій на одному ядрі фізичного процесора.
Ситема віртуальних процесів містить SMP/AMP планувальник, який
управлє CPS-програмами які виконують інтерпретатори на кожному з фізичних ядер процесора.
p.
Мотивація для побудови інтерпретатору, який повністю розміщується
разом з программою в L1 кеші (який лімітований 64КБ-256КБ) базується
на успіху таких віртуальних машин як LuaJIT, V8, HotSpot,
а також векторних мов програмування типу К та J. Якби ми могли
побудувати дійсно швидкий інтерпретатор який би виконував програми цілком в L1 кеші, байткод та
стріми якого були би вирівняні по словам архітектури, а для векторних
обчислень застосовувалися би AVX інструкції, які, як відомо
перемагають по ціні-якості GPU обчислення, то такий інтерпретатор міг би,
навіть без спеціалізованої JIT компіляції, скласти конкуренцію
сучасним промисловим інтерпретаторам, таким як Erlang, Python, K, LuaJIT.
Для дослідження цієї гіпотези мною було побудовано експериментальний
інтерпретатор без байт-коду, але з вирівняним по словам архітерктури
стрімом команд, які є безпосередньою машинною презентацією конструкторів індуктивних типів (enum)
мови Rust.
p.
Ключовим викликом тут стали лінійні типи мови Rust, які не
дозволяють звертатися до посилань, які вже були оброблені, а це
впливає на всю архітектуру тензорного преставлення змінних в
мові інтерпретатор CPS, яка наслідує певним чином мову К.
p.
Середовище виконання мість базову бібліотеку формалізовану в PureScript,
а також серію експериментів <a href="https://n2o.dev">N2O.DEV</a>,
повні версіх яких доступні для мови Erlang, Elixir та Hamler.
section
h1 Вищі мови програмування
p.
Тут йдеться про мови програмування придатні для доведення
теорем, та їх таксономію від найелементарніших (чистої системи
з одним типом Π) до найпотужніших гомотопічних систем. Одна
така гомотопічна система є кінцевим завданням цього розділу
— побудова моделі гомотопічного верифікатора. В процесі його
побудови в цьому розділі ми розглянемо під мікроскопом складові частини його нижчих мовних рівнів.
Застосуємо категорну семантику для мов програмування і будемо розглядати мови програмування як моноїдальні
мовні категорі, об’єкти яких є просторами усіх програм цих мов програмування,
а морфізми — правила верифікації та компіляції цих програм.
Мови розкладаються у спектральну (індексовану натуральними числами N → U)
послідовність мов, кожен елемент якої є мовою програмування,
яка не містить синтаксичне дерево вищої мови програмування.
p.
Система вищих мов мість базові бібліотеки PURE для системи PTS
та HOMOTOPY для системи MLTT/CCHM/HTS. Для побудови вищих мов
використовувалися мови OCaml та Erlang.
+tex.
$\mathbf{Alonzo}$ — просто типізоване лямбда-числення Каррі.
+tex.
$\mathbf{Henk}$ — чиста система з всвесвітами Кокана.
+tex.
$\mathbf{Per}$ — система Поулін-Моурін.
+tex.
$\mathbf{Anders}$ — гомотопічна система з двома рівностями.
+tex.
$\mathbf{Urs}$ — еквіваріантна супергомотопічна система типів.
.index
<center><table cellspacing=5><tr><td width=5><img src="https://n2o.space/img/pdf.jpg" width=35></td><td width=400>
<a href="https://groupoid.github.io/formal.one/monography.pdf">
<h3>МОНОГРАФІЯ.PDF</h3>
</a></td></tr></table></center>
include footer