-
Notifications
You must be signed in to change notification settings - Fork 15
/
documentation.html
2301 lines (1913 loc) · 143 KB
/
documentation.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
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<!-- 2020-12-21 Mon 21:22 -->
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>Musa Al-hassy's Personal Glossary</title>
<meta name="generator" content="Org mode" />
<meta name="author" content="Musa Al-hassy" />
<style type="text/css">
<!--/*--><![CDATA[/*><!--*/
.title { text-align: center;
margin-bottom: .2em; }
.subtitle { text-align: center;
font-size: medium;
font-weight: bold;
margin-top:0; }
.todo { font-family: monospace; color: red; }
.done { font-family: monospace; color: green; }
.priority { font-family: monospace; color: orange; }
.tag { background-color: #eee; font-family: monospace;
padding: 2px; font-size: 80%; font-weight: normal; }
.timestamp { color: #bebebe; }
.timestamp-kwd { color: #5f9ea0; }
.org-right { margin-left: auto; margin-right: 0px; text-align: right; }
.org-left { margin-left: 0px; margin-right: auto; text-align: left; }
.org-center { margin-left: auto; margin-right: auto; text-align: center; }
.underline { text-decoration: underline; }
#postamble p, #preamble p { font-size: 90%; margin: .2em; }
p.verse { margin-left: 3%; }
pre {
border: 1px solid #ccc;
box-shadow: 3px 3px 3px #eee;
padding: 8pt;
font-family: monospace;
overflow: auto;
margin: 1.2em;
}
pre.src {
position: relative;
overflow: auto;
padding-top: 1.2em;
}
pre.src:before {
display: none;
position: absolute;
background-color: white;
top: -10px;
right: 10px;
padding: 3px;
border: 1px solid black;
}
pre.src:hover:before { display: inline; margin-top: 14px;}
/* Languages per Org manual */
pre.src-asymptote:before { content: 'Asymptote'; }
pre.src-awk:before { content: 'Awk'; }
pre.src-C:before { content: 'C'; }
/* pre.src-C++ doesn't work in CSS */
pre.src-clojure:before { content: 'Clojure'; }
pre.src-css:before { content: 'CSS'; }
pre.src-D:before { content: 'D'; }
pre.src-ditaa:before { content: 'ditaa'; }
pre.src-dot:before { content: 'Graphviz'; }
pre.src-calc:before { content: 'Emacs Calc'; }
pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
pre.src-fortran:before { content: 'Fortran'; }
pre.src-gnuplot:before { content: 'gnuplot'; }
pre.src-haskell:before { content: 'Haskell'; }
pre.src-hledger:before { content: 'hledger'; }
pre.src-java:before { content: 'Java'; }
pre.src-js:before { content: 'Javascript'; }
pre.src-latex:before { content: 'LaTeX'; }
pre.src-ledger:before { content: 'Ledger'; }
pre.src-lisp:before { content: 'Lisp'; }
pre.src-lilypond:before { content: 'Lilypond'; }
pre.src-lua:before { content: 'Lua'; }
pre.src-matlab:before { content: 'MATLAB'; }
pre.src-mscgen:before { content: 'Mscgen'; }
pre.src-ocaml:before { content: 'Objective Caml'; }
pre.src-octave:before { content: 'Octave'; }
pre.src-org:before { content: 'Org mode'; }
pre.src-oz:before { content: 'OZ'; }
pre.src-plantuml:before { content: 'Plantuml'; }
pre.src-processing:before { content: 'Processing.js'; }
pre.src-python:before { content: 'Python'; }
pre.src-R:before { content: 'R'; }
pre.src-ruby:before { content: 'Ruby'; }
pre.src-sass:before { content: 'Sass'; }
pre.src-scheme:before { content: 'Scheme'; }
pre.src-screen:before { content: 'Gnu Screen'; }
pre.src-sed:before { content: 'Sed'; }
pre.src-sh:before { content: 'shell'; }
pre.src-sql:before { content: 'SQL'; }
pre.src-sqlite:before { content: 'SQLite'; }
/* additional languages in org.el's org-babel-load-languages alist */
pre.src-forth:before { content: 'Forth'; }
pre.src-io:before { content: 'IO'; }
pre.src-J:before { content: 'J'; }
pre.src-makefile:before { content: 'Makefile'; }
pre.src-maxima:before { content: 'Maxima'; }
pre.src-perl:before { content: 'Perl'; }
pre.src-picolisp:before { content: 'Pico Lisp'; }
pre.src-scala:before { content: 'Scala'; }
pre.src-shell:before { content: 'Shell Script'; }
pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
/* additional language identifiers per "defun org-babel-execute"
in ob-*.el */
pre.src-cpp:before { content: 'C++'; }
pre.src-abc:before { content: 'ABC'; }
pre.src-coq:before { content: 'Coq'; }
pre.src-groovy:before { content: 'Groovy'; }
/* additional language identifiers from org-babel-shell-names in
ob-shell.el: ob-shell is the only babel language using a lambda to put
the execution function name together. */
pre.src-bash:before { content: 'bash'; }
pre.src-csh:before { content: 'csh'; }
pre.src-ash:before { content: 'ash'; }
pre.src-dash:before { content: 'dash'; }
pre.src-ksh:before { content: 'ksh'; }
pre.src-mksh:before { content: 'mksh'; }
pre.src-posh:before { content: 'posh'; }
/* Additional Emacs modes also supported by the LaTeX listings package */
pre.src-ada:before { content: 'Ada'; }
pre.src-asm:before { content: 'Assembler'; }
pre.src-caml:before { content: 'Caml'; }
pre.src-delphi:before { content: 'Delphi'; }
pre.src-html:before { content: 'HTML'; }
pre.src-idl:before { content: 'IDL'; }
pre.src-mercury:before { content: 'Mercury'; }
pre.src-metapost:before { content: 'MetaPost'; }
pre.src-modula-2:before { content: 'Modula-2'; }
pre.src-pascal:before { content: 'Pascal'; }
pre.src-ps:before { content: 'PostScript'; }
pre.src-prolog:before { content: 'Prolog'; }
pre.src-simula:before { content: 'Simula'; }
pre.src-tcl:before { content: 'tcl'; }
pre.src-tex:before { content: 'TeX'; }
pre.src-plain-tex:before { content: 'Plain TeX'; }
pre.src-verilog:before { content: 'Verilog'; }
pre.src-vhdl:before { content: 'VHDL'; }
pre.src-xml:before { content: 'XML'; }
pre.src-nxml:before { content: 'XML'; }
/* add a generic configuration mode; LaTeX export needs an additional
(add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
pre.src-conf:before { content: 'Configuration File'; }
table { border-collapse:collapse; }
caption.t-above { caption-side: top; }
caption.t-bottom { caption-side: bottom; }
td, th { vertical-align:top; }
th.org-right { text-align: center; }
th.org-left { text-align: center; }
th.org-center { text-align: center; }
td.org-right { text-align: right; }
td.org-left { text-align: left; }
td.org-center { text-align: center; }
dt { font-weight: bold; }
.footpara { display: inline; }
.footdef { margin-bottom: 1em; }
.figure { padding: 1em; }
.figure p { text-align: center; }
.equation-container {
display: table;
text-align: center;
width: 100%;
}
.equation {
vertical-align: middle;
}
.equation-label {
display: table-cell;
text-align: right;
vertical-align: middle;
}
.inlinetask {
padding: 10px;
border: 2px solid gray;
margin: 10px;
background: #ffffcc;
}
#org-div-home-and-up
{ text-align: right; font-size: 70%; white-space: nowrap; }
textarea { overflow-x: auto; }
.linenr { font-size: smaller }
.code-highlighted { background-color: #ffff00; }
.org-info-js_info-navigation { border-style: none; }
#org-info-js_console-label
{ font-size: 10px; font-weight: bold; white-space: nowrap; }
.org-info-js_search-highlight
{ background-color: #ffff00; color: #000000; font-weight: bold; }
.org-svg { width: 90%; }
/*]]>*/-->
</style>
<link href="https://alhassy.github.io/org-notes-style.css" rel="stylesheet" type="text/css" />
<link href="https://alhassy.github.io/floating-toc.css" rel="stylesheet" type="text/css" />
<link href="https://alhassy.github.io/blog-banner.css" rel="stylesheet" type="text/css" />
<style>
/* From: https://endlessparentheses.com/public/css/endless.css */
/* See also: https://meta.superuser.com/questions/4788/css-for-the-new-kbd-style */
kbd
{
-moz-border-radius: 6px;
-moz-box-shadow: 0 1px 0 rgba(0,0,0,0.2),0 0 0 2px #fff inset;
-webkit-border-radius: 6px;
-webkit-box-shadow: 0 1px 0 rgba(0,0,0,0.2),0 0 0 2px #fff inset;
background-color: #f7f7f7;
border: 1px solid #ccc;
border-radius: 6px;
box-shadow: 0 1px 0 rgba(0,0,0,0.2),0 0 0 2px #fff inset;
color: #333;
display: inline-block;
font-family: 'Droid Sans Mono', monospace;
font-size: 80%;
font-weight: normal;
line-height: inherit;
margin: 0 .1em;
padding: .08em .4em;
text-shadow: 0 1px 0 #fff;
word-spacing: -4px;
box-shadow: 2px 2px 2px #222; /* MA: An extra I've added. */
}
</style>
<link rel="stylesheet" type="text/css" href="https://alhassy.github.io/org-special-block-extras/tooltipster/dist/css/tooltipster.bundle.min.css"/>
<link rel="stylesheet" type="text/css" href="https://alhassy.github.io/org-special-block-extras/tooltipster/dist/css/plugins/tooltipster/sideTip/themes/tooltipster-sideTip-punk.min.css" />
<script type="text/javascript">
if (typeof jQuery == 'undefined') {
document.write(unescape('%3Cscript src="https://code.jquery.com/jquery-1.10.0.min.js"%3E%3C/script%3E'));
}
</script>
<script type="text/javascript" src="https://alhassy.github.io/org-special-block-extras/tooltipster/dist/js/tooltipster.bundle.min.js"></script>
<script>
$(document).ready(function() {
$('.tooltip').tooltipster({
theme: 'tooltipster-punk',
contentAsHTML: true,
animation: 'grow',
delay: [100,500],
// trigger: 'click'
trigger: 'custom',
triggerOpen: {
mouseenter: true
},
triggerClose: {
originClick: true,
scroll: true
}
});
});
</script>
<style>
abbr {color: red;}
.tooltip { border-bottom: 1px dotted #000;
color:red;
text-decoration: none;}
</style>
<script type="text/javascript">
// @license magnet:?xt=urn:btih:e95b018ef3580986a04669f1b5879592219e2a7a&dn=public-domain.txt Public Domain
<!--/*--><![CDATA[/*><!--*/
function CodeHighlightOn(elem, id)
{
var target = document.getElementById(id);
if(null != target) {
elem.classList.add("code-highlighted");
target.classList.add("code-highlighted");
}
}
function CodeHighlightOff(elem, id)
{
var target = document.getElementById(id);
if(null != target) {
elem.classList.remove("code-highlighted");
target.classList.remove("code-highlighted");
}
}
/*]]>*///-->
// @license-end
</script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
displayAlign: "center",
displayIndent: "0em",
"HTML-CSS": { scale: 100,
linebreaks: { automatic: "false" },
webFont: "TeX"
},
SVG: {scale: 100,
linebreaks: { automatic: "false" },
font: "TeX"},
NativeMML: {scale: 100},
TeX: { equationNumbers: {autoNumber: "AMS"},
MultLineWidth: "85%",
TagSide: "right",
TagIndent: ".8em"
}
});
</script>
<script type="text/javascript"
src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-AMS_HTML"></script>
</head>
<body>
<div id="content">
<h1 class="title">Musa Al-hassy's Personal Glossary</h1>
<div id="table-of-contents">
<h2>Table of Contents</h2>
<div id="text-table-of-contents">
<ul>
<li><a href="#Logics">1. <a href="#Logics">Logics</a></a></li>
<li><a href="#Properties-of-Operators-Relations">2. <a href="#Properties-of-Operators-Relations">Properties of Operators</a></a></li>
<li><a href="#Properties-of-Homogeneous-Relations">3. <a href="#Properties-of-Homogeneous-Relations">Properties of <i>Homogeneous</i> Relations</a></a></li>
<li><a href="#Properties-of-Heterogeneous-Relations">4. <a href="#Properties-of-Heterogeneous-Relations">Properties of <i>Heterogeneous</i> Relations</a></a></li>
</ul>
</div>
</div>
<blockquote>
<p>
<i>Knowledge is software for your brain: The more you know, the more problems you can solve!</i>
</p>
</blockquote>
<p>
<abbr class="tooltip" title="Hussein ibn Ali is the grandson of Prophet Muhammad, who is known to have<br>declared <strong>“Hussain is from me and I am from Hussain; God loves whoever loves Hussain.”</strong><br><br>He is honoured as “The Chief of Martyrs” for his selfless stand for social justice<br>against Yazid, the corrupt 7ᵗʰ caliph. The Karbala Massacre is commemorated annually<br>in the first Islamic month, Muharram, as a reminder to stand against oppression and tyranny;<br>Jesus Christ, son of Mary, makes an indirect appearance in the story.<br><br>A terse summary of the chain of events leading to the massacre may be found at<br>https://www.al-islam.org/articles/karbala-chain-events.<br><br>An elegant English recitation recounting the Karbala Massacre may be found at<br>https://youtu.be/2i9Y3Km6h08 ---“Arbaeen Maqtal - Sheikh Hamam Nassereddine - 1439”.<br><hr><br> <strong>Charles Dickens:</strong> <em>“If Hussain had fought to quench his worldly desires...then I</em><br><em>do not understand why his sister, wife, and children accompanied him. It stands<br>to reason therefore, that he sacrificed purely for Islam.”</em><br><br><strong>Gandhi:</strong> <em>“I learned from Hussain how to achieve victory while being oppressed.”</em><br><br><strong>Thomas Carlyle:</strong> <em>“The victory of Hussein, despite his minority, marvels me.”</em><br><br><strong>Thomas Masaryk:</strong> <em>“Although our clergies also move us while describing the<br>Christ's sufferings, but the zeal and zest that is found in the followers of</em><br><em>Hussain will not be found in the followers of Christ. And it seems that the<br>suffering of Christ against the suffering of Hussain is like a blade of straw</em> <em>in<br>front of a huge mountain.”</em>">Hussain</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFFF;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Hussain</h3>
<p>
Hussein ibn Ali is the grandson of Prophet Muhammad, who is known to have
declared <b>“Hussain is from me and I am from Hussain; God loves whoever loves Hussain.”</b>
</p>
<p>
He is honoured as “The Chief of Martyrs” for his selfless stand for social justice
against Yazid, the corrupt 7ᵗʰ caliph. The Karbala Massacre is commemorated annually
in the first Islamic month, Muharram, as a reminder to stand against oppression and tyranny;
Jesus Christ, son of Mary, makes an indirect appearance in the story.
</p>
<p>
A terse summary of the chain of events leading to the massacre may be found at
<a href="https://www.al-islam.org/articles/karbala-chain-events">https://www.al-islam.org/articles/karbala-chain-events</a>.
</p>
<p>
An elegant English recitation recounting the Karbala Massacre may be found at
<a href="https://youtu.be/2i9Y3Km6h08">https://youtu.be/2i9Y3Km6h08</a> —“Arbaeen Maqtal - Sheikh Hamam Nassereddine - 1439”.
</p>
<hr />
<p>
<b>Charles Dickens:</b> <i>“If Hussain had fought to quench his worldly desires…then I</i>
<i>do not understand why his sister, wife, and children accompanied him. It stands
to reason therefore, that he sacrificed purely for Islam.”</i>
</p>
<p>
<b>Gandhi:</b> <i>“I learned from Hussain how to achieve victory while being oppressed.”</i>
</p>
<p>
<b>Thomas Carlyle:</b> <i>“The victory of Hussein, despite his minority, marvels me.”</i>
</p>
<p>
<b>Thomas Masaryk:</b> <i>“Although our clergies also move us while describing the
Christ's sufferings, but the zeal and zest that is found in the followers of</i>
<i>Hussain will not be found in the followers of Christ. And it seems that the
suffering of Christ against the suffering of Hussain is like a blade of straw</i> <i>in
front of a huge mountain.”</i>
</p>
</div>
<div id="outline-container-Logics" class="outline-2">
<h2 id="Logics"><span class="section-number-2">1</span> <a href="#Logics">Logics</a></h2>
<div class="outline-text-2" id="text-Logics">
<p>
<abbr class="tooltip" title="A <em>(Partial, resp. Total) Graph</em> <em>G = (V, E, src, tgt)</em> consists of<br>  + <EM>V</EM>, a set of “points, nodes, vertices”<br>  + <EM>E</EM>, a set of “arcs, edges”<br>  + <em>src, tgt : E ↔ V</em>, a pair of <em>partial (resp. total)</em> functions.<br><br>⟦ Tersely put, in any category, a <em>graph</em> is a parallel pair of morphisms. ⟧<br><br><em>Edge parallelism</em> is the relation <em>Ξ = src ⨾ src ˘ ∩ tgt ⨾ tgt˘</em>; two arcs are<br>related when they have the same starting point and the same ending point, which<br>both exist. Joyously, the name ‘Ξ’ is a neat reminder of the concept:<br>The name is three parallel lines, for the concept of edge(line) parallelism.<br><br>+ A graph is <em>total</em> exactly when <em>Id ⊆ Ξ</em>; and so Ξ is an equivalence.<br>+ A graph has <em>no parallel arrows</em> exactly when <em>Ξ ⊆ Id</em>.<br>+ A graph is <em>simple</em> exactly when <em>Ξ = Id</em>.<br><br>The <em>associated relation</em> is the relation <em>_⟶_ = src ˘ ⨾ tgt</em> that relates two nodes<br>when the first is the source of some edge that happens to have the second point<br>as its target. One uses the associated relation to study properties not<br>involving partial or parallel arrows. One writes <em>⟵</em> for <em>⟶˘</em>;<br>one writes ⟶⋆ for the <em>reachability</em> relation.<br><br>+ Node <em>y</em> is <em>reachable via a non-empty path</em> from node <em>x</em> exactly when <em>x ⟶⁺ y</em>.<br> - Node <em>x</em> lies on a cycle exactly when <em>x ⟶⁺ x</em>.<br> - A graph is <em>DAG, acylic, circuit-free,</em> exactly when <em>⟶⁺ ⊆ ∼Id</em>; i.e., <em>⟶⁺ ∩ Id = ⊥</em>.<br> - An acyclic graph is a (<em>directed) forest</em> exactly when ⟶ is injective; i.e.,<br>  every node has at most one predecessor; i.e., <em>⟶ ⨾ ⟵ ⊆ Id</em>.<br>+ A node <em>r</em> is a <em>root</em> exactly when every node is reachable from it; i.e., <em>{r} × V ⊆ ⟶⋆;</em><br> i.e., <em>𝕃 r ⨾ ⟶⋆ = ⊤</em> where <em>𝕃 r</em> is defined by <em>𝕃 r = (ℝ r)˘</em> and <em>x 〔ℝ r〕 y  ≡  x = r</em>.<br> - <em>x〔𝕃 r ⨾ R〕 y  ≡  r〔R〕 y</em> and <em>x 〔R ⨾ ℝ r〕 y  ≡  x 〔R〕 r</em><br> - A <em>tree</em> is a forest with a root.<br>+ A graph is <em>loop free</em> exactly when <em>⟶ ⊆ ∼Id</em>.<br>+ A graph is <em>strongly connected</em> exactly when <em>⟶⋆ = ⊤</em>; i.e., <em>∼Id ⊆ ⟶⁺</em>;<br> i.e., every point is reachable from any <em>other</em> point; i.e., <em>∼Id ⊆ ⟶ ∩ ⟵˘</em>;<br> i.e., any two distinct points lie on an undirected circuit.<br> - The equivalence classes of <em>⟶⋆ ∩ ⟵⋆</em> are the <em>strongly connected components</em>.<br>+ <em>Terminal∣sinks</em> are nodes from which it is <em>not</em> possible to proceed <em>any</em> further;<br> i.e., terminals have no successors; the domain of <em>∼(⟶ ⨾ ⊤)</em> is all terminals.<br>+ <em>Initial∣sources</em> are nodes from which it is <em>not</em> possible to proceed backward;<br> i.e., initials have no predecessors; the domain of <em>∼(⟵ ⨾ ⊤)</em> is all initials.">graph</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFFF;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>graph</h3>
<p>
A <i>(Partial, resp. Total) Graph</i> \(G = (V, E, src, tgt)\) consists of
</p>
<ul class="org-ul">
<li>\(V\), a set of “points, nodes, vertices”</li>
<li>\(E\), a set of “arcs, edges”</li>
<li>\(src, tgt : E ↔ V\), a pair of <i>partial (resp. total)</i> functions.</li>
</ul>
<p>
⟦ Tersely put, in any category, a <i>graph</i> is a parallel pair of morphisms. ⟧
</p>
<p>
<i>Edge parallelism</i> is the relation \(Ξ = src ⨾ src ˘ ∩ tgt ⨾ tgt˘\); two arcs are
related when they have the same starting point and the same ending point, which
both exist. Joyously, the name ‘Ξ’ is a neat reminder of the concept:
The name is three parallel lines, for the concept of edge(line) parallelism.
</p>
<ul class="org-ul">
<li>A graph is <i>total</i> exactly when <i>Id ⊆ Ξ</i>; and so Ξ is an equivalence.</li>
<li>A graph has <i>no parallel arrows</i> exactly when <i>Ξ ⊆ Id</i>.</li>
<li>A graph is <i>simple</i> exactly when <i>Ξ = Id</i>.</li>
</ul>
<p>
The <i>associated relation</i> is the relation <i><span class="underline">⟶</span> = src ˘ ⨾ tgt</i> that relates two nodes
when the first is the source of some edge that happens to have the second point
as its target. One uses the associated relation to study properties not
involving partial or parallel arrows. One writes <i>⟵</i> for <i>⟶˘</i>;
one writes ⟶⋆ for the <i>reachability</i> relation.
</p>
<ul class="org-ul">
<li>Node <i>y</i> is <i>reachable via a non-empty path</i> from node <i>x</i> exactly when <i>x ⟶⁺ y</i>.
<ul class="org-ul">
<li>Node <i>x</i> lies on a cycle exactly when <i>x ⟶⁺ x</i>.</li>
<li>A graph is <i>DAG, acylic, circuit-free,</i> exactly when <i>⟶⁺ ⊆ ∼Id</i>; i.e., <i>⟶⁺ ∩ Id = ⊥</i>.</li>
<li>An acyclic graph is a (<i>directed) forest</i> exactly when ⟶ is injective; i.e.,
every node has at most one predecessor; i.e., \(⟶ ⨾ ⟵ ⊆ Id\).</li>
</ul></li>
<li>A node <i>r</i> is a <i>root</i> exactly when every node is reachable from it; i.e., <i>{r} × V ⊆ ⟶⋆;</i>
i.e., <i>𝕃 r ⨾ ⟶⋆ = ⊤</i> where <i>𝕃 r</i> is defined by \(𝕃 r = (ℝ r)˘\) and \(x 〔ℝ r〕 y \;≡\; x = r\).
<ul class="org-ul">
<li>\(x〔𝕃 r ⨾ R〕 y \;≡\; r〔R〕 y\) and \(x 〔R ⨾ ℝ r〕 y \;≡\; x 〔R〕 r\)</li>
<li>A <i>tree</i> is a forest with a root.</li>
</ul></li>
<li>A graph is <i>loop free</i> exactly when <i>⟶ ⊆ ∼Id</i>.</li>
<li>A graph is <i>strongly connected</i> exactly when <i>⟶⋆ = ⊤</i>; i.e., <i>∼Id ⊆ ⟶⁺</i>;
i.e., every point is reachable from any <i>other</i> point; i.e., <i>∼Id ⊆ ⟶ ∩ ⟵˘</i>;
i.e., any two distinct points lie on an undirected circuit.
<ul class="org-ul">
<li>The equivalence classes of <i>⟶⋆ ∩ ⟵⋆</i> are the <i>strongly connected components</i>.</li>
</ul></li>
<li><i>Terminal∣sinks</i> are nodes from which it is <i>not</i> possible to proceed <i>any</i> further;
i.e., terminals have no successors; the domain of <i>∼(⟶ ⨾ ⊤)</i> is all terminals.</li>
<li><i>Initial∣sources</i> are nodes from which it is <i>not</i> possible to proceed backward;
i.e., initials have no predecessors; the domain of <i>∼(⟵ ⨾ ⊤)</i> is all initials.</li>
</ul>
</div>
<p>
<abbr class="tooltip" title="An <em>expression</em> is either a ‘variable’ or a ‘function application’; i.e., the name<br>of a function along with a number of existing expressions.<br><br> Expr ::= Constant  -- E.g., 1 or “apple”<br>   | Variable  -- E.g., x or apple (no quotes!)<br>   | Application -- E.g., f(x₁, x₂, …, xₙ)<br><br>( One reads ‘:=’ as <em>becomes</em> and so the addition of an extra colon results in a<br>‘stutter’: One reads ‘∷=’ as <em>be-becomes</em>. The symbol ‘|’ is read <em>or</em>. )<br><br>Notice that a constant is really just an application with <em>n</em> being <em>0</em> arguments<br>and so the first line in the definition above could be omitted.<br><br><hr><br><br>In a sense, an expression is like a sentence with the variables acting as<br>pronouns and the function applications acting as verb clauses and the argument<br>to the application are the participants in the action of the verbal clause.<br><br>A <strong>variable of type τ</strong> is a <em>name</em> denoting a yet unknown <em>value</em> of type τ;<br>i.e., “it is a pronoun (nickname) referring to a person in the collection of people τ”.<br>E.g., to say <em>x</em> is an integer variable means that we may treat it<br>as if it were a number whose precise value is unknown.<br>Then, if we let =Expr τ= refer to the expressions denoting <em>values</em> of type τ;<br>then a <strong>meta-variable</strong> is simply a normal variable of type =Expr τ=.<br><br>That is, when we write phrases like =“Let E be an expression”=, then the <em>name</em> <EM>E</EM><br>varies and so is a variable, but it is an expression and so may consist of a<br>function application or a variable. <strong>That is, <EM>E</EM> is a variable that may stand<br>for variables.</strong> This layered inception is resolved by referring to <EM>E</EM> as not<br>just any normal variable, but instead as a <strong>meta-variable</strong>: A variable capable of<br>referring to other (simpler) variables.<br><br><hr><br><br>Expressions, as defined above, are also known as <em>abstract syntax trees</em> (AST) or<br><em>prefix notation</em>. Then <em>textual substitution</em> is known as ‘grafting trees’ (a<br>monadic bind).<br><br>Their use can be clunky, such as by requiring many parentheses and implicitly<br>forcing a syntactic distinction between equivalent expressions; e.g.,<br><em>gcd(m,gcd(n,p))</em> and <em>gcd(gcd(m,n),p)</em> look difference even though <em>gcd</em> is<br>associative.<br><br>As such, one can declare <em>precedence levels</em> ---a.k.a. <em>binding power</em>--- to reduce<br>parentheses, one can declare fixity ---i.e., have arguments around operation<br>names---, and, finally, one can declare association ---whether sequential<br>instances of an operation should be read with implicit parenthesis to the right<br>or the to the left--- to reduce syntactic differences. The resulting expression<br>are now known to be in a <em>concrete syntax</em> ---i.e., in a syntactic shape that is<br>more concrete.<br><br>That is, the <strong>conventions</strong> on how a <em>string</em> should be parsed as a <em>tree</em> are known as a<br><strong>precedence, fixity, and associativity rules.</strong><br><br>Similarly, not for operators but one treats <em>relations</em> <strong>conjunctionally</strong> to reduce<br>the number of ‘and’(∧) symbols; e.g. <em>x ≤ y + 2 = z  ≡  x ≤ (y + 2)  ∧  (y + 2) = z</em>.<br>This is very useful to avoid repeating lengthy common expressions, such as <em>y + 2</em>.">Expression</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFCC;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Expression</h3>
<p>
An <i>expression</i> is either a ‘variable’ or a ‘function application’; i.e., the name
of a function along with a number of existing expressions.
</p>
<pre class="example" id="org2667093">
Expr ::= Constant -- E.g., 1 or “apple”
| Variable -- E.g., x or apple (no quotes!)
| Application -- E.g., f(x₁, x₂, …, xₙ)
</pre>
<p>
( One reads ‘:=’ as <i>becomes</i> and so the addition of an extra colon results in a
‘stutter’: One reads ‘∷=’ as <i>be-becomes</i>. The symbol ‘|’ is read <i>or</i>. )
</p>
<p>
Notice that a constant is really just an application with <i>n</i> being <i>0</i> arguments
and so the first line in the definition above could be omitted.
</p>
<hr />
<p>
In a sense, an expression is like a sentence with the variables acting as
pronouns and the function applications acting as verb clauses and the argument
to the application are the participants in the action of the verbal clause.
</p>
<p>
A <b>variable of type τ</b> is a <i>name</i> denoting a yet unknown <i>value</i> of type τ;
i.e., “it is a pronoun (nickname) referring to a person in the collection of people τ”.
E.g., to say \(x\) is an integer variable means that we may treat it
as if it were a number whose precise value is unknown.
Then, if we let <code>Expr τ</code> refer to the expressions denoting <i>values</i> of type τ;
then a <b>meta-variable</b> is simply a normal variable of type <code>Expr τ</code>.
</p>
<p>
That is, when we write phrases like <code>“Let E be an expression”</code>, then the <i>name</i> \(E\)
varies and so is a variable, but it is an expression and so may consist of a
function application or a variable. <b>That is, \(E\) is a variable that may stand
for variables.</b> This layered inception is resolved by referring to \(E\) as not
just any normal variable, but instead as a <b>meta-variable</b>: A variable capable of
referring to other (simpler) variables.
</p>
<hr />
<p>
Expressions, as defined above, are also known as <i>abstract syntax trees</i> (AST) or
<i>prefix notation</i>. Then <i>textual substitution</i> is known as ‘grafting trees’ (a
monadic bind).
</p>
<p>
Their use can be clunky, such as by requiring many parentheses and implicitly
forcing a syntactic distinction between equivalent expressions; e.g.,
<i>gcd(m,gcd(n,p))</i> and <i>gcd(gcd(m,n),p)</i> look difference even though <i>gcd</i> is
associative.
</p>
<p>
As such, one can declare <i>precedence levels</i> —a.k.a. <i>binding power</i>— to reduce
parentheses, one can declare fixity —i.e., have arguments around operation
names—, and, finally, one can declare association —whether sequential
instances of an operation should be read with implicit parenthesis to the right
or the to the left— to reduce syntactic differences. The resulting expression
are now known to be in a <i>concrete syntax</i> —i.e., in a syntactic shape that is
more concrete.
</p>
<p>
That is, the <b>conventions</b> on how a <i>string</i> should be parsed as a <i>tree</i> are known as a
<b>precedence, fixity, and associativity rules.</b>
</p>
<p>
Similarly, not for operators but one treats <i>relations</i> <b>conjunctionally</b> to reduce
the number of ‘and’(∧) symbols; e.g. \(x ≤ y + 2 = z \quad≡\quad x ≤ (y + 2) \,∧\, (y + 2) = z\).
This is very useful to avoid repeating lengthy common expressions, such as <i>y + 2</i>.
</p>
</div>
<p>
<abbr class="tooltip" title="How we prove a theorem <em>P  n</em> ranging over natural numbers <em>n</em>?<br><br>For instance, suppose the property <EM>P</EM> is that using only 3 and 5 dollar bills,<br>any amount of money that is at-least 8 dollars can be formed.<br><br>Since there are an infinite number of natural numbers, it is not possibly to<br>verify <em>P  n</em> is true by <em>evaluating</em> <em>P  n</em> at each natural number <em>n</em>.<br><br><strong>Knocking over dominos is induction:</strong><br>The natural numbers are like an infinite number of dominoes ---i.e., standing<br>tiles one after the other, in any arrangement. Can all dominoes be knocked over?<br>That is, if we construe <em>P  n</em> to mean “the <em>n</em>-th domino can be knocked over”,<br>then the question is “is <em>∀ n • P  n</em> true”. Then, clearly if we can knock over<br>the first domino, <EM>P  0</EM>, and if when a domino is knocked over then it also<br>knocks over the next domino, <em>P  n ⇒ P  (n + 1)</em>, then ‘clearly’ all dominoes<br>will be knocked over. This ‘basic observation’ is known as <em>induction</em>.<br><br><strong>Climbing a ladder is induction:</strong><br>The natural numbers are like an infinite ladder ascending to heaven. Can we<br>reach every step, rung, on the ladder? That is, if we construe <em>P  n</em> to mean<br>“the <em>n</em>-th rung is reachable”, then the question is “is <em>∀ n • P  n</em><br>true”. Then, clearly if we can reach the first rung, <EM>P  0</EM>, and whenever we<br>climb to a rung then we can reach up and grab the next rung, <em>P  n ⇒ P  (n +<br>1)</em>, then ‘clearly’ all rungs of the ladder can be reached. This ‘basic<br>observation’ is known as <em>induction</em>.<br><br><strong>Constant functions are induction:</strong><br>A predicate <EM>P : ℕ → 𝔹</EM> is a function. When is such a function constantly the<br>value <em>\true</em>? That is, when is <em>∀ n • P  n = \true</em>? Clearly, if <EM>P</EM> starts<br>off being <em>\true</em> ---i.e., <em>P 0</em>--- and it preserves truth at every step ---i.e.,<br><em>P n ⇒ P (n + 1)</em>--- then <em>P n</em> will be true for any choice of <em>n</em>.<br><br>That is, if we consider <em>(ℕ, ≤)</em> and <em>(𝔹, ⇒)</em> as ordered sets and <EM>P</EM> starts at<br>the ‘top’ of 𝔹 ---i.e., <em>P 0 = true</em>--- and it is ascending ---i.e., <em>P n ⇒ P (n +<br>1)</em>--- and so ‘never goes down’, then clearly it must stay constantly at the top<br>value of 𝔹. This ‘basic observation’ is known as <em>induction</em>.<br><br><br>⟦ For the money problem, we need to start somewhere else besides 0. ⟧<br><br><strong>Principle of (“Weak”) Mathematical Induction:</strong><br>To show that a property <EM>P</EM> is true for all natural numbers starting with some<br>number <em>n_0</em>, show the following two properties:<br>+ Base case :: Show that <em>P  n₀</em> is true.<br>+ Inductive Step :: Show that whenever (the <strong>inductive hypothesis</strong>) <em>n</em> is a<br> natural number that such that <em>n ≥ n₀</em> and <em>P  n</em> is true, then <em>P  (n + 1)</em><br> is also true.<br><br>⟦ For the money problem, we need to be able to use the fact that to prove<br><em>P (n + 1)</em> we must have already proven <EM>P</EM> for all smaller values. ⟧<br><br><strong>Principle of (“Strong”) Mathematical Induction</strong>:<br>To show that a property <EM>P</EM> is true for all natural numbers starting with some<br>number <em>n_0</em>, show the following two properties:<br>+ Base case :: Show that <em>P  n₀</em> is true.<br>+ Inductive Step :: Show that whenever (the <strong>inductive hypothesis</strong>) <em>n</em> is a<br> natural number that such that <em>n ≥ n₀</em> and <em>P  n_0, P  (n_0 + 1), P  (n_0 +<br> 2), …, P  n</em> are true, then <em>P  (n + 1)</em> is also true.<br><br>⟦ The ‘strength’ of these principles refers to the strength of the inductive<br>hypothesis. The principles are provably equivalent. ⟧<br><br># (It is also a way to say that ℕ has non-empty meets.)<br><strong>The Least Number Principle (LNP) ---Another way to see induction:</strong><br>Every non-empty subset of the natural numbers must have a least element,<br>‘obviously’. This is (strong) induction.<br># Possibly infinite!<br><br>Application of LNP to showing that algorithms terminate:<br>In particular, every decreasing non-negative sequence of integers<br><em>r₀ > r₁ > r₂ > ⋯</em> must terminate.<br>#+end_box">Induction</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFFF;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Induction</h3>
<p>
How we prove a theorem \(P\, n\) ranging over natural numbers \(n\)?
</p>
<p>
For instance, suppose the property \(P\) is that using only 3 and 5 dollar bills,
any amount of money that is at-least 8 dollars can be formed.
</p>
<p>
Since there are an infinite number of natural numbers, it is not possibly to
verify \(P\, n\) is true by <i>evaluating</i> \(P\, n\) at each natural number \(n\).
</p>
<p>
<b>Knocking over dominos is induction:</b>
The natural numbers are like an infinite number of dominoes —i.e., standing
tiles one after the other, in any arrangement. Can all dominoes be knocked over?
That is, if we construe \(P\, n\) to mean “the <i>n</i>-th domino can be knocked over”,
then the question is “is \(∀ n • P\, n\) true”. Then, clearly if we can knock over
the first domino, \(P\, 0\), and if when a domino is knocked over then it also
knocks over the next domino, \(P\, n ⇒ P\, (n + 1)\), then ‘clearly’ all dominoes
will be knocked over. This ‘basic observation’ is known as <i>induction</i>.
</p>
<p>
<b>Climbing a ladder is induction:</b>
The natural numbers are like an infinite ladder ascending to heaven. Can we
reach every step, rung, on the ladder? That is, if we construe \(P\, n\) to mean
“the <i>n</i>-th rung is reachable”, then the question is “is \(∀ n • P\, n\)
true”. Then, clearly if we can reach the first rung, \(P\, 0\), and whenever we
climb to a rung then we can reach up and grab the next rung, \(P\, n ⇒ P\, (n +
1)\), then ‘clearly’ all rungs of the ladder can be reached. This ‘basic
observation’ is known as <i>induction</i>.
</p>
<p>
<b>Constant functions are induction:</b>
A predicate \(P : ℕ → 𝔹\) is a function. When is such a function constantly the
value \(\true\)? That is, when is \(∀ n • P\, n = \true\)? Clearly, if \(P\) starts
off being \(\true\) —i.e., <i>P 0</i>— and it preserves truth at every step —i.e.,
<i>P n ⇒ P (n + 1)</i>— then <i>P n</i> will be true for any choice of \(n\).
</p>
<p>
That is, if we consider \((ℕ, ≤)\) and \((𝔹, ⇒)\) as ordered sets and \(P\) starts at
the ‘top’ of 𝔹 —i.e., <i>P 0 = true</i>— and it is ascending —i.e., <i>P n ⇒ P (n +
1)</i>— and so ‘never goes down’, then clearly it must stay constantly at the top
value of 𝔹. This ‘basic observation’ is known as <i>induction</i>.
</p>
<p>
⟦ For the money problem, we need to start somewhere else besides 0. ⟧
</p>
<p>
<b>Principle of (“Weak”) Mathematical Induction:</b>
To show that a property \(P\) is true for all natural numbers starting with some
number \(n_0\), show the following two properties:
</p>
<dl class="org-dl">
<dt>Base case</dt><dd>Show that \(P\, n₀\) is true.</dd>
<dt>Inductive Step</dt><dd>Show that whenever (the <b>inductive hypothesis</b>) \(n\) is a
natural number that such that \(n ≥ n₀\) and \(P\, n\) is true, then \(P\, (n + 1)\)
is also true.</dd>
</dl>
<p>
⟦ For the money problem, we need to be able to use the fact that to prove
\(P\,(n + 1)\) we must have already proven \(P\) for all smaller values. ⟧
</p>
<p>
<b>Principle of (“Strong”) Mathematical Induction</b>:
To show that a property \(P\) is true for all natural numbers starting with some
number \(n_0\), show the following two properties:
</p>
<dl class="org-dl">
<dt>Base case</dt><dd>Show that \(P\, n₀\) is true.</dd>
<dt>Inductive Step</dt><dd>Show that whenever (the <b>inductive hypothesis</b>) \(n\) is a
natural number that such that \(n ≥ n₀\) and \(P\, n_0, P\, (n_0 + 1), P\, (n_0 +
2), …, P\, n\) are true, then \(P\, (n + 1)\) is also true.</dd>
</dl>
<p>
⟦ The ‘strength’ of these principles refers to the strength of the inductive
hypothesis. The principles are provably equivalent. ⟧
</p>
<p>
<b>The Least Number Principle (LNP) —Another way to see induction:</b>
Every non-empty subset of the natural numbers must have a least element,
‘obviously’. This is (strong) induction.
</p>
<p>
Application of LNP to showing that algorithms terminate:
In particular, every decreasing non-negative sequence of integers
\(r₀ > r₁ > r₂ > ⋯\) must terminate.
#+end<sub>box</sub>
</p>
</div>
<p>
<abbr class="tooltip" title="The <strong>(simultaneous textual) Substitution operation</strong> <em>E[\vec x ≔ \vec F]</em> replaces<br>all variables <em>\vec x</em> with parenthesised expressions <em>\vec F</em> in an expression<br><EM>E</EM>. In particular, <em>E[x ≔ F]</em> is just <EM>E</EM> but with all occurrences of <em>x</em><br>replaced by <em>“(F)”</em>. This is the “find-and-replace” utility you use on your<br>computers.<br><br>Textual substitution on expressions is known as “grafting” on trees: Evaluate<br><em>E[x ≔ F]</em> by going down the tree <EM>E</EM> and finding all the ‘leaves’ labelled <em>x</em>,<br>cut them out and replace them with the new trees <EM>F</EM>.<br><br>Since expressions are either variables of functions applications,<br>substitution can be defined inductively/recursively by the following two clauses:<br><br>+ <em>y[x ≔ F]       = if x = y then F else y fi</em><br>+ <em>f(t₁, …, tₙ)[x ≔ F] = f(t₁′, …, tₙ′)  where tᵢ′ = tᵢ[x ≔ F]</em><br><br><hr><br><br>Sequential ≠ Simultaneous:<br> <em>(x + 2 · y)[x ≔ y][y ≔ x] ≠ (x + 2 · y)[x, y ≔ y, x]</em><br><br>Python (https://alhassy.github.io/PythonCheatSheet/CheatSheet.pdf), for example, has simultaneous <em>assignment</em>;<br>e.g., <code>x, y = y, x</code> is used to swap the value of two variables.<br><br><hr><br><br>A <em>function</em> <em>f</em> is a rule for computing a value from another value.<br><br>If we define <em>f  x = E</em> using an expression, then <em>function application</em> can be<br>defined using textual substitution: <em>f   X = E[x ≔ X]</em>. That is, expressions<br>can be considered functions of their variables ---but it is still expressions<br>that are the primitive idea, the building blocks.">Textual_Substitution</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFCC;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Textual_Substitution</h3>
<p>
The <b>(simultaneous textual) Substitution operation</b> \(E[\vec x ≔ \vec F]\) replaces
all variables \(\vec x\) with parenthesised expressions \(\vec F\) in an expression
\(E\). In particular, \(E[x ≔ F]\) is just \(E\) but with all occurrences of \(x\)
replaced by \(“(F)”\). This is the “find-and-replace” utility you use on your
computers.
</p>
<p>
Textual substitution on expressions is known as “grafting” on trees: Evaluate
\(E[x ≔ F]\) by going down the tree \(E\) and finding all the ‘leaves’ labelled \(x\),
cut them out and replace them with the new trees \(F\).
</p>
<p>
Since expressions are either variables of functions applications,
substitution can be defined inductively/recursively by the following two clauses:
</p>
<ul class="org-ul">
<li><i>y[x ≔ F] = if x = y then F else y fi</i></li>
<li><i>f(t₁, …, tₙ)[x ≔ F] = f(t₁′, …, tₙ′) where tᵢ′ = tᵢ[x ≔ F]</i></li>
</ul>
<hr />
<p>
Sequential ≠ Simultaneous:
<i>(x + 2 · y)[x ≔ y][y ≔ x] ≠ (x + 2 · y)[x, y ≔ y, x]</i>
</p>
<p>
<a href="https://alhassy.github.io/PythonCheatSheet/CheatSheet.pdf">Python</a>, for example, has simultaneous <i>assignment</i>;
e.g., <code>x, y = y, x</code> is used to swap the value of two variables.
</p>
<hr />
<p>
A <i>function</i> \(f\) is a rule for computing a value from another value.
</p>
<p>
If we define \(f\, x = E\) using an expression, then <i>function application</i> can be
defined using textual substitution: \(f \, X = E[x ≔ X]\). That is, expressions
can be considered functions of their variables —but it is still expressions
that are the primitive idea, the building blocks.
</p>
</div>
<p>
<abbr class="tooltip" title="Formally, a “proof” is obtained by applying a number of “rules” to known results<br>to obtain new results; a “theorem” is the conclusion of a “proof”. An “axiom”<br>is a rule that does not need to be applied to any existing results: It's just a<br>known result.<br><br>That is, a <strong>rule</strong> <EM>R</EM> is a tuple <EM>P₁, …, Pₙ, C</EM> that is thought of as ‘taking<br><strong>premises</strong> (instances of known results) <EM>Pᵢ</EM>’ and acting as a ‘natural,<br>reasonable justification’ to obtain <strong>conclusion</strong> <EM>C</EM>. A <strong>proof system</strong> is a<br>collection of rules. At first sight, this all sounds very abstract and rather<br>useless, however it is a <em>game</em>: <strong>Starting from rules, what can you obtain?</strong> Some<br>games can be very fun! Another way to see these ideas is from the view of<br>programming:<br><br>+ Proving ≈ Programming<br>+ Logic  ≈ Trees (algebraic data types, 𝒲-types)<br>+ Rules  ≈ Constructors<br>+ Proof  ≈ An application of constructors<br>+ Axiom  ≈ A constructor with no arguments<br><br>Just as in elementary school one sees addition ‘+’ as a fraction with the<br>arguments above the horizontal line and their sum below the line, so too is that<br>notation reused for inference rules: Premises are above the fraction's bar and<br>the conclusion is below.<br>                  12<br>P₁, P₂, …, Pn          + 7<br><hr>R   versues   ----<br>   C              19<br><br>Just as there are meta-variables and meta-theorems, there is ‘meta-syntax’:<br>- The use of a fraction to delimit premises from conclusion is a form of ‘implication’.<br>- The use of a comma, or white space, to separate premises is a form of ‘conjunction’.<br><br>If our expressions actually have an implication and conjunction operation, then<br>inference rule above can be presented as an axiom <EM>P₁  ∧  ⋯  ∧  Pₙ  ⇒  C</EM>.<br><br>The inference rule says “if the <EM>Pᵢ</EM> are all valid, i.e., true in <em>all states</em>,<br>then so is <EM>C</EM>”; the axiom, on the other hand, says “if the <EM>Pᵢ</EM> are true in <em>a<br>state</em>, then <EM>C</EM> is true in <em>that state</em>.” Thus the rule and the axiom are not<br>quite the same.<br><br>Moreover, the rule is not a Boolean expression. Rules are thus more general,<br>allowing us to construct systems of reasoning that have no concrete notions of<br>‘truth’ ---e.g., the above arithmetic rule says from the things above the<br>fraction bar, using the operation ‘+’, we <em>can get</em> the thing below the bar, but<br>that thing (19) is not ‘true’ as we may think of conventional truth.<br><br>Finally, the rule asserts that <EM>C</EM> follows from <EM>P₁, …, Pₙ</EM>. The formula <em>P₁<br> ∧  ⋯  ∧  Pₙ  ⇒  C</em>, on the other hand, is an expression (but it need not<br>be a theorem).<br><br>A “theorem” is a syntactic concept: Can we play the game of moving symbols to<br>get this? Not “is the meaning of this true”! ‘Semantic concepts’ rely on<br>‘states’, assignments of values to variables so that we can ‘evaluate, simplify’<br>statements to deduce if they are true.<br><br>Syntax is like static analysis; semantics is like actually running the program<br>(on some, or all possible inputs).<br><br><hr><br><br>One reads/writes a <em>natural deduction proof (tree)</em> from the very <strong>bottom</strong>: Each<br>line is an application of a rule of reasoning, whose assumptions are above the<br>line; so read/written upward. The <strong>benefit</strong> of this approach is that <strong>rules guide<br>proof construction</strong>; i.e., it is goal-directed.<br><br>However the <strong>downsides are numerous</strong>:<br>- So much horizontal space is needed even for simple proofs.<br>- One has to <strong>repeat</strong> common subexpressions; e.g., when using transitivity of equality.<br>- For comparison with other proof notations, such as Hilbert style,<br> see Prolog (http://www.cse.yorku.ca/~logicE/misc/logicE_intro.pdf][Equational Propositional Logic]].<br><br> This is more ‘linear’ proof format; also known as <em>equational style</em> or<br> <em>calculational proof</em>. This corresponds to the ‘high-school style’ of writing a<br> sequence of equations, one on each line, along with hints/explanations of how<br> each line was reached from the previous line.<br><br><hr><br><br>Finally, an inference rule says that it is possible to start with the givens<br><EM>Pᵢ</EM> and obtain as result <EM>C</EM>. The idea to use <strong>inference rules as computation</strong><br>is witnessed by the [[https://alhassy.github.io/PrologCheatSheet/CheatSheet.pdf) programming language.">Inference_Rule</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFCC;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Inference_Rule</h3>
<p>
Formally, a “proof” is obtained by applying a number of “rules” to known results
to obtain new results; a “theorem” is the conclusion of a “proof”. An “axiom”
is a rule that does not need to be applied to any existing results: It's just a
known result.
</p>
<p>
That is, a <b>rule</b> \(R\) is a tuple \(P₁, …, Pₙ, C\) that is thought of as ‘taking
<b>premises</b> (instances of known results) \(Pᵢ\)’ and acting as a ‘natural,
reasonable justification’ to obtain <b>conclusion</b> \(C\). A <b>proof system</b> is a
collection of rules. At first sight, this all sounds very abstract and rather
useless, however it is a <i>game</i>: <b>Starting from rules, what can you obtain?</b> Some
games can be very fun! Another way to see these ideas is from the view of
programming:
</p>
<ul class="org-ul">
<li>Proving ≈ Programming</li>
<li>Logic ≈ Trees (algebraic data types, 𝒲-types)</li>
<li>Rules ≈ Constructors</li>
<li>Proof ≈ An application of constructors</li>
<li>Axiom ≈ A constructor with no arguments</li>
</ul>
<p>
Just as in elementary school one sees addition ‘+’ as a fraction with the
arguments above the horizontal line and their sum below the line, so too is that
notation reused for inference rules: Premises are above the fraction's bar and
the conclusion is below.
</p>
<pre class="example" id="org2d9a2e1">
12
P₁, P₂, …, Pn + 7
---------------R versues ----
C 19
</pre>
<p>
Just as there are meta-variables and meta-theorems, there is ‘meta-syntax’:
</p>
<ul class="org-ul">
<li>The use of a fraction to delimit premises from conclusion is a form of ‘implication’.</li>
<li>The use of a comma, or white space, to separate premises is a form of ‘conjunction’.</li>
</ul>
<p>
If our expressions actually have an implication and conjunction operation, then
inference rule above can be presented as an axiom \(P₁ \,∧\, ⋯ \,∧\, Pₙ \,⇒\, C\).
</p>
<p>
The inference rule says “if the \(Pᵢ\) are all valid, i.e., true in <i>all states</i>,
then so is \(C\)”; the axiom, on the other hand, says “if the \(Pᵢ\) are true in <i>a
state</i>, then \(C\) is true in <i>that state</i>.” Thus the rule and the axiom are not
quite the same.
</p>
<p>
Moreover, the rule is not a Boolean expression. Rules are thus more general,
allowing us to construct systems of reasoning that have no concrete notions of
‘truth’ —e.g., the above arithmetic rule says from the things above the
fraction bar, using the operation ‘+’, we <i>can get</i> the thing below the bar, but
that thing (19) is not ‘true’ as we may think of conventional truth.
</p>
<p>
Finally, the rule asserts that \(C\) follows from \(P₁, …, Pₙ\). The formula \(P₁
\,∧\, ⋯ \,∧\, Pₙ \,⇒\, C\), on the other hand, is an expression (but it need not
be a theorem).
</p>
<p>
A “theorem” is a syntactic concept: Can we play the game of moving symbols to
get this? Not “is the meaning of this true”! ‘Semantic concepts’ rely on
‘states’, assignments of values to variables so that we can ‘evaluate, simplify’
statements to deduce if they are true.
</p>
<p>
Syntax is like static analysis; semantics is like actually running the program
(on some, or all possible inputs).
</p>
<hr />
<p>
One reads/writes a <i>natural deduction proof (tree)</i> from the very <b>bottom</b>: Each
line is an application of a rule of reasoning, whose assumptions are above the
line; so read/written upward. The <b>benefit</b> of this approach is that <b>rules guide
proof construction</b>; i.e., it is goal-directed.
</p>
<p>
However the <b>downsides are numerous</b>:
</p>
<ul class="org-ul">
<li>So much horizontal space is needed even for simple proofs.</li>
<li>One has to <b>repeat</b> common subexpressions; e.g., when using transitivity of equality.</li>
<li><p>
For comparison with other proof notations, such as Hilbert style,
see <a href="http://www.cse.yorku.ca/~logicE/misc/logicE_intro.pdf">Equational Propositional Logic</a>.
</p>
<p>
This is more ‘linear’ proof format; also known as <i>equational style</i> or
<i>calculational proof</i>. This corresponds to the ‘high-school style’ of writing a
sequence of equations, one on each line, along with hints/explanations of how
each line was reached from the previous line.
</p></li>
</ul>
<hr />
<p>
Finally, an inference rule says that it is possible to start with the givens
\(Pᵢ\) and obtain as result \(C\). The idea to use <b>inference rules as computation</b>
is witnessed by the <a href="https://alhassy.github.io/PrologCheatSheet/CheatSheet.pdf">Prolog</a> programming language.
</p>
</div>
<p>
<abbr class="tooltip" title="A <em>logic</em> is a formal system of reasoning...<br><br>A <em>logic</em> is a set of symbols along with a set of <em>formulas</em> formed from the<br>symbols, and a set of <em>inference rules</em> which allow formulas to be derived from<br>other formulas. (The formulas may or may not include a notion of variable.)<br><br>Logics are purely syntactic objects; an <em>inference rule</em> is a syntactic mechanism<br>for deriving “truths” or “theorems”.<br><br>In general, proofs are evidence of truth of a claim; by demonstrating that the<br>claim follows from some <em>obvious truth</em> using rules of reasoning that <em>obviously<br>preserve truth.</em>">Logic</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFCC;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Logic</h3>
<p>
A <i>logic</i> is a formal system of reasoning…
</p>
<p>
A <i>logic</i> is a set of symbols along with a set of <i>formulas</i> formed from the
symbols, and a set of <i>inference rules</i> which allow formulas to be derived from
other formulas. (The formulas may or may not include a notion of variable.)
</p>
<p>
Logics are purely syntactic objects; an <i>inference rule</i> is a syntactic mechanism
for deriving “truths” or “theorems”.
</p>
<p>
In general, proofs are evidence of truth of a claim; by demonstrating that the
claim follows from some <i>obvious truth</i> using rules of reasoning that <i>obviously
preserve truth.</i>
</p>
</div>
<p>
<abbr class="tooltip" title="A <em>theorem</em> is a syntactic object, a string of symbols with a particular property.<br><br>A <em>theorem</em> of a calculus is either an axiom or the conclusion of an inference<br>rule whose premises are theorems.<br><br>Different axioms could lead to the same set of theorems, and many texts use<br>different axioms.<br><br><hr><br><br>A “theorem” is a syntactic concept: Can we play the game of moving symbols to<br>get this? Not “is the meaning of this true”! ‘Semantic concepts’ rely on<br>‘states’, assignments of values to variables so that we can ‘evaluate, simplify’<br>statements to deduce if they are true.<br><br>Syntax is like static analysis; semantics is like actually running the program<br>(on some, or all possible inputs).<br><br><hr><br><br>A <strong>meta-theorem</strong> is a general statement about our logic that we prove to be<br>true. That is, if 𝑬 is collection of rules that allows us to find truths, then a<br><em>theorem</em> is a truth found using those rules; whereas a meta-theorem/ is property<br>of 𝑬 itself, such as what theorems it can have. That is, theorems are _in_ 𝑬 and<br>meta-theorems are _about_ 𝑬. For example, here is a meta-theorem that the<br>equational logic 𝑬 has (as do many other theories, such as lattices): An<br><em>equational</em> theorem is true precisely when its ‘dual’ is true. Such metatheorems<br>can be helpful to discover new theorems.<br><br># A meta-theorem is a theorem about theorems.">Theorem</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFFF;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Theorem</h3>
<p>
A <i>theorem</i> is a syntactic object, a string of symbols with a particular property.
</p>
<p>
A <i>theorem</i> of a calculus is either an axiom or the conclusion of an inference
rule whose premises are theorems.
</p>
<p>
Different axioms could lead to the same set of theorems, and many texts use
different axioms.
</p>
<hr />
<p>
A “theorem” is a syntactic concept: Can we play the game of moving symbols to
get this? Not “is the meaning of this true”! ‘Semantic concepts’ rely on
‘states’, assignments of values to variables so that we can ‘evaluate, simplify’
statements to deduce if they are true.
</p>
<p>
Syntax is like static analysis; semantics is like actually running the program
(on some, or all possible inputs).
</p>
<hr />
<p>
A <b>meta-theorem</b> is a general statement about our logic that we prove to be
true. That is, if 𝑬 is collection of rules that allows us to find truths, then a
<i>theorem</i> is a truth found using those rules; whereas a meta-theorem/ is property
of 𝑬 itself, such as what theorems it can have. That is, theorems are <span class="underline">in</span> 𝑬 and
meta-theorems are <span class="underline">about</span> 𝑬. For example, here is a meta-theorem that the
equational logic 𝑬 has (as do many other theories, such as lattices): An
<i>equational</i> theorem is true precisely when its ‘dual’ is true. Such metatheorems
can be helpful to discover new theorems.
</p>
</div>
<p>
<abbr class="tooltip" title="A <em>theorem</em> in the technical sense is an expression derived<br>from axioms using inference rules.<br><br>A <em>metatheorem</em> is a general <strong>statement</strong> about a logic that<br>one argues to be <strong>true</strong>.<br><br>For instance, “any two theorems are equivalent” is a statement that speaks about<br>expressions which happen to be theorems. A logic may not have the linguistic<br>capability to speak of its own expressions and so the statement may not be<br>expressible as an expression <strong>within</strong> the logic ---and so cannot be a theorem of<br>the logic.<br><br>For instance, the logic 𝒑𝑞 has expressions formed from the symbols “𝒑”, “𝒒”, and<br>“-” (dash). It has the axiom schema <em>x𝒑-𝒒x-</em> and the rule “If <em>x𝒑y𝒒z</em> is a theorem<br>then so is <em>x-𝒑y-𝒒z-</em>”. Notice that <em>x, y, z</em> are <em>any</em> strings of dashes;<br>the language of this logic does not have variables and so cannot even speak<br>of its own expressions, let alone its own theorems!<br><br>[Informal] theorems about [technical, logic-specific] theorems are thus termed<br>‘metatheorems’.">Metatheorem</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFCC;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Metatheorem</h3>
<p>
A <i>theorem</i> in the technical sense is an expression derived
from axioms using inference rules.
</p>
<p>
A <i>metatheorem</i> is a general <b>statement</b> about a logic that
one argues to be <b>true</b>.
</p>
<p>
For instance, “any two theorems are equivalent” is a statement that speaks about
expressions which happen to be theorems. A logic may not have the linguistic
capability to speak of its own expressions and so the statement may not be
expressible as an expression <b>within</b> the logic —and so cannot be a theorem of
the logic.
</p>
<p>
For instance, the logic 𝒑𝑞 has expressions formed from the symbols “𝒑”, “𝒒”, and
“-” (dash). It has the axiom schema \(x𝒑-𝒒x-\) and the rule “If \(x𝒑y𝒒z\) is a theorem
then so is \(x-𝒑y-𝒒z-\)”. Notice that \(x, y, z\) are <i>any</i> strings of dashes;
the language of this logic does not have variables and so cannot even speak
of its own expressions, let alone its own theorems!
</p>
<p>
[Informal] theorems about [technical, logic-specific] theorems are thus termed
‘metatheorems’.
</p>
</div>
<p>
<abbr class="tooltip" title="A <em>calculus</em> is a method or process of reasoning by calculation<br>with symbols. A <em>propositional calculus</em> is a method of calculating with Boolean<br>(or propositional) expressions.<br><br><hr><br><br>Calculus: Formalised reasoning through calculation.<br><br>‘Hand wavy’ English arguments tend to favour case analysis —considering what<br>could happen in each possible scenario— which increases exponentially with each<br>variable; in contrast, equality-based calculation is much simpler since it<br>delegates intricate case analysis into codified algebraic laws.">Calculus</abbr> (<abbr class="tooltip" title="A <em>calculus</em> is a method or process of reasoning by calculation<br>with symbols. A <em>propositional calculus</em> is a method of calculating with Boolean<br>(or propositional) expressions.<br><br><hr><br><br>Calculus: Formalised reasoning through calculation.<br><br>‘Hand wavy’ English arguments tend to favour case analysis —considering what<br>could happen in each possible scenario— which increases exponentially with each<br>variable; in contrast, equality-based calculation is much simpler since it<br>delegates intricate case analysis into codified algebraic laws.">Propositional Calculus</abbr>)
</p>
<div style="padding: 1em; background-color: #CCFFFF;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Calculus</h3>
<p>
A <i>calculus</i> is a method or process of reasoning by calculation
with symbols. A <i>propositional calculus</i> is a method of calculating with Boolean
(or propositional) expressions.
</p>
<hr />
<p>
Calculus: Formalised reasoning through calculation.
</p>
<p>
‘Hand wavy’ English arguments tend to favour case analysis —considering what
could happen in each possible scenario— which increases exponentially with each
variable; in contrast, equality-based calculation is much simpler since it
delegates intricate case analysis into codified algebraic laws.
</p>
</div>
<p>
<abbr class="tooltip" title="<strong>Syntax</strong> refers to the structure of expressions, or the rules for putting symbols<br>together to form an expression. <strong>Semantics</strong> refers to the meaning of expressions<br>or how they are evaluated.<br><br>An expression can contain variables, and evaluating such an expression requires<br>knowing what values to use for these variables; i.e., a <strong>state</strong>: A list of<br>variables with associated values. E.g., evaluation of <em>x - y + 2</em> in the state<br>consisting of <em>(x, 5)</em> and <em>(y, 6)</em> is performed by replacing <em>x</em> and <em>y</em> by<br>their values to yield <em>5 - 6 + 2</em> and then evaluating that to yield <em>1</em>.<br><br>A Boolean expression <EM>P</EM> is <strong>satisfied</strong> in a state if its value is <em>true</em> in that<br>state; <EM>P</EM> is <strong>satisfiable</strong> if there is a state in which it is satisfied; and <EM>P</EM><br>is <strong>valid</strong> (or is a <strong>tautology</strong>) if it is satisfied in every state.<br><br><hr><br><br>Often operations are defined by how they are evaluated (<strong>operationally</strong>), we<br>take the alternative route of defining operations by how they can be manipulated<br>(<strong>axiomatically</strong>); i.e., by what properties they satisfy.<br><br>For example, evaluation of the expression <EM>X = Y</EM> in a state yields the value<br><em>true</em> if expressions <EM>X</EM> and <EM>Y</EM> have the same value and yields <em>false</em> if they<br>have different values. This characterisation of equality is in terms of<br>expression <em>evaluation</em>. For <em>reasoning about expressions</em>, a more useful<br>characterisation would be a set of <em>laws</em> that can be used to show that two<br>expressions are equal, <strong>without</strong> calculating their values.<br>--- c.f., static analysis versues running a program.<br><br>For example, you know that <em>x = y</em> equals <em>y = x</em>, regardless of the values of<br><em>x</em> and <em>y</em>. A collection of such laws can be regarded as a definition of<br>equality, <strong>provided</strong> two expressions have the same value in all states precisely<br>when one expression can be translated into the other according to the laws.<br><br>Usually, in <em>a</em> logic, theorems correspond to expressions that are true in all<br>states.<br><br><hr><br><br>That is, instead of defining expressions by how they are evaluated, we may<br>define expressions in terms of how they can be manipulated ---c.f., a calculus.<br><br>For instance, we may define basic manipulative properties of operators ---i.e.,<br><em>axioms</em>--- by considering how the operators behave operationally on particular<br>expressions. That is, one may use an operational, intuitive, approach to obtain<br>an axiomatic specification (characterisation, interface) of the desired<br>properties.<br><br>More concretely, since <em>(p ≡ q) ≡ r</em> and <em>p ≡ (q ≡ r)</em> evaluate to<br>the same value for any choice of values for <em>p, q, r</em>, we may insist that a part<br>of the definition of equivalence is that it be an associative operation.<br><br>Sometimes a single axiom is not enough to ‘pin down’ a unique operator ---i.e.,<br>to ensure we actually have a well-defined operation--- and other times this is<br>cleanly possible; e.g., given an ordering ‘≤’(‘⇒, ⊆, ⊑’) we can define minima<br>‘↓’ (‘∧, ∩, ⊓’) by the axiom: “x ↓ y is the greatest lower bound”;<br>i.e., <em>z ≤ x ↓ y  ≡  z ≤ x  ∧  z ≤ y</em>.">Semantics</abbr>
</p>
<div style="padding: 1em; background-color: #CCFFCC;border-radius: 15px; font-size: 0.9em; box-shadow: 0.05em 0.1em 5px 0.01em #00000057;"><h3>Semantics</h3>
<p>
<b>Syntax</b> refers to the structure of expressions, or the rules for putting symbols
together to form an expression. <b>Semantics</b> refers to the meaning of expressions