forked from UniFormal/uniformal.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathold.html
348 lines (293 loc) · 14.3 KB
/
old.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
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
<!DOCTYPE html>
<html>
<head>
<title>The MMT Language and System</title>
<script type="text/javascript" src="lib/jquery.js"></script>
<script type="text/javascript" src="lib/overview.js"></script>
<meta charset="UTF-8"/>
<link rel="stylesheet" href="lib/overview.css"/>
</head>
<body>
<div class="wrapper">
<div class="header">
<h1>MMT - Language and System for the Uniform Representation of Knowledge</h1>
<span class="buttons">
<a href="/doc/index.html">Documentation</a>
<a href="/doc/philosophy/index.html">Research</a>
<a href="/doc/setup/index.html">Download</a>
<a href="/doc/development/index.html">Community</a>
</span>
<div class="subtitle-wrapper">
<span class="subtitle area active">MMT integrates the 4 major paradigms for representing scientific knowledge.</span>
<span class="subtitle aspect passive">All aspects of MMT avoid a commitment to semantic foundation, representational paradigm, or application work flow.</span>
</div>
</div>
<div class="diagram">
<table>
<tr>
<td class="aspect passive">
<div class="title">Representation Languages</div>
<div class="tagline">MMT represents all knowledge in one simple framework</div>
<ul class="features">
<li data-id="decl">Subsumes virtually any declarative language</li>
<li data-id="objects">Uniform treatment of virtually any formal object</li>
<li data-id="modsys">Powerful module system</li>
<li data-id="extend">Highly extensible at all levels</li>
</ul>
</td>
<td class="area active">
<div class="title">Narration</div>
<div class="tagline">MMT subsumes natural languages</div>
<ul class="features">
<li data-id="mix">Seamless mixing of formal/informal content</li>
<li data-id="format">Arbitrary concrete syntax: presentation MathML, LaTeX, ...</li>
<li data-id="degrade">Graceful degradation of formal algorithms to narrative content</li>
<li data-id="latex">Deep integration with LaTeX authoring workflow</li>
</ul>
</td>
<td class="aspect passive">
<div class="title">Applications</div>
<div class="tagline">MMT enables generic large-scale implementations</div>
<ul class="features">
<li data-id="edit">IDE for semantics editing support</li>
<li data-id="build">Build Manager for incremental, parallel compilation</li>
<li data-id="browse">Semantics-aware content browser</li>
<li data-id="mathhub">Project hosting platform</li>
<li data-id="integrate">Interoperability layer for semantics-preserving knowledge exchange</li>
</ul>
</td>
</tr>
<tr>
<td class="area active">
<div class="title">Deduction</div>
<div class="tagline">MMT subsumes logical languages</div>
<ul class="features">
<li data-id="logic">Declarative definitions of logics including syntax, proof theory, model theory</li>
<li data-id="modlog">Modular composition of logics from library of language features</li>
<li data-id="lfx">Rapid prototyping of logical systems</li>
<li data-id="foundind">No foundational commitment to a formal system or semantics</li>
</ul>
</td>
<td class="center">
<div class="details-container">
<!-- Details for each features. Only one of these is visible at a given time. -->
<div class="details" data-id="default">
<div class="hoverhint">hover over a feature to see details</div>
</div>
<!-- Language -->
<div class="details" data-id="modsys">
Theory morphisms uniformly represent
<ul>
<li>abstraction and refinement,</li>
<li>inclusion and inheritance,</li>
<li>functors and parametrization,</li>
<li>translations and interpretations.</li>
</ul>
</div>
<div class="details" data-id="decl">
MMT declarations uniformly represent
<ul>
<li>sort, type, universe symbols,</li>
<li>constant, function, predicate symbols,</li>
<li>connectives, binders, operators,</li>
<li>axioms, theorem, inference rules.</li>
</ul>
</div>
<div class="details" data-id="objects">
MMT declarations uniformly represent
<ul>
<li>types, kinds,</li>
<li>terms, function, formulas,</li>
<li>literals of any kind,</li>
<li>proofs, derivations.</li>
</ul>
</div>
<div class="details" data-id="extend">
MMT theories can introduce not only new symbols but also notations, implementation rules, and high-level language features.
</div>
<!-- Applications -->
<div class="details" data-id="edit">
MMT acts as a <a href="http://www.jedit.org">jEdit</a> plugin to provide IDE functionality.
<!-- add screen shot of context-sensitive auto-completion -->
</div>
<div class="details" data-id="browse">
The MMT web browser provides numerous advanced features including interactive type inference or definition lookup.
<!-- add screen shot of type inference -->
</div>
<div class="details" data-id="build">
The MMT build manager is designed for fast rebuilding of large projects including arbitrary importers and exporter for external formats.
<!-- add screen shot of queue browser -->
</div>
<div class="details" data-id="mathhub">
<a href="http://mathhub.info">MathHub</a> builds on MMT and <a href="https://gitlab.com">GitLab</a> to provide a GitHub-style platform for mathematics.
<!-- add mathhub screen shot -->
</div>
<div class="details" data-id="integrate">
MMT uses theories as interfaces to bridge between different languages.
<!-- add triangle picture for interface theories -->
</div>
<!-- Logical -->
<div class="details" data-id="parse">
MMT notations support mixfix syntax, precedences, implicit arguments, binding, sequence arguments/variables.
<!-- add jedit screen shot of complex math object -->
</div>
<div class="details" data-id="check">
Reconstruction of omitted types and implicit arguments in the presence of dependent types, polymorphism, rewriting, ...
<!-- add jedit screen shot of type-checked proof -->
</div>
<div class="details" data-id="simplify">
Arbitrary computation and rewrite rules.
<!-- add jedit screen shot or rewrite rule -->
</div>
<div class="details" data-id="compute">
MMT will allow interpretation of stateful programs.
</div>
<div class="details" data-id="prove">
Only 3 rules yield a basic theorem prover for forward- and backward chaining.
No limitation with respect to advanced prover infrastructures.
</div>
<!-- Management -->
<div class="details" data-id="present">
Generation of arbitrary formats such as high-quality presentation MathML using only notations.
<!-- add web screen shot of proof tree rendering -->
</div>
<div class="details" data-id="change">
Differencing of concrete and abstract syntax for fast rechecking.
</div>
<div class="details" data-id="search">
General query language and <a href="http://search.mathweb.org/">MathWebSearch</a> allow fast search in large libraries.
<!-- add mathwebsearch screen shot -->
</div>
<div class="details" data-id="project">
MMT archives allow for collaboration, hosting, and distribution of projects.
<!-- add mathhub screen shot -->
</div>
<!-- Narration -->
<div class="details" data-id="mix">
Formal objects inside rigorous but informal documents.<br/>
Informal comments inside formal representations.<br/>
<!-- add stex screen shot -->
</div>
<div class="details" data-id="format">
Escape back and forth between MMT and e.g., HTML and LaTeX.
<!-- add jedit screen shot of MMT-in-text-in-MMT -->
</div>
<div class="details" data-id="degrade">
Algorithms like type-checking of formulas perform as good as they can in the presence of narrative subformulas.
<!-- -->
</div>
<div class="details" data-id="latex">
sTeX package for LaTeX allows semantic markup of narrative LaTeX documents.<br/>
mmt package for LaTeX allows type-checking and type-setting MMT formulas.
<!-- -->
</div>
<!-- Deduction -->
<div class="details" data-id="logic">
Logics are defined as theories in the logical framework.
<!-- screen shot of conjunction in jedit -->
</div>
<div class="details" data-id="modlog">
The <a href="https://latin.omdoc.org/">LATIN</a> project has built a library of logic features, e.g.,
<ul>
<li>conjunction</li>
<li>lambda-abstraction</li>
<li>excluded middle</li>
<li>set theoretical models</li>
<!-- screen shot of latin atlas -->
</div>
<div class="details" data-id="foundind">
MMT systematically avoids any commitment. All logical features are represented in the framework.
<!-- screen shot of FOL = IFOL+tnd in jedit -->
</div>
<div class="details" data-id="lfx">
The logical framework is itself flexible, and different frameworks can be composed modularly.
<!-- meta-theory graph -->
</div>
<!-- Computation -->
<div class="details" data-id="progfound">
Current work transfers the framework built for logics languages to programming languages.
<!-- -->
</div>
<div class="details" data-id="proglang">
Features of programming languages and their semantics and interrelations will be represented declaratively in MMT.
<!-- -->
</div>
<div class="details" data-id="modprog">
Type systems, computation features, and interpretation rules will be declared modularly and composed to form individual programming languages.
<!-- -->
</div>
<div class="details" data-id="logcomp">
MMT will allow representing proofs and programs in the same formalism.<br/>
This avoids an ontological distinction between tactics (programs about proofs) and software verification (proofs about programs).
<!-- -->
</div>
<!--Tabulation -->
<div class="details" data-id="data">
MMT supports finitary representations of complex mathematical objects that can be stored in standard databases and easily interchanged and queried.
<!-- add jedit screen shot of elliptic curve -->
</div>
<div class="details" data-id="codec">
Type-driven codecs are used to convert automatically between high-level mathematical representations and standard database languages for efficient low-level representation.
<!-- add jedit screen shot of codec use -->
</div>
<div class="details" data-id="query">
MMT allows using high-level languages to query the low-level representations.
<!-- -->
</div>
<div class="details" data-id="odk">
Used in <a href="http://opendreamkit.org/">OpenDreamKit</a> for LMFDB, OEIS, findstat.
<!-- -->
</div>
</div>
</td>
<td class="area active">
<div class="title">Computation</div>
<div class="tagline">MMT will subsume programming languages</div>
<ul class="features">
<li data-id="progfound">Object-oriented, functional, and imperative features</li>
<li data-id="proglang">Declarative definitions of programming languages</li>
<li data-id="modprog">Modular composition of programming languages and their semantics</li>
<li data-id="logcomp">Seamlessly program about logics, reason about programs</li>
</ul>
</td>
</tr>
<tr>
<td class="aspect passive">
<div class="title">Soundness-Critical Services</div>
<div class="tagline">MMT allows generic solutions to deep problems</div>
<ul class="features">
<li data-id="parse">Parsing</li>
<li data-id="check">Type Checking</li>
<li data-id="simplify">Simplification</li>
<li data-id="compute">Computation (ongoing)</li>
<li data-id="prove">Theorem Proving (ongoing)</li>
</ul>
All algorithms are rule-based and rules can be combined modularly.<br/>
Thus, languages can be modified at minimal cost.
</td>
<td class="area active">
<div class="title">Tabulation</div>
<div class="tagline">MMT subsumes data description languages</div>
<ul class="features">
<li data-id="data">Concrete representation of abstract mathematical objects</li>
<li data-id="codec">Standardized codec language for interchanging data</li>
<li data-id="query">Uniform query language across databases (ongoing)</li>
<li data-id="odk">Integrated with major databases of computational mathematics</li>
</ul>
</td>
<td class="aspect passive">
<div class="title">Management Services</div>
<div class="tagline">MMT allows generic knowledge management solutions</div>
<ul class="features">
<li data-id="present">Rendering using MathML</li>
<li data-id="search">Search and Querying</li>
<li data-id="change">Change Management</li>
<li data-id="project">Project Management</li>
</ul>
</td>
</tr>
</table>
</div>
</div>
</body>
</html>