git @ Cat's Eye Technologies Eqthy / 82d987c
Add document describing equational logic itself. Chris Pressey 2 years ago
2 changed file(s) with 134 addition(s) and 5 deletion(s). Raw diff Collapse all Expand all
+1
-5
doc/Eqthy.md less more
2323
2424 * the axioms that have been previously defined
2525 * the theorems that have been previously proved
26 * the rules of inference of equational logic, which are
27 * Reflexivity (A=A)
28 * Transitivity (if A=B and B=C then A=C)
29 * Substitution (if x(A)=y(A) then x(B)=y(B))
30 * Congruence (if A=B then x(A)=x(B))
26 * the rules of inference of [equational logic](Equational-Logic.md)
3127
3228 The sequence of equations following a theorem is a proof. Each equation in
3329 the proof is optionally annotated with a hint that follows it, indicating what
+133
-0
doc/Equational-Logic.md less more
0 Equational Logic
1 ================
2
3 For the purpose of describing the underpinnings of Eqthy, this
4 document gives some information about **equational logic**.
5
6 ## Definition
7
8 The rules of inference of equational logic are:
9
10 * Reflexivity (A=A)
11 * Symmetry (if A=B then B=A)
12 * Transitivity (if A=B and B=C then A=C)
13 * Substitution (if x(A)=y(A) then x(B)=y(B))
14 * Congruence (if A=B then x(A)=x(B))
15
16 TODO: state those more formally
17
18 ## Notes
19
20 It took me a relatively long time to wrap my head around equational logic,
21 so I will provide some notes on it here, and links to resources.
22
23 I would put it like this: _Equational logic is the deductive aspect of universal algebra._
24 It provides the "syntax" where the algebraic structure provides the "semantics".
25
26 By itself, it captures only the idea of _equating things_:
27
28 * Equation is a relation which is _reflexive_, _symmetric_, and _transitive_;
29 * In the manner of elementary algebra, "equals may always be replaced by equals".
30
31 But by itself, it cannot prove many theorems of interest. To do that, it needs to be
32 supplemented by extra axioms stipulating exactly which things _should_, for the sake of
33 argument, be considered equal. These axioms describe an _algebraic structure_.
34 When the extra axioms are put together with equational logic, this is said to be the
35 _equational theory_ of the structure.
36
37 For example, the axioms for a group are:
38
39 * _Associativity_: **(x * y) * z = x * (y * z)**
40 * _Existence of an Identity Element_: **x * e = e * x = e**
41 * _Existence of Inverse Elements_: **x * x^-1 = x^-1 * x = e**
42
43 In the statement of each of these axioms, the variables are implicitly universally quantified.
44 This is standard practice.
45
46 The following sections list some of the resources that I banged my head against repeatedly
47 while trying to grasp these concepts.
48
49 ### 📝 Wikipedia
50
51 As of this writing, [Equational logic (Wikipedia)](https://en.wikipedia.org/wiki/Equational_logic)
52 does not contain a very clear explanation. This is because it
53 focuses on a particular equational logic, **E**, from the
54 second edition of the book "A Logical Approach to Discrete Math"
55 by David Gries and Fred Schneider. While it is a very interesting book
56 ([the 1st edition is borrowable from archive.org)](https://archive.org/details/logicalapproacht0000grie)),
57 its presentation of equational logic is somewhat unorthodox:
58
59 * The axiom they call **Leibniz** most other sources call **Congruence**,
60 and some sources describe it in a different fashion. (The book
61 explains how these two descriptions are equivalent.)
62 * The axiom they call **Equanimity** is not a part of the
63 equational logic proper, rather, it exists to support the
64 _equational theory of equality_ that **E** is undergirding,
65 and to bridge it _to_ the equational logic. (If you have
66 an equational logic supporting a different equational theory,
67 for example the equational theory of groups, you don't need
68 Equanimity.)
69 * They don't have **Reflexivity** and **Symmetry** as axioms, but
70 most other sources do. (These are instead axioms of their
71 equational theory of equality, which they can "lift up" to
72 the equational level using Equanimity.)
73
74 ### 📝 Wolfram MathWorld
75
76 As of this writing, [Equational Logic (Wolfram MathWorld)](https://mathworld.wolfram.com/EquationalLogic.html)
77 provides a more orthodox, but rather terse, exposition of equational logic.
78
79 Its Axiom 4 is often called **Congruence** elsewhere in the
80 literature, and is equivalent to Gries and Schneider's **Leibniz**
81 rule; and its Axiom 5 is often called **Substitution** or
82 **Replacement** elsewhere.
83
84 ### 📝 Dynamic Logic
85
86 The book "Dynamic Logic" by David Harel, Dexter Kozen, and Jerzy Tiuryn,
87 which [can be borrowed from archive.org](https://archive.org/details/dynamiclogicfoun00davi_0),
88 contains a section on Equational Logic (section 3.3), which serves as
89 a very good introduction.
90
91 ### 📝 Papers by George F. McNulty
92
93 Professor George F. McNulty of USC has written two excellent resources on equational logic:
94
95 * [Field Guide to Equational Logic (1992)](https://www.sciencedirect.com/science/article/pii/074771719290013T)
96 * [Equational Logic course notes (Spring 2017)](https://people.math.sc.edu/mcnulty/alglatvar/equationallogic.pdf)
97
98 These are both somewhat denser than the encyclopedic entries above, and cover
99 the connection between equational logic and universal algebra in more depth,
100 as well as results about equational logic as an object of study in itself.
101
102 The course notes have a few highlights definitely worth mentioning here:
103
104 * p.13: A stepwise equational proof of a theorem of ring theory
105 * p.21: Birkhoff's axioms for equational logic (basically the same as those on Wolfram MathWorld)
106 * also p.21: Tarski's axioms (a more minimal set of axioms; I'm not sure how they work yet)
107
108 The field guide lists many results in equational logic, but the most interesting
109 to me is section 6, which describes Tarski's relation algebra and how formulae of
110 first-order logic of up to 3 variables (but no more!) may be translated to it.
111
112 ### "Equational Reasoning"
113
114 The phrase "equational reasoning" refers to *informally* using an
115 equational theory to determine the meaning of (usually) a fragment
116 of a program in a programming language, which is (usually)
117 referentially transparent.
118
119 TODO: Add reference to an article that illustrates this
120
121 ### "Modulo an Equational Theory"
122
123 The phrase "modulo an equational theory" refers to automatically treating
124 two terms as equal if there is a proof of their equality in an equational
125 theory. This is sometimes employed in theorem provers, etc. to reduce
126 the amount of trivial proof work that is needed to show a result, especially
127 when it comes to "standard" equational axioms such as associativity and
128 commutivity. Instead of going through all the steps to show that
129 `a.(b.(c.d))` = `((a.b).c).d` (where `.` is associative), the two terms
130 are automatically considered equal.
131
132 TODO: Add reference to a tool that implements this (egg?)