#+title: Musa Al-hassy's Personal Glossary # +OPTIONS: broken-links:auto # The last one has the styling for lists. #+begin_quote Knowledge is software for your brain: The more you know, the more problems you can solve! #+end_quote :template:... #+begin_documentation Hussain :show t :color blue :label (Karbala Cosmic_Tragedy) Hussein ibn Ali is the grandson of Prophet Muhammad, who is known to have declared “Hussain is from me and I am from Hussain; God loves whoever loves Hussain.” 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. A terse summary of the chain of events leading to the massacre may be found at https://www.al-islam.org/articles/karbala-chain-events. An elegant English recitation recounting the Karbala Massacre may be found at https://youtu.be/2i9Y3Km6h08 ---“Arbaeen Maqtal - Sheikh Hamam Nassereddine - 1439”. -------------------------------------------------------------------------------- Charles Dickens: “If Hussain had fought to quench his worldly desires...then I do not understand why his sister, wife, and children accompanied him. It stands to reason therefore, that he sacrificed purely for Islam.” Gandhi: “I learned from Hussain how to achieve victory while being oppressed.” Thomas Carlyle: “The victory of Hussein, despite his minority, marvels me.” Thomas Masaryk: “Although our clergies also move us while describing the Christ's sufferings, but the zeal and zest that is found in the followers of 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 in front of a huge mountain.” #+end_documentation * Logics :PROPERTIES:... #+begin_documentation graph :show t :color blue A (Partial, resp. Total) Graph consists of + a set of “points, nodes, vertices” + a set of “arcs, edges” + a pair of partial (resp. total) functions. ⟦ Tersely put, in any category, a graph is a parallel pair of morphisms. ⟧ Edge parallelism is the relation 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. + A graph is total exactly when Id ⊆ Ξ; and so Ξ is an equivalence. + A graph has no parallel arrows exactly when Ξ ⊆ Id. + A graph is simple exactly when Ξ = Id. The associated relation is the relation _⟶_ = src ˘ ⨾ tgt 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 ⟵ for ⟶˘; one writes ⟶⋆ for the reachability relation. + Node y is reachable via a non-empty path from node x exactly when x ⟶⁺ y. - Node x lies on a cycle exactly when x ⟶⁺ x. - A graph is DAG, acylic, circuit-free, exactly when ⟶⁺ ⊆ ∼Id; i.e., ⟶⁺ ∩ Id = ⊥. - An acyclic graph is a (directed) forest exactly when ⟶ is injective; i.e., every node has at most one predecessor; i.e., + A node r is a root exactly when every node is reachable from it; i.e., {r} × V ⊆ ⟶⋆; i.e., 𝕃 r ⨾ ⟶⋆ = ⊤ where 𝕃 r is defined by and - and - A tree is a forest with a root. + A graph is loop free exactly when ⟶ ⊆ ∼Id. + A graph is strongly connected exactly when ⟶⋆ = ⊤; i.e., ∼Id ⊆ ⟶⁺; i.e., every point is reachable from any other point; i.e., ∼Id ⊆ ⟶ ∩ ⟵˘; i.e., any two distinct points lie on an undirected circuit. - The equivalence classes of ⟶⋆ ∩ ⟵⋆ are the strongly connected components. + Terminal∣sinks are nodes from which it is not possible to proceed any further; i.e., terminals have no successors; the domain of ∼(⟶ ⨾ ⊤) is all terminals. + Initial∣sources are nodes from which it is not possible to proceed backward; i.e., initials have no predecessors; the domain of ∼(⟵ ⨾ ⊤) is all initials. #+end_documentation #+begin_documentation Expression :show t An expression 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” | Variable -- E.g., x or apple (no quotes!) | Application -- E.g., f(x₁, x₂, …, xₙ) #+end_example ( One reads ‘:=’ as becomes and so the addition of an extra colon results in a ‘stutter’: One reads ‘∷=’ as be-becomes. The symbol ‘|’ is read or. ) Notice that a constant is really just an application with n being 0 arguments and so the first line in the definition above could be omitted. -------------------------------------------------------------------------------- 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 variable of type τ is a name denoting a yet unknown value of type τ; i.e., “it is a pronoun (nickname) referring to a person in the collection of people τ”. E.g., to say 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 Expr τ refer to the expressions denoting values of type τ; then a meta-variable is simply a normal variable of type Expr τ. That is, when we write phrases like “Let E be an expression”, then the name varies and so is a variable, but it is an expression and so may consist of a function application or a variable. That is,is a variable that may stand for variables. This layered inception is resolved by referring to as not just any normal variable, but instead as a meta-variable: A variable capable of referring to other (simpler) variables. -------------------------------------------------------------------------------- Expressions, as defined above, are also known as abstract syntax trees (AST) or prefix notation. Then textual substitution is known as ‘grafting trees’ (a monadic bind). Their use can be clunky, such as by requiring many parentheses and implicitly forcing a syntactic distinction between equivalent expressions; e.g., gcd(m,gcd(n,p)) and gcd(gcd(m,n),p) look difference even though gcd is associative. As such, one can declare precedence levels ---a.k.a. binding power--- 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 concrete syntax ---i.e., in a syntactic shape that is more concrete. That is, the conventions on how a string should be parsed as a tree are known as a precedence, fixity, and associativity rules. Similarly, not for operators but one treats relations conjunctionally to reduce the number of ‘and’(∧) symbols; e.g. This is very useful to avoid repeating lengthy common expressions, such as y + 2. #+end_documentation #+begin_documentation Induction :show t :color blue How we prove a theorem ranging over natural numbers For instance, suppose the property is that using only 3 and 5 dollar bills, any amount of money that is at-least 8 dollars can be formed. Since there are an infinite number of natural numbers, it is not possibly to verify is true by evaluating at each natural number Knocking over dominos is induction: 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 to mean “the n-th domino can be knocked over”, then the question is “is true”. Then, clearly if we can knock over the first domino, and if when a domino is knocked over then it also knocks over the next domino, then ‘clearly’ all dominoes will be knocked over. This ‘basic observation’ is known as induction. Climbing a ladder is induction: 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 to mean “the n-th rung is reachable”, then the question is “is true”. Then, clearly if we can reach the first rung, and whenever we climb to a rung then we can reach up and grab the next rung, then ‘clearly’ all rungs of the ladder can be reached. This ‘basic observation’ is known as induction. Constant functions are induction: A predicate is a function. When is such a function constantly the value That is, when is Clearly, if starts off being ---i.e., P 0--- and it preserves truth at every step ---i.e., P n ⇒ P (n + 1)--- then P n will be true for any choice of That is, if we consider and as ordered sets and starts at the ‘top’ of 𝔹 ---i.e., P 0 = true--- and it is ascending ---i.e., P n ⇒ P (n + 1)--- and so ‘never goes down’, then clearly it must stay constantly at the top value of 𝔹. This ‘basic observation’ is known as induction. ⟦ For the money problem, we need to start somewhere else besides 0. ⟧ Principle of (“Weak”) Mathematical Induction: To show that a property is true for all natural numbers starting with some number show the following two properties: + Base case :: Show that is true. + Inductive Step :: Show that whenever (the inductive hypothesis) is a natural number that such that and is true, then is also true. ⟦ For the money problem, we need to be able to use the fact that to prove we must have already proven for all smaller values. ⟧ Principle of (“Strong”) Mathematical Induction: To show that a property is true for all natural numbers starting with some number show the following two properties: + Base case :: Show that is true. + Inductive Step :: Show that whenever (the inductive hypothesis) is a natural number that such that and are true, then 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.) The Least Number Principle (LNP) ---Another way to see induction: 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 must terminate. #+end_box #+end_documentation #+begin_documentation Textual_Substitution :show t The (simultaneous textual) Substitution operation replaces all variables with parenthesised expressions in an expression In particular, is just but with all occurrences of replaced by This is the “find-and-replace” utility you use on your computers. Textual substitution on expressions is known as “grafting” on trees: Evaluate by going down the tree and finding all the ‘leaves’ labelled cut them out and replace them with the new trees Since expressions are either variables of functions applications, substitution can be defined inductively/recursively by the following two clauses: + y[x ≔ F] = if x = y then F else y fi + f(t₁, …, tₙ)[x ≔ F] = f(t₁′, …, tₙ′) where tᵢ′ = tᵢ[x ≔ F] -------------------------------------------------------------------------------- Sequential ≠ Simultaneous: (x + 2 · y)[x ≔ y][y ≔ x] ≠ (x + 2 · y)[x, y ≔ y, x] Python, for example, has simultaneous assignment; e.g., x, y = y, x is used to swap the value of two variables. -------------------------------------------------------------------------------- A function is a rule for computing a value from another value. If we define using an expression, then function application can be defined using textual substitution: That is, expressions can be considered functions of their variables ---but it is still expressions that are the primitive idea, the building blocks. #+end_documentation #+begin_documentation Inference_Rule :show t 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. That is, a rule is a tuple that is thought of as ‘taking premises (instances of known results) and acting as a ‘natural, reasonable justification’ to obtain conclusion A proof system is a collection of rules. At first sight, this all sounds very abstract and rather useless, however it is a game: Starting from rules, what can you obtain? Some games can be very 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 be presented as an axiom The inference rule says “if the are all valid, i.e., true in all states, then so is ; the axiom, on the other hand, says “if the are true in a state, then is true in that state.” Thus the rule and the axiom are not quite 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 can get the thing below the bar, but that thing (19) is not ‘true’ as we may think of conventional truth. Finally, the rule asserts that follows from The formula 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 some, or all possible inputs). -------------------------------------------------------------------------------- One reads/writes a natural deduction proof (tree) from the very bottom: Each line is an application of a rule of reasoning, whose assumptions are above the line; so read/written upward. The benefit of this approach is that rules guide proof construction; i.e., it is goal-directed. However the downsides are numerous: - So much horizontal space is needed even for simple proofs. - One has to repeat common subexpressions; e.g., when using transitivity of equality. - For comparison with other proof notations, such as Hilbert style, see Equational Propositional Logic. This is more ‘linear’ proof format; also known as equational style or calculational proof. 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. -------------------------------------------------------------------------------- Finally, an inference rule says that it is possible to start with the givens and obtain as result The idea to use inference rules as computation is witnessed by the Prolog programming language. #+end_documentation #+begin_documentation Logic :show t A logic is a formal system of reasoning... A logic is a set of symbols along with a set of formulas formed from the symbols, and a set of inference rules which allow formulas to be derived from other formulas. (The formulas may or may not include a notion of variable.) Logics are purely syntactic objects; an inference rule 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 some obvious truth using rules of reasoning that obviously preserve truth. #+end_documentation #+begin_documentation Theorem :show t :color blue A theorem is a syntactic object, a string of symbols with a particular property. A theorem 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 many 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 some, or all possible inputs). -------------------------------------------------------------------------------- A meta-theorem 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 theorem 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 in 𝑬 and meta-theorems are about 𝑬. For example, here is a meta-theorem that the equational logic 𝑬 has (as do many other theories, such as lattices): An equational 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. #+end_documentation #+begin_documentation Metatheorem :show t A theorem in the technical sense is an expression derived from axioms using inference rules. A metatheorem is a general statement about a logic that one argues to be true. 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 within 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 and the rule “If is a theorem then so is . Notice that are any 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’. #+end_documentation ( Calculus) #+begin_documentation Calculus :label Propositional_Calculus :show t :color blue A calculus is a method or process of reasoning by calculation with symbols. A propositional calculus 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. #+end_documentation #+begin_documentation Semantics :label (Axiomatic_Semantics Operational_Semantics) :show t Syntax refers to the structure of expressions, or the rules for putting symbols together to form an expression. Semantics refers to the meaning of expressions or how they are evaluated. An expression can contain variables, and evaluating such an expression requires knowing what values to use for these variables; i.e., a state: A list of variables with associated values. E.g., evaluation of in the state consisting of andis performed by replacing and by their values to yield and then evaluating that to yield A Boolean expression is satisfied in a state if its value is true in that state; is satisfiable if there is a state in which it is satisfied; and is valid (or is a tautology) if it is satisfied in every state. -------------------------------------------------------------------------------- Often operations are defined by how they are evaluated (operationally), we take the alternative route of defining operations by how they can be manipulated (axiomatically); i.e., by what properties they satisfy. For example, evaluation of the expression in a state yields the value true if expressions and have the same value and yields false if they have different values. This characterisation of equality is in terms of expression evaluation. For reasoning about expressions, a more useful characterisation would be a set of laws that can be used to show that two expressions are equal, without calculating their values. --- c.f., static analysis versues running a program. For example, you know that equals regardless of the values of and A collection of such laws can be regarded as a definition of equality, provided two expressions have the same value in all states precisely when one expression can be translated into the other according to the laws. Usually, in a logic, theorems correspond to expressions that are true in all states. -------------------------------------------------------------------------------- That is, instead of defining expressions by how they are evaluated, we may define expressions in terms of how they can be manipulated ---c.f., a calculus. For instance, we may define basic manipulative properties of operators ---i.e., axioms--- 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 and evaluate to the same value for any choice of values for 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., #+end_documentation #+begin_documentation Calculational Proof :show t A story whose events have smooth transitions connecting them. # A proof wherein each step is connected to the next step by an explicit # justification. This is a ‘linear’ proof format; also known as equational style or calculational proof. 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. ( This is similar to programming which encourages placing comments to communicate 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 be mentioned explicitly. For comparison with other proof notations see Equational Propositional Logic. -------------------------------------------------------------------------------- We advocate calculational proofs in which reasoning is goal directed and justified by simple axiomatic laws that can be checked syntactically rather than semantically. ---Program Construction by Roland Backhouse -------------------------------------------------------------------------------- Calculational proofs introduce notation and recall theorems as needed, thereby making each step of the argument easy 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 being weakened (“⇒”). 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. #+end_documentation ** Misc :ignore: :PROPERTIES:... #+begin_documentation Programming :show t Programming is solving the equation R ⇒[C] G in the unknown C; i.e., it is the activity of finding a ‘recipe’ that satisfies a given specification. Sometimes we may write R ⇒[?] G and solve for ‘?’. Programming is a goal-directed activity: From a specification, a program is found by examining the shape of its postcondition. #+end_documentation #+begin_documentation Specification :show t :color blue A specification is an equation of a certain shape. Programming is the activity of solving a specification for its unknown. Its unknown is called a program. See also “Programming”. #+end_documentation #+begin_documentation Proving_is_Programming :show t :color blue Problems may be formulated and solved using, possibly implicitly, the construction of correct programs: “for all x satisfying R(x), there is a y such that G(x,y) is true” ≈ ∀ x • R x ⇒ ∃ y • G x y ≈ R {𝑺} G for some program 𝑺 with inputs x and outputs y This is known as a constructive proof since we have an algorithm 𝑺 that actually shows how to find a particular y to solve the problem, for any given x. In contrast, non-constructive proofs usually involving some form of counting followed by a phrase “there is at least one such y …”, without actually indicating how to find it! The “R {𝑺} G” is known as a ‘Hoare triple’ and it expresses “when begun in a state satisfying R, program 𝑺 will terminate in a state satisfying G.” -------------------------------------------------------------------------------- + Proving ≈ Programming + Logic ≈ Trees (algebraic data types, 𝒲-types) + Rules ≈ Constructors + Proof ≈ An application of constructors + Axiom ≈ A constructor with no arguments #+end_documentation #+begin_documentation Algorithmic Problem Solving :show t :color blue 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. #+end_documentation # Computing science is all about solving algorithmic problems (or, as some # authors pre- fer to say, it is all about instructing computers to solve # problems). #+begin_documentation Natural Transformation :label (nat-trans polymorphism) :show t :color blue Natural transformations are essentially polymorphic functions that make no choices according to the input type; e.g., reverse : List τ → List τ makes no choices depending on the type τ. #+end_documentation #+begin_documentation Category Theory :label cat :show t A theory of typed composition; e.g., typed monoids. #+end_documentation * Properties of Operators :PROPERTIES:... #+begin_documentation Associative :show t :color blue An operation ⊕ is associative when it satisfies 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., is equivalent to Hence, we can write instead of or When an operation is associative, it is best to avoid “making a choice” of how sequences of ⊕ should be read, by using parentheses ---unless to make things clear or explicit for manipulation. -------------------------------------------------------------------------------- More generally, for any two operations ⊕ and ⊞, the “(left to right) mutual associativity of ⊕ and ⊞” is the property It allows us to omit parentheses in mixed sequences of ⊕ and ⊞. For instance, addition and subtraction are (left to right) mutually associative. #+end_documentation #+begin_documentation Identity :show t An operation ⊕ has identity 𝑰 when it satisfies If it satisfies only the first equation, one says that “𝑰 is a left-identity for ⊕”. If it satisfies only the second equation, one says that “𝑰 is a right-identity for ⊕”. For example, implication only has a left identity, and subtraction only has a right identity, An identity implies that occurrences of “⊕ 𝑰” and “𝑰 ⊕” in an expression are redundant. Thus, may be replaced by in any expression without changing the value of the expression. Therefore, we usually eliminate such occurrences unless something encourages us to leave them in. #+end_documentation #+begin_documentation Distributive :show t :color blue An operation ⊗ distributes over ⊕ when they satisfy “left-distributivity” and “right-distributivity” When ⊕ = ⊗, one says that the operation is “self-distributive”. Distributivity can be viewed in two ways, much like distributivity of multiplication × over addition +. Replacing the left side by the right side could be called “multiplying out”; replacing the right side by the left side, “factoring”. #+end_documentation #+begin_documentation Commutative :show t :color green An operation ⊕ is commutative or symmetric if it satisfies x ⊕ y = y ⊕ x. 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. #+end_documentation * Properties of Homogeneous Relations :PROPERTIES:... #+begin_documentation Reflexive :show t :color blue Elements are related to themselves -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, reflexivity means there is loop “ ⟳ ” at each node. -------------------------------------------------------------------------------- R is reflexive exactly when everything is related to itself. ≡ ∀ x • x 〔R〕 x ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. #+end_documentation #+begin_documentation Transitive :show t :color green A relation ⊑ is transitive when it satisfies a ⊑ b ∧ b ⊑ c ⇒ a ⊑ c; i.e., a ⊑ b ⊑ c ⇒ a ⊑ c ---that is, “we can chain ⊑” so that from a proof of a ⊑ b ⊑ c we can get from the first to the final part and so have a proof of a ⊑ c. Loosely put, whenever a and c have a common relative then they are themselves related. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, transitivity means paths can always be shortened (but nonempty). -------------------------------------------------------------------------------- By the shunting rule, transitivity can be read as a ‘monotonicity’ property for the operation that turns a value x into the proposition a ⊑ x; this maps ordered relationships b ⊑ c to ordered propositions a ⊑ b ⇒ a ⊑ c. Likewise, transitivity can be read as an ‘*antitonicity*’ property for the operation mapping a value x to the proposition x ⊑ c; this maps ordered relationships a ⊑ b to ordered propositions b ⊑ c ⇒ a ⊑ c. -------------------------------------------------------------------------------- Relation R is transitive ≡ Things related to things that are related, are themselves related. ≡ Whenever x is related to y and y is related to z, then also x will be related to z ≡ ∀ x, y, z • x 〔 R 〕 y 〔R 〕 z ⇒ x 〔R〕 z ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ 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. #+end_documentation #+begin_documentation Symmetric :show t :color blue The relationship is mutual; if one thing is related to the other, then the other is also related to the first. is symmetric ≡ If x is related to y, then y is also related to x. ≡ ∀ x, y • x 〔R〕 y ⇒ y 〔 R〕 x ≡ ≡ ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, symmetry means the graphs is undirected. 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 undirected graphs. - Undirected edges represent pairs of arrows pointing in opposite directions. Coreflexives are symmetric: -------------------------------------------------------------------------------- Interestingly, every homogeneous relation R may be partitioned into an asymmetric part and a symmetric part ---i.e., and where ⊥ is the empty relation. #+end_documentation #+begin_documentation Antisymmetric :show t :color blue Different elements cannot be mutually related; i.e., Mutually related items are necessarily indistinguishable. 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 often shows two sets are equal by using the antisymmetry of ‘⊆’. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, antisymmetry means Mutually related nodes are necessarily self-loops. -------------------------------------------------------------------------------- is antisymmetric ≡ ∀ x, y • x 〔R〕 y ∧ y 〔 R〕 x ⇒ x = y ≡ ∀ x, y • x ≠ y ⇒ ¬ (x 〔R〕 y ∧ y 〔 R〕 x) ≡ ∀ x, y • x ≠ y ⇒ x 〔R̸〕 y ∨ y 〔 R̸〕 x ≡ ≡ ≡ R ╳ R = Id ---‘╳’ is symmetric quotient Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. ( As a simple graph, an antisymmetric relation has at most one arrow between any two different nodes. ) #+end_documentation #+begin_documentation Asymmetric :show t :color blue The relationship is mutually exclusive. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, asymmetric means: There's at most 1 edge (regardless of direction) relating any 2 nodes. -------------------------------------------------------------------------------- is asymmetric ≡ ∀ x, y • x 〔R〕 y ⇒ ¬ y 〔R〕 x ≡ ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. Asymmetrics are irreflexive ---just pick x = y in the above ∀-formulation ;-) -------------------------------------------------------------------------------- Interestingly, every homogeneous relation R may be partitioned into an asymmetric part and a symmetric part ---i.e., and where ⊥ is the empty relation. #+end_documentation #+begin_documentation Preorder :show t :color blue A preorder models the notion of ‘inclusion’ or ‘at most’ or ‘before’ or ‘predecessor of’; and so requires: Everything is included in itself and inclusion is transitive. is a preorder ≡ is transitive and reflexive ≡ ≡ ≡ ---“indirect inclusion from above” ≡ ---“indirect inclusion from below” Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. If it is additionally antisymmetric, one says we have an order. - The relation is the greatest equivalence contained in a preorder Indeed, it's clearly symmetric and reflexive, and transitive since ‘⨾’ sub-distributes over ‘∩’ and R and R˘ are transitive. Then, for any equivalence Ξ ⊆ R, we have Ξ = Ξ ˘ ⊆ R ˘ and so Ξ ⊆ R ∩ R˘. Instead of reflexivity, if we have irreflexivity we get strict order: is a strict order ≡ is transitive and irreflexive ≡ ≡ ≡ ≡ is transitive and asymmetric ( Warning! A “strict order” is not an order that is somehow strict. ) Orders and strict orders come in pairs: Every order induces a strict order conversely, every strict order gives rise to an order As such, it is customary to denote order relations by symbols such as ≤, ⊆. ≼, ⊑ and their associated strict orders by related symbols <, ⊂, ≺, ⊏, respectively, with *lack the horizontal line ‘─’ below the symbol to indicate irreflexivity ---i.e., the line is a suggestive reminder of equality. When letters are used to denote orders, one may see E for an order since it is reminiscent of ≤ and ⊆, and may see C for a strict order since it is reminiscent of < and ⊂. Using ‘≤’ for an arbitrary order is not ideal since readers may confuse it with the familiar linear orders for numbers. #+end_documentation #+begin_documentation Equivalence :show t :color blue An equivalence models the notion of ‘similarity’; Everything is similar to itself, being similar is a mutual relationship, and it is transitive. is an equivalence ≡ is a symmetric preorder ≡ is transitive and reflexive and symmetric ≡ ≡ ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. -------------------------------------------------------------------------------- For example, “2 + 3” and “5” are clearly *not the same*”: The first is a string of 3 symbols, whereas the latter is a string of a single symbol. However, they are equivalent when we evaluate them and so we want to pretend they are the same, not by using equality, but by using an equivalence relation. ( This equivalence relation is obtained using transitive closure as where is the evaluation, reduction relation. ) In general, “sharing the same feature 𝒇” is an equivalence relation. That is, if is a function, then ∼ is an equivalence relation defined by -------------------------------------------------------------------------------- Characterising Equivalences with “Indirect Equivalence”: Ξ is an equivalence ≡ -------------------------------------------------------------------------------- Equivalence relations coincide with partitions. #+end_documentation #+begin_documentation Linear :show t :color blue Any two (possibly identical) members are related; (the associated graph can be drawn similar to a line; i.e., the nodes can be arranged in a sequence). ( In graph terminology, linear is also referred to as strongly complete. ) ( Sometimes a linear order is called a complete order. ) is linear ≡ ∀ x, y • x 〔R〕 y ∨ y 〔R〕 x ≡ ≡ ≡ is asymmetric Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. -------------------------------------------------------------------------------- A linear order corresponds to a full upper triangular matrix, after suitably arranging rows and columns. A linear (pre)-order has no (distinct) incomparable elements. Any linear ordering E, with associated strict order C, satisfies i.e., any linear order ‘⊑’ satisfies Likewise, for liner order, we have transitivity E⨾C⨾E = C and weakening C ⊆ E; i.e., Every order E can be extended to a linear order E′; i.e., E ⊆ E′. For the finite case this is known as topological sort, and for the infinite case this is known as the Szpilrajn extension. - For the finite case, the idea is as follows: If E is not linear, then there are two incomparable elements x, y (i.e., outside E ∪ E˘), so we may define an ordering E₁ ≔ E ∪ {(x, y)}. We iterate this process and Eₙ will eventually become linear. This process maintains “the order E, less the incomparable elements, is linear” invariant throughout. Since each step reduces the number of incomparable elements, it must terminate, and the invariant then ensures the resulting order is linear. (•̀ᴗ•́)و #+end_documentation #+begin_documentation Semilinear :show t :color blue Any two different members are related; (the associated graph can be drawn similar to a line). ( In graph terminology, semilinear is also referred to as complete; e.g., “the complete graph on n nodes” refers to ) is semilinear ≡ ∀ x, y • x ≠ y ⇒ x 〔R〕 y ∨ y 〔R〕 x ≡ ≡ ≡ is antisymmetric Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. A relation without incomparable elements is semilinear. A semilinear and asymmetric relationis known as a tournament since it models the win-loss situation of a typical sports tournament: Semilinearity and asymmetry ensure teams do not play against themselves and that there is no draw ---i.e., there must be a winner. A tournament R is characterised by R ∪ R˘ = ∼Id. #+end_documentation * Properties of Heterogeneous Relations :PROPERTIES:... #+begin_documentation Univalent :show t :color blue Univalent (partially defined function): Equal elements are related to equal elements; i.e., an element cannot be related to two different elements. That is, every source value x is associated at most one target value y. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, univalence means: Any arcs from the same source actually coincide. That is, Every node has at most one outgoing edge. -------------------------------------------------------------------------------- is univalent ≡ ∀ x, y, y′ • x 〔 R 〕 y ∧ x 〔R〕 y′ ⇒ y = y′ ≡ ≡ ≡ ≡ ∀ S • R ⨾ ∼ S = R ⨾ ⊤ ∩ ∼(R ⨾ S) ≡ ∀ Q, S • R ⨾ (Q ∩ S) = R ⨾ Q ∩ R ⨾ S ---c.f., ⨾ sub-distributes over ∩ ≡ ∀ Q, S • Q⨾R ∩ S = (Q ∩ S ⨾ R˘)⨾R ---c.f., the Dedekind rule Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. -------------------------------------------------------------------------------- The formula reads “If x is R-related to a value different from y, then it is not R-related to y.” It continues to hold when we replace the identity by an arbitrary relation. The 5th row reads, the preimage of the complement is the same as the complement of the preimage intersected with the domain. In fact, for univalent we also have e.g., the people who do “not (own an Audi car)” are exactly the people who “(own a non-Audi car) or do not(own any car)” ---assuming a person can own at most one car. For a map the 6th row becomes: using conventional direct image notation; i.e., for a function, the preimage of an intersection is the intersection of preimages. Likewise, for a map we have the intersection ofwith a function's image is the same as the image of an intersection involving the preimage of $B$; i.e., #+end_documentation #+begin_documentation Total :show t :color blue Total: Every source value x is associated at least one target value y. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, totality means: Every node has at least one outgoing edge. is total ≡ ∀ x • ∃ y • x 〔 R 〕 y ≡ (“defined everywhere”) ≡ ≡ ≡ ≡ ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. -------------------------------------------------------------------------------- The formula reads “If x is not R-related to y, then x is R related to some element different from y.” It continues to hold when we replace the identity by an arbitrary relation. The final formula says that is post-annihilated by the empty relation only. Note: for any i.e., the complement of a relation's domain is everything precisely when the relation is empty. #+end_documentation #+begin_documentation Map :show t :color blue Map (totally defined function): Every source value x is associated exactly one target value y. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple relation, being a mapping means: Every node has exactly one outgoing edge. -------------------------------------------------------------------------------- is a map ≡ is total and univalent ≡ ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. -------------------------------------------------------------------------------- The final rule says the preimage of the complement is the complement of the preimage; or, using conventional direct image notation, In conventional direct image notation, this amount to a Galois connection: A mapping is so very close to being invertible since mappings always satisfy: and Shunting rule:* If is a map, then More generally, given an equivalence Ξ, if relation F is total and Ξ-univalent ---i.e., F˘ ⨾ F ⊆ Ξ--- and if S is Ξ-target-saturated ---i.e., S ⨾ Ξ = S--- then #+end_documentation #+begin_documentation Surjective :show t :color blue Surjective: Every source value y is associated at least one source value x. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, surjectivity means: Every node has at least one incoming edge. -------------------------------------------------------------------------------- is surjective ≡ is total ≡ ≡ ≡ ≡ ∀ S • R ⨾ S = ⊥ ≡ S = ⊥ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. #+end_documentation #+begin_documentation Injective :show t :color blue Injective: Every source value y is associated at most one source value x. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, injective means: Every node has at most one incoming edge. -------------------------------------------------------------------------------- is injective ≡ is univalent ≡ ≡ Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. #+end_documentation #+begin_documentation Bijective :show t :color blue Bijective: Every source value y is associated exactly one source value x. is bijective ≡ is injective and surjective -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, bijectivity means: Every node has exactly one outgoing edge. #+end_documentation #+begin_documentation Iso :show t :color blue An iso is a bijective mapping, also known as a permutation. An isomorphism is a non-lossy protocol associating inputs to outputs. -------------------------------------------------------------------------------- A relation can be visualised as a drawing: A dot for each element of and a directed line between two points exactly when That is relations are simple graphs; one refers to the directed lines as edges and the dots as nodes. As a simple graph, an iso is a bunch of circles: Any number of cycles, such that every node lies on exactly one. -------------------------------------------------------------------------------- If relation is finite, then Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. #+end_documentation #+begin_documentation Difunctional :show t :color blue This property generalises injectivity, univalence, and equivalence... Recall, - Univalent: Every source value x is associated at most one target value y. + I.e., if x goes to y and y′ then y = y′. + I.e., - Injective: Every source value y is associated at most one source value x. + I.e., if y comes from x and x′ then x = x′. + I.e., - Equivalence: Any given equivalence classes are either identical or disjoint. # + I.e., + Moreover, it is a homogenous relation. Now, a possibly heterogenous relation R is difunctional exactly when That is, in-fact we have equality Using Schröder, this amounts to Clearly, converse preserves difunctionality. For difunctional R, 1. R ⨾ (Q ∩ R˘ ⨾ S) = R ⨾ Q ∩ R ⨾ R˘ ⨾ S 2. 3. 4. if R is also total. Where ⨾, ⊤, ⊥, Id, ˘, ∼ are relation composition, the universal relation, the empty relation, the identity relation, relation converse (transpose), and complement. -------------------------------------------------------------------------------- The equivalence target-saturation of a univalent relation is difunctional; i.e., if R is univalent and Ξ is an equivalence, then is difunctional. #+end_documentation