obaptheory.txt 1.2.3 UTF-8 2023-12-18 *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* MISER THEORETICAL CONCEPTION ============================ ‹ob› UNIVERSAL APPLICATIVE FUNCTIONS ------------------------------------ For the mathematical structure, ‹ob› = 〈Ob,Of,Ot〉, we represent a universal function, obap.ap(p,x) and important companion obap.ev(p,x,e) employed in its representation and separately useful via obap.eval(e). The use of prefix ob.ap (obap for short) reflects the reliance on ‹ob› with identification of additional primitive individuals on which the obap.ap and obap.eval function representations depend. Obap1. Universal Apply Function obap.ap(p,x) determines the application of ob p, taken as expression of an operator procedure, to ob x, taken as the operand obap.eval(exp) determines the evaluation of ob exp taken as an applicative expression Universality of obap.ap(p,x) is taken to mean that for every function, F, on obs that is effectively-computable, there is an ob p that expresses an effective procedure such that obap.ap(p,x) = F(x) is determined, where p, x, and any y = F(x) are expressed as canonical forms. The grand objective is to establish that not only is obap.ap(p,x) a universal function in this respect, but that it provides a model of commputation as powerful as any other, in harmony with the Church-Turing thesis. This hinges on demonstration that other deterministic models of computation are representable in ‹ob› and applications of obap.ap(p,x). Confirmation of these claims is developed separately. Here we formalize obap.ap(p,x) and obap.eval(exp) in the theory Ot. 1. Preliminaries 2. Additional Notions 3. The Apply Function 4. The Evaluation Functions 5. Notes and References 1. PRELIMINARIES First, the structure ‹ob› is employed in its entirety, as defined at . The CFob notation for expession of ob canonical forms is employed (cf. ). Viz., a. The right-associative infix pair operator, ::, is introduced, with x :: y = ob.c(x,y) t :: u :: v:: ... :: y :: z = t :: (u :: (v :: ... :: (y :: z) ... ) ) n. The prefix form ‵ x is equivalent to ob.e(x). E.g., ‵(ob.NIL :: ‵ ‵ob.NIL :: ‵ob.NIL) = ob.e(ob.c( ob.NIL, ob.c( ob.e(ob.e(ob.NIL)), ob.e(ob.NIL) ) )) with the (optional) indentation as a visual aid to recognition of pairings. In addition, function and predicate representations introduced here without prefix "obap." are to be taken as private "helpers" in the representation of obap.ap(p,x) and obap.eval(e); they are not presumed to be available separately and do not dictate the form (or means) of valid computational interpretation. Obap2. Primitive Individuals Nine named individuals are distinguished as primitives, including ob.NIL: is-primitive(x) ⇒ ob.is-individual(x) is-primitive(ob.NIL) is-primitive(obap.A) is-primitive(obap.B) is-primitive(obap.E) 4 obs that signify application of elementary functions in scripts is-primitive(obap.SELF) is-primitive(obap.ARG) 2 obs that signify references to script-evaluation operands is-primitive(obap.EV) 1 ob that signifies a special unary operator in scripts is-primitive(obap.C) is-primitive(obap.D) 2 obs that signify special binary operators in scripts The last five constitute special forms in the evaluation of obs as expressions of scripts. For simplicity of expression, the CFob notation for primitive individuals uses the name with only the prefix ".". For example, .NIL, .A, and .SELF. 2. ADDITIONAL NOTIONS Obap3. Literal Individuals The supply of lindies (Ob8) is augmented as follows obap.is-lindy(x) ⇔ (x = Ʃ's' ∨ x = Ʃ'?s'∨ x = Ʃ'?.s') where s is a finite-length character string consisting of one or more alphanumeric characters The additional forms with prefixed '?' and '?.' are here independent of those without such prefixes. They are also distinguished from other lindies in the same manner as the undecorated lindies. Their utilitarian presence is related to questionable occurrences of binding names and undefined primitives in oFrugal processing. See the treatment of binding names in . As a pragmatic matter, the prefix forms should not be used intentionally. They need not survive input to oFrugal and may be treated as erroneous. Here, we introduce a way in which lindies have an useful limitation of applicative interpretation. obap.is-lindy(x) => is-pure-lindy-trace(x) (a) is-pure-lindy-trace(x :: y) (b) ⇔ is-pure-lindy-trace(x) ∧ is-pure-lindy-trace(y) ¬ is-pure-lindy-trace(ob.e(x)) (c) is-pure-lindy-trace(x :: .ob.NIL) (d) ⇔ is-pure-lindy-trace(x) Apply of a lindy to operands in scripts cannot proceed further; there is no intrinsic applicative interpretation. Instead, it is convenient to have (perhaps-intended) apply yield a trace form, an evaluation that is not taken farther (Obap4(c)). Preservation of pure-lindy traces is a pragmatic arrangement of no particular theoretical importance. Pure-lindy traces can be helpful in identifying defects and also in preserving intentional symbolic forms as themselves. They also provide a semblance of expressive strings in the absence of any other type of entity in ‹ob›. The claim: Apart from Obap3(d), excessive creation of enclosures is simply avoided compared with is-pure-lindy-trace being replaced by obap.is-lindy in Obap4(c). With is-pure-lindy-trace, there is tidier preservation of applicative structure, despite there being no applicative interpretation beyond the form itself. Note that pure-lindy forms are still parsed and subject to being marched through Obap6(d) and Obap6(i). 3. THE APPLY FUNCTION Obap4. obap.ap(p,x) obap.ap(ob.e(k),x) = k obap.ap(ob.NIL, x) = x obap.ap(obap.A, x) = ob.a(x) obap.ap(obap.B, x) = ob.b(x) obap.ap(obap.C, x) = obap.C :: ob.e(x) :: obap.ARG (a) obap.ap(obap.D, x) = obap.D :: ob.e(x) :: obap.ARG obap.ap(obap.E, x) = ob.e(x) obap.ap(obap.SELF, x) = ob.e(obap.SELF) :: ob.e(x) (b) obap.ap(obap.ARG, x) = ob.e(obap.ARG) :: ob.e(x) obap.ap(obap.EV, x) = ob.e(obap.EV) :: ob.e(x) three non-lindy trace cases for the absence of sensible interpretation for these primitives as operators apart from their syntactic function in ev(p, x, e) below (Obap6). is-pure-lindy-trace(p) ∧ is-pure-lindy-trace(x) (c) ⇒ obap.ap(p,x) = p :: x is-pure-lindy-trace(p) ∧ ¬ is-pure-lindy-trace(x) ⇒ obap.ap(p,x) = p :: ob.e(x) Pure lindy forms are resolved to trace forms in this manner to be more informative on inspection when an occurrence is unintended. There is also an intended usage of pure lindy traces as a form of text expression. ¬ is-pure-lindy-trace(p) (d) => ob.is-pair(p) ⇒ obap.ap(p,x) = ev(p,x,p) In (b, above) the obap.ap evaluations for obap.C and obap.D determine partial applications, effectively curried use of functions ob.c and obap.d, consistent with the special-form treatment of obap.C and obap.D in Obap6(e-f) below. When p is a pair that is not a pure lindy trace, in satisfaction of (d, above) obap.ap(p,x) is tantamount to an expression in which obap.SELF signifies p and obap.ARG signifies x per (Obap6(c)). 4. THE EVALUATION FUNCTIONS Obap5. obap.eval(e) obap.eval(e) = ev(obap.SELF, obap.ARG, e) effectively forcing an Obap4(b) trace in the event of top-level occurrences of obap.SELF and obap.ARG in operand e. Obap6. ev(p,x,e) evaluation of script e as part of determining the application of procedure script ob p to operand ob x. This internal function is mutually-recursive with obap.ap. ev(p,x,ob.e(y)) = y (a) is-evref(obap.SELF) (b) is-evref(obap.ARG) ev(p,x,obap.SELF) = p (c) ev(p,x,obap.ARG) = x ob.is-individual(e) ∧ ¬ is-evref(e) ⇒ ev(p,x,e) = e (d) is-evbinop(obap.C) is-evbinop(obap.D) ev(p,x,obap.C::e1::e2) (e) = ob.c(ev(p,x,e1), ev(p,x,e2)) ev(p,x,obap.D::e1::e2) (f) = d(ev(p,x,e1), ev(p,x,e2)) x = y ⇒ d(x,y) = obap.A x ≠ y ⇒ d(x,y) = obap.B function d(x,y) being exclusive to ev here and providing for selection of alternatives based on application of the comparison result. This is the basis for conditional processing of deterministic computational-interpretation cases. See 4.2 The Uβ Conditional Selectors in . is-evbinop(e1) ∧ ob.is-singleton(e2) (g) ⇒ ev(p,x,e1::e2) = obap.ap(e1, ev(p,x,e2)) introducing continuation via Obap4(a) when binop forms (e-f) are not fully satisfied is-evunop(obap.EV) ev(p,x,obap.EV :: e2) = ev(p,x, ev(p,x,e2)) (h) is-specialop(p) ⇔ is-evunop(p) ∨ is-evbinop(p) ¬ is-specialop(e1) (i) ⇒ ev(p,x,e1::e2) = obap.ap(ev(p,x,e1), ev(p,x,e2)) the normal evaluation of a pair is application of the evaluation of the a-part to the evaluation of the b-part, provided that the a-part is not a specialop 5. NOTES AND REFERENCES [XML10] W3C. Extensible Markup Language (XML) 1.0 (Fifth Edition). W3C Recommendation 26 November 2008. Available on the Internet at . *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* Copyright 2017-2023 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› Universal Applicative Functions. Miser Theory Conception text file obaptheory.txt version 1.2.3 dated 2023-12-18, available on the Internet as a version of *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* TODO * Ensure there's a tombstone on the miser/oMiser folder. * Ensure that attributions have the refactored locations. * Be very clear about the inspiration of this in McCarthy's LISP approach. * Items related to the ob-exp concrete syntax should be resolved there, and under oFrugal. Link to the detailed cases. * In the reference notation and UTF8 files, the ‵ (REVERSED PRIME) is the official glyph for the ob.e unary operator. As an accomodation for texts that rely on the Basic Latin character codes, the ` (GRAVE ACCENT) is an acceptable substitution, including when fonts lack the ‵ glyph. The ob-exp.txt grammar must account for this. * The three obap.ap(p,x) (pure)-lindy cases on p must be reverified with the current test suite and with a streamlined mockup. Create an issue and track that accomplishment. It is important that the combinators.txt verification be preserved. * Add Notes and References section to connect this with related project materials and also the origins of the ideas reflected here, especially Robinson, McCarthy, Strachey, Burge, and Landin. (Scott comes in later.) Consideration of strings having strings as individual beads, as employed in ALGOL 60, and actually implemented that way strikes me as a contribution of Douglas T. Ross. It is easier with list structures and ob.e(x). * Say more about obap.A and obap.B in the context of boole.txt and contrast with treatment of ‹bp› and of combinators.txt with regard to Scott's formulation. * The determination of trace forms is the oMiser approach to handling of undefined situations. There is no exception mechanism at the oMiser level and it is common for an operation to simply return an unmodified object as a trace instead of any further result evaluation. A consequence is that there is use as a hack for symbolic execution and for interpretation of pure lindy traces as text structures that can be treated as strings. * It is desirable for output containing pure trace forms be presentable in applicative rather than pairing ('::') form. This should be either an option or simply the way of doing this sort of thing. Then presenting list [x,y, ...] forms also needs to be considered. Oh my. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1.2.3 2023-12-18T18:46Z Cleanup URLs and smooth some connections 1.2.2 2023-11-10T05:24Z Adjusted to the chosen refactoring location. 1.2.1 2023-11-10T05:14Z Tombstone with refactoring continued from . 1.2.0 2023-08-25T00:05Z Proofread and aligned with obtheory.txt 0.2.0 2023-08-24T21:51Z Major rework around pure-lindy forms 0.1.3 2023-07-13T19:41Z Tidy up around pure lindy trace forms to enable output variation and interpretation as text structures. 0.1.2 2022-08-11T20:27Z Touch-ups and review of pure-lindy case 0.1.1 2022-08-01T20:49Z Refer now to oFrugal/ob-exp.txt 0.1.0 2022-01-04T01:10Z Introduce the conditional lindies to satisfy the context-free completeness of oFrugal pragmatic interpretations. 0.0.34 2020-05-12-17:17:22 Reidentify and Reflow cases to provide for fine- grained citation in proofs/derivations. Annotation cases further. 0.0.33 2019-02-24-13:42 Touch ups with the obap.ap(p,x) pure-lindy cases completed. Re-organize a little and make all private function and predicate definitions have no prefix (neither obap. nor ob.). 0.0.32 2019-02-14-09:55 Manage TODOs, complete Lindy cases, touch up text, and note that the revised formulation's verification is required. 0.0.31 2019-02-13-15:50 Touch ups and Manage TODOs 0.0.30 2018-10-24-16:30 Say "canonical form" instead of "canonical ob" 0.0.29 2018-10-16-15:23 Adjust the Ʃ-expression of Lindies to use '. Improve the layout and proof-read one more time. 0.0.28 2018-03-20-10:05 Move TODOs on historical and background matters to the new miser/background.txt document for further development. 0.0.27 2018-03-14-09:43 Correct obap.is-specialop(p) predicate, use Ʃ= as less ambiguous for string identity, and some touch-ups. 0.0.26 2018-03-12-14:46 Clean up some typography and review TODOs 0.0.25 2018-01-10-11:58 Correct obap.ap conditions on pure-lindy-trace case for obap.ap(p1::p2, x), with hat-tip to Roman Susi. 0.0.24 2018-01-09-21:30 Simplify the trace use of lindies to fixed-point on cases where is-pure-lindy-trace(ob) applies. 0.0.23 2018-01-03-09:46 Introduce obap.is-specialop(p) to isolate the special cases of p::e2 from the default e1::e2 treatment as application. Based on observation by Roman Susi in ordmid/miser GitHub #4. 0.0.22 2018-01-03-09:26 Manage TODOs, make some touch-ups in the narrative related to recursion. Use reverse-prime, ‵ U+2025, consistently where it is introduced. 0.0.21 2017-12-27-11:37 Clarify universality a bit more in the synopsis. Clean-up some text and also Review/Expand TODOs. 0.0.20 2017-11-12-10:15 Manage TODOs. Change to ‵ (reverse prime) in the prefix equivalent of e(x). 0.0.19 2017-11-02-12:52 Manage TODOs. Introduce ‵x prefix for e(x). 0.0.18 2017-10-12-11:39 Rename obap.is-every-free-lindy to obap.is-pure-lindy for cases when a script is a non-reducible trace. Define the negative case. Improve the description of trace production. 0.0.17 2017-10-09-12:00 Simplify the obap.ap(p,x) lindy trace case, continuing application if the operand, x, is not everywhere lindy. 0.0.16 2017-10-09-09:24 Remove extraneous "(" in obap.is-every-free-lindy(p) 0.0.15 2017-10-05-09:53 Change obap.apint(obap.EV,x) to be treated the same as other non-binary eval special forms in producing traces. 0.0.14 2017-10-04-09:44 Adjust TODs, Take the woowoo out of lindies. Make lindy apps the same for lindy apint and is-every-free-lindy(p) cases. 0.0.13 2017-09-29-08:29 Adjust the synopsis, correcting the text and making it a bit more informally readable. 0.0.12 2017-09-28-15:37 Add obap.EV, its applicative interpretation and its special form in obap.ev. 0.0.11 2017-09-28-14:48 Adjust TODOs. Remove ob.PROC and ob.DEF for treat- ment of extension mechanisms. Simplify the introduction of notions about universality based on discussion with Paul McJones. Recover the change from is-lindy-every-free to is-every-free-lindy that got lost somewhere. 0.0.10 2017-09-25-19:59 Restate Obap8 to have the definitons of obap.proc(p), obab.def(x), and the applicative interpretations of obap.PROC and obap.DEF to parallel the approach for other parts of obaptheory. 0.0.9 2017-09-25-16:57 Adjust TODOs, introduce ob.PROC and ob.DEF 0.0.8 2017-09-20-10:09 Reflect the application of lindies in a manner that supports symbolic traces of evaluations, based on the lack of any distinct interpretations of lindies as anything else. 0.0.7 2017-09-19-19:45 Add is-lindy-every-free(x) and is-lindy-everywhere(x). Recast the statement of universal computation in terms of effective- universality of the functions obap.ap(p,x) and obap.eval(exp). 0.0.6 2017-09-16-10:22 More TODOs and some touch-ups. Consistently use obap.* for notions expressed in obaptheory beyond the primitive ob.* ones that remain applicable to all of Ob. 0.0.5 2017-09-12-15:05 Remove Treatment of individuals not in evidence. There is no reason for this in obaptheory. Simplify lindies to be just symbols that represent themselves and have no theoretical significance beyond applicative evaluation as traces. 0.0.4 2017-09-12-12:56 Restore obap.SELF and obap.ARG to primitives and correct their tracing cases. Rework explanatory material. Add TODOs including historical notes for now. 0.0.3 2017-09-11-19:55 Remembered to add definition for ob.d(x,y) 0.0.2 2017-09-11-19:20 Proof-reading corrections, text touch-ups 0.0.1 2017-09-11-19.04 Create the initial draft. *** end of obaptheory.txt ***