combinators.txt 0.1.7 UTF-8 2024-01-15 *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* The Miser Project ================= INTERPRETATION OF COMBINATORS IN ‹obap› --------------------------------------- Combinators are important theoretical objects related to the lambda (λ) calculus. There are ‹ob› computational interpretations of combinators from which a complete computational representation is assured. The development here is sufficient for that; the approach also serves as a demonstration that can be adapted in other representations. Achievement of a combinator-system interpretation in oMiser is important demonstration that oMiser provides a universal computational mechanism at the same strength as other approaches (including λ-calculus) accepted as having that power. Practical benefit of oMiser computational representation of combinators, beyond the theoretical generality, is exploiting that the oMiser interpretations are interpretation-preserving of functional type with respect to the operation of application interpreted as obap.ap. This affords representations of hierarchies of composed functions and levels of abstraction under the ‹ob› model of computation. Development of oMiser combinator representations proceeds from the theory of combinators as a structure of the kind employed in Miser Project. That is carried through to demonstration of interpretation-preserving utility in oMiser scripts. CONTENT 1. MATHEMATICAL STRUCTURE An abstract theory in the manner of obtheory that is at a powerful though not-so-grounded level of abstraction 1.1 Theory of Combinator Arithmetic, ‹ca› 1.2 Useful Simple Combinators 1.3 What Combinator Is It? 1.4 The Power of Combinators 2. FUNCTIONAL TYPE AND INTERPRETATION PRESERVATION The important quality that, embodied in concrete representations of combinators, extends to intended interpretations of oMiser scripts as functions on many types of computational entity 2.1 Functional Type 2.2 Interpretation Preservation by Functional Type 2.3 The Avenue to Concrete Interpretations 2.4 Restricted Interpretation as Types 3. The oMISER UTILITY COMBINATOR IDIOMS Demonstration of scripts that are equivalent to combinators under a straightforward interpretation 3.1 Combinator Representation Constraints 3.2 Representing K, I, and S 3.3 Derived Utility Combinators B, C, D, T, and W 4. EXOTIC COMBINATORS: CONDITIONAL AND RECURSIVE OPERATION Achievement of recursive operation and conditional evaluation in terms of combinators 4.1 Conditional Behavior 4.2 The Uβ Conditional Selectors 4.3 Truth Indifference 4.4 Y Combinator Interpretation 5. FROM THEORY TO PRACTICE Bootstrapping from ‹ca› interpretation as a lever for the applicative generality of ‹ob› and obaptheory realized in the operational computation model of oMiser. 6. REFERENCES AND RESOURCES Sources of further details and theoretical work behind the kind of functional programming that oMiser affords 1. MATHEMATICAL STRUCTURE 1.1 Theory of Combinator Arithmetic, ‹ca› The account of [Rosenbloom1950] is adapted here. C0. For combinators x and y, | x y is the combinator formed by application of (operator) x to (operand) y. C1. For combinator x, x ≈ x. C2. For combinators x and y, x ≈ y ⇒ y ≈ x. C3. For combinators x, y, and z, x ≈ y ∧ y ≈ z ⇒ x ≈ x. C4. For combinators x, y, a, and b, x ≈ y ∧ a ≈ b ⇒ | x a ≈ | y b. C5. S and K are combinators. C6. For combinators x, y, and z, ||| S x y z ≈ || x z | y z. C7. For combinators x and y, || K x y ≈ x. CE. For combinators x and y, if | x a ≈ | y a for all combinators, a, then x ≈ y. The logical notation is that used in obtheory.txt, . The structure, ‹ca› = 〈CA,{apply},CAt〉has the single function, apply, designated by operator "|" and CAt is FOL without "=". This is not about ‹ob›. The combinators are not obs. Likewise, the application, | f x, is an application of combinators that yields combinators. It must not be confused with the obap.ap of obaptheory, , where application is of the procedure encoded in one ob, as operator, to the other as operand. The notation with "|" for application is an useful reminder that this is an expression in the ‹ca› style of applicative expression. It is convenient to omit leading "|" since those "|" can be supplied automatically: the total number of "|" must be one less than the number of terms in the expression. Write S x y z for ||| S x y z K x y for || K x y x z | y z for || x z | y z In text and some other places, at least one "|" is often retained to signal that the expression is in ‹ca›'s CAt rather than in ‹ob›'s Ot. The symbol "≈" is for equivalence of combinators. This is distinct from the "=" equality relationship among obs. Although "≈" is tantamount to an equality in ‹ca›, that inference is avoided here. It is unclear that there are distinguishable, unique mathematical entities for combinators. Skirt the question by using "≈", since, like functions, combinators have no canonical forms of expression. ‹ca› lacks definiteness and identifiability as tacitly assumed in Miser Project reliance on FOL= for ‹ob›. 1.2 Useful Simple Combinators It is known for ‹ca› that all combinators can be expressed in terms of combinators S and K alone (with certain reservations concerning concrete interpretations that will be addressed in further sections, especially 4.2). Some derived combinators are so handy that there are constant names for them. There are also equivalent λ-expressions, shown below. S x y z ≈ x z | y z S ≈ λx.λy.λz.( (x z)(y z) ) K x y ≈ x K ≈ λx.λy.x I x ≈ x I ≈ S K K ≈ λx.x B f g x ≈ f | g x B ≈ S | K S K ≈ λf.λg.λx.( f(g x) ) C f x g ≈ f | g x C ≈ S | D S | K K ≈ λf.λx.λg.( f(g x) ) D f x g y ≈ f x | g y D ≈ B B ≈ λf.λx.λg.λy.( (f x)(g y) ) T x f ≈ f x T ≈ C I ≈ λx.λf.( f x ) W f x ≈ f x x W ≈ S S | S K ≈ λf.λx.( (f x) x ) In these λ-expressions there are no combinator "constants" (i.e, S, K, and others) and variables in those expressions are ones for which there is an outer (preceding) λ term. This closed form of λ-expression is inter- changeable with the notation for combinators of (1.1), as demonstrated with the equivalences above. The translation is straight-forward. Precise rules for using λ-expression forms and reasoning about them are complicated by the use of variables. For a typical explanation, see [Révész1988: 2.1]. Detailed descriptions are found on the Internet, e.g., , with more on ‹ca› at . A comprehensive treatment is in [Barendregt1981]. Equivalent λ-expressions make the applicative structure more apparent, easier to express, and suggestive of intermediate forms. That utility will be exploited later by introduction of a computationally-derived λ-abstraction operation implemented with an oMiser script. Here, in Miser Project usage, parentheses are retained in (closed) λ-expressions as shown above to avoid any ambiguity in application order between typical λ-calculus notations having left-to-right association of application operation and the unparenthesized right-to-left association of Frugalese. See for the oFrugal notation, its computational-interpretation semantics, and the grammar of such expressions employed beginning in section 2.3, below. 1.3 What Combinator Is It? Formally, all there is to do is manipulate formulas of combinators in ways that demonstrate two forms are equivalent. To assess the nature of some combinator in achieving a particular applicative arrangement, a simple approach consists of the following: * Given some combinator expression having only constants (such as B, K, and S) write the expression applied to a succession of variables, a, b, c, ... . Expand the expression wherever application of a combinator constant can be replaced by its equivalent defined form. Stop application to variables once expansion leaves no combinator-constant symbols or when that is clearly not achievable. * An expansion can also go no further when not all of the arguments of a defined combinator are available, including when a variable of unknown definition is shown as the operator of an application. For example, given | S K, expand via S K a b = K b | a b ≈ b. In the case of | S K a b, notice that | S K a b ≈ b ≈ I b, and so by (CE) | S K a ≈ I for any combinator, a, including K. Consider B I a b ≈ I | a b ≈ a b. Then B I a ≈ a ≈ I a by (CE), and B I ≈ I by (CE) as well. There is more difficulty determining what combinator | W W W might be. Substituting in | W a b ≈ | a b b simply yields | W W W and there is no progress to be made. Additional exotic cases of practical importance are addressed in Section 4, below. 1.4 The Power of Combinators Even in ‹ca›, where the only mathematical entities are the combinators, whether expressed in a pure combinatory manner or with closed λ-expressions, it is possible to represent all manner of data and operations on such entities. Such representations are found in [Burge1975], [Révész1988: Chapters 3-4], and [Paulson1996]. [Scott2012], focusing on the λ-calculus view, sketches a variety of constructions and connections in mathematical logic and other theoretical mathematical approaches. Some of these will be investigated later when oMiser representations of such schemes are assessed. Fundamentally, the combinators and equivalent closed λ-expressions are all about ways of composing functions from other ones. Although this can be employed indefinitely presuming combinators as the only entities, the capabilities of ‹ca› are also of practical use in composing other types of functions, so long as those functions are compatible with the combinators applied to them. This power is exploited in the computational representation of combinators via oMiser script obs in Section 3. The bridge is via functional type and interpretation-preserving use of combinators and combinator-like entities. 2. FUNCTIONAL TYPE AND INTERPRETATION PRESERVATION Despite ‹ca› having application as the only operation and combinators as the only entities, there is another level of abstraction immediately available as a potential interpretation of ‹ca› in other structures: that of functional types having a (counterpart) application operator. 2.1 Functional Type The usual notation for functional type is used here, as in [Burge1975:1.2, Feferman1977:2.1, Scott1993:1]. Greek letters signify arbitrary types. x: α f: α → β express that x is an entity of type α and f is a function that when applied to an operand of type α determines a result of type β. The type of f is (α → β). Types can be composed further by substitutions in that pattern. Here "type" is an emergent notion that is observable about combinators; the notion of type is not incorporated in ‹ca› as such. From inspection of the definitions (1.2) functional type is inferred in this emergent sense for well-known combinators. K x y ≈ x y: α x: β K: β → (α → β) S x y z = x z | y z z: α y: α → β x: α → (β → γ) S: (α → (β → γ)) → (α → β) → (α → γ) I x ≈ x x: α I: α → α B f g x ≈ f | g x x: α g: α → β f: β → γ B: (β → γ) → (α → β) → (α → γ) C f x g ≈ f | g x x: α g: α → β f: β → γ C: (β → γ) → α → (α → β) → γ D f x g y ≈ f x | g y y: α g: α → β x: γ f: γ → (β → δ) D: (γ → (β → δ)) → γ → (α → β) → (α → δ) T x f ≈ f x x: α f: α → β T: α → (α → β) → β W f x ≈ f x x x: α f: α → (α → β) W: (α → (α → β)) -> (α → β) 2.2 Interpretation Preservation via Functional Type Functional types with respect to ‹ca› reveal the extent to which a combinator representation can be indifferent to functional interpretation of entities involving various types under the same system of application where the combinators are also representable. The trivial case is when all of the type variables are replaced by the same specific type, whether CA or Ob (construed as base types). Combinators taken as interpretation-preserving of functional types, as here, are said to be polymorphic with regard to the accomodation of fixed types of operands and operators that preserve the functional-type pattern. 2.3 The Avenue to Concrete Interpretations The oMiser interpretation of ‹ca› combinators, in a manner that preserves functional type, is as follows. * The interpretation of | x y is as obap.ap(cx, cy) where cx and cy are oMIser representations of combinators x and y, respectively. * For successful interpretation of ‹ca› in ‹ob› it is not required that every ob be such a representation, but that the deductions in ‹ca› hold for those Obs that are and that all (computable) ‹ca› cases are accounted for. Having a script, ^cK repressenting combinator K, it must be the case that, in oFrugalese notation, (^cK x) y = x so if x represents a combinator, that interpretation is preserved just as it is for x interpretable as representing an entity of any particular type. In this manner, ^cK representation of combinator K is satisfied and functional type is also honored. The ^-notation as part of a constant name is oFrugalese for a binding to a constant ob. The names in the forms such as ^cK are adopted to signify (particular) oMiser representations of the corresponding combinator. See . Likewise, supposing there is a script, ^cS, such that, in oFrugalese, ((^cS x) y) z = (x z) (y z), ^cS: (α → (β → γ)) → (α → β) → (α → γ) suffices when x, y, and z have interpretation as combinators or as other types of entities consistent with the functional type of combinator S. It is sufficient for ^cS operation to preserve the interpretations of x, y, and z and that those operand interpretations satisfy their role in the functional-type pattern (α → (β → γ)) → (α → β) → (α → γ). Here there are Ot "=" and definite computational results, yet preserving interpretation with regard to functional type. This pervasive condition is designated quasi-combinatory. IMPORTANT: Interpretation-preservation flexibility as described here relies on the use of obap.ap as the counterpart of functional application in the system for which an interpretation is being claimed. More-indirect approaches can be operationally successful. That is not presumed here. 2.4 Restricted Interpretation as Types In ‹ca› there are only combinators and the application operation; in ‹ob› there are only obs, some primitive functions, and other functions on obs including applicative operations obap.ap and obap.eval. Within those respective theoretical structures, as given for oMiser, the notion of different functional types and different individual types is a higher level of abstraction based on achievement of interpretations that do not extent to all obs as operators and operands with respect to application. Not every ob represents a combinator even though every ob has an applicative interpretation. In the context of digital computation, the orchestration of available types in representation of other (higher-order) types is characteristic of computer software programming. There are practices which are employed to engineer such layering of abstractions in dependable ways. A. Preserved interpretations. Restraints are applied in the design, combination, and operation of scripts such that particular representa- tions are confirmed to be representative of particular types. For example, the representation of combinators by obs that are used in accordance with the related functional types. The demonstration that the abstraction is preserved is usually established externally and with computational tests that confirm satisfaction and preservation of particular-type semblance. There will often be edge cases beyond which the interpretation fails, and the implementation must reflect adequate wariness. B. Distinguished interpretations. Having a computational means to discriminate entities that definitely satisfy a particular representation from those that are not so distinguished. This can be used by procedures to verify that their operands satisfy an intended representation by the procedure authors. Wariness around guarding the intended interpretation is accomplished by defensive measures in the implementations themselves. C. Designated interpretations. Providing some sort of decoration on entities that names or annotates the representations themselves. This provides a strict labelling of a type representation for an entity, a kind of armor signally an intended representation. It is important to distinguish that a particular representation of a type is involved, distinct from other representations of the same type. Typically, there are many ways to represent entities of some type, and it then becomes interesting to deal with (1) the different interpretations that a single computational entity might satisfy and (2) inter-operation with different representations of the same type. By virtue of (2) it will be appropriate to identify a representation with the type and the specific interpretation that the computational representation satisfies in the case (C). The oMiser idioms for combinators (the particular ^cS, etc.) are used in Miser Project investigation of such levels of computational abstraction. 3. oMISER UTILITY COMBINATOR IDIOMS 3.1 Combinator Representation Constraints The complete conditions on the concrete representation of combinators via obs are * The application obap.ap(cf,cx) of ‹ob› is interpreted as the application | f x of ‹ca›, where cf, cx are interpreted as combinators f, x respectively * The application of an ob representative of a combinator exhibuts the same polymorphic functional type as the represented combinator. * The application of an ob interpretation of a combinator determines a definite result in accordance with the combinator's definition. o Here, the determination is of ‹ob› equality, "=" with regard to the derivation and its result. o There is no counterpart of ‹ca› equivalence, "≈" in ‹ob›. When "≈" is asserted with respect to obs, it is relative to the ‹ca› interpretations offered here. o The relational "f ≅ g" is used to signify that obs f and g, interpreted as operator scripts, are either identical or have the same effect when taken to represent functions in ‹ob› of the same functional type. * The computational interpretation in ‹ob› is imperative and eager. Application operations are carried out once the operator and the operand are each computationally determined (as canonical obs), not before and not later. Any result is by deterministic procedure. (In practice, there are variations/optimizations indistinguishable from strict adherence to this condition.) 3.2 Representing K, I, and S Three simple combinator representations are derived completely to illustrate ‹ob› interpretation in ‹ob› (cf. 2.3), keeping in mind that these are cases calling for preserved functional type (2.4(A)). 3.2.1 Representing K ^cK = obap.E ^cK ≈ K For | K x y ≈ x, obap.ap(obap.ap(obap.E, a), b) = a. Also, obap.eval((obap.E :: ` a) :: ` b) = a for any obs a, b, including representations of combinators. In oFrugalese, (.E x) y = x This is very direct because obap.ap(obap.E,x) = ob.e(x), obap.ap(ob.e(x),y) = x, and obap.eval(obap.E) = obap.E, by definition. Although it seems rather wasteful and even risky to evaluate y for no apparent purpose (since the attempted evaluation might fail to yield a result), it happens that there are valuable idioms where y is fixed (e.g., `z) and is so-encapsulated within a script as a payload for some idiomatic purpose. We will see that this provides a mechanism for communicating state and conducting transformations on states. IMPORTANT. It is part of the strict semantics for oMiser that an application (^cK x) y cannot be simplified unless it is assured that evaluation of y has a definite computational result whenever evaluation of x does. Cf. section 3.1. 3.2.2 Representing | I x ≈ x ^cI = ob.NIL ^cI ≈ I For | I x ≈ x, obap.ap(ob.NIL, a) = a. Also, obap.eval(ob.NIL :: ` a) = a In oFrugalese, .NIL x = x This is also very direct because obap.ap(ob.NIL,x) = x, and obap.eval(ob.NIL) = ob.NIL, also all by definition. 3.2.3 Representing | S x y z ≈ x z | y z ^cS ≈ S where ^cS = .C :: `.C :: .C :: (.E :: .C :: (.E :: .ARG) :: `.ARG) :: `(.C :: (.E :: .ARG) :: `.ARG), obap.ap(^cS, x) = .C :: `( `x :: .ARG) :: .C :: (.E :: .ARG) :: `.ARG), obap.ap(obap.ap(^cS, x), y) = (`x :: .ARG) :: `y :: .ARG), obap.ap(obap.ap(obap.ap(^cS, x), y), z) = obap.ap( obap.ap(x, z), obap.ap(y, z) ), and in oFrugalese, ^cS(x, y) z = x(z) y z. 3.3 Derived Utility Combinators B, C, D, T, and W For the additional useful combinators (1.2), particular operator-script ob representations are taken as idioms for them. The derivations have been confirmed using the SML/NJ mockup at . These tend to be more compact than equivalent combinator representations obtained by application of ^cS, ^cK, and other combinator idioms alone. Automation of such streamlining and further optimizations are topics for treatment elsewhere. 3.3.1 Representing | B f g x ≈ f | g x ^cB ≈ B where ^cB = .C :: `.C :: .C :: ( .E :: .E :: .ARG ) :: `( .C :: ( .E :: .ARG ) :: `.ARG ) 3.3.2 Representing | C f x g = f | g x ^cC ≈ C where ^cC = .C :: `.C :: .C :: ( .E :: .E :: .ARG ) :: `( .C :: `.ARG :: .E :: .ARG ) 3.3.3 Representing | D f x g y = f x | g y ^cD ≈ D where ^cD = obap.ap(^cB, ^cB) = .C :: ``^cB :: .C :: (.E :: .ARG) :: `.ARG = .C :: ``( .C :: `.C :: .C :: ( .E :: .E :: .ARG ) :: `( .C :: ( .E :: .ARG ) :: `.ARG ) ) :: .C :: ( .E :: .ARG ) :: `.ARG 3.3.4 Representing | T x f ≈ f x ^cT ≈ T where ^cT = .C :: `.ARG :: .E :: .ARG 3.3.5 Representing | W f x ≈ f x x ^cW ≈ W where ^cW = .C :: ( .C :: ( .E :: .ARG ) :: `.ARG ) :: `.ARG 4. EXOTIC COMBINATORS: CONDITIONAL AND RECURSIVE OPERATION 4.1 Conditional Behavior In the use of mathematical theories, such as Ot, to represent computable functions, there are two important provisions that have not been seen, so far, in ‹ca›. * Definition by cases. There are distinguished cases in the characterization of obs in ‹ob›. There are even more cases established in the characterization of the application function, obap.ap(p,x). Imperative computation based on distinguished cases is important, with deterministic selection of only satisfied cases leading to a determined computational yield. * Recursion. A companion to separation of cases is the conditional use of the function being characterized in an expression that applies in a specified case. Computational interpretation is by conditional reuse of the procedure in a manner that reduces the computation to a (simpler) use of the same procedure. There is recursion in the definition of obap.ap(p,x) and implicitly in transitive relations of ‹ob› and in structural inductions. Both occur in the use of Ot to characterize computable functions, including the claimed universal function, obap.ap. 4.2 The Uβ Conditional Selectors The quasi-combinator Uβ is fixed on a definite type, β, having exactly two values, such that for Uβ: β → (α → (α → α) ), | Uβ c x y is equivalent to either x or y depending on which of two definite cases is satisfied by the operand, c | Uβ c ≈ K, when c is of the first case, and then | K x y ≈ x ≈ K I, when c is of the second case, and then | K I x y ≈ y Requiring that operands x and y be of the same functional type, α, is consistent with the notion that they each satisfy the same interpretation/representation context in the intended place of use. In order for the two cases of type β to provide definite selection of one of x or y, it is not proposed that type β consist of combinators. For computational interpretation, c must be determined and its elements precisely distinguished by computational means. That's lacking in ‹ca›. With oMiser, an appealing choice for β is a type consisting of the two primitive individuals obap.A and obap.B. Concrete type obAB is defined accordingly. obap.A: obAB, obap.B: obAB with restriction of ob values to obAB accomplished at least by interpretation-preserving limitation on the use of UobAB (section 2.4(A)). obAB is a base type, one that is not functional in nature but which may be a type within an "→" functional-type form. Now UobAB can be specified. UobAB: obAB → (α → (α → α) ) | UobAB obap.A ≈ K | UobAB obap.B ≈ K I with representation ^cUobAB ≈ UobAB ≅ .ARG :: `(^cK :: ^cK ^cI) ≅ .ARG :: `(.E :: `.NIL) depending on the expression provided for c being such that any result will always be one of obap.A or obap.B such that ^UobAB(c) is definite. The type naming "obAB" is a mnenomic aid to the selection of x versus selection of y in | UobAB c x y. For any Uβ, the corresponding type obAB value is achieved by formulation | Uβ c obap.A obap.B where c is of functional type β. Finally, restriction to obAB can always be ensured within the capabilities of the ‹ob› obap.ap function by some filter on any ob, such as is-A: Ob → obAB is-A(x) = obap.A when x = obap.A = obap.B otherwise with ^is-A ≅ obap.D :: obap.A :: obap.ARG ≅ (obap.D :: obap.A) then using ^cUobAx = ^cB(^cUobAB,^is-A) to represent a kind of UobAx conditional, trading on the fact that obap.ap(obap.ap(obap.D, x), y) = obap.A when x = y = obap.B otherwise accounting for the appeal of UobAB. Many arrangements of this kind are at hand, with preferences among them based on intended representations. 4.3 Truth Indifference Combinator (Uβ b) is inspired by the form | ⊃ b x y of [Scott1993], also written (b → x, y), where the type of b has two distinct values, signified ⊤ and ⊥. (U⊤⊥ could designate Scott's strict type ⊤⊥, a.k.a type o from [Church1940].) There is a similar treatment to | ⊃ b x y with the form | D x y b in [Feferman1977: 2.1.2], where | D x y 0 = x and | D x y 1 = y, with distinguished individuals 0 and 1. One can also interpret a type, such as obAB, as representing truth (obap.A) and falsity (obap.B) with respect to some condition such as the result of obap.eval(.D :: x :: y). Likewise, one convention is to treat combinators K and | K I (represented by ^cK and (^cK ^cI)) as designating "true" and "false", respectively, as in [Barendregt1981:6.2.2, Revesz1998:3.1, Scott1993]. This skates over the fact that ^cK and (^cK ^cI) are definite distinct obs, a claim that can't be made for representations of K and | K I. The presumption of such a distinguished type has roots all the way back to [Church1940] and is perpetuated by [Scott1993]. With respect to computational interpretations of logical notions it is valuable to avoid claiming "truth" as any kind of (computational) object. In the case of obAB and ^cUobAB, there's handy applicative use of obap.A and obap.B as selectors of the first or second of a pair and anything else is some higher-level interpretation/representation. There will be some idiomatic oMiser computational definitions that are valuable in representing Boolean logical operations. type obAB will be employed in one representation of a structure, ‹bp›. It is not what the type obAB "is." The file boole.txt illustrates some rather different representations of Boolean Algebras, and those could be applied here as well. Cf. where the notions of truth and falsity are also finessed. Akin to the observation of the interpretation-preserving nature of combinator functional types, Uβ and type β are taken to be "truth" indifferent in the sense of truth-value interpretation-preserving, depending on how the alternatives x and y of | Uβ c x y are construed when c is so-construed. 4.4 The Y Combinator Interpretation Consider, now, an applicative expression, f, where there is a case selection in which one wants to apply f itself as part of the continuing evaluation of a determined case. Assume the typical form f ≈ λx.(... (f M) ...) f: α → β where the (f M), and other occurrences of (f ...) in the expression are conditionally-chosen based on satisfaction of particular cases. No evaluation of a particular (f M) occurs unless the governing case is satisfied. There is no form of lambda-expression or combinator-expression by which the expression of f can refer to and employ that expression as a whole. One solution is by first applying the following transformation, replacing all occurrences of f of this kind in the right-hand side to achieve fs ≈ λf.λx.(... (f M) ...), fs: (α → β) → (α → β) Clearly, fs is not f. It has the form of expression f, but there is now an operand to be supplied for use where application of operand f occurs in fs application to the next operand, x. Notice that, on the other hand, hand, fs has no references of any kind to itself. The functional type does reflect an important constraint. The next step is to suppose the existence of a combinator, Y, that will make the recursive connection, satisfying f ≈ Y fs ≈ fs(Y fs) ≈ fs(f). Y: ((α → β) → (α → β)) → (α → β) Whatever Y is, when applied to fs it provides a version where fs is applied to its first operand, the recursive version (Y fs). It is not necessary to ponder this too closely. It suffices to determine how an interpretation, ^cY, is achieved that fully satisfies this defining Y combinator characteristic in oMiser. When evaluation of any ((^cY fs) M) is carried out via oMiser obap.ap expansion obap.ap((^cY fs), eM) = obap.ev((^cY fs), eM, ^cY fs), with eM, the evaluated M as operand, and (^cY fs), the evaluated recursive form interpreted as f At this point with obap.ev, (^cY fs) is available as the value of obap.SELF and eM is available as the value of obap.ARG. What is needed to continue is (fs (^cY fs)) eM. This leads to the solution (^cY fs) ≅ (`fs :: .SELF) :: .ARG so that ^cY ≈ Y with ^cY = .C :: (.C :: (.E :: .ARG) :: `.SELF ) :: `.ARG This imperative solution for the Y combinator, and the presumption that a recursion occurs conditionally by case is an example of provisions to be made for systems, such as oMiser, where obap.ap(p,x) operands are "by value" [Paulson1996:p.391]. 5. FROM THEORY TO PRACTICE It is hereby claimed that interpretation of ‹ca› in ‹ob› with obap.ap is established. This is one demonstration that oMiser exhibits a model of computation at the level of other accepted ones. That establishes obap.ap (and the companion obap.eval) as universal computation functions. There needs to be some work on the theoretical side to contend with the particular approach to Y combinator and the dependence on distinguishable conditions for cases. These seem essential for an operational model, the objective here. The computational model behind oMiser operation is simple and provides for useful contrast among existing computation models. The operational bridge with Turing Computability, among others, is of interest. That is not the same as being expressive and utilitarian as a means of computation. It is a goal to bootstrap from well-founded theoretical foundation of the model to a level of convenient usage. That will involve progression through several stages, described further in companion materials. There is also something valuable to recognize about combinators, λ-abstraction, and functional types in the ‹ob› = 〈Ob,Of,Ot〉 structure. There is a tendency to speak of higher-order functions. Yet in the case of this structure, there is nothing "new" in Of. The computational interpretation of the universal function is still confined to the computable functions in Of, from Ob -> Ob. There are no "more" functions or types in this sense. What is accomplished is greater expressibility and convenient reuse of defined scripts that compose scripts to evoke types under given restrictions of representation. The "extension" is conservative in this sense. That's quite marvelous. Just not magical. 6. NOTES AND REFERENCES [Barendregt1981] Barendregt, Hendrik Pieter. The Lambda Calculus: Its Syntax and Semantics. North-Holland (Amsterdam: 1981). ISBN 0-444-85490-8. [Burge1975] Burge, William H. Recursive Programming Techniques. Addison-Wesley (Reading, MA: 1975). ISBN 0-201-14450-6. Although the approach starts with a functional-style, the interconnections and definability in terms of combinators and closed λ-expressions is worked up to in Chapter 1, with further refinement (and implementation matters) thereafter. [Church1940] Church, Alonzo. A Formulation of the Simple Theory of Types. J. Symbolic Logic 5, 2 (June 1940), 56-68. DOI: 10.2307/2266170 available on JSTOR . Identified as inspirational in [Scott1993] and [Paulson2018], this work identifies simple type ο (omicron) as the type of propositions and represents a logic thereby. That may now be quaint with the type taken to consist of distinguished binary cases as in the manner of our discriminator, Uβ. The notation for functional type has also been refined over the years to the form adopted here. [CL2018] Combinatory Logic, Wikipedia Article, accessed on the Internet on 2018-05-15 at . [Feferman1977] Feferman, Solomon. Theories of Finite Type Related to Mathematical Practice. Chapter D.4 in "Handbook of Mathematical Logic," Jon Barwise (ed.), North Holland (Amsterdam: 1977), ISBN 0-444-86388-5 pbk. [Paulson1996] Pauson, Lawrence C. ML for the Working Programmer, ed.2. Cambridge University Press (Cambridge: 1991, 1996). ISBN 0-521-56543-X pbk. Digging into the combinators, λ-calculus, and representation of other types as interpretations of λ-expressions occurs in Chapter 9, Writing Interpreters for the λ-Calculus, starting in section 9.5. [Paulson2018] Paulson, Lawrence C. Formalising Mathematics in Simple Type Theory. arXiv preprint arXiv:1804.07860. 2018-04-20. Available at . [Révész1988] Révész, György E. Lambda-Calculus, Combinators and Functional Programming. Cambridge University Press (Cambridge: 1988), ISBN 0-521-345589-8. The notational use of (f)(x)y for conventional f(x(y)), applicative f(x y), and combinatory | f | x y requires careful reading. Chapter 3, Combinators and Constant Symbols, provides extensive examples also relevant to computational representations. Section 2.4 provides a treatment of λ-expressions that can be adapted to the closed use in (1.2) here. [Rosenbloom1950] Rosenbloom, Paul C. The Elements of Mathematical Logic. Dover (New York: 1950). ISBN 0-486-60227-3 pbk. The notation for expressing combinators (1.1 here) and the expression of‹ca› are derived from section III.4, Combinatory Logics. [Scott1977] Scott, Dana S. Logic and Programming Languages. 1976 ACM Turing Award Lecture. Comm. ACM 20, 9 (September 1977), 634-641. PDF availabe at . The discussion on semantic structures and function space is a valuable collateral on the use of monotonicity and continuity in [Scott1993], a paper originally circulated informally in 1969. [Scott1993] Scott, Dana S. A Type-Theoretic Alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science 121, 1-2 (December 1993), 411-440. At . The type-theoretic approach treats type as definite and distinguished even though the combinators are interpretable as polymorphic in the manner proposed here for combinator representation in oMiser. [Scott2012] Scott, Dana S. λ-Calculus Then & Now. Annotated slides presented at conferences, PDF version of 2012-08-25 available on the Internet at . Presented at the ACM Turing Centenary Celebration, San Francisco, June 15-16, 2012. Video presentation at . *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* Copyright 2018-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. Representation of Combinators in the ‹ob› Model of Computation. Miser Theory Conception text file combinators.txt version 0.1.7 dated 2024-01-15, available on the Internet as a version of TODO * In Section 2, establish the associativity of "->". * In 2.3, line 236, ensure that ob-exp.txt is the correct reference on ^. * Review the bibliographic references and reconcile with bib/ * This is just too gnarly. Need to figure out a way to break it down, do progressive disclosure, *something," * Link to other materials of the Miser Project that explore some of these matters in greater detail. Connect to combdemo.sml, and also work in Ycombinator (.txt or .sml?), and comblib.sml. * The characterization of obap.ap in obaptheory.txt does not compel an eager, imperative interpretation. It affords one and the correspondence with a deterministic operational interpretation is straightforward. This distinction needs to be made clear: it is the engineering of oMiser that provides the deterministic operational representation. This needs to be affirmed elsewhere and relied upon here. * Add links to additional companion materials hinted at in Section 5. * Revamp and simplify, relying on the refinements in obtheory.txt, obaptheory.txt, boole.txt, and the "Interpretation, Representation, Computation, Manifestation" article. * Identify all companion files and related articles. * Make certain that the definitions of combinators continue to verify after updating of the SML/NJ mockup. * Rework section 4.2 on Uβ to include the idiomatic case that involves conditional evaluation. *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* 0.1.7 2024-01-15T21:02Z Minor fix, adjustment of the title 0.1.6 2023-12-18T18:12Z Correct URLs in the text 0.1.5 2023-11-10T20:22Z Continue refactoring adjustments 0.1.4 2023-11-10T20:10Z Refactor to orcmid.github.io/miser/obrep/, leaving a tombstone in its place. 0.1.3 2022-08-01TT20.32Z Refer to the oFrugal/ob-exp.txt 0.1.2 2022-06-22T17:00Z Touch-ups and section 5 addition about how the support for types does not expand the repetoire of computable functions in ‹ob› = 〈Ob,Of,Ot〉. 0.1.1 2022-03-12T19:15Z Touch-ups after review 0.1.0 2020-02-01-16:03 Smooth use of interpretation and representation, with editorial tidying enough to promote to 0.1.0. 0.0.22 2019-10-08-10:05 Introduce and acknowledge [Church1940] as the progenitor of functional type and the requirement for a concrete β (Boolean truth-valued) type. Identify [Paulson2018] as part of that. 0.0.21 2019-03-15-10:39 Touch-ups, wordsmithing, manage TODOs 0.0.20 2019-02-14-12:16 Revamp based on the latest obtheory.txt and obaptheory.txt, manage TODOs, and smooth some text. 0.0.19 2018-06-22-11:47 Reworking on the bridge between theoretical and practical use of combinator representations and the value of ‹ca› interpretation with respect to models of computation. Add section 5 on the progression from theory into practice for the Miser Project. 0.0.18 2018-06-17-15:23 First Draft of 4.4 The Y Combinator Interpretation 0.0.17 2018-06-17-11:16 Touched-up readiness for 4.3 on Recursion 0.0.16 2018-06-11-14:56 Add section 4.1 on handling conditional distinction by cases, touching up as usual. 0.0.15 2018-06-01-14:46 Touch ups on conditionality and accomodation of the deterministic computation model of obap.ap. Refactor to cover the conditionality before recursion. 0.0.14 2018-05-30-09:33 Tweek 4.3/4.4. Touch up elsewhere. Manage TODOs considering whether the narrative should be re-organized to aid in consideration of deterministic performance matters. 0.0.13 2018-05-28-11:45 Bring 4.3/4.4 closer to being entirely extensional. 0.0.12 2018-05-22-15:03 Touch-ups and wrangling with 4.4 0.0.11 2018-05-21-10:03 Split 4.4 Truth Indifference out of 4.3 and streamline the treatment. 0.0.10 2018-05-20-13:25 Complete the draft of 4.3, introducing Uβ and Truth Indifference. Related touch-ups. 0.0.9 2018-05-18-17:40 Touch-ups, have functional-type derivation of K be on the same pattern as the others (arguments taken right to left). Expand section 4 and add draft of 4.1.3 for the U combinator. 0.0.8 2018-03-08-15:37 Complete the first full draft of section 3 on the representation of the basic utility combinators. 0.0.7 2018-03-07-14:16 Complete full draft of section 2 on Functional Type and Interpretation Preservation 0.0.6 2018-03-02-19:14 Continue refinement and working through to section 2.4 0.0.5 2018-02-26-10:39 Continue polishing and lead up to 2.4 on restricted interpretation. 0.0.4 2018-02-21-14:48 Introduce 2.1 on Functional Type; manage TODOs 0.0.3 2018-02-17-10:56 Polish and set the stage for the Y combinator. 0.0.2 2018-02-13-10:00 Get past the Combinator Theory enough to talk about interpretation preservation. Introduce λ-expressions. 0.0.1 2018-02-11-21:10 Add section 1.1-1.2 In continuing development of the mathematical structure of combinators. 0.0.0 2018-02-10-13:28 Placeholder and boiler plate for a description of the nature of combinators, the chosen representations, and the power of interpretation-preserving operation. *** end of combinators.txt ***