obtheory.txt 1.4.2 UTF-8 2024-04-19 *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* MISER THEORETICAL CONCEPTION ============================ The latest version is always available at this location. ‹ob› MATHEMATICAL STRUCTURE --------------------------- The mathematical structure, ‹ob› = 〈Ob,Of,Ot〉consists of Ob, nothing but obs, the domain of discourse Of, nothing but functions on obs Ot, the applied-logic axiomatic theory in which the structure is characterized for any obs whatsoever Obs are abstract mathematical entities. They can be construed as encoding of data along with theoretical expression of effectively-computable functions on such data. This is the foundation on which the oMiser model of computation is errected. The appeal of ‹ob› among computational models is how interpretation of obs as programs exhibits the stored-program principle and the manner in which levels of abstraction become available and useful in general-purpose computing. The Miser Project provides an operational implementation that demonstrates shared universality with prominent models recognized as Church-Turing Complete. An informal overview, with illustrative usage, is found in the file . CONTENT 1. LOGICAL NOTATION Notation for First Order Logic with Equality (FOL=) employed in mathematical characterization of ‹ob› as well as of other structures. 2. AXIOMATIC NOTIONS Four functions, together with "=" that are sufficient for expressing all Obs, given a supply of initial individuals. Every computable function in Of (and decidable predicates) can be expressed in Ot in terms of the axiomatic provisions. 3. DENUMERABILITY AND EFFECTIVENESS Constraints on the composition of obs in relationship to other obs such that there is a precedence ordering among them. Conditions on the effective representation of functions in Ot are elaborated. Canonical forms are established for distinguishing and identifying obs. 4. NOTES AND REFERENCES 1. LOGICAL NOTATION For Ot, standard First-Order Logic with Equality (FOL=) is employed [Wikipedia2019]. An equational format is used with variables understood to be universally quantified over the domain of discourse, Ob. Set theory is not employed. The reading of ∀x is "for any x" or "given an ob, x"; ∀ quantifiers preceding an entire formula are generally implicit. Form ∃x with regard to the existence/non-existence of obs for satisfying a condition is limited (cf. Ob9(g), below). Logical aspects of theory Ot are expressed using the following notation. We intend truth-value semantics of deductions involving propositions expressed in Ot. Use of notions "true" and "false" is in that sense. p ⇔ q read p if-and-only-if q, true when both are true or both are false, a kind of logical equality relation p ⇒ q read if p then q; when p ⇒ q and p both hold, it is deducible that q holds. p ∨ q is logical or, true when p and q are not both false p ∧ q is logical and, true when p and q are both true ¬ p is logical not, true when p is false, false when p is true x = y is the identity relationship, with ≠ its negation x ¶ y is read as x precedes y, an ordering relationship that applies over Ob Although these can be seen as rules for computation, Ot is a deductive theory. E.g., if it is asserted that p ⇔ q and also ¬ p, deduction that ¬ q holds is a logical consequence; if it is asserted that p ⇒ q and also p, deduction that q holds is a logical inference. The law of excluded middle holds: It is the case that ¬(p ∧ ¬p) and also ¬(¬p) ⇔ p as well as (p ⇒ q) ⇔ (¬p ∨ q). 2. PRIMITIVE NOTIONS Specific predicates and functions are introduced by presentation of their characteristics via mathematical conditions that distinguish them. Functions ob.a, ob.b, ob.c, ob.e and allied relations are taken as given and completely specified. Ob1. Pairs z = ob.c(x,y) ⇒ ob.a(z) = x ∧ ob.b(z) = y z = ob.c(ob.a(z),ob.b(z)) ⇔ ob.a(z) ≠ z ∧ ob.b(z) ≠ z Ob2. Enclosures z = ob.e(x) ⇒ ob.a(z) = x ∧ ob.b(z) = z z = ob.e(ob.a(z)) ⇔ ob.a(z) ≠ z ∧ ob.b(z) = z Ob3. Individuals ob.is-individual(z) ⇔ ob.a(z) = z ∧ ob.b(z) = z Ob4. Structural Discrimination Predicates ob.is-singleton(z) ⇔ ob.b(z) = z. ob.is-pair(z) ⇔ ¬ ob.is-singleton(z) ob.is-enclosure(z) ⇔ ob.is-singleton(z) ∧ ob.a(z) ≠ z Ob5. Totality ob.is-individual(z) ∨ ob.is-enclosure(z) ∨ ob.is-pair(z) It is a consequence that each ob is exactly one of pair, enclosure, or individual and there are no others. (ob.is-individual(z) ∧ ¬ ob.is-enclosure(z) ∧ ¬ ob.is-pair(z)) ∨ (ob.is-enclosure(z) ∧ ¬ ob.is-individual(z) ∧ ¬ ob.is-pair(z)) ∨ (ob.is-pair(z) ∧ ¬ ob.is-enclosure(z) ∧ ¬ ob.is-individual(z)) Ob6. Structural Identity u = ob.c(v,w) ∧ z = ob.c(x,y) ⇒ (u = z ⇔ v = x ∧ w = y) (a) u = ob.e(v) ∧ z = ob.e(x) ⇒ (u = z ⇔ v = x) (b) ob.is-pair(u) ∧ ob.is-singleton(z) ⇒ u ≠ z (c) ob.is-individual(u) ∧ ob.a(z) ≠ z ⇒ u ≠ z (d) Ob7. Identity Among Primitive Individuals ob.is-individual(ob.NIL) (a) ob-is-primitive(ob.NIL) (b) There are a limited number of fixed-name primitive individuals. They can be taken as given. These are not definable in terms of others. Individuals identified by upper-case namings, such as ob.NIL, are distinct if and only if their names differ. Those individuals are also distinct from individuals of any other kind that may arise. Ob8. Uninterpreted Literal Individuals ob.is-lindy(x) ⇔ x = Ʃ's' where s is a finite-length character string consisting of one or more alphanumeric characters In the CFob notation for expressing Obs, lindy Ʃ's' is simply expressed by the string "s" text. See Ob10, below, and the companion file CFob.txt. IMPLEMENTATION NOTE: In computer representations, the alphanumeric characters permitted in strings "s" are Unicode glyphs, encoded in UTF-8, in the form of XML Names without any "." and ":" characters [XML10:2.3 Common Syntactic Constructs, Names and Tokens]. It is also permissible for "s" to begin with a numeral and to be entirely numerical. The only feature of lindies is their differentiation. Ʃ's' = Ʃ't' ⇔ s Ʃ= t where s Ʃ= t signifies identity of the string texts ob.is-lindy(x) ⇒ ob.is-individual(x) ob.is-lindy(x) ∧ ¬ ob.is-lindy(y) ⇒ x ≠ y Lindies are distinct conveniently-named individuals that have no intrinsic significance. They are available to applications of obs for any purpose as distinct literals, such as Ʃ'日本語', Ʃ'ABCs', Ʃ'letterQ', Ʃ'foo', Ʃ'4', Ʃ'فارسی', etc. 3. DENUMERABILITY AND EFFECTIVENESS Ob9. The ¶ Precedence Condition ¬ (x ¶ x) (a), irreflexive (x ¶ y) ⇒ ¬ (y ¶ x) (b), asymmetrical (x ¶ y) ∧ (y ¶ z) ⇒ (x ¶ z) (c), transitive x = y ∨ x ¶ y ∨ y ¶ x (d), distinction x = y ⇔ ¬ (x ¶ y ∨ y ¶ x) z = ob.e(y) ⇒ (y ¶ z) (e), construction z = ob.c(x,y) ⇒ (x ¶ z) ∧ (y ¶ z) ob.is-individual(x) ⇒ x ¶ ob.e(x) (f), floating ob.is-individual(x) ⇒ x ¶ ob.c(x,y) ob.is-individual(x) ⇒ x ¶ ob.c(y,x) ob-is-elemental(x) (g), grounding ⇔ ob.is-lindy(x) ∨ ob-is-primitive(x) ob.is-elemental(x) ⇒ ¬ꓱy[y ¶ x] ¬ob.is-elemental(x) ⇒ ꓱy[y ¶ x] Ob10. Denumerable Canonical Form Ob consists of those distinct, finitely-expressible obs satisfying conditions Ob1-Ob9 and expressed (1) without use of variables, (2) without any functions other than ob.c and ob.e, and (3) without extraneous parentheses. Such expressions are canonical forms in that each form is unique to a particular ob and any ob is determined via a canonical form. Ob is unbounded and denumerable provided that the individuals be denumerable. This is the case for the canonical forms, and the obs are in one-to-one correspondence with their canonical forms. We say that an ob is definite, or determined, when its canonical form can be exhibited explicitly. This case is important because computation, for oMiser, can be viewed as systematic determination of definite obs from given definite ones. This is comparable to the situation with arithmetic where decimal numerals are typical canonical forms for (natural) numbers. Certain extensions to ‹ob› will augment the variety of canonical forms without altering the denumerability of them, preserving Ob1-Ob9. Ob11. Effectively-Computable Functions in Of Without addressing fine technicalities here, a function F over Ob (and in Of by definition) is claimed to be effectively-computable if, given any definite obs as arguments, any definite result is determined by a finite deduction based entirely on the Ot characterization of F. It can be the case that there is no definite result for some definite arguments. Predicates of Ot are effectively-computable as satisfied or not in a similar manner and termed effectively-decidable. Observe that ob.a(x), ob.b(x), ob.c(x,y), ob.e(x), the six ob.is-... predicates, and the "=" relation are all effectively-computable in this sense. They are also total in the sense that a definite result is determined whenever there are definite arguments. In contrast, x ¶ y is only partially-determined. When x ≠ y is determined, it need not be deducible which of x ¶ y or y ¶ x holds. This is the case among definite individuals that are distinguished by literal identifiers (e.g., lindies) and no other condition on comparability. The strength of Ob9 is that ¬(x ¶ x) be preserved. The mathematical benefit of the strict partial-ordering x ¶ y is the availability of structural induction for reasoning about functions in Of. Later, when we make computational interpretations of ‹ob›, there'll be no need for an explicit counterpart of x ¶ y. It is sufficient that no ob interpretation can appear as a component within its own composition, however deeply, and supporting operations cannot violate that constraint in the computational interpretation. In valid computational interpretations, counterparts of obs are immutable and have no cycles, the special case of singletons notwithstanding. 4. NOTES AND REFERENCES The notions of individual, enclosure, singleton, and pair have their inspiration in the nested-array work of [More1979] and the foundation structure of LISP [McCarthy1960]. The importance of enclosure as a structural feature of obs was observed in an incompleteness regarding nested strings in [Strachey1965]. Representations of strings that have other strings as their beads, a limited feature of ALGOL 60, was introduced by Doug Ross and colleagues in the AED system [Ross1967]. There are notions about storage there that are worth reviewing for Miser. The computational model founded on ‹ob› for oMiser is a fully-applicative scheme inspired through my association with Peter Landin and William H. Burge in the mid-1960s, with operation now via a list-processing abstraction. "Effectively computable" and "effective computability" are used in the manner of the title of [Rogers1987]. Employment, for now, is as a kind of deduction separate from computational interpretations (e.g., as algorithms), akin to the term employed in [Church1936] before a general-purpose digital computer had ever been seen or described. For the Miser Project, computability is not directly aligned with Turing Computability, despite demonstrable equivalence in the Church-Turing sense. When we speak of the effectively-computable functions on obs, as obs are characterized here, the claim will be that ‹ob› has equivalent power to all systems for the CT-computable functions. When a universal function is also formulated, its correspondence to a Universal Turing Machine will be one of the confirming demonstrations and Church-Turing Completeness will be claimed. Ob7-Ob9 must be augmented in the case of extensions that introduce new distinct individuals constructed from other obs. Supplementary definitions will be provided along with the introduction of such extensions. An account of this foundational theory for the abstract data type that underlies all oMiser implementations is narrated in a progression of blog posts. This material will be supplanted by material to be established at . * Miser Project: Hark! Is That a Theory I See Before Me? on the mathematical-logic notation used at the mathematical level * Miser Project: ‹ob› Primitive Functions including introduction of Ob1-Ob7 here. * Miser Project: Narrowing ‹ob› for Computational Interpretation including introduction of Ob8-Ob10 here. * Miser Project: Representing Data as Obs introducing computational interpretations of obs and obs as encodings (interpretations for) data as an initial step toward the oMiser computational model. A compact canonical form expression is defined. * Miser Project: Representing Functions in ‹ob›’s Abstract World reasoning about functions on obs and then exploring interpretation of other structures with representation of functions in each other and in ‹ob›. There is extensive attention to interpretations and representations of Boolean Algebras by way of illustration and for future application. See . * Miser Project: Interpretation, Representation, Computation, and Manifestation expanding on some specialized notions applied throughout development of the Miser Project. [Burge1975] Burge, William H. Recursive Programming Techniques. Addison-Wesley (Reading, MA: 1975). ISBN 0-201-14450-6. See (../../bib/authors.htm#Burge1975). [Church1936] Church, Alonzo. An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics 58 (1936), 345-363. Reprinted on pp.88-115 with supplemental notes in [Davis1965]. See (../../bib/authors.htm#Church1936). [Davis1965] Davis, Martin (ed.). The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Rave Press (New York: 1965). ISBN 0-911216-01-4. See (../../bib/authors.htm#Davis1965). [McCarthy1960] McCarthy, John. Recursive functions of symbolic expressions and their computation by machine, Part I. Comm. ACM 3, 4 (April 1960), 184-195. doi>10.1145/367177.367199 available at . See (../../bib/authors.htm#McCarthy1960). [More1979] More, Trenchard. The nested rectangular array as a model of data. pp. 55-73 in "APL '79 Proceedings of the international conference on APL: Part 1." doi>10.1145/390009.804440 available at . See (../../bib/authors.htm#More1979). [Rogers1987] Rogers, Hartley, Jr. Theory of Recursive Functions and Effective Computability. MIT Press (Cambridge, MA: 1987). ISBN 0-262-68052-1 pbk. See (../../bib/authors#Rogers1987). [Ross1967] Ross, Douglas T. The AED Free Storage Package. Comm. ACM 10, 8 (August 1967), 482-492. See (../../bib/authors#Ross1967). [Strachey1965] Strachey, Christopher. A General Purpose Macrogenerator. The Computer Journal 8, 3 (January 1965), 225-241. Available at . See (../../bib/authors.htm#Strachey1965) [Wikipedia2018a] Canonical form. 2018-10-10 article available on the Internet at . See (../../bib/authors.htm#Wikipedia2018a). [Wikipedia2018b] Structural induction. 2018-09-09 article available on the Internet at . See (../../bib/authors.htm#Wikipedia2018b). [Wikipedia2019] First-order logic. 2019-01-07 article available on the Internet at . See (../../bib/authors.htm#Wikipedia2019). *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* Copyright 2017-2020, 2023-2024 Dennis E. Hamilton Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at http://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* ATTRIBUTION Hamilton, Dennis E. ‹ob› Mathematical Structure. Miser Theory Conception text file obtheory.txt version 1.4.2 dated 2024-04-19 available on the Internet as a version of . TODO * Figure out what to do about well-definedness. Is this an Ob11 or Ob12 condition? I claim it is implicit in Ob11 and it can be made explicit in one of the companion text files such as miser/theory.txt. * Rely on the Stanford Encyclopedia of Philosophy (SEP) treatment of the Church-Turing thesis and how we navigate the CT-computable. Put this where it belongs in obaptheory.txt, not here. * Consider Markdown versions that GitHub will render in a more-presentable form. Keep in mind that the .txt version had been intended to be always definitive. * Ensure that all of the citations and references here are available via orcmid.github.io/bib/ so they can be linked from the web version of obtheory.txt. *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* 1.4.2 2024-04-19T18:57Z More touch-ups and clarification on qualtifiers 1.4.1 2024-04-14T20:15Z Introduce ob-is-elemental on Ob9 and tighten x ¶ y 1.4.0 2024-04-14T17:20Z Expand Ob9 to establish that primitives and lindies have no predecessors. 1.3.3 2024-03-26T17:09Z Add link for Davis1965 1.3.2 2024-03-11T17:07Z Bibliography touch-ups 1.3.1 2024-02-13T20:16Z More touch-ups to stay within finitism. 1.3.0 2024-01-15T18:22Z Clarify sense of ∀x and way of speaking about ‹ob›. 1.2.4 2023-11-24T19:14Z Improve the note on origins, check citations 1.2.3 2023-11-19T21:33Z Establish the references here in ../../bib 1.2.2 2023-11-09T23:11Z Adjusted to orcmid.github.io/miser/ob/ location 1.2.1 2023-11-09T23:04Z Tombstoned at Orcmid GitHub miser/omiser/obtheory.txt 1.2.0 2023-08-24T23:52Z Proofed and aligned with obaptheory,text version 1.1.0 2023-08-24T20:31Z Transpose the introduction of Lindies to here. 1.0.1 2020-01-15-08:29 Correct file top-line typos and a change of links from Wordpress to Blogger. Mention https://orcmid.github.io/miser/ 1.0.0 2019-11-07-12:49 Replace Wordpress Miser Project links with ones to Orcmid's Lair on Blogger, declaring version 1.0.0. 0.2.11 2019-10-31-13:43 Wordsmithing and beginning adjustment of blog post locations 0.2.10 2019-10-30-10:12 Fix a line-wrap 0.2.9 2019-05-11-09:10 Adjust to wording suggested by William L. Anderson in issue #19, cross-reference with ob.txt, and manage TODOs. 0.2.8 2019-03-23-10:28 Correct text flow, add [Rogers1987] and [Church1936] remarking use of "effective computability" here, and referencing the further Orcmid's Live Hideout article of 2019-02-11. 0.2.7 2019-01-19-12:07 In Notes, connect the arrival at ‹ob› to inspirations in work of John McCarthy, Trenchard More, Christopher Strachey, Peter Landin and W. H. Burge. 0.2.6 2019-01-18-11:47 In Ob10, name x ¶ y as a strict partial-ordering. 0.2.5 2019-01-17-12:40 After conversation with Bill Anderson, replaced the preamble to reflect the purpose of introducing structure ‹ob›. 0.2.4 2019-01-10-10:49 Correct the count of primitive functions in the table of content. Touch up a little. 0.2.3 2019-01-08-10:16 Manage TODOs, add attribution, expand notes and repair definition of p ⇔ q caught by William L. Anderson (issue #16). 0.2.2 2018-12-14-10:45 Update Notes to reflect additional blog articles. 0.2.1 2018-11-17-14:05 Wordsmithing and tough-ups 0.2.0 2018-11-14-08:38 Editorial cleanups, add table of contents, and more connective text. 0.1.2 2018-11-02-13:13 Introduce structural induction as a critical benefit of requiring the existence of the partial well-ordering via x ¶ y. 0.1.1 2018-10-22-17:37 Correct a surprising typo in the definition of ¬ p. 0.1.0 2018-10-17-15:41 Clarify the situation of canonical forms and update the Notes and References. Manage TODOs. Reflect confidence with the increase to version 0.1.0. 0.0.32 2018-09-04-10:56 Correct howler in Ob10 about strength of Ob8, since it is a negation that must be preserved. Touch up and also manage TODOs. 0.0.31 2018-09-04-08:30 Expand and identify Ob8(d) as distinction. This is a theorem and worth making explicit for our purposes. 0.0.30 2018-08-29-12:37 Layout touch-ups, refinement of Ob8-Ob10 and initiation of Notes and References. Manage TODOs. 0.0.29 2018-08-26-10:22 Clean up white space and headings, manage TODOs. 0.0.28 2018-07-25-18:02 Correct serious error in Ob8. 0.0.27 2018-07-14-12:50 Manage TODOs, anticipating Ob8 requiriing extension later on. 0.0.26 2018-07-09-15:33 Correct line flow and a typo. There is no change of substance, making this a worthy substitute for reference from existing blog posts. 0.0.25 2018-07-07-11:05 Repair text-flow in Visual Code and point out the intended truth-value semantics of Ot. 0.0.24 2017-12-29-16:48 Adjust Ob8 and Ob10 so that x ¶ y is taken as a sufficient constraint without explicit, strict ordering having to be determined in a model. Thanks to Roman Susi (rnd0101) for Questions #1 discussion at . 0.0.23 2017-12-27-10:45 Touch-up, especially in Ob8-Ob10. Review TODOs. 0.0.22 2017-11-23-14:44 Replace ^ with ∧ in a couple of places. Touch up Ob9-Ob10 to make canonical form relevant to computation and leave open the prospect of effectively-computable partial functions. 0.0.21 2017-11-12-09:58 Manage TODOs. Touch up the text. 0.0.20 2017-11-11-11:28 Cleanup Ob10 on Effective Computability. 0.0.19 2017-09-28-13:04 Adjust TODOs. Address some comments and suggestions from Paul McJones (private communication). 0.0.18 2017-09-17-11:22 Describe ¶ as asymmetrical rather than non-commutative (hat tip to Paul McJones). Expand Ob10 for improved informal treatment of representation for effectively-computable functions. 0.0.17 2017-09-14-18:49 Add Ob10 on effective computability. 0.0.16 2017-09-06-18:02 Correct the GitHub link and add work items about further steps. 0.0.15 2017-09-05-18:11 Make ob.NIL an individual explicitly and simplify Ob7 somewhat. 0.0.14 2017-09-03-09:38 Make the Ob5 Totality partitioning consequence formally-explicit. 0.0.13 2017-08-28-08:56 Touch-up and add TODO about well-definedness. 0.0.12 2017-08-27-11:43 Wordsmithing and assertion of classical conditions. 0.0.11 2017-08-26-09:56 Smooth the description of the logical notation and distinguish it from similar-appearing computational operations. 0.0.10 2017-08-24-10:17 Adapted from the SML mockup obtest.sml 0.0.9 for reference in all mockups and the expanded development for oMiser. *** end of obtheory.txt ***