-
Notifications
You must be signed in to change notification settings - Fork 15
/
Copy pathgrim.html
1835 lines (1384 loc) · 82.9 KB
/
grim.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
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html>
<html>
<head>
<title>The Grim formula language</title>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" >
<meta name="viewport" content="width=device-width, initial-scale=1">
<style type="text/css">
body { font-family: roboto, arial, sans-serif; line-height: 1.5em; margin: 2em; background-color:#fcfcfc; }
#main { max-width:900px; margin-left: auto; margin-right: auto; }
/* p { text-align:justify; text-justify:inter-word; } */
h2 { margin-top: 2em; border-bottom:0.1em solid black; }
h3 { margin-top: 1.5em; }
table { border-collapse:collapse; background-color:#fff; }
table, th, td { border: 1px solid #aaa; }
th, td { padding:0.3em; }
tt { border:1px solid #ccc; background-color:#fff; padding:0.2em; }
pre {
background-color: #f4f4f4;
line-height: 1.3em;
margin-left: 2em;
margin-right: 2em;
white-space: pre-wrap;
white-space: -moz-pre-wrap;
white-space: -pre-wrap;
white-space: -o-pre-wrap;
word-wrap: break-word;
}
</style>
<link href="https://fonts.googleapis.com/css?family=Roboto" rel="stylesheet">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous">
<script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js" integrity="sha384-y23I5Q6l+B6vatafAwxRu/0oK/79VlbSz7Q9aiSZUvyWYIYsd+qj+o24G5ZU2zJz" crossorigin="anonymous"></script>
<script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/contrib/auto-render.min.js" integrity="sha384-kWPLUVMOks5AQFrykwIup5lo0m3iMkkHrD0uJ4H5cjeGihAutqP0yW0J6dpFiVkI" crossorigin="anonymous"></script>
<script>
document.addEventListener("DOMContentLoaded", function() {
renderMathInElement(document.body, {delimiters: [
{left: "$$", right: "$$", display: true},
{left: "$", right: "$", display: false},
]
});
});
</script>
</head>
<body>
<div id="main">
<h1 style="margin-top:0.3em; margin-bottom:0.35em">The Grim formula language (draft)</h1>
<p><i>Updated 2019-12-10</i> -- <a href="https://github.com/fredrik-johansson/fungrim">Source code on GitHub</a></p>
@toc@
<h2>Introduction</h2>
<p>
<b>Grim</b> is a symbolic language for representing mathematical formulas.
Grim is human-readable, computer-readable (enabling algorithmic
manipulation of symbolic expressions), and can be converted to LaTeX for rendering.
Grim is being developed as a means to represent mathematics in semantic form
in <a href="http://fungrim.org">FunGrim: the Mathematical Functions Grimoire</a>.
A secondary goal is to have a reliable symbolic interface for
<a href="http://arblib.org">Arb</a> numerical evaluation.
</p>
<p>
Grim has two components:
<ul>
<li>A simple core language for symbolic expressions (similar to Lisp S-expressions
and Wolfram language M-expressions).</li>
<li>A vocabulary of hundreds of builtin symbols for mathematical
objects and operations (most of which are documented in FunGrim).
</li>
</ul>
</p>
<p>
At this time, no attempt is made to provide a complete specification.
Grim is defined by the reference implementation in Python (<tt>pygrim</tt>,
which currently handles LaTeX conversion and some numerical
evaluation via Arb), together with
the 2500+ formulas added to FunGrim so far which both serve as documentation and as an informal
test suite.
</p>
<ul>
<li><span style="color:red"><b>Warning: Grim is currently alpha-level, and anything in this document may change. There
are many known inconsistencies. Feedback is welcome on anything from mathematical foundations
to syntax and naming.</b></span></li>
</ul>
<h3>Quick examples</h3>
<table>
<tr><th>Grim</th><th>Generated LaTeX</th><th>Rendered formula</th></tr>
<tr>
<td>
<tt style="border:0">
Implies(Element(n, ZZ), Equal(Sin(Mul(Pi, n)), 0))
</tt>
</td>
<td>
<tt style="border:0">
\left(n \in \mathbb{Z}\right) \implies \left(\sin\!\left(\pi n\right) = 0\right)</tt>
</td>
<td>
@@@Implies(Element(n, ZZ), Equal(Sin(Mul(Pi, n)), 0))@@@
</td>
</tr>
<tr>
<td>
<tt style="border:0">
Equal(Exp(z), Sum(Div(Pow(z, n), Factorial(n)), For(n, 0, Infinity)))
</tt>
</td>
<td>
<tt style="border:0">
{e}^{z} = \sum_{n=0}^{\infty} \frac{{z}^{n}}{n !}</tt>
</td>
<td>
@@@Equal(Exp(z), Sum(Div(Pow(z, n), Factorial(n)), For(n, 0, Infinity)))@@@
</td>
</tr>
<tr>
<td>
<tt style="border:0">
Equal(Det(Matrix(BellNumber(Add(i, j)), For(i, 0, n), For(j, 0, n))), Product(Factorial(k), For(k, 1, n)), BarnesG(Add(n, 2)))</tt></td>
<td>
<tt style="border:0">
\operatorname{det}\displaystyle{\begin{pmatrix} B_{0 + 0} & B_{0 + 1} & \cdots & B_{0 + n} \\ B_{1 + 0} & B_{1 + 1} & \cdots & B_{1 + n} \\ \vdots & \vdots & \ddots & \vdots \\ B_{n + 0} & B_{n + 1} & \ldots & B_{n + n} \end{pmatrix}} = \prod_{k=1}^{n} k ! = G\!\left(n + 2\right)</tt></td>
<td>@@@Equal(Det(Matrix(BellNumber(Add(i, j)), For(i, 0, n), For(j, 0, n))), Product(Factorial(k), For(k, 1, n)), BarnesG(Add(n, 2)))@@@</td>
</tr>
</table>
<h3>Goals</h3>
<ul>
<li><b>Open source</b>. Mathematics should be free!</li>
<li><b>Easy to write</b>. Grim is uniform, and
when combined with infix arithmetic (as discussed further below),
nearly as compact as LaTeX.</li>
<li><b>Easy to parse</b>.
In fact, Grim formulas can be written within many existing
programming languages (such as Python, JavaScript, Julia),
relying only on the language's native syntax.</li>
<li><b>Symbolic</b>. Grim represents mathematics
semantically.
Grim expressions are meant to be easy to manipulate by symbolic
computation software and precise enough
to be used by theorem-proving software.
</li>
</ul>
<h3>Non-goals</h3>
<p>Grim is <b>not designed to be a typesetting language</b>.
The details of how to display a formula are meant to be handled
by the Grim-to-LaTeX converter.
Nevertheless, Grim is designed to map naturally to
conventional mathematical notation, and it does
allow including typesetting hints in formulas where the
default rendering is inadequate.
</p>
<p>Grim is also <b>not strict about semantic correctness</b>!
It is possible to write purely
"syntactical" formulas in Grim just for the purpose of rendering via LaTeX.
This is often necessary when the goal is just to display a formula
(not to do symbolic computation with the expression)
and a semantically correct version would be
too cumbersome to express;
hopefully, future improvements to the language
will make such situations less common.
</li>
<ul>
<li><span style="color:red">TODO: semantic and non-semantic formulas
could be distinguished explicitly.</span></li>
</ul>
<p>
Grim is <b>not designed to be a general-purpose programming language</b>
although
it can be used to encode simple functional programs
performing mathematical calculations.
In contrast to full-blown Lisp-like programming languages,
Grim is not meant to be used to
manipulate symbolic expressions "from within";
it is meant to be embedded in a host programming language where
the host language can be used to traverse expression trees.
Another limitation is that Grim lacks concrete data structures for programming,
being mainly concerned with representing idealized and immutable mathematical objects.
In general, the abstractions in Grim are designed
more for expressing pure mathematics than for expressing programs.
</p>
<p>Grim is <b>not an automatic rewrite system</b>. Most computer algebra systems
implement rules for automatically rewriting symbolic expressions in "canonical form"
(for example, converting @@x + x@@ to @@2*x@@)
and must be told explicitly not to do so when rewriting
is unwanted.
The default assumption in Grim is that expressions are preserved verbatim.
Grim expressions can be used as a basis for a rewrite system
and the semantic specification is intended to serve as a guide
for mathematically correct rewriting,
but the specification of the Grim formula language itself does
not mandate any form of automatic rewriting.
Some rewriting in the <i>presentation</i> of a formula may take place
during conversion to LaTeX, but this does not represent a change
to the underlying Grim source expression.
</p>
<p>Grim is <b>not a good fit for all branches of mathematics</b>.
The primary goal is to express concrete results involving (complex)
numbers and functions on numbers, and the
builtin symbols and their semantics reflect this design.
A future module/namespace system could potentially
make the language more versatile.</p>
<h2>Syntax and representation of expressions</h2>
<h3>Grim expressions</h3>
<p>Grim has a single data structure: symbolic expression trees.
A <i>Grim expression</i> is either of the following:</p>
<ul>
<li>An atom (atomic expression), being either:</li>
<ul>
<li>An integer literal, like <tt>0</tt>, <tt>1</tt> or <tt>-42</tt>.</li>
<li>A symbol, like <tt>x</tt>, <tt>Pi</tt>, <tt>Sin</tt> or <tt>Integral</tt>.</li>
<li>A Unicode string, like <tt>"A grim expression: 😀"</tt>.</li>
</ul>
<li>
A non-atom (non-atomic expression), having the form <tt>f(x1, x2, ..., xn)</tt> where
<tt>f</tt>, <tt>x1</tt>, <tt>x2</tt>, ..., <tt>xn</tt> are expressions. The expression
<tt>f</tt> is called the <i>head</i> and
<tt>x1</tt>, <tt>x2</tt>, ..., <tt>xn</tt> are called the <i>arguments</i> of the expression.
</li>
</ul>
<h3>Example</h3>
<p>
An entry in FunGrim is represented by a single Grim expression
that contains various metadata as well as the main formula
as subexpressions. For example:</p>
<pre>
Entry(ID("22dc6e"),
Formula(Equal(Fibonacci(n), Add(Fibonacci(Sub(n, 1)), Fibonacci(Sub(n, 2))))),
Variables(n),
Assumptions(Element(n, ZZ)))
</pre>
<p>The formula is the recurrence relation for Fibonacci numbers: @@Equal(Fibonacci(n), Add(Fibonacci(n-1), Fibonacci(n-2)))@@.
The metadata in this case specifies the FunGrim entry ID (<tt>22dc6e</tt>, as a string),
lists the free variables in the formula (here the single variable <tt>n</tt>),
and provides conditions on the variables ("assumptions"),
in this case @@Element(n, ZZ)@@, such that the formula represents a theorem.
</p>
<h3>Some points of caution</h3>
<ul>
<li>Grim distinguishes between
the atomic expression <tt>f</tt> and the non-atomic
expression <tt>f()</tt> where <tt>f</tt> is called with an empty argument list.
<ul>
<li><span style="color:red">TODO: should atoms also have a head (e.g. <tt>Integer</tt>, <tt>Symbol</tt>, <tt>Text</tt>)?</span></li>
</ul>
</li>
<li>The head of an expression need not be an atom; <tt>f(g(a))(x, y)</tt> is valid.</li>
<li>
Symbol names at this time are limited to ASCII Latin letters, digits and underscores,
where a digit may not appear as the first character. Since symbol names
cannot start with digits or the minus symbol, integer literals can also just
be thought of as a distinguished class of symbols.
<ul>
<li><span style="color:red">TODO: should probably allow Unicode</span></li>
</ul>
</li>
</ul>
<h3>String representation and infix operators</h3>
<p>
Every Grim expression has a canonical string representation, for example
<tt>Add(3, Mul(-5, x))</tt>. The simple syntax ensures that Grim expressions
are syntactically valid in common programming languages.
The current backend code for FunGrim (<tt>pygrim</tt>)
simply embeds Grim as a domain-specific
language within Python, using Python's native integer literals and
function call syntax (the necessary symbols have to be created
as Python variables).</p>
<p>The same Grim expression could be represented with different syntax
where this is convenient, for example in Lisp syntax as <tt>(Add 3 (Mul -5 x))</tt> or
with infix arithmetic operators as <tt>3 + (-5 * x)</tt>.
Indeed, because function-call syntax is clumsy for complex arithmetic expressions,
we will frequently write Grim expressions in an <b>extended syntactical form</b>
using <b>infix arithmetic operators (+, -, *, /, **) as well as parentheses
for grouping</b>.
In the Python implementation, operators are simply handled by overloading
the Python-level arithmetic operators (with the operator precedence rules of Python).
We need to be careful: for example, we can do <tt>x / 3</tt> to construct
the Grim expression <tt>Div(x, 3)</tt> in Python when <tt>x</tt> is a Grim
symbol, but <tt>1 / 3</tt> in Python
does not give <tt>Div(1, 3)</tt>.
</p>
<h3>Symbols available for variables</h3>
<p>
Symbols reserved for builtin objects (such as <tt>Add</tt> and <tt>ZZ</tt>)
start with an uppercase letter and are at least two
characters long, so all single-letter symbols and all symbols beginning
with a lowercase character can be used for variables.
The Python implementation defines at least the following Python variables
as Grim symbols:
</p>
@example@ Set(a, b, c, d, e, f, g, h, i, j, k, l, ell, m, n, o, p, q, r, s, t, u, v, w, x, y, z) @example@
@example@ Set(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z) @example@
@example@ Set(alpha, beta, gamma, delta, epsilon, zeta, eta, theta, iota, kappa, lamda, mu, nu, xi, pi, rho, sigma, tau, phi, chi, psi, omega) @example@
@example@ Set(Alpha, Beta, GreekGamma, Delta, Epsilon, Zeta, Eta, Theta, Iota, Kappa, Lamda, Mu, Nu, Xi, GreekPi, Rho, Sigma, Tau, Phi, Chi, Psi, Omega) @example@
<p>
Most Greek letter names are available as symbols and are recognized
by the LaTeX converter.
There are some exceptions: <tt>Gamma</tt> is reserved
for the gamma function,
and <tt>Pi</tt> is reserved for the constant @@Pi@@; one should use <tt>GreekGamma</tt>
and <tt>GreekPi</tt> for the Greek capital letters as variables.
The alternative spelling <tt>lamda</tt> / <tt>Lamda</tt> is used for "lambda" since
<tt>lambda</tt> is a reserved keyword in Python.
</p>
<p>A convenience hack: a symbol name ending with an underscore results
in function calls being rendered as subscripts (but watch out as <tt>a_</tt>
is not the same symbol as <tt>a</tt>, and the symbols
are not implicitly connected):</p>
@example@ Tuple(a_(n), gamma_(m,n), f_(n)(x)) @example@
<ul>
<li><span style="color:red">
TODO: provide a way to declare custom rendering rules for variables.
</li>
</ul>
<h2>Mathematical universe</h2>
<p>In symbolic computation, it is important to distinguish between
<b>expressions</b> and the <b>values</b> they represent.
The symbolic expressions
@@Expr(4)@@, @@Add(2,2)@@ and
@@Pow(2, 2)@@
are different as expressions,
but represent the same value, the integer 4, in an imagined mathematical universe.
We will often refer to values in the mathematical universe as <b>objects</b>.
The universe of objects that can be described using
Grim expressions includes the following:</p>
<ul>
<li><b>Booleans</b>. True and False.</li>
<li><b>Tuples</b>. Finite ordered collections of objects.</li>
<li><b>Sets</b>. Possibly infinite unordered collections of objects.</li>
<li><b>Functions</b>. Functions, describing maps between sets.</li>
<li><b>Numbers (and number-like objects)</b>. This comprises the integers and certain standard extensions and completions with respect to algebraic operations and limits; including rational and algebraic numbers, real and complex numbers, as well as formal polynomials and power series over numbers, and infinities.</li>
<li><b>Matrices</b>. Matrices are considered arithmetical objects, but distinct from scalar numbers.</li>
<li><span style="color:red">
TODO: Equivalence classes / extensional sets of objects: to allow representing various arithmetic objects: residues of integers modulo @@N@@, finite field elements, algebraic number field elements, and truncated power series; in all cases viewed as equivalence classes and not as representatives in an explicit embedding.</li>
</ul>
<p>
Each item on this list denotes a family of objects belonging to a <b>type</b>
disjoint from the other types.
The notion of type is used informally here, and this
list is not systematic or exhaustive.
</p>
<h3>Equality</h3>
<p>
The ordinary equality predicate <tt>Equal</tt> (@@Equal(a, b)@@) and
its logical negation <tt>NotEqual</tt> (@@NotEqual(a, b)@@) are defined
to compare values (objects), not to compare the expressions as syntactical trees of symbols.
The same goes for the predicates for set membership, etc.
</p>
<p>
The <tt>Equal</tt> function is defined to compare objects pedantically
within the mathematical universe:
@@Equal(a, b)@@ if and only if @@a@@ and @@b@@ are exactly
the same object. If @@Equal(a, b)@@,
we will accordingly have @@Equal(f(a), f(b))@@ for any function @@f@@.
Objects of different types are considered unequal
even if they are in some sense isomorphic. This contract is intended
to provide a solid foundation for symbolic rewriting.
In contexts where this notion of equality is too strong, one should
work with alternative comparison functions representing different
notions of equivalence,
isomorphism, etc.
</p>
<ul>
<li><span style="color:red">
TODO: consider setoids / extensional sets.
</li>
</ul>
<p>
To keep predicates and definitions involving numbers and arithmetic
functions simple,
all ordinary numbers belong to the same type:
there is no distinction between 3 viewed
as a natural number, integer, rational number,
real number, or complex number.
On the other hand, collection-like objects belong to different types:
the 1-tuple @@Tuple(3)@@, the set @@Set(3)@@, the one-by-one
matrix @@Tuple(3)@@ and the constant function @@Function(x, 3)@@ <!-- todo: should be Matrix(...) -->
are all considered distinct objects, and distinct from the integer 3.
</p>
<p>A subtle point is that if @@a@@ and @@b@@ both represent mathematical objects, then the
value of the equality test
@@Equal(a, b)@@ is considered an element of @@Set(False, True)@@
even if this equality is undecidable (or simply algorithmically hard to decide); inability to compute
a value (reduce an expression to a simpler expression in the same
equivalence class) is an out-of-universe concept and not
an in-universe concept.</p>
<h3>Foundations and implementations</h3>
<p>
Symbolic expressions are finite and computable as syntactical structures.
One way to think of values is as
equivalence classes of symbolic expressions,
where @@Expr(4)@@ and @@Add(2,2)@@ belong
to the same equivalence class. However,
mathematical objects need not be explicitly computable.
The set @@RR@@ is considered a subset (as well as an element) of the mathematical universe,
but being uncountable, most of its elements cannot be represented individually
by symbolic expressions. Whether the elements of @@RR@@ actually "exist" is a philosophical question, but we can
manipulate the symbol @@RR@@ and expressions such as @@Set(x**2, ForElement(x, RR))@@
as if the elements exist.</p>
<p>
The mathematical universe is not based on a particular
formalized foundation of mathematics,
and the Grim language does not specify how to perform concrete computations
with objects (indeed, it allows expressing objects that are provably not computable!).
The idea is that for actual computations, the user will implement
a translation between Grim expressions and data structures and algorithms for
the relevant kinds of objects.
An example of this is the Arb backend for numerical evaluation,
which understands a subset of Grim symbols related to
real and complex numbers.
The purpose of the documented Grim semantics, apart from describing the
correct call syntax,
is to disambiguate cases where different interpretations could be made,
so that translations can be done consistently.
</p>
<p>The universe can be extended ad-hoc by defining
the meaning of previously undefined symbols and expressions.
For example, a user might define the meaning of the symbol
<tt>Fruits</tt> as representing a set of objects denoted
by the symbols <tt>Apple</tt> and <tt>Orange</tt>
and then define the meaning of operations such as @@Less(Expr(symbol_name="Apple"), Expr(symbol_name="Orange"))@@.
"Define the meaning" here means providing the intended
translations in an external environment using the Grim language.</p>
<h2>Symbols, variables and expression operators</h2>
<p>
Symbols within formulas can denote specific objects
(such as the constant <tt>Pi</tt> or the function <tt>Add</tt>)
or variables.
A symbol such as <tt>x</tt> without a builtin meaning
can be used as a <b>variable</b>, whose meaning depends
on the context.
In a context where <tt>x</tt> has not been defined, any expression containing <tt>x</tt> is viewed
purely as an expression which does not represent a mathematical object.
We will distinguish between two kinds of variables:
<b>free variables</b> and <b>bound variables</b>.
(A third type of variable, an <i>indeterminate</i> is discussed
further in the section on <i>formal polynomials and power series</i>. An
indeterminate is not actually a variable but a distinct kind of
mathematical object.)
</p>
<p>In formulas such as
@@Brackets(Where(Sin(x), Def(x, Pi/6)))@@, the function definition @@Function(x, x**2)@@,
the set comprehension @@Set(x, ForElement(x, RR), Greater(x, 0))@@,
the integral @@Integral(x**2, For(x, a, b))@@
or the quantified statement @@All(GreaterEqual(x**2, 0), ForElement(x, RR))@@,
the symbol <tt>x</tt> is a bound variable.
Binding a variable is a local operation: it
overrides any meaning previously assigned to the same symbol
outside the surrounding evaluation context, and the binding
has no effect outside of the expression where it is used.
</p>
<p>Some builtin symbols represent neither objects nor variables; they act
as special <b>expression operators</b>.
In an ordinary function call <tt>f(x1, x2, ..., xn)</tt>, the
arguments represent values (possibly unknown
values represented by variables), and
any argument can be replaced by
any other expression representing the same value without changing
the meaning. In an expression operation
<tt>f(x1, x2, ..., xn)</tt>, some of the arguments may need to be
processed as symbolic expressions.
Operators that deal with binding variables belong to this category.
There is no syntactical difference between ordinary function calls
and expression operations;
which interpretation applies depends on the head <tt>f</tt>
and whether the arguments contain special expression operators
such as <tt>For</tt>, documented below.
Code for manipulating expressions semantically must detect
expression operators on a case by case basis.
</p>
<h3>Free variables</h3>
<p>In a formula such as @@LessEqual(Abs(Sin(x)), 1)@@,
the symbol <tt>x</tt> represents a free variable unless other
context is provided.
A formula containing free variables does not represent a single mathematical
object but a range of possible mathematical objects;
the interpretation is usually is that the formula holds when @@x@@ is
replaced by any concrete value satisfying certain assumptions.
In FunGrim entries, all free variables and accompanying assumptions
must be declared explicitly as part of the entry metadata; in the example, <tt>Variables(x)</tt>
and <tt>Assumptions(Element(x, RR))</tt>.
This information can be used to interpret the formula as a quantified logical
formula which no longer contains a free variable:
@@All(LessEqual(Abs(Sin(x)), 1), ForElement(x, RR))@@.</p>
<p>Assumptions can be more complicated; for example, the content
of the <tt>Assumptions()</tt> accompanying
a formula with the free variables <tt>Variables(x, y)</tt> might read:</p>
@example@ Or(And(Element(x, ZZ), Element(y, RR)), And(Element(x, RR), Element(y, CC), Or(Greater(x, 0), NotEqual(Add(x, y), 0)))) @example@
<p>Assumptions should always specify the base set of each variable unambiguously,
typically by specifying @@Element(x, S)@@ where @@S@@ is a known set.
It is not sufficient to state @@Greater(x, 0)@@ implying that @@x@@ should be
a positive real number, because there may be other objects in the universe that
satisfy this relation (for example, @@+Infinity@@).</p>
</p>
<h3>Where/Def-expressions: local definitions</h3>
<p>The simplest example of a locally bound variable is a symbol used
as an alias for a specific value. Such aliases can be created
using the <tt>Def</tt> expression operator.</p>
@example@ Def(x, a) | Defines the meaning of the symbol <tt>x</tt> to represent the value of @@a@@ in the scope of the parent operator. @example@
<p>The <tt>Def</tt> expression has to appear as an
argument to an expression operator that applies the variable binding.
Currently the only such operator is <tt>Where</tt>:</p>
@example@ Where(f(x,y), Def(x, 1/Pi), Def(y, x+1)) | The <tt>Where</tt> operator
returns the value of its first argument after executing the definition
statements in the subsequent arguments. The definition statements
are interpreted left to right and the right-hand side values in definitions can depend
on the symbols defined in the preceding definitions. @example@
@example@ Where(Equal(GCD(a, b), d, Add(Mul(a, u), Mul(b, v))), Def(Tuple(d, u, v), XGCD(a, b))) | The <tt>Where</tt> operator allows destructuring assignment (binding a tuple of variables to a tuple of values). The extended GCD function (XGCD) returns a triplet of integers. @example@
<h3>Fun-expressions: constructing functions</h3>
<p>The <tt>Fun</tt> expression operator allows constructing anonymous functions:</p>
@example@ Fun(x, Sin(x) * Cos(x)) @example@
@example@ Fun(Tuple(x, y), Sin(x+y)*Cos(x-y)) @example@
<p>Locally named functions can be constructed by combining <tt>Where</tt>/<tt>Def</tt> with <tt>Fun</tt>:</p>
@example@ Where(f(Pi/3), Def(f, Fun(x, Sin(x)+Cos(x)))) @example@
<p>More information is provided in the section on functions
and function spaces.</p>
<h3>For-expressions: iterations and comprehensions</h3>
<p>
The expression <tt>For(x, ...)</tt> binds the symbol <tt>x</tt> as
an iteration or set comprehension
variable in the parent expression, where any additional arguments <tt>...</tt>
are parameters defining the iteration.
The interpretation of the parameters is up to the parent operator.
Most operators recognize <tt>For()</tt> with two parameters as
specifying a range of integers to iterate over:</p>
@example@ Sum(Factorial(n), For(n, 2, 10)) | The <tt>For</tt> operator binds the variable <tt>n</tt> locally and specifies an iteration range
in the scope of the parent <tt>Sum</tt> operator. @example@
<p>
When <tt>For(n, a, b)</tt> is used in this sense, the endpoints @@a@@ and @@b@@
should represent
integers or possibly @@Equal(a, -Infinity)@@ and/or @@Equal(b, Infinity)@@ where an infinite
sequence makes sense. The iteration sequence is empty if @@Less(b, a)@@.
Of course, the endpoints can be variables.
</p>
@example@ Sum(Div(1, Factorial(n)), For(n, N, Infinity)) | An infinite series. @example@
<p>
Some operators may interpret the <tt>For</tt> expression
differently. For example, <tt>Integral()</tt> understands two
parameters as representing the endpoints (not necessarily integers)
of a directed line segment to integrate over:
</p>
@example@ Equal(Integral(Cos(x), For(x, a, b)), -Integral(Cos(x), For(x, b, a))) @example@
<p>
<tt>ForElement(x, S)</tt> binds the variable <tt>x</tt> just like <tt>For(x)</tt>, but
additionally tells the parent operator that <tt>x</tt> is to range over the
elements of the set <tt>S</tt>.
</p>
@example@ Equal(Sum(1/n**2, ForElement(n, SetMinus(ZZ, Set(0)))), Pi**2/3) @example@
<p>
Iteration with <tt>For</tt> and <tt>ForElement</tt> is often used in
set comprehensions and as part of quantified formulas,
and often together with filter predicates:</p>
@example@ Tuple(n**2, For(n, 1, 10)) @example@
@example@ Set(f(z), ForElement(z, CC), Greater(Re(z), 0)) @example@
<p>
This is discussed further below in the section on logic, sets and tuples.
</p>
<h3>Repeat-expressions and Step-expressions: variable-length argument lists</h3>
<p><tt>Repeat()</tt> and <tt>Step()</tt> expressions allow creating
variable-length argument lists.</p>
<p><tt>Repeat()</tt> generates a repeating sequence:</p>
@example@ Repeat(1, n) @example@
@example@ Repeat(1, 2, 3, n) @example@
<p><tt>Step()</tt> generates a sequence between two integer endpoints:</p>
@example@ Step(Pow(k, 2), For(k, a, b)) @example@
<p>The sequence is empty if @@Less(b, a)@@, and undefined if @@a@@ and @@b@@
are not integers.</p>
<p>
The <tt>Repeat()</tt> and <tt>Step()</tt>
expressions do not represent mathematical objects; they only exist
at the expression level. To construct a mathematical object,
they must be used in the argument list of a function:</p>
@example@ Tuple(Step(1/k, For(k, a, b))) @example@
<p>
The <tt>Repeat()</tt> and <tt>Step()</tt> expressions generate runs of arguments that can be
placed in arbitrary locations among other arguments:</p>
@example@ f(Repeat(-1, n), 0, Step(1/k, For(k, 1, 10)), 2) @example@
<p>These expressions can be composed:</p>
@example@ Tuple(Step(Repeat(n, n), For(n, 0, N))) @example@
<p>In this example, explicitly listing the first few items makes the pattern
clearer:</p>
@example@ Tuple(1, 2, 2, Step(Repeat(n, n), For(n, 3, N))) @example@
<p>Watch out, however: the second version is not equivalent to the first version when
@@Equal(N, 0)@@ or @@Equal(N, 1)@@ since the second version always includes the leading 1, 2, 2.
Visual pattern matching can be dangerous!
</p>
<ul>
<li><span style="color:red">
TODO: Repeat() and Step() are potentially redundant; consider allowing
For() directly anywhere and/or using a common Block() construct.
</li>
</ul>
<h2>Logic, sets and tuples</h2>
<p>
The core mathematical abstractions in Grim deal with
elementary logic and set theory.
</p>
<h3>Boolean logic</h3>
@example@ Equal(True, Not(False)) @example@
@example@ Equivalent(Not(Or(P, Q)), And(Not(P), Not(Q))) | One of De Morgan's laws.
Usage note: the @@Equivalent(a, b)@@ operator does not differ semantically
from the usual @@Equal(a, b)@@ operator for boolean values; it simply highlights that the equality
is between booleans as opposed to an equality between some other objects.
@example@
<!--
@example@ Tuple(And(Step(a_(i), For(i, 1, n))), Or(Step(b_(i), For(i, 1, n)))) @example@
-->
@example@ Element(RiemannHypothesis, Set(True, False)) | Boolean constants
may be used to denote the truth value of unresolved mathematical conjectures, such
as the Riemann hypothesis. This symbol can be used in the left-hand side
of an implication or in the assumptions of a formula to denote
a result conditional on the hypothesis. @example@
<h3>Conditional values</h3>
<p>The <tt>Cases</tt> operator allows choosing a value depending
on the value of a logical predicate or a combination of predicates.</p>
@example@ Equal(Sign(x), Cases(Tuple(-1, Less(x, 0)), Tuple(0, Equal(x, 0)), Tuple(1, Greater(x, 0)))) | Conditional formulas
can be written using the <tt>Cases</tt> operator. @example@
@example@ Equal(Abs(x), Cases(Tuple(x, GreaterEqual(x, 0)), Tuple(0, Equal(x, 0)), Tuple(1, Or(Equal(x, 1), Equal(x, -1))), Tuple(-x, Otherwise))) |
The conditions in the <tt>Cases</tt> operator can overlap, but the values for the
overlapping cases should be compatible with each other so that
the order of evaluation does not matter.
The special <tt>Otherwise</tt> case is used when no other conditions match. If no <tt>Otherwise</tt>
case is provided, the conditions should cover all possible inputs. (In this example as well
as the example above, the variable @@x@@ presumably represents a real number.) @example@
<h3>Logical formulas with quantifiers</h3>
<p>Quantified logical statements can be written using the <tt>All</tt> and <tt>Exists</tt>
operators, which work much like set comprehensions
@@Set(P(x), ForElement(x, S), Q(x))@@
(in which @@S@@ is an arbitrary set, @@P@@ is a predicate,
and @@Q@@ is an optional predicate to restrict to a subset of @@S@@).
The <tt>All</tt> operator expresses
the universal quantifier, while the <tt>Exists</tt> operator expresses
the existence quantifier.</p>
@example@ Equivalent(All(P(x), ForElement(x, S)), NotElement(False, Set(P(x), ForElement(x, S)))) @example@
@example@ Equivalent(All(P(x), ForElement(x, S), Q(x)), NotElement(False, Set(P(x), ForElement(x, S), Q(x)))) @example@
@example@ Equivalent(Exists(P(x), ForElement(x, S)), Element(True, Set(P(x), ForElement(x, S)))) @example@
@example@ Equivalent(Exists(P(x), ForElement(x, S), Q(x)), Element(True, Set(P(x), ForElement(x, S), Q(x)))) @example@
<p>Two concrete examples:</p>
@example@ All(GreaterEqual(Exp(x), 1), ForElement(x, RR), GreaterEqual(x, 0)) @example@
@example@ Exists(Equal(Exp(x), 2), ForElement(x, RR), GreaterEqual(x, 0)) @example@
<p>
A distinction should be made between logical formulas containing
free variables and "self-contained" logical formulas such as
the two examples above in which the variables are bound.
</p>
@example@ Implies(And(Element(x, RR), GreaterEqual(x, 0)), GreaterEqual(Exp(x), 1)) | This expression
is incomplete as a fully quantified representation of a theorem, because <tt>x</tt>
is not being declared as a bound variable; to make sense, <tt>x</tt> should be defined in the surrounding
scope either as a free or bound variable. @example@
@example@ All(GreaterEqual(Exp(x), 1), ForElement(x, RR), GreaterEqual(x, 0)) |
A complete quantified formula: <tt>x</tt> is a locally bound variable. @example@
@example@ All(Implies(GreaterEqual(x, 0), GreaterEqual(Exp(x), 1)), ForElement(x, RR)) |
Logically equivalent to the previous example. @example@
@example@ All(Implies(And(Element(x, RR), GreaterEqual(x, 0)), GreaterEqual(Exp(x), 1)), For(x)) |
Normally, the domain of the bound variable should be specified as part of the <tt>All</tt>
operator, but this form is acceptable when the <tt>Implies</tt> expression
contains a domain statement. @example@
<h3>Printing logical formulas</h3>
<p>Some logical operators and are rendered as text
by default instead of using symbols since this tends
to make the logic easier to read outside
of contexts where one is working with logical formulas
for their own sake. The printing style can be overridden by wrapping an expression in <tt>Logic()</tt>.</p>
@example@ All(Exists(And(Greater(x+y, 0), Not(Or(Element(x, A), Element(y, B)))), ForElement(y, T)), ForElement(x, S), Greater(x, 0)) @example@
@example@ Logic(All(Exists(And(Greater(x+y, 0), Not(Or(Element(x, A), Element(y, B)))), ForElement(y, T)), ForElement(x, S), Greater(x, 0))) @example@
<h3>Constructing sets and tuples</h3>
<p>Sets and tuples can be constructed by calling the <tt>Set</tt> and <tt>Tuple</tt> functions.
The arguments can be a finite list of explicit elements, or a set comprehension
or list comprehension using <tt>For</tt> / <tt>ForElement</tt> expressions.</p>
@example@ Set(1, 2, Pi) @example@
@example@ Set() | The empty set. @example@
@example@ Set(n**2, ForElement(n, ZZ), NotEqual(n, 0)) | Set comprehension. @example@
@example@ Set(Tuple(), Tuple(1), Tuple(1,2), Tuple(1,2,Infinity)) @example@
<p>Usage note: the singleton tuple <tt>Tuple(x)</tt> (rendered as @@Tuple(x)@@) is NOT the same object as the element @@x@@.</p>
@example@ Tuple(n, For(n, 2, 5)) @example@
@example@ Tuple(n, For(n, 1, 0)) @example@
@example@ List(1, 2, 3, 4) | Tentatively, <tt>List</tt> generates a tuple and is semantically indistinguishable from <tt>Tuple</tt>; the only difference is that <tt>List</tt> prints with square brackets. @example@
@example@ Set(n, For(n, 0, Infinity)) @example@
@example@ Set(n**2, For(n, -Infinity, Infinity)) @example@
@example@ Set(PrimeNumber(n), For(n, 1, Infinity)) @example@
@example@ Set(Pow(-1, n), ForElement(n, ZZ)) @example@
@example@ Set(f(n), For(n, -Infinity, -2)) @example@
@example@ Equal(Set(f(n), For(n, a, b)), Set(f(n), ForElement(n, ZZ), LessEqual(a, n, b))) @example@
<h3>Operations on sets and tuples</h3>
@example@ Equivalent(Element(x, S), Not(NotElement(x, S))) | Set membership. @example@
@example@ Or(Subset(S, T), SubsetEqual(S, U)) @example@
<ul>
<li><span style="color:red">
TODO: should these be called <tt>ProperSubset</tt>, <tt>Subset</tt> instead?
</li>
</ul>
@example@ Tuple(Union(S, T), Intersection(S, T), SetMinus(S, T)) | Set arithmetic. @example@
@example@ Equal(Cardinality(Set(0, 1, 2)), 3) | The cardinality of a set. @example@
@example@ Equal(Cardinality(RR), Cardinality(CC), Pow(2, Cardinality(ZZ)), Pow(2, Cardinality(QQ))) | Cardinalities of infinite sets.
Usage note: the symbol @@Infinity@@ (<tt>Infinity</tt>) is used in arithmetic and limits
with numbers
and does not represent the cardinality of a set.
One should use @@Cardinality(ZZ)@@ to represent the cardinality of a countably infinite set. @example@
@example@ Length(A) | The length of the tuple @@A@@. @example@
@example@ Item(A, n) | The item at position @@n@@ in the tuple @@A@@ (index from 1). @example@
@example@ Concatenation(A, B) | Concatenation of tuples. This function can be called with an arbitrary number of arguments. @example@
@example@ Equal(Concatenation(Tuple(a, b), Tuple(c, d, e), Tuple()), Tuple(a, b, c, d, e)) @example@
@example@ CartesianProduct(X, Y) | The set of all tuples @@Tuple(x, y)@@ with @@And(Element(x, X), Element(y, Y))@@. More generally, this function can be called with @@n@@ arguments to construct @@n@@-tuples. This function should not be confused with the ordinary product function <tt>Mul</tt> which computes arithmetic products pointwise when applied to sets. @example@
@example@ Equal(CartesianPower(X, n), CartesianProduct(Repeat(X, n))) | This function should not be confused with the ordinary power function <tt>Pow</tt> which computes arithmetic powers pointwise when applied to sets. Note the special case @@CartesianPower(X, 1)@@ representing 1-tuples, giving a different set than @@X@@. @example@
<p>The following sets are useful:</p>
@example@ Sets(S) | The set of all sets with elements in @@S@@. @example@
@example@ Sets(S, n) | The set of all sets with elements in @@S@@ and having cardinality @@n@@. @example@
@example@ Tuples(S) | The set of all tuples with elements in @@S@@. @example@
@example@ Tuples(S, n) | The set of all tuples with elements in @@S@@ and having length @@n@@. @example@
<h3>Abstract sets</h3>
<p>
The set @@ZZ@@ is an example of a "concrete" mathematical set; though infinite, it
is meaningful to iterate over its elements. There are also "abstract" builtin
sets which describe properties of objects; the actual scope of such sets is undefined.
An example of an abstract set is @@Universe@@, which is simply defined to contain any object:
</p>
@example@ Universe | The universe of all objects. @example@
<p>Another example is @@Rings@@ which is the abstract set of concrete sets that are rings,
such as @@ZZ@@ (discussed further in the section on algebraic structures).</p>
<h2>Numbers and arithmetic</h2>
<p>Grim provides various builtin functions
for working with integers, rational, algebraic, real and complex numbers.
Most such functions are documented in FunGrim. Here we describe
some of the basic concepts.</p>
<h3>Numbers and arithmetic</h3>
@example@ And(Equal(Add(Div(1, 3), Div(2, 3)), 1), Equal(Pow(Sqrt(2), 2), 2), NotEqual(Pow(2, 64), 0), Equal(Sin(Pi), 0)) | Grim numbers are mathematical numbers, not approximations. @example@
@example@ Equal(ConstI, Sqrt(-1), Pow(-1, Div(1, 2)), Exp(Div(1,2) * Log(-1))) | Numerical functions extend to complex numbers.
Multivalued functions such as @@Sqrt(z)@@ and @@Log(z)@@ give the principal branches. (Information about branch cuts can be found in FunGrim.)
Other interpretations of standard mathematical functions may be introduced as separate symbols. @example@
@example@ Add(Mul(3, a), Sub(2, 5), Div(1, 3), Pow(b, 4)) | Arithmetic operations (without using infix syntax). @example@
@example@ a*b + c/3 + x**2 + Div(1,2) - Pow(2,3) | Arithmetic operations using infix syntax in Python. (Function calls need to be used when both operands are integers, to bypass Python's arithmetic.) @example@
@example@ Equal(Neg(Neg(x)), x, Pos(x)) | Usage note: @@Pos(x)@@ represents the identity function. @example@
@example@ Tuple(Less(a, b), LessEqual(a, b), Greater(a, b), GreaterEqual(a, b), Equal(a, b), NotEqual(a, b)) | Comparisons. @example@
@example@ Equal(Decimal("-3.25"), -Div(325,100)) | Grim does not have floating-point literals or floating-point numbers as a distinct type. The <tt>Decimal</tt> function takes a decimal floating-point string as input, describing a rational number. @example@
@example@ And(Equal(Decimal("2.0e-123456789"), Div(2, Pow(10, 123456789))), Less(3, Pow(10,Pow(10,Pow(10,Pow(10,10)))))) | Reminder that we are working with symbolic expressions: numbers are not "evaluated" when constructing expressions, so we do not need to worry about large numbers causing overflow or being inefficient. @example@
<h3>Infinities and undefined values</h3>
@example@ Infinity | This symbol represents a quantity larger than any real number. By definition, @@Equal(Pos(Infinity), Infinity)@@.
Multiplication of @@Infinity@@ by a nonzero complex number represents an infinite limit
with the given direction in the complex plane. In particular, @@Set(-Infinity, ConstI*Infinity, -(ConstI*Infinity))@@ are frequently used. @example@
@example@ UnsignedInfinity | This symbol represents a quantity with infinite magnitude and undefined sign.
It is typically used to represent the value of meromorphic functions at poles,
including the special case of dividing a nonzero number by zero: @@Equal(Div(1, 0), UnsignedInfinity)@@.
The set @@Union(CC, Set(UnsignedInfinity))@@ represents the complex Riemann sphere. @example@
@example@ Equal(Tuple(1 / Infinity, 1 / UnsignedInfinity, Infinity + Infinity, UnsignedInfinity + UnsignedInfinity, Infinity - Infinity, Infinity / Infinity), Tuple(0, 0, Infinity, Undefined, Undefined, Undefined)) | Arithmetic involving infinities
gives a number or infinity when the limiting value is unambiguous, otherwise is usually undefined. @example@
@example@ Equal(Pow(0, 0), 1) | This special case is well-defined, as a matter of convention. @example@
@example@ Equal(Infinity + 1, Infinity + ConstI, Infinity) | Any infinity completely absorbs any (finite) number added to it.
This includes the case of complex numbers added to the infinities @@Set(Infinity, -Infinity)@@ with real direction.
This convention will make some people unhappy some of the time, but so would the opposite convention. @example@
<h3>Sets of numbers</h3>
@example@ Tuple(ZZ, QQ, RR, CC, AlgebraicNumbers) | Standard sets of numbers. @example@
@example@ And(NotElement(Sqrt(2), QQ), Element(Sqrt(2), AlgebraicNumbers), NotElement(Pi, AlgebraicNumbers), Element(Pi, RR)) @example@
@example@ Equal(QQ, Set(Div(p, q), For(Tuple(p, q)), And(Element(p, ZZ), Element(q, SetMinus(ZZ, Set(0)))))) @example@
@example@ Equal(CC, Set(Add(x, Mul(y, ConstI)), For(Tuple(x, y)), And(Element(x, RR), Element(y, RR)))) @example@
@example@ Tuple(ClosedInterval(a,b), OpenInterval(a,b), ClosedOpenInterval(a, b), OpenClosedInterval(a, b)) |
Intervals represent contiguous subsets of the extended real line @@Equal(S, Union(RR, Set(-Infinity, Infinity)))@@,
with or without endpoints included.
The endpoints must be elements of @@S@@. @example@
@example@ Tuple(ZZGreaterEqual(1), ZZGreaterEqual(0), ZZLessEqual(0), Range(1, 10)) | Useful ranges of integers. @example@
@example@ Equal(Div(ClosedOpenInterval(4, 6), -2), OpenClosedInterval(-3, -2)) | Arithmetic operations between numbers and sets of numbers apply pointwise. @example@
@example@ Equal(Add(ClosedInterval(a, b), ClosedInterval(c, d)*ConstI), Set(x+y*ConstI, ForElement(Tuple(x, y), CartesianProduct(ClosedInterval(a, b), ClosedInterval(c, d))))) | Applying an arithmetic operation to two sets of numbers evaluates the operation over the Cartesian product of arguments. @example@
@example@ And(Subset(AlgebraicNumbers, CC), Element(Sqrt(-1), AlgebraicNumbers), Element(Sqrt(-1), CC)) | The algebraic numbers are considered canonically embedded in the complex numbers. @example@
<h3>p-adic numbers</h3>
<p>The <i>p</i>-adic numbers (for a given prime @@p@@) are an extension of the rational numbers.</p>
@example@ And(Subset(ZZ, ZZp(p)), Subset(QQ, QQp(p)), Subset(ZZp(p), QQp(p))) @example@
<p>The <i>p</i>-adic number 1 is considered the same object as the integer 1 and the complex number 1,
and rational arithmetic involving <i>p</i>-adic numbers requires no special notation.
However, mixing <i>p</i>-adic numbers with irrational real and complex numbers is meaningless.
Any operation that implicitly or explicitly involves norms or limits (such as summation of infinite series
and evaluation of transcendental functions) must be expressed using dedicated
functions for the <i>p</i>-adic norm.
</p>
<ul>
<li><span style="color:red">
TODO: This is tentative...
</li>
<li><span style="color:red">
TODO: Algebraic numbers with <i>p</i>-adic numbers.
</li>
</ul>
<h2>Functions</h2>