-
Notifications
You must be signed in to change notification settings - Fork 15
/
documentation.org.html
1390 lines (1173 loc) · 111 KB
/
documentation.org.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 PUBLIC "-//W3C//DTD HTML 4.01//EN">
<!-- Created by htmlize-1.56 in css mode. -->
<html>
<head>
<title>documentation.org</title>
<style type="text/css">
<!--
body {
color: #81dd71e888a5;
background-color: #fbf8ef;
}
.bold {
/* bold */
font-weight: bold;
}
.comment {
/* font-lock-comment-face */
color: #640eb2edbb7d;
background-color: #ecf3ec;
}
.custom-button {
/* custom-button */
color: #81dd71e888a5;
background-color: #efeae9;
}
.hl-line {
/* hl-line */
background-color: #efeae9;
}
.italic {
/* italic */
font-style: italic;
}
.org-block-begin-line {
/* org-block-begin-line */
color: #a85d9783bef0;
background-color: #ddd8eb;
}
.org-block-end-line {
/* org-block-end-line */
color: #a85d9783bef0;
background-color: #ddd8eb;
}
.org-code {
/* org-code */
color: #66b7c5bdcfc6;
}
.org-document-info-keyword {
/* org-document-info-keyword */
color: #e48ba0f57312;
}
.org-document-title {
/* org-document-title */
color: #88ef57507df2;
font-size: 140%;
font-weight: bold;
text-decoration: underline;
}
.org-drawer {
/* org-drawer */
color: #71aa4437fecf;
}
.org-hide {
/* org-hide */
color: #fbfbf8f7efef;
}
.org-latex-and-related {
/* org-latex-and-related */
color: #a5de67123d2c;
}
.org-level-1 {
/* org-level-1 */
color: #6c4097edccfa;
font-size: 130%;
font-weight: bold;
}
.org-level-2 {
/* org-level-2 */
color: #5ef8a97c8bd2;
font-size: 120%;
font-weight: bold;
}
.org-link {
/* org-link */
color: #640eb2edbb7d;
text-decoration: underline;
}
.org-list-dt {
/* org-list-dt */
font-weight: bold;
}
.org-meta-line {
/* org-meta-line */
color: #e48ba0f57312;
}
.org-property-value {
}
.org-quote {
/* org-quote */
color: #655370;
background-color: #e8e3f0;
font-style: italic;
}
.org-special-keyword {
/* org-special-keyword */
color: #88ef57507df2;
}
.org-table {
/* org-table */
color: #81dd71e888a5;
background-color: #edf1ed;
}
.org-tag {
/* org-tag */
color: #e48ba0f57312;
}
.org-verbatim {
/* org-verbatim */
color: #6c4097edccfa;
}
.underline {
/* underline */
text-decoration: underline;
}
.writegood-passive-voice {
/* writegood-passive-voice-face */
text-decoration: underline;
}
.writegood-weasels {
/* writegood-weasels-face */
text-decoration: underline;
}
a {
color: inherit;
background-color: inherit;
font: inherit;
text-decoration: inherit;
}
a:hover {
text-decoration: underline;
}
-->
</style>
</head>
<body>
<pre>
<span class="org-document-info-keyword">#+title:</span> <span class="org-document-title">Musa Al-hassy's Personal Glossary
</span><span class="comment"># +OPTIONS: broken-links:auto</span>
<span class="org-meta-line">#+HTML_HEAD: <link href="<a href="https://alhassy.github.io/org-notes-style.css">https://alhassy.github.io/org-notes-style.css</a>" rel="stylesheet" type="text/css" /></span>
<span class="org-meta-line">#+HTML_HEAD: <link href="<a href="https://alhassy.github.io/floating-toc.css">https://alhassy.github.io/floating-toc.css</a>" rel="stylesheet" type="text/css" /></span>
<span class="org-meta-line">#+HTML_HEAD: <link href="<a href="https://alhassy.github.io/blog-banner.css">https://alhassy.github.io/blog-banner.css</a>" rel="stylesheet" type="text/css" /></span>
<span class="comment"># The last one has the styling for lists.</span>
<span class="org-block-begin-line">#+begin_quote
</span><span class="org-quote"><span class="italic">Knowledge is software for your brain: The more you know, the more problems you can solve!</span></span><span class="org-quote">
</span><span class="org-block-end-line">#+end_quote
</span>
<span class="org-drawer">:template:</span>...
<span class="org-link"><span class="custom-button"><a href="doc:Hussain">doc:Hussain</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Hussain :show t :color blue :label (Karbala Cosmic_Tragedy)
</span>Hussein ibn Ali is the grandson of Prophet Muhammad, who <span class="writegood-passive-voice">is known</span> to have
declared <span class="bold">“Hussain is from me and I am from Hussain; God loves whoever loves Hussain.”</span>
He <span class="writegood-passive-voice">is honoured</span> as “The Chief of Martyrs” for his selfless stand for social justice
against Yazid, the corrupt 7ᵗʰ caliph. The Karbala Massacre <span class="writegood-passive-voice">is commemorated</span> annually
<span class="hl-line">in the first Islamic month, Muharram, as a reminder to stand against oppression and tyranny;
</span>Jesus Christ, son of Mary, makes an indirect appearance in the story.
A terse summary of the chain of events leading to the massacre may <span class="writegood-passive-voice">be found</span> at
<span class="org-link"><a href="https://www.al-islam.org/articles/karbala-chain-events">https://www.al-islam.org/articles/karbala-chain-events</a></span>.
An elegant English recitation recounting the Karbala Massacre may <span class="writegood-passive-voice">be found</span> at
<span class="org-link"><a href="https://youtu.be/2i9Y3Km6h08">https://youtu.be/2i9Y3Km6h08</a></span> ---“Arbaeen Maqtal - Sheikh Hamam Nassereddine - 1439”.
--------------------------------------------------------------------------------
<span class="bold">Charles Dickens:</span> <span class="italic">“If Hussain had fought to quench his worldly desires...then I</span>
<span class="italic">do not understand why his sister, wife, and children accompanied him. It stands
to reason therefore, that he sacrificed purely for Islam.”</span>
<span class="bold">Gandhi:</span> <span class="italic">“I learned from Hussain how to achieve victory while </span><span class="italic"><span class="writegood-passive-voice">being oppressed</span></span><span class="italic">.”</span>
<span class="bold">Thomas Carlyle:</span> <span class="italic">“The victory of Hussein, despite his minority, marvels me.”</span>
<span class="bold">Thomas Masaryk:</span> <span class="italic">“Although our clergies also move us while describing the
Christ's sufferings, but the zeal and zest that </span><span class="italic"><span class="writegood-passive-voice">is found</span></span><span class="italic"> in the followers of</span>
<span class="italic">Hussain will not </span><span class="italic"><span class="writegood-passive-voice">be found</span></span><span class="italic"> in the followers of Christ. And it seems that the
suffering of Christ against the suffering of Hussain is like a blade of straw</span> <span class="italic">in
front of a </span><span class="italic"><span class="writegood-weasels">huge</span></span><span class="italic"> mountain.”</span>
<span class="org-block-end-line">#+end_documentation
</span><span class="org-level-1">* Logics</span>
<span class="org-drawer">:PROPERTIES:</span>...
<span class="org-link"><span class="custom-button"><a href="doc:graph">doc:graph</a></span></span>
<span class="org-block-begin-line">#+begin_documentation graph :show t :color blue
</span>A <span class="italic">(Partial, resp. Total) Graph</span><span class="org-latex-and-related"> $G = (V, E, src, tgt)$ </span>consists of
+<span class="org-latex-and-related"> $V$,</span> a set of “points, nodes, vertices”
+<span class="org-latex-and-related"> $E$,</span> a set of “arcs, edges”
+<span class="org-latex-and-related"> $src, tgt : E <img src="../.emacs.d/emojis/emojione-v2.2.6-22/2194.png" alt="↔" /> V$,</span> a pair of <span class="italic">partial (resp. total)</span> functions.
⟦ Tersely put, in any category, a <span class="italic">graph</span> is a parallel pair of morphisms. ⟧
<span class="italic">Edge parallelism</span> is the relation<span class="org-latex-and-related"> $Ξ = src ⨾ src ˘ ∩ tgt ⨾ tgt˘$;</span> two arcs <span class="writegood-passive-voice">are
related</span> 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.
+ A graph is <span class="italic">total</span> exactly when <span class="italic">Id ⊆ Ξ</span>; and so Ξ is an equivalence.
+ A graph has <span class="italic">no parallel arrows</span> exactly when <span class="italic">Ξ ⊆ Id</span>.
+ A graph is <span class="italic"><span class="writegood-weasels">simple</span></span> exactly when <span class="italic">Ξ = Id</span>.
The <span class="italic">associated relation</span> is the relation <span class="italic">_⟶_ = src ˘ ⨾ tgt</span> that relates two nodes
when the first is the source of <span class="writegood-weasels">some</span> 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 <span class="italic">⟵</span> for <span class="italic">⟶˘</span>;
one writes ⟶⋆ for the <span class="italic">reachability</span> relation.
+ Node <span class="italic">y</span> is <span class="italic">reachable via a non-empty path</span> from node <span class="italic">x</span> exactly when <span class="italic">x ⟶⁺ y</span>.
- Node <span class="italic">x</span> lies on a cycle exactly when <span class="italic">x ⟶⁺ x</span>.
- A graph is <span class="italic">DAG, acylic, circuit-free,</span> exactly when <span class="italic">⟶⁺ ⊆ ∼Id</span>; i.e., <span class="italic">⟶⁺ ∩ Id = ⊥</span>.
- An acyclic graph is a (<span class="italic">directed) forest</span> exactly when ⟶ is injective; i.e.,
every node has at most one predecessor; i.e.,<span class="org-latex-and-related"> $⟶ ⨾ ⟵ ⊆ Id$.</span>
+ A node <span class="italic">r</span> is a <span class="italic">root</span> exactly when every node is reachable from it; i.e., <span class="italic">{r} × V ⊆ ⟶⋆;</span>
i.e., <span class="italic">𝕃 r ⨾ ⟶⋆ = ⊤</span> where <span class="italic">𝕃 r</span> <span class="writegood-passive-voice">is defined</span> by<span class="org-latex-and-related"> $𝕃 r = (ℝ r)˘$ </span>and<span class="org-latex-and-related"> $x 〔ℝ r〕 y \;≡\; x = r$.</span>
-<span class="org-latex-and-related"> $x〔𝕃 r ⨾ R〕 y \;≡\; r〔R〕 y$ </span>and<span class="org-latex-and-related"> $x 〔R ⨾ ℝ r〕 y \;≡\; x 〔R〕 r$
</span> - A <span class="italic">tree</span> is a forest with a root.
+ A graph is <span class="italic">loop free</span> exactly when <span class="italic">⟶ ⊆ ∼Id</span>.
+ A graph is <span class="italic">strongly connected</span> exactly when <span class="italic">⟶⋆ = ⊤</span>; i.e., <span class="italic">∼Id ⊆ ⟶⁺</span>;
i.e., every point is reachable from any <span class="italic">other</span> point; i.e., <span class="italic">∼Id ⊆ ⟶ ∩ ⟵˘</span>;
i.e., any two distinct points lie on an undirected circuit.
- The equivalence classes of <span class="italic">⟶⋆ ∩ ⟵⋆</span> are the <span class="italic">strongly connected components</span>.
+ <span class="italic">Terminal∣sinks</span> are nodes from which it is <span class="italic">not</span> possible to proceed <span class="italic">any</span> further;
i.e., terminals have no successors; the domain of <span class="italic">∼(⟶ ⨾ ⊤)</span> is all terminals.
+ <span class="italic">Initial∣sources</span> are nodes from which it is <span class="italic">not</span> possible to proceed backward;
i.e., initials have no predecessors; the domain of <span class="italic">∼(⟵ ⨾ ⊤)</span> is all initials.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Expression">doc:Expression</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Expression :show t
</span>
An <span class="italic">expression</span> is either a ‘variable’ or a ‘function application’; i.e., the name
of a function along with a number of existing expressions.
#+begin_example
Expr ::= Constant -- E.g., 1 or “apple”
<span class="org-table">| Variable -- E.g., x or apple (no quotes!)</span>
<span class="org-table">| Application -- E.g., f(x₁, x₂, …, xₙ)</span>
#+end_example
( One reads ‘:=’ as <span class="italic">becomes</span> and so the addition of an extra colon results in a
‘stutter’: One reads ‘∷=’ as <span class="italic">be-becomes</span>. The symbol ‘|’ <span class="writegood-passive-voice">is read</span> <span class="italic">or</span>. )
Notice that a constant is really just an application with <span class="italic">n</span> being <span class="italic">0</span> arguments
and so the first line in the definition above could <span class="writegood-passive-voice">be omitted</span>.
--------------------------------------------------------------------------------
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.
A <span class="bold">variable of type τ</span> is a <span class="italic">name</span> denoting a yet unknown <span class="italic">value</span> of type τ;
i.e., “it is a pronoun (nickname) referring to a person in the collection of people τ”.
E.g., to say<span class="org-latex-and-related"> $x$ </span>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 <span class="org-verbatim">Expr τ</span> refer to the expressions denoting <span class="italic">values</span> of type τ;
then a <span class="bold">meta-variable</span> is <span class="writegood-weasels">simply</span> a normal variable of type <span class="org-verbatim">Expr τ</span>.
That is, when we write phrases like <span class="org-verbatim">“Let E be an expression”</span>, then the <span class="italic">name</span><span class="org-latex-and-related"> $E$
</span>varies and so is a variable, but it is an expression and so may consist of a
function application or a variable. <span class="bold">That is,</span><span class="bold"><span class="org-latex-and-related"> $E$ </span></span><span class="bold">is a variable that may stand
for variables.</span> This layered inception <span class="writegood-passive-voice">is resolved</span> by referring to<span class="org-latex-and-related"> $E$ </span>as not
just any normal variable, but instead as a <span class="bold">meta-variable</span>: A variable capable of
referring to other (simpler) variables.
--------------------------------------------------------------------------------
Expressions, as defined above, are also known as <span class="italic">abstract syntax trees</span> (AST) or
<span class="italic">prefix notation</span>. Then <span class="italic">textual substitution</span> <span class="writegood-passive-voice">is known</span> as ‘grafting trees’ (a
monadic bind).
Their use can be clunky, such as by requiring <span class="writegood-weasels">many</span> parentheses and implicitly
forcing a syntactic distinction between equivalent expressions; e.g.,
<span class="italic">gcd(m,gcd(n,p))</span> and <span class="italic">gcd(gcd(m,n),p)</span> look difference even though <span class="italic">gcd</span> is
associative.
As such, one can declare <span class="italic">precedence levels</span> ---a.k.a. <span class="italic">binding power</span>--- 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 <span class="writegood-passive-voice">be read</span> 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 <span class="italic">concrete syntax</span> ---i.e., in a syntactic shape that is
more concrete.
That is, the <span class="bold">conventions</span> on how a <span class="italic">string</span> should <span class="writegood-passive-voice">be parsed</span> as a <span class="italic">tree</span> <span class="writegood-passive-voice">are known</span> as a
<span class="bold">precedence, fixity, and associativity rules.</span>
Similarly, not for operators but one treats <span class="italic">relations</span> <span class="bold">conjunctionally</span> to reduce
the number of ‘and’(∧) symbols; e.g.<span class="org-latex-and-related"> $x ≤ y + 2 = z \quad≡\quad x ≤ (y + 2) \,∧\, (y + 2) = z$.</span>
This is <span class="writegood-weasels">very</span> useful to avoid repeating lengthy common expressions, such as <span class="italic">y + 2</span>.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Induction">doc:Induction</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Induction :show t :color blue
</span>How we prove a theorem<span class="org-latex-and-related"> $P\, n$ </span>ranging over natural numbers<span class="org-latex-and-related"> $n$?</span>
For instance, suppose the property<span class="org-latex-and-related"> $P$ </span>is that using only 3 and 5 dollar bills,
any amount of money that is at-least 8 dollars can <span class="writegood-passive-voice">be formed</span>.
Since there are an infinite number of natural numbers, it is not possibly to
verify<span class="org-latex-and-related"> $P\, n$ </span>is true by <span class="italic">evaluating</span><span class="org-latex-and-related"> $P\, n$ </span>at each natural number<span class="org-latex-and-related"> $n$.</span>
<span class="bold">Knocking over dominos is induction:</span>
The natural numbers are like an infinite number of dominoes ---i.e., standing
tiles one after the other, in any arrangement. Can all dominoes <span class="writegood-passive-voice">be knocked</span> over?
That is, if we construe<span class="org-latex-and-related"> $P\, n$ </span>to mean “the <span class="italic">n</span>-th domino can <span class="writegood-passive-voice">be knocked</span> over”,
then the question is “is<span class="org-latex-and-related"> $∀ n • P\, n$ </span>true”. Then, <span class="writegood-weasels">clearly</span> if we can knock over
the first domino,<span class="org-latex-and-related"> $P\, 0$,</span> and if when a domino <span class="writegood-passive-voice">is knocked</span> over then it also
knocks over the next domino,<span class="org-latex-and-related"> $P\, n ⇒ P\, (n + 1)$,</span> then ‘<span class="writegood-weasels">clearly</span>’ all dominoes
will <span class="writegood-passive-voice">be knocked</span> over. This ‘basic observation’ <span class="writegood-passive-voice">is known</span> as <span class="italic">induction</span>.
<span class="bold">Climbing a ladder is induction:</span>
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<span class="org-latex-and-related"> $P\, n$ </span>to mean
“the <span class="italic">n</span>-th rung is reachable”, then the question is “is<span class="org-latex-and-related"> $∀ n • P\, n$
</span>true”. Then, <span class="writegood-weasels">clearly</span> if we can reach the first rung,<span class="org-latex-and-related"> $P\, 0$,</span> and whenever we
climb to a rung then we can reach up and grab the next rung,<span class="org-latex-and-related"> $P\, n ⇒ P\, (n +
1)$,</span> then ‘<span class="writegood-weasels">clearly</span>’ all rungs of the ladder can <span class="writegood-passive-voice">be reached</span>. This ‘basic
observation’ <span class="writegood-passive-voice">is known</span> as <span class="italic">induction</span>.
<span class="bold">Constant functions are induction:</span>
A predicate<span class="org-latex-and-related"> $P : ℕ → 𝔹$ </span>is a function. When is such a function constantly the
value<span class="org-latex-and-related"> $\true$?</span> That is, when is<span class="org-latex-and-related"> $∀ n • P\, n = \true$?</span> <span class="writegood-weasels">Clearly</span>, if<span class="org-latex-and-related"> $P$ </span>starts
off being<span class="org-latex-and-related"> $\true$ </span>---i.e., <span class="italic">P 0</span>--- and it preserves truth at every step ---i.e.,
<span class="italic">P n ⇒ P (n + 1)</span>--- then <span class="italic">P n</span> will be true for any choice of<span class="org-latex-and-related"> $n$.</span>
That is, if we consider<span class="org-latex-and-related"> $(ℕ, ≤)$ </span>and<span class="org-latex-and-related"> $(𝔹, ⇒)$ </span>as ordered sets and<span class="org-latex-and-related"> $P$ </span>starts at
the ‘top’ of 𝔹 ---i.e., <span class="italic">P 0 = true</span>--- and it is ascending ---i.e., <span class="italic">P n ⇒ P (n +
1)</span>--- and so ‘never goes down’, then <span class="writegood-weasels">clearly</span> it must stay constantly at the top
value of 𝔹. This ‘basic observation’ <span class="writegood-passive-voice">is known</span> as <span class="italic">induction</span>.
⟦ For the money problem, we need to start somewhere else besides 0. ⟧
<span class="bold">Principle of (“Weak”) Mathematical Induction:</span>
To show that a property<span class="org-latex-and-related"> $P$ </span>is true for all natural numbers starting with <span class="writegood-weasels">some</span>
number<span class="org-latex-and-related"> $n_0$,</span> show the following two properties:
+ <span class="org-list-dt">Base case ::</span> Show that<span class="org-latex-and-related"> $P\, n₀$ </span>is true.
+ <span class="org-list-dt">Inductive Step ::</span> Show that whenever (the <span class="bold">inductive hypothesis</span>)<span class="org-latex-and-related"> $n$ </span>is a
natural number that such that<span class="org-latex-and-related"> $n ≥ n₀$ </span>and<span class="org-latex-and-related"> $P\, n$ </span>is true, then<span class="org-latex-and-related"> $P\, (n + 1)$
</span> is also true.
⟦ For the money problem, we need to be able to use the fact that to prove<span class="org-latex-and-related">
$P\,(n + 1)$ </span>we must have already proven<span class="org-latex-and-related"> $P$ </span>for all smaller values. ⟧
<span class="bold">Principle of (“Strong”) Mathematical Induction</span>:
To show that a property<span class="org-latex-and-related"> $P$ </span>is true for all natural numbers starting with <span class="writegood-weasels">some</span>
number<span class="org-latex-and-related"> $n_0$,</span> show the following two properties:
+ <span class="org-list-dt">Base case ::</span> Show that<span class="org-latex-and-related"> $P\, n₀$ </span>is true.
+ <span class="org-list-dt">Inductive Step ::</span> Show that whenever (the <span class="bold">inductive hypothesis</span>)<span class="org-latex-and-related"> $n$ </span>is a
natural number that such that<span class="org-latex-and-related"> $n ≥ n₀$ </span>and<span class="org-latex-and-related"> $P\, n_0, P\, (n_0 + 1), P\, (n_0 +
2), …, P\, n$ </span>are true, then<span class="org-latex-and-related"> $P\, (n + 1)$ </span>is also true.
⟦ The ‘strength’ of these principles refers to the strength of the inductive
hypothesis. The principles are provably equivalent. ⟧
# (It is also a way to say that ℕ has non-empty meets.)
<span class="bold">The Least Number Principle (LNP) ---Another way to see induction:</span>
Every non-empty subset of the natural numbers must have a least element,
‘obviously’. This is (strong) induction.
# Possibly infinite!
Application of LNP to showing that algorithms terminate:
In particular, every decreasing non-negative sequence of integers<span class="org-latex-and-related">
$r₀ > r₁ > r₂ > ⋯$ </span>must terminate.
#+end_box
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Textual_Substitution">doc:Textual_Substitution</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Textual_Substitution :show t
</span>The <span class="bold">(simultaneous textual) Substitution operation</span><span class="org-latex-and-related"> $E[\vec x ≔ \vec F]$ </span>replaces
all variables<span class="org-latex-and-related"> $\vec x$ </span>with parenthesised expressions<span class="org-latex-and-related"> $\vec F$ </span>in an expression<span class="org-latex-and-related">
$E$.</span> In particular,<span class="org-latex-and-related"> $E[x ≔ F]$ </span>is just<span class="org-latex-and-related"> $E$ </span>but with all occurrences of<span class="org-latex-and-related"> $x$
</span>replaced by<span class="org-latex-and-related"> $“(F)”$.</span> This is the “find-and-replace” utility you use on your
computers.
Textual substitution on expressions <span class="writegood-passive-voice">is known</span> as “grafting” on trees: Evaluate<span class="org-latex-and-related">
$E[x ≔ F]$ </span>by going down the tree<span class="org-latex-and-related"> $E$ </span>and finding all the ‘leaves’ labelled<span class="org-latex-and-related"> $x$,</span>
cut them out and replace them with the new trees<span class="org-latex-and-related"> $F$.</span>
Since expressions are either variables of functions applications,
substitution can <span class="writegood-passive-voice">be defined</span> inductively/recursively by the following two clauses:
+ <span class="italic">y[x ≔ F] = if  x = y  then  F  else  y  fi</span>
+ <span class="italic">f(t₁, …, tₙ)[x ≔ F] = f(t₁′, …, tₙ′)  where  tᵢ′ = tᵢ[x ≔ F]</span>
--------------------------------------------------------------------------------
Sequential ≠ Simultaneous:
<span class="italic">(x + 2 · y)[x ≔ y][y ≔ x] ≠ (x + 2 · y)[x, y ≔ y, x]</span>
<span class="org-link"><a href="https://alhassy.github.io/PythonCheatSheet/CheatSheet.pdf">Python</a></span>, for example, has simultaneous <span class="italic">assignment</span>;
e.g., <span class="org-code">x, y = y, x</span> <span class="writegood-passive-voice">is used</span> to swap the value of two variables.
--------------------------------------------------------------------------------
A <span class="italic">function</span><span class="org-latex-and-related"> $f$ </span>is a rule for computing a value from another value.
If we define<span class="org-latex-and-related"> $f\, x = E$ </span>using an expression, then <span class="italic">function application</span> can <span class="writegood-passive-voice">be
defined</span> using textual substitution:<span class="org-latex-and-related"> $f \, X = E[x ≔ X]$.</span> That is, expressions
can <span class="writegood-passive-voice">be considered</span> functions of their variables ---but it is still expressions
that are the primitive idea, the building blocks.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Inference_Rule">doc:Inference_Rule</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Inference_Rule :show t
</span>
Formally, a “proof” <span class="writegood-passive-voice">is obtained</span> 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 <span class="writegood-passive-voice">be applied</span> to any existing results: It's just a
known result.
That is, a <span class="bold">rule</span><span class="org-latex-and-related"> $R$ </span>is a tuple<span class="org-latex-and-related"> $P₁, …, Pₙ, C$ </span>that <span class="writegood-passive-voice">is thought</span> of as ‘taking
<span class="bold">premises</span> (instances of known results)<span class="org-latex-and-related"> $Pᵢ$’</span> and acting as a ‘natural,
reasonable justification’ to obtain <span class="bold">conclusion</span><span class="org-latex-and-related"> $C$.</span> A <span class="bold">proof system</span> is a
collection of rules. At first sight, this all sounds <span class="writegood-weasels">very</span> abstract and rather
useless, however it is a <span class="italic">game</span>: <span class="bold">Starting from rules, what can you obtain?</span> <span class="writegood-weasels">Some</span>
games can be <span class="writegood-weasels">very</span> fun! Another way to see these ideas is from the view of
programming:
+ Proving ≈ Programming
+ Logic ≈ Trees (algebraic data types, 𝒲-types)
+ Rules ≈ Constructors
+ Proof ≈ An application of constructors
+ Axiom ≈ A constructor with no arguments
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.
#+begin_example
12
P₁, P₂, …, Pn + 7
---------------R versues ----
C 19
#+end_example
Just as there are meta-variables and meta-theorems, there is ‘meta-syntax’:
- The use of a fraction to delimit premises from conclusion is a form of ‘implication’.
- The use of a comma, or white space, to separate premises is a form of ‘conjunction’.
If our expressions actually have an implication and conjunction operation, then
inference rule above can <span class="writegood-passive-voice">be presented</span> as an axiom<span class="org-latex-and-related"> $P₁ \,∧\, ⋯ \,∧\, Pₙ \,⇒\, C$.</span>
The inference rule says “if the<span class="org-latex-and-related"> $Pᵢ$ </span>are all valid, i.e., true in <span class="italic">all states</span>,
then so is<span class="org-latex-and-related"> $C$”</span>; the axiom, on the other hand, says “if the<span class="org-latex-and-related"> $Pᵢ$ </span>are true in <span class="italic">a
state</span>, then<span class="org-latex-and-related"> $C$ </span>is true in <span class="italic">that state</span>.” Thus the rule and the axiom are not
<span class="writegood-weasels">quite</span> the same.
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 <span class="italic">can get</span> the thing below the bar, but
that thing (19) is not ‘true’ as we may think of conventional truth.
Finally, the rule asserts that<span class="org-latex-and-related"> $C$ </span>follows from<span class="org-latex-and-related"> $P₁, …, Pₙ$.</span> The formula<span class="org-latex-and-related"> $P₁
\,∧\, ⋯ \,∧\, Pₙ \,⇒\, C$,</span> on the other hand, is an expression (but it need not
be a theorem).
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.
Syntax is like static analysis; semantics is like actually running the program
(on <span class="writegood-weasels">some</span>, or all possible inputs).
--------------------------------------------------------------------------------
One reads/writes a <span class="italic">natural deduction proof (tree)</span> from the <span class="writegood-weasels">very</span> <span class="bold">bottom</span>: Each
line is an application of a rule of reasoning, whose assumptions are above the
line; so read/written upward. The <span class="bold">benefit</span> of this approach is that <span class="bold">rules guide
proof construction</span>; i.e., it is goal-directed.
However the <span class="bold">downsides are numerous</span>:
- So much horizontal space <span class="writegood-passive-voice">is needed</span> even for <span class="writegood-weasels">simple</span> proofs.
- One has to <span class="bold">repeat</span> common subexpressions; e.g., when using transitivity of equality.
- For comparison with other proof notations, such as Hilbert style,
see <span class="org-link"><a href="http://www.cse.yorku.ca/~logicE/misc/logicE_intro.pdf">Equational Propositional Logic</a></span>.
This is more ‘linear’ proof format; also known as <span class="italic">equational style</span> or
<span class="italic">calculational proof</span>. 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 <span class="writegood-passive-voice">was reached</span> from the previous line.
--------------------------------------------------------------------------------
Finally, an inference rule says that it is possible to start with the givens<span class="org-latex-and-related">
$Pᵢ$ </span>and obtain as result<span class="org-latex-and-related"> $C$.</span> The idea to use <span class="bold">inference rules as computation</span>
<span class="writegood-passive-voice">is witnessed</span> by the <span class="org-link"><a href="https://alhassy.github.io/PrologCheatSheet/CheatSheet.pdf">Prolog</a></span> programming language.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Logic">doc:Logic</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Logic :show t
</span>A <span class="italic">logic</span> is a formal system of reasoning...
A <span class="italic">logic</span> is a set of symbols along with a set of <span class="italic">formulas</span> formed from the
symbols, and a set of <span class="italic">inference rules</span> which allow formulas to <span class="writegood-passive-voice">be derived</span> from
other formulas. (The formulas may or may not include a notion of variable.)
Logics are purely syntactic objects; an <span class="italic">inference rule</span> is a syntactic mechanism
for deriving “truths” or “theorems”.
In general, proofs are evidence of truth of a claim; by demonstrating that the
claim follows from <span class="writegood-weasels">some</span> <span class="italic">obvious truth</span> using rules of reasoning that <span class="italic">obviously
preserve truth.</span>
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Theorem">doc:Theorem</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Theorem :show t :color blue
</span>A <span class="italic">theorem</span> is a syntactic object, a string of symbols with a particular property.
A <span class="italic">theorem</span> of a calculus is either an axiom or the conclusion of an inference
rule whose premises are theorems.
Different axioms could lead to the same set of theorems, and <span class="writegood-weasels">many</span> texts use
different axioms.
--------------------------------------------------------------------------------
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.
Syntax is like static analysis; semantics is like actually running the program
(on <span class="writegood-weasels">some</span>, or all possible inputs).
--------------------------------------------------------------------------------
A <span class="bold">meta-theorem</span> 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
<span class="italic">theorem</span> 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 <span class="writegood-weasels">many</span> other theories, such as lattices): An
<span class="italic">equational</span> theorem is true precisely when its ‘dual’ is true. Such metatheorems
can be helpful to discover new theorems.
# A meta-theorem is a theorem about theorems.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Metatheorem">doc:Metatheorem</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Metatheorem :show t
</span>A <span class="italic">theorem</span> in the technical sense is an expression derived
from axioms using inference rules.
A <span class="italic">metatheorem</span> is a general <span class="bold">statement</span> about a logic that
one argues to be <span class="bold">true</span>.
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 <span class="bold">within</span> the logic ---and so cannot be a theorem of
the logic.
For instance, the logic 𝒑𝑞 has expressions formed from the symbols “𝒑”, “𝒒”, and
“-” (dash). It has the axiom schema<span class="org-latex-and-related"> $x𝒑-𝒒x-$ </span>and the rule “If<span class="org-latex-and-related"> $x𝒑y𝒒z$ </span>is a theorem
then so is<span class="org-latex-and-related"> $x-𝒑y-𝒒z-$”</span>. Notice that<span class="org-latex-and-related"> $x, y, z$ </span>are <span class="italic">any</span> 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!
[Informal] theorems about [technical, logic-specific] theorems are thus termed
‘metatheorems’.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Calculus">doc:Calculus</a></span></span> (<span class="org-link"><span class="custom-button"><a href="doc:Propositional_Calculus">Propositional</a></span></span><span class="org-link"><a href="doc:Propositional_Calculus"> Calculus</a></span>)
<span class="org-block-begin-line">#+begin_documentation Calculus :label Propositional_Calculus :show t :color blue
</span>A <span class="italic">calculus</span> is a method or process of reasoning by calculation
with symbols. A <span class="italic">propositional calculus</span> is a method of calculating with Boolean
(or propositional) expressions.
--------------------------------------------------------------------------------
Calculus: Formalised reasoning through calculation.
‘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.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Semantics">doc:Semantics</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Semantics :label (Axiomatic_Semantics Operational_Semantics) :show t
</span>
<span class="bold">Syntax</span> refers to the structure of expressions, or the rules for putting symbols
together to form an expression. <span class="bold">Semantics</span> refers to the meaning of expressions
or how they <span class="writegood-passive-voice">are evaluated</span>.
An expression can contain variables, and evaluating such an expression requires
knowing what values to use for these variables; i.e., a <span class="bold">state</span>: A list of
variables with associated values. E.g., evaluation of<span class="org-latex-and-related"> $x - y + 2$ </span>in the state
consisting of<span class="org-latex-and-related"> $(x, 5)$ </span>and<span class="org-latex-and-related"> $(y, 6)$ </span><span class="writegood-passive-voice">is performed</span> by replacing<span class="org-latex-and-related"> $x$ </span>and<span class="org-latex-and-related"> $y$ </span>by
their values to yield<span class="org-latex-and-related"> $5 - 6 + 2$ </span>and then evaluating that to yield<span class="org-latex-and-related"> $1$.</span>
A Boolean expression<span class="org-latex-and-related"> $P$ </span>is <span class="bold">satisfied</span> in a state if its value is <span class="italic">true</span> in that
state;<span class="org-latex-and-related"> $P$ </span>is <span class="bold">satisfiable</span> if there is a state in which it <span class="writegood-passive-voice">is satisfied</span>; and<span class="org-latex-and-related"> $P$
</span>is <span class="bold">valid</span> (or is a <span class="bold">tautology</span>) if it <span class="writegood-passive-voice">is satisfied</span> in every state.
--------------------------------------------------------------------------------
<span class="writegood-weasels">Often</span> operations <span class="writegood-passive-voice">are defined</span> by how they <span class="writegood-passive-voice">are evaluated</span> (<span class="bold">operationally</span>), we
take the alternative route of defining operations by how they can <span class="writegood-passive-voice">be manipulated</span>
(<span class="bold">axiomatically</span>); i.e., by what properties they satisfy.
For example, evaluation of the expression<span class="org-latex-and-related"> $X = Y$ </span>in a state yields the value
<span class="italic">true</span> if expressions<span class="org-latex-and-related"> $X$ </span>and<span class="org-latex-and-related"> $Y$ </span>have the same value and yields <span class="italic">false</span> if they
have different values. This characterisation of equality is in terms of
expression <span class="italic">evaluation</span>. For <span class="italic">reasoning about expressions</span>, a more useful
characterisation would be a set of <span class="italic">laws</span> that can <span class="writegood-passive-voice">be used</span> to show that two
expressions are equal, <span class="bold">without</span> calculating their values.
--- c.f., static analysis versues running a program.
For example, you know that<span class="org-latex-and-related"> $x = y$ </span>equals<span class="org-latex-and-related"> $y = x$,</span> regardless of the values of<span class="org-latex-and-related">
$x$ </span>and<span class="org-latex-and-related"> $y$.</span> A collection of such laws can <span class="writegood-passive-voice">be regarded</span> as a definition of
equality, <span class="bold">provided</span> two expressions have the same value in all states precisely
when one expression can <span class="writegood-passive-voice">be translated</span> into the other according to the laws.
Usually, in <span class="italic">a</span> logic, theorems correspond to expressions that are true in all
states.
--------------------------------------------------------------------------------
That is, instead of defining expressions by how they <span class="writegood-passive-voice">are evaluated</span>, we may
define expressions in terms of how they can <span class="writegood-passive-voice">be manipulated</span> ---c.f., a calculus.
For instance, we may define basic manipulative properties of operators ---i.e.,
<span class="italic">axioms</span>--- by considering how the operators behave operationally on particular
expressions. That is, one may use an operational, intuitive, approach to obtain
an axiomatic specification (characterisation, interface) of the desired
properties.
More concretely, since<span class="org-latex-and-related"> $(p ≡ q) ≡ r$ </span>and<span class="org-latex-and-related"> $p ≡ (q ≡ r)$ </span>evaluate to
the same value for any choice of values for<span class="org-latex-and-related"> $p, q, r$,</span> we may insist that a part
of the definition of equivalence is that it be an associative operation.
Sometimes a single axiom is not enough to ‘pin down’ a unique operator ---i.e.,
to ensure we actually have a well-defined operation--- and other times this is
cleanly possible; e.g., given an ordering ‘≤’(‘⇒, ⊆, ⊑’) we can define minima
‘↓’ (‘∧, ∩, ⊓’) by the axiom: “x ↓ y is the greatest lower bound”;
i.e.,<span class="org-latex-and-related"> $z ≤ x ↓ y \quad≡\quad z ≤ x \,∧\, z ≤ y$.</span>
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Calculational_Proof">doc:Calculational_Proof</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Calculational Proof :show t
</span>A story whose events have smooth transitions connecting them.
# A proof wherein each step <span class="writegood-passive-voice">is connected</span> to the next step by an explicit
# justification.
This is a ‘linear’ proof format; also known as <span class="italic">equational style</span> or <span class="italic">calculational
proof</span>. 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 <span class="writegood-passive-voice">was
reached</span> from the previous line. ( This is similar to <span class="bold">programming</span> which
encourages placing <span class="italic">comments</span> to <span class="italic">communicate</span> what's going on to future readers. )
The structure of equational proofs allows implicit use of infernece rules
Leibniz, Transitvitity & Symmetry & Reflexivity of equality, and
Substitution. In contrast, the structure of proof trees is no help in this
regard, and so all uses of inference rules must <span class="writegood-passive-voice">be mentioned</span> explicitly.
For comparison with other proof notations see <span class="org-link"><a href="http://www.cse.yorku.ca/~logicE/misc/logicE_intro.pdf">Equational Propositional Logic</a></span>.
--------------------------------------------------------------------------------
We advocate <span class="italic">calculational proofs</span> in which reasoning is goal directed and
justified by <span class="writegood-weasels">simple</span> axiomatic laws that can <span class="writegood-passive-voice">be checked</span> syntactically rather than
semantically. ---<span class="italic">Program Construction</span> by Roland Backhouse
--------------------------------------------------------------------------------
Calculational proofs introduce notation and recall theorems as needed, thereby
making each step of the argument <span class="writegood-weasels">easy</span> to verify and follow. Thus, such arguments
are more accessible to readers unfamiliar with the problem domain.
--------------------------------------------------------------------------------
The use of a formal approach let us keep track of when our statements are
equivalent (“=”) rather than <span class="writegood-passive-voice">being weakened</span> (“⇒”). That is, the use of English
to express the connection between steps is usually presented naturally using “if
this, then that” statements ---i.e., implication--- rather than stronger notion
of equality.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-hide">*</span><span class="org-level-2">* Misc </span><span class="org-level-2"><span class="org-tag">:ignore:</span></span>
<span class="org-drawer">:PROPERTIES:</span>...
<span class="org-link"><span class="custom-button"><a href="doc:Programming">doc:Programming</a></span></span>
<span class="org-block-begin-line"> #+begin_documentation Programming :show t
</span> Programming is solving the equation <span class="italic">R ⇒[C] G</span> in the unknown <span class="italic">C</span>; i.e., it is the
activity of finding a ‘recipe’ that satisfies a given specification. Sometimes
we may write <span class="italic">R ⇒[?] G</span> and solve for ‘?’. Programming is a goal-directed activity: From a specification, a program <span class="writegood-passive-voice">is found</span> by examining the shape of its postcondition.
<span class="org-block-end-line"> #+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Specification">doc:Specification</a></span></span>
<span class="org-block-begin-line"> #+begin_documentation Specification :show t :color blue
</span> A specification is an equation of a certain shape.
<span class="italic">Programming</span> is the activity of solving a specification
for its unknown. Its unknown <span class="writegood-passive-voice">is called</span> a <span class="italic">program</span>.
See also “Programming”.
<span class="org-block-end-line"> #+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Proving_is_Programming">doc:Proving_is_Programming</a></span></span>
<span class="org-block-begin-line"> #+begin_documentation Proving_is_Programming :show t :color blue
</span> Problems may <span class="writegood-passive-voice">be formulated</span> and solved using, possibly implicitly, the
construction of correct programs:
<span class="italic">“for all x satisfying R(x), there is a y such that G(x,y) is true”</span>
≈ <span class="italic">∀ x • R x ⇒ ∃ y • G x y</span>
≈ <span class="italic">R {𝑺} G for </span><span class="italic"><span class="writegood-weasels">some</span></span><span class="italic"> program 𝑺 with inputs x and outputs y</span>
This <span class="writegood-passive-voice">is known</span> as a <span class="italic">constructive proof</span> since we have an algorithm 𝑺 that actually
shows how to find a particular <span class="italic">y</span> to solve the problem, for any given x. In
contrast, non-constructive proofs usually involving <span class="writegood-weasels">some</span> form of counting
followed by a phrase “there is at least one such <span class="italic">y</span> …”, without actually
indicating <span class="italic">how</span> to find it!
The <span class="italic">“R {𝑺} G”</span> <span class="writegood-passive-voice">is known</span> as a ‘Hoare triple’ and it expresses “when begun in a
state satisfying <span class="italic">R</span>, program 𝑺 will terminate in a state satisfying <span class="italic">G</span>.”
--------------------------------------------------------------------------------
+ Proving ≈ Programming
+ Logic ≈ Trees (algebraic data types, 𝒲-types)
+ Rules ≈ Constructors
+ Proof ≈ An application of constructors
+ Axiom ≈ A constructor with no arguments
<span class="org-block-end-line"> #+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Algorithmic_Problem_Solving">doc:Algorithmic_Problem_Solving</a></span></span>
<span class="org-block-begin-line"> #+begin_documentation Algorithmic Problem Solving :show t :color blue
</span> There are two ways to read this phrase.
Algorithmic-problem solving is about solving problems that
involve the construction of an algorithm for their solution.
Algorithmic problem-solving is about problem solving in general,
using the principles of correct-by-construction algorithm-design.
<span class="org-block-end-line"> #+end_documentation
</span><span class="comment"> # Computing science is all about solving algorithmic problems (or, as </span><span class="comment"><span class="writegood-weasels">some</span></span>
<span class="comment"> # authors pre- fer to say, it is all about instructing computers to solve</span>
<span class="comment"> # problems).</span>
<span class="org-link"><span class="custom-button"><a href="doc:nat-trans">doc:nat-trans</a></span></span>
<span class="org-block-begin-line"> #+begin_documentation Natural Transformation :label (nat-trans polymorphism) :show t :color blue
</span> Natural transformations are essentially polymorphic functions that make <span class="italic">no</span>
choices according to the input type; e.g., <span class="org-verbatim">reverse : List τ → List τ</span> makes no
choices depending on the type <span class="org-code">τ</span>.
<span class="org-block-end-line"> #+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:cat">doc:cat</a></span></span>
<span class="org-block-begin-line"> #+begin_documentation Category Theory :label cat :show t
</span> A theory of typed composition; e.g., typed monoids.
<span class="org-block-end-line"> #+end_documentation
</span>
<span class="org-level-1">* Properties of Operators</span>
<span class="org-drawer">:PROPERTIES:</span>...
<span class="org-link"><span class="custom-button"><a href="doc:Associative">doc:Associative</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Associative :show t :color blue
</span>An operation <span class="underline">⊕</span> is associative when it satisfies<span class="org-latex-and-related"> $(p ⊕ q) ⊕ r = p ⊕ (q ⊕ r)$.</span>
Associativity allows us to be informal and insert or delete pairs of
parentheses in sequences of ⊕'s, just as we do with sequences of
additions ---e.g.,<span class="org-latex-and-related"> $a + b + c + d$ </span>is equivalent to<span class="org-latex-and-related"> $a + (b + c) + d$.</span>
Hence, we can write<span class="org-latex-and-related"> $p ⊕ q ⊕ r$ </span>instead of<span class="org-latex-and-related"> $(p ⊕ q) ⊕ r$ </span>or<span class="org-latex-and-related"> $p ⊕ (q ⊕ r)$.</span>
When an operation is associative, it is best to avoid “making a choice” of how
sequences of ⊕ should <span class="writegood-passive-voice">be read</span>, by using parentheses ---unless to make things
clear or explicit for manipulation.
--------------------------------------------------------------------------------
More generally, for any two operations <span class="underline">⊕</span> and <span class="underline">⊞</span>, the “(left to right) mutual
associativity of ⊕ and ⊞” is the property<span class="org-latex-and-related"> $(x ⊕ y) ⊞ z = x ⊕ (y ⊞ z)$.</span> It allows
us to omit parentheses in mixed sequences of ⊕ and ⊞. For instance, addition and
subtraction are (left to right) mutually associative.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Identity">doc:Identity</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Identity :show t
</span>An operation <span class="underline">⊕</span> has identity 𝑰 when it satisfies<span class="org-latex-and-related"> $𝑰 ⊕ x = x = x ⊕ 𝑰$.</span>
If it satisfies only the first equation,<span class="org-latex-and-related"> $𝑰 ⊕ x = x$,</span> one says
that “𝑰 is a left-identity for ⊕”. If it satisfies only the second
equation,<span class="org-latex-and-related"> $x ⊕ 𝑰 = x$,</span> one says that “𝑰 is a right-identity for ⊕”.
For example, implication only has a left identity,<span class="org-latex-and-related"> $(false ⇒ x) = x$,</span> and
subtraction only has a right identity,<span class="org-latex-and-related"> $(x - 0) = x$.</span>
An identity implies that occurrences of “⊕ 𝑰” and “𝑰 ⊕” in an expression are
redundant. Thus,<span class="org-latex-and-related"> $x ⊕ 𝑰$ </span>may <span class="writegood-passive-voice">be replaced</span> by<span class="org-latex-and-related"> $x$ </span>in any expression without
changing the value of the expression. Therefore, we usually eliminate such
occurrences unless something encourages us to leave them in.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Distributive">doc:Distributive</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Distributive :show t :color blue
</span>An operation ⊗ distributes over ⊕ when they satisfy
“left-distributivity”<span class="org-latex-and-related"> $x ⊗ (y ⊕ z) = (x ⊗ y) ⊕ (x ⊗ y)$
</span>and
“right-distributivity”<span class="org-latex-and-related"> $(y ⊕ z) ⊗ x = (y ⊗ x) ⊕ (z ⊗ x)$.</span>
When ⊕ = ⊗, one says that the operation is “self-distributive”.
Distributivity can <span class="writegood-passive-voice">be viewed</span> in two ways, much like distributivity of
multiplication × over addition +. Replacing the left side by the right side
could <span class="writegood-passive-voice">be called</span> “multiplying out”; replacing the right side by the left side,
“factoring”.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Commutative">doc:Commutative</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Commutative :show t :color green
</span>An operation <span class="underline">⊕</span> is <span class="italic">commutative</span> or <span class="italic">symmetric</span> if it satisfies <span class="italic">x ⊕ y = y ⊕ x</span>.
This property indicates (semantically) that the value of an ⊕-expression doesn't
depend on the order of its arguments and (syntactically) we may swap their order
when manipulating ⊕-expressions.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-level-1">* Properties of </span><span class="org-level-1"><span class="italic">Homogeneous</span></span><span class="org-level-1"> Relations</span>
<span class="org-drawer">:PROPERTIES:</span>...
<span class="org-link"><span class="custom-button"><a href="doc:Reflexive">doc:Reflexive</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Reflexive :show t :color blue
</span><span class="italic">Elements </span><span class="italic"><span class="writegood-passive-voice">are related</span></span><span class="italic"> to themselves</span>
--------------------------------------------------------------------------------
A relation<span class="org-latex-and-related"> $R : V → V$ </span>can <span class="writegood-passive-voice">be visualised</span> as a drawing: A dot for each element<span class="org-latex-and-related">
$x$ </span>of<span class="org-latex-and-related"> $V$,</span> and a directed line<span class="org-latex-and-related"> $x ⟶ y$ </span>between two points exactly when<span class="org-latex-and-related"> $x 〔R〕
y$.</span> That is relations are <span class="italic"><span class="writegood-weasels">simple</span></span><span class="italic"> graphs</span>; one refers to the directed lines as
<span class="italic">edges</span> and the dots as <span class="italic">nodes</span>.
As a <span class="writegood-weasels">simple</span> graph, reflexivity means <span class="italic">there is loop “ ⟳ ” at each node.</span>
--------------------------------------------------------------------------------
<span class="italic">R</span> is reflexive exactly when <span class="italic">everything </span><span class="italic"><span class="writegood-passive-voice">is related</span></span><span class="italic"> to itself</span>.
≡ <span class="italic">∀ x • x 〔R〕 x</span>
≡ <span class="org-latex-and-related"> $Id ⊆ R$
</span>
Where <span class="italic">⨾, ⊤, ⊥, Id, ˘, ∼</span> are relation composition, the universal relation, the
empty relation, the identity relation, relation converse (transpose), and complement.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Transitive">doc:Transitive</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Transitive :show t :color green
</span>A relation <span class="underline">⊑</span> is <span class="italic">transitive</span> when it satisfies <span class="italic">a ⊑ b  ∧  b ⊑ c  ⇒  a ⊑ c</span>;
i.e., <span class="italic">a ⊑ b ⊑ c  ⇒ a ⊑ c</span> ---that is, “we can chain ⊑” so that from a proof of <span class="italic">a
⊑ b ⊑ c</span> we can get from the first to the final part and so have a proof of
<span class="italic">a ⊑ c</span>.
Loosely put, whenever <span class="italic">a</span> and <span class="italic">c</span> have a common relative then they are themselves
related.
--------------------------------------------------------------------------------
A relation<span class="org-latex-and-related"> $R : V → V$ </span>can <span class="writegood-passive-voice">be visualised</span> as a drawing: A dot for each element<span class="org-latex-and-related">
$x$ </span>of<span class="org-latex-and-related"> $V$,</span> and a directed line<span class="org-latex-and-related"> $x ⟶ y$ </span>between two points exactly when<span class="org-latex-and-related"> $x 〔R〕
y$.</span> That is relations are <span class="italic"><span class="writegood-weasels">simple</span></span><span class="italic"> graphs</span>; one refers to the directed lines as
<span class="italic">edges</span> and the dots as <span class="italic">nodes</span>.
As a <span class="writegood-weasels">simple</span> graph, transitivity means <span class="italic">paths can always </span><span class="italic"><span class="writegood-passive-voice">be shortened</span></span><span class="italic"> (but
nonempty).</span>
--------------------------------------------------------------------------------
By the shunting rule, transitivity can <span class="writegood-passive-voice">be read</span> as a <span class="bold">‘monotonicity’</span> property for
the operation that turns a value <span class="italic">x</span> into the proposition <span class="italic">a ⊑ x</span>; this maps ordered
relationships <span class="italic">b ⊑ c</span> to ordered propositions <span class="italic">a ⊑ b ⇒ a ⊑ c</span>.
Likewise, transitivity can <span class="writegood-passive-voice">be read</span> as an ‘*antitonicity*’ property for the
operation mapping a value <span class="italic">x</span> to the proposition <span class="italic">x ⊑ c</span>; this maps ordered
relationships <span class="italic">a ⊑ b</span> to ordered propositions <span class="italic">b ⊑ c ⇒ a ⊑ c</span>.
--------------------------------------------------------------------------------
Relation <span class="italic">R</span> is transitive
≡ <span class="italic">Things related to things that </span><span class="italic"><span class="writegood-passive-voice">are related</span></span><span class="italic">, are themselves related.</span>
≡ Whenever <span class="italic">x</span> <span class="writegood-passive-voice">is related</span> to <span class="italic">y</span> and <span class="italic">y</span> <span class="writegood-passive-voice">is related</span> to <span class="italic">z</span>, then also <span class="italic">x</span> will
<span class="writegood-passive-voice">be related</span> to <span class="italic">z</span>
≡ <span class="italic">∀ x, y, z • x 〔 R 〕 y 〔R 〕 z ⇒ x 〔R〕 z</span>
≡ <span class="org-latex-and-related"> $R ⨾ R ⊆ R$
</span>
Where <span class="italic">⨾, ⊤, ⊥, Id, ˘, ∼</span> are relation composition, the universal relation, the
empty relation, the identity relation, relation converse (transpose), and complement.
--------------------------------------------------------------------------------
A transitive relation is irreflexive precisely when it is asymmetric.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Symmetric">doc:Symmetric</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Symmetric :show t :color blue
</span><span class="italic">The relationship is mutual; if one thing </span><span class="italic"><span class="writegood-passive-voice">is related</span></span><span class="italic"> to the other, then the other
is also related to the first.</span>
<span class="org-latex-and-related"> $R$ </span>is symmetric
≡ If <span class="italic">x</span> <span class="writegood-passive-voice">is related</span> to <span class="italic">y</span>, then <span class="italic">y</span> is also related to <span class="italic">x</span>.
≡ <span class="italic">∀ x, y • x 〔R〕 y ⇒ y 〔 R〕 x</span>
≡ <span class="org-latex-and-related"> $R ˘ ⊆ R$
</span>≡ <span class="org-latex-and-related"> $R ∩ R˘ ⊆ R$
</span>≡ <span class="org-latex-and-related"> $R ˘ = R$
</span>
Where <span class="italic">⨾, ⊤, ⊥, Id, ˘, ∼</span> are relation composition, the universal relation, the
empty relation, the identity relation, relation converse (transpose), and complement.
--------------------------------------------------------------------------------
A relation<span class="org-latex-and-related"> $R : V → V$ </span>can <span class="writegood-passive-voice">be visualised</span> as a drawing: A dot for each element<span class="org-latex-and-related">
$x$ </span>of<span class="org-latex-and-related"> $V$,</span> and a directed line<span class="org-latex-and-related"> $x ⟶ y$ </span>between two points exactly when<span class="org-latex-and-related"> $x 〔R〕
y$.</span> That is relations are <span class="italic"><span class="writegood-weasels">simple</span></span><span class="italic"> graphs</span>; one refers to the directed lines as
<span class="italic">edges</span> and the dots as <span class="italic">nodes</span>.
As a <span class="writegood-weasels">simple</span> graph, symmetry means the graphs is <span class="italic">undirected</span>.
That is, as graphs, symmetric relations contains either exactly two arrows ---in
opposite directions--- between any two elements or none at all. As such, for
clarity, one prefers “squeezing any two arrows in opposite directions” into one
‘undirected’ line and so obtains <span class="bold">undirected graphs</span>.
- Undirected edges represent pairs of arrows pointing in opposite directions.
Coreflexives are symmetric:<span class="org-latex-and-related"> $R ⊆ Id ⇒ R ˘ = R$.</span>
--------------------------------------------------------------------------------
<span class="writegood-weasels">Interestingly</span>, every homogeneous relation <span class="italic">R</span> may be <span class="italic">partitioned</span> into an
asymmetric part<span class="org-latex-and-related"> $A = R ∩ ∼R˘$ </span>and a symmetric part<span class="org-latex-and-related"> $S = R ∩ R˘$
</span>---i.e.,<span class="org-latex-and-related"> $R = A ∪ S$ </span>and<span class="org-latex-and-related"> $A ∩ S = ⊥$ </span>where ⊥ is the empty relation.
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Antisymmetric">doc:Antisymmetric</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Antisymmetric :show t :color blue
</span><span class="italic">Different elements cannot be mutually related; i.e.,
Mutually related items are necessarily indistinguishable.</span>
Such relations allow us to prove equality between two elements;
we have only to show that the relationship holds in both directions.
* E.g, one <span class="writegood-weasels">often</span> shows two sets are equal by using the antisymmetry of ‘⊆’.
--------------------------------------------------------------------------------
A relation<span class="org-latex-and-related"> $R : V → V$ </span>can <span class="writegood-passive-voice">be visualised</span> as a drawing: A dot for each element<span class="org-latex-and-related">
$x$ </span>of<span class="org-latex-and-related"> $V$,</span> and a directed line<span class="org-latex-and-related"> $x ⟶ y$ </span>between two points exactly when<span class="org-latex-and-related"> $x 〔R〕
y$.</span> That is relations are <span class="italic"><span class="writegood-weasels">simple</span></span><span class="italic"> graphs</span>; one refers to the directed lines as
<span class="italic">edges</span> and the dots as <span class="italic">nodes</span>.
As a <span class="writegood-weasels">simple</span> graph, antisymmetry means <span class="italic">Mutually related nodes are necessarily self-loops</span>.
--------------------------------------------------------------------------------
<span class="org-latex-and-related"> $R$ </span>is antisymmetric
≡ <span class="italic">∀ x, y • x 〔R〕 y ∧ y 〔 R〕 x ⇒ x = y</span>
≡ <span class="italic">∀ x, y • x ≠ y ⇒ ¬ (x 〔R〕 y ∧ y 〔 R〕 x)</span>
≡ <span class="italic">∀ x, y • x ≠ y ⇒ x 〔R̸〕 y ∨ y 〔 R̸〕 x</span>
≡ <span class="org-latex-and-related"> $R ∩ R ˘ ⊆ Id$
</span>≡ <span class="org-latex-and-related"> $R ˘ ⊆ ∼ R ∪ Id$
</span>≡ <span class="italic">R ╳ R = Id</span> ---‘╳’ is symmetric quotient
Where <span class="italic">⨾, ⊤, ⊥, Id, ˘, ∼</span> are relation composition, the universal relation, the
empty relation, the identity relation, relation converse (transpose), and complement.
( As a <span class="writegood-weasels">simple</span> graph, an antisymmetric relation has <span class="italic">at most</span> one arrow between
any two different nodes. )
<span class="org-block-end-line">#+end_documentation
</span>
<span class="org-link"><span class="custom-button"><a href="doc:Asymmetric">doc:Asymmetric</a></span></span>
<span class="org-block-begin-line">#+begin_documentation Asymmetric :show t :color blue
</span><span class="italic">The relationship is mutually exclusive.</span>
--------------------------------------------------------------------------------
A relation<span class="org-latex-and-related"> $R : V → V$ </span>can <span class="writegood-passive-voice">be visualised</span> as a drawing: A dot for each element<span class="org-latex-and-related">
$x$ </span>of<span class="org-latex-and-related"> $V$,</span> and a directed line<span class="org-latex-and-related"> $x ⟶ y$ </span>between two points exactly when<span class="org-latex-and-related"> $x 〔R〕
y$.</span> That is relations are <span class="italic"><span class="writegood-weasels">simple</span></span><span class="italic"> graphs</span>; one refers to the directed lines as
<span class="italic">edges</span> and the dots as <span class="italic">nodes</span>.
As a <span class="writegood-weasels">simple</span> graph, asymmetric means: <span class="italic">There's at most 1 edge (regardless of
direction) relating any 2 nodes</span>.
--------------------------------------------------------------------------------
<span class="org-latex-and-related"> $R$ </span>is asymmetric
≡ <span class="italic">∀ x, y • x 〔R〕 y ⇒ ¬ y 〔R〕 x</span>
≡ <span class="org-latex-and-related"> $R ∩ R ˘ ⊆ ⊥$
</span>≡ <span class="org-latex-and-related"> $R ˘ ⊆ ∼ R$
</span>
Where <span class="italic">⨾, ⊤, ⊥, Id, ˘, ∼</span> are relation composition, the universal relation, the
empty relation, the identity relation, relation converse (transpose), and complement.
Asymmetrics are irreflexive ---just pick <span class="italic">x = y</span> in the above ∀-formulation ;-)
--------------------------------------------------------------------------------