What are Individuals and Lindies all about? #2
Comments
First, About NotationTo facilitate distinction of constants for obs (i.e., fixed individuals in the domain of discourse), I need a way to distinguish, in plaintext, between variables in expressions of the logical theory, Ot, and such constants. The primitive individuals that are distinguished in the formulation of the universal function have names such as In homage to ALGOL 60, when there is more typographical freedom for reference notation, bold-face could be used, and I prefer The primitives are fixed and distinguishable. The lindies are more like the atoms of LISP. They are distinguished by their "print names." In There is a grammar for the lexical form of s, but for now just assume alphanumeric string beginning with a letter. Lindies are completely distinct from the primitives, and that is reflected in the notation. In addition, primitives have specific and distinct interpretations with respect to obap.ap and obap.eval. Lindies, on the other hand, although distinguished, have no individual significance with respect to the universal function. Their notional significance is as themselves -- literals. They can be freely chosen for whatever purpose an user desires. Since every ob has an interpretation as a script, p, in obap.ap(p,x) and obap.eval(p), what is to be made of lindies then? |
|
"Lindies are completely distinct from the primitives". Why lindies are needed? What is the reason Occam's Razor spared them so far? Why they need to be different from user-defined individuals? For example, even atoms (in Erlang or Prolog, not quite sure about LISP) are interchangeable to some degree with strings/lists, and in other languages string constants are enough for what atoms do. |
Some level-setting:
My hope is that the next response on this question will help to clarify the intended arrangement. PS: I had wanted to avoid reflection where lindy-names can be extracted as strings and strings can be used to name lindies. Likewise, I wanted to avoid allowing definable individuals (to be introduced in a later extension) revealing their definitions. However, I can't do without that for oFrugal to operate properly. Reflection is also important in demonstrating scripts that provide simulators of obap.ap and obap.eval. That works best if obs interpreted in the simulations are the same ones having the direct obap.ap and obap.eval interpretations. I.e., obap.ap(obap.ap(apsim, p),x) = obap.ap(p, x) and apsim is non-trivial. |
Second: About Applicative Interpretationupdated 2018-01-11: Make important correction in the rule for applicative interpretation of lindies. For oMiser, every ob has an applicative interpretation. So obap.eval(exp) determines at most one definite ob for each given canonical ob as exp. Similarly, obap.ap(p,x) determines at most one definite ob for each given p and x combination of canonical obs. This wording acknowledges that some applicative evaluations might not produce any result, even when exp, p, and x are so definite. The term applicative interpretation applies to how p is interpreted via obap.ap(p, x). The term applicative expression/evaluation applies to how exp is interpreted as an expression of applicative operations (that is, obap(p,x) cases) in accordance with obap.eval(exp). The General Applicative SchemeFor obap.eval(exp), if exp = e1 :: e2, the ordinary eval of exp is as obap.ap(eval(e1),eval(e2)). In other words, this e1 :: e2 evaluation is as the application of the evaluation of e1 to the evaluation of e2. For obap.ap(p,x), when p is a singleton, the applicative interpretation of p determines what function of x is provided. Every singleton p has a definite applicative interpretation. When p is not a singleton in obap.ap(p,x), the applicative interpretation of p is ordinarily determined by the evaluation of obap.ev(p,x,p). That is like obap.eval(p) except that the obs supplied as p and x are available in the evaluation as operands supplied to the applicative evaluation. The extra-ordinary case is when interpretation of p is defined to be a trace for which further evaluation is not attempted. This will be addressed in the Third part of the response to this question. Specific Applicative InterpretationsThe course of applicative interpretation typically arrives at operations where p in obap.ap(p,x) is a singleton. There is a definite applicative interpretation for every singleton case. Similarly, there is a definite evaluation case when exp is a singleton in obap.ev(p, x, exp). There are also some special cases when s is a singleton and evaluation of a script expression has form s::more in obap.ev(p,x,"s*::more). Below, obap.ap is abbreviated ap and we use simply ev(exp) when the p,x are understood (or unimportant). Elementary-Primitive Applicative InterpretationsFour primitive individuals evaluate as themselves and have straightforward applicative interpretations.
Enclosure Applicative InterpretationEnclosures evaluate as the enclosed ob. The applicative interpretation of an enclosure is also the enclosed ob.
Unary Use of Binary OperatorsTwo other primitive individuals evaluate as themselves and signify special operators in evaluations where they precede a pair. They have special applicative interpretations when preceding a singleton in an evaluation.
where the result of obap.d(x,y) is Special-Form Expression OperatorsThe three remaining primitives serve as operators that have special significance in the evaluation of the expression/script forms of obs.
The interpretation of these individuals is specific to their occurrence in an ob that is being evaluated as an applicative expression. There is no comparable applicative interpretation because the evaluations are entirely dependent on p and x in a current evaluation. There must be an applicative interpretation and in this case that requirement is satisfied by producing a trace of the attempted applicative operation. For example, ap( These forms are termed "traces" since applicative interpretation goes no farther. A trace is such that ap(trace, non-trace) = ev(trace) = trace. Given how Lindy Applicative InterpretationLindies are freely-chosen individuals with no individual interpretations other than as themselves. The requirement for applicative interpretations is satisfied by creation of traces. There is no basis for anything further.
The production of a trace as a result may be indication of a mistake in the creation of an ob for use as an applicative expression. And, because the production of traces is a well-defined situation, there is prospective intentional use. This, and some trace-intending/-extending measures, deserve separate attention. |
|
Great description! (BTW, have I missed some article with this information somewhere is the above description new one? Of course, all that is in the theory itself, but this is more human-readable).
Aha! Here I see the key for lazy evaluation. Basically, the theory does not specify two evals (in Maybe, you have thought of possible laziness differently, for example, coding simulation of evaluation / application functions, but do you think laziness can have a hook already at destructing pair? That is, the second eval does not happen immediately? In other words, there is a possibility Maybe, I am missing some simpler mechanism you assumed to enable laziness (thus making oMiser layer more expressive). One way, which came to my mind, is that My intuition is that enclosures are better suited for laziness, but I can't see how specifically it can be helping lazy IF-THEN-ELSE, for example... I need to play with some run-time implementation to get more insights though. |
Quick Note.
|
Ok... The closest analogy I can see here is type safety. (eg, used in MLs). In (some? many?) FP languages type checking and interpretation are separated. I do not follow latest developments, but I guess type-checking must be eager, and interpretation can be whatever. ML family perhaps went to extreme with type-safety, some languages are not type-safe at all (C, C++), so the spectrum is wide. After your explanation above I understand that oMiser does both at the same time. Even though there are no types, it's just inevitable to check the constructions. I'd even said, that many of those conditions in the theory really are camouflaged type checks, it's that types are encoded structurally instead of being "in parallel". Unfortunately, I've never worked with Hindley-Milner algorithm, but I suspect if oMiser's tree is given to it, it will be capable to deduce types! |
|
In the context of this question, I tried to figure out the ontology of miser, ob and obap. I got that idea in the morning, that theory's Obs and lindies remind me... semantic web approach. So I thought of application, where obs are RDF resources, that is URIs (or IRIs), and lindies are data attributes of type string. Primitives are just special resources of the ob / obap ontologies (they can even have almost same abbreviations as in the theory, only using colon instead of dot Then all those numerous is-functions I turned into classes in RDF understanding, where there is this Open World assumption and any resource can have any classes unless explicitly disjoint. I have not yet experimented, but RDF graph, based on the ontology, can be an alternative language for oMiser programs. And any decent OWL reasoner will be preliminary "type-checker". Then there is a need for some Turing-complete engine to evaluate the program or, alternatively, SPARQL can be used to query the program or to query the results of computation. What I like in RDF is that it's very primitive foundations: triples. Still it makes powerful knowledge representation media, which I think can be one of the pillars of Eternal Programming. One important feature at the very low level is concatenativeness: it's very easy and logically ok to just merge any number of RDF graphs together to combine knowledge. With open world it's harder to say "NOT", of course, because there may be some additional knowledge inaccessible at the moment of inference, which has the needed fact. But this is life: We do not have only yes / no answers, sometimes, it's proper to say "do not know". First results here. The description logic (as reported by Protege software) so far is ALCH(D), but I only scratched the surface (individuals are not shown on the following OWLViz diagram):
So now basically I am thinking of specific implementation of oMiser, which will be the Turing-complete rule language to interpret algorithmic knowledge in the form of RDF graph (and result in RDF graph or whatever further research will find more suitable). In this implementation I can offload heavy-lifting to some RDF library, yet to decide, and I think I will not be concerned at all with checking cycles. Not yet sure whether to go with Prolog or stick with Python's rdflib I am better familiar with. Plus some practicalities to be resolved, for example, now I have Pair as a class for and ob, but there is also a need for object relation called "pair", which corresponds to the PS. Perhaps, |
I think that is possible in some constrained cases, but not for every applicative expression at the oMiser level. This will come up in examination of (higher-level) representation of combinators in ‹ob›. I think there will be polymorphic type inference first. |
|
It can be quite involved, but it seems current technology does it for even for machine code. This is more curiosity than something I'd liked to personally pursue. |
Thank you. That is a valuable find. The ob representation of scripts to obap.eval and obap.ap are essentially machine-language programs and attempting to "decompile" them to a higher level with (denotational) types is a valuable idea. The case does apply to oMiser and it is something on the radar. This will matter in the case of program transformation, where, if certain idioms are known, optimisations are possible. This is going to come up around lambda-abstractions and working with combinators and optimizations of applicative operations across apply operations when type restrictions can be inferred. I have in mind nailing down oMiser at the obaptheory level and working on these other matters at a level of oMiser-application. Any optimization idea that are taken into an oMiser implementation itself will be invisible (apart from changes in performance). That's all for future consideration with oFrugal/oMiser as a working laboratory fixtures. |
|
Apart from any clarification and refinement in editing, I have completed the "Second: About Applicative Interpretation" comment now. The next thing I want to motivate is the use of traces and the additional properties on constructions involving lindies. That is coming up, here. I notice that "applicative interpretation" is a broad term that I use rather broadly. Please note that the apint(p,x) sub-function used on behalf of the Ot representation of function obap.ap(p,x) simply collects together the applicative interpretations where ob-is-individual(p). Is there a better name than "apint" for this case? Also, those are all of the cases for ob individuals so far. There will be some extensions later on. |
|
Thanks! That is high quality description (I mean "About Applicative Interpretation" comment), which deserves to be in the miser documentation rather than here. As for the term "applicative interpretation", I was thinking it's about some process in the applicative programming language, perhaps, interpreting expression according to the "script", where script is a result of a purely applicative programming (composition of functions). But now that you raised this terminology point, I am no longer sure the term is descriptive enough, especially in "apint" abbreviation, where first thought is it's about integers. (but then there are no integers here) OTOH, it's definitely about interpretation during application of the script, right? BTW, are there any examples of the programs, something, which can help to decipher ob/obap theory semantics? I mean, "hello world", "factorial", tower of Hanoi, GCD algorithms or something everyone is familiar with or at least algo to add two numbers? |
Right. Based on our exchanges, I think I want to say that an applicative-expression is an ob, exp, for which obap.eval(exp) interprets and evaluates as the applicative operations that are expressed in it. I would say that obap.ap(p,x) interprets p as the script for an applicative operation it applies to the operand ob, x. I think, when our discussion stabilizes a bit, I need to rework the basic descriptions (and also fix the various indy-related predicate names). |
oMiser is so primitive that there are nothing like numbers or strings, and no input-output. The input-output part could be handled by oFrugal though. Even arithmetic has to be defined. There are some examples in the obapcheck.sml file, but they clearly do not resemble what they accomplish very much. oMiser is not very expressive compared to even moderately-higher-level languages. Here's a simple representation for (Peano) arithmetic:
It is an interesting feature of this representation that subtraction by diminishing is easy, as is addition by 1 (successor). So there are rather crude kinds of counting and testing available. It is also an interesting contrast with untyped λ-calculus where substraction is considered difficult. Here's a simple (inefficient) kind of test. Let x be the number of times some action is to be performed. Let y be how many performances have been already, starting with the rN of 0. At least one performance remains to be done if x dim y is not 0 (i.e., is not a singleton). A practical version would be to simply check if x is 0 (a singleton) already and if not, perform a repetition in which x is diminished by 1. Even more practical is traversal of a list structure where a singleton represents the empty list. Here, the diminish function on the list is like taking the tail n times, where the tail of the empty list is the empty list. That's the kind of idea involved in programming via ob applicative expressions. It's not that these representations are practical to use. The first-order interest is that such representations are possible and we can consider the computational-model capabilities on those terms. There are two useful examples in obapcheck.sml. Using the ob.txt reference notation, there is introduction of an ob, cS, which, if I have done it properly, represents the combinator, S, such that Ob cS can be viewed as representing the hand-Curried λ-expression λx λy λz ( x(z) y(z) ) and that's exactly how I derived it. updated 2018-01-09: corrected two typos |
|
Thanks! During the week it's hard to contribute for me, but I will follow everything you write. FYI, I've asked this question at stackexchange CS Q&A site. Lets see if anything useful comes up. I think, efficient transformations and optimizations are crucial for upper levels of computational stack. |
I think of type-checking (at least in ML) as static so it happens at compile time (i.e., before interpretation). ML is also eager/greedy in the sense that evaluation is not lazy. oMiser requires no [static] type checking, since everything is an ob. There is a kind of type inference that can be made, and that will be interesting to explore as a prospective avenue to introduction of types. It will show up when we represent combinators and lambda-abstraction. |
Third: About Traces and Lindiesupdate 2018-01-10: Complete discussion of pure-lindy traces and use in symbolic execution. There is a somewhat paradoxical notion introduced with traces and having an interpretation for interpretation-free lindies. TracesTraces occur in three ways.
N.B: Thanks to insistent @rnd0101 (and earlier Paul McJones) questioning of the mysterious lindy-structure predicates, this explanatory effort has inspired improvement in obaptheory.txt representation of this situation and the nomenclature used. -- orcmid 2018-01-09 Lindy Traces and Symbolic ExecutionThere could be further special cases that would capture more when the applicative script, p, is a pure-lindy trace and the operand, x, is not. It is an arbitrary choice to build up only the case where p and x are pure-lindy traces themselves. This is also expedient from an engineering perspective. It then becomes useful in engineering of complex applicative interpretations. Example 1: Confirmed Representation of a CombinatorPreviously, the ob cS was presented. It is claimed that this ob represents what is know as combinator S with specific applicative interpretation. In the SML mockup file obapcheck.sml, there is domonstration of that applicative interpretation by "symbolic execution" using the pure-lindy traces ƩX, ƩY, and ƩZ for x, y, and z respectively. The results of ap(ap(ap(cS,ƩX),ƩY), ƩZ) and of eval( ( ( ‵cS :: ‵ƩX ) :: ‵ƩY ) :: ‵ƩZ ) are each the symbolic-execution produced pure-lindy trace (ƩX :: ƩZ) :: (ƩY :: ƩZ). More important than that result is that script cS was derived by working backwards from that desired result as demonstrated in the obapcheck.sml mockup. This also helps to ensure that the introduction of pure-lindy traces did not short-stop and obscure anything in the applicative interpretation of cS as a representation of combinator S. The representation of combinators, including S, is important, later, in demonstration of the universality of obap.ap and obap.eval. Combinator representations are also representative of ways that scripts can be used to combine other scripts into ones with composed applicative interpretations, a fundamental facility in functional-programming. Example 2: List Processing OperationAnother test case in obapcheck.sml concerns list processing. Symbolic execution was important in derivation and verification of the ob identified as "has." The idea is that has(x) applied to a list, L of items will report whether x is in the list or not. A list is represented, in this case, as an ob where end is a singleton and the list could be otherwise empty. ap(ap(has, x), L) will yield obap.B if x is not one of the vi and obap.A if it is. Representing the truth-value by obap.A and false-value by obap.B, the script, has, can be taken to represent the functional-programming-style predicate fun has(x) List = let hasX L
= not is-singleton L
andalso (x = a L orelse hasX( b L )
in hasX ListSymbolic execution is indispensible in the formulation and verification of the has script. It will take more gradual development to development of facility with such derivations. This will be expedited by introduction of scripts, akin to the combinators, as idioms for construction of these more-extensive scripts. Some ObservationsThe pure-lindy trace condition and traces generally are an engineering solution to the case when there is no already-defined applicative interpretation that is coherent with special-form employment of individuals. The benefit is a kind of fixed exception treatment that has operations yield definite results when there is nothing further to be done. Traces and pure-lindy traces are enshrined in the ‹ob› Ot theory to impose what is essentially an engineering decision on all valid computational interpretations of the mathematical formulation. It is thereby assured that oMiser implementations are interoperable in this respect, and any results from evaluation of representations of the same scripts will be the same. This opens the door for exploitation of pure-lindy traces in confirmation of the correct operation of scripts by providing symbolic execution as part of test suites and as an aid in the derivation of scripts. Symbolic execution (and symbolic reduction of formulas) is a well-known method in confirmation that evaluation of a given formula or execution of a particular procedure yields a particular (canonical) result. This is usually performed mentally or with pencil-and-paper (now, maybe text editor). It is by a kind of heuristic operation using "pretend" variables and seeing how far an evaluation can go without disturbing those variables. The oMiser ob and applicative interpretations are so primitive that having some mechanical way to explore evaluations via computer-aided symbolic execution is very important, as will be seen repeatedly in development of actual scripts for practical operations at the oMiser level. Cautionary Note. One needs to be careful in reliance on pure-lindy traces in the development and confirmation of oMiser scripts. Because they are traces, they can be misleading when their preservation occurs where computations with different operands would take different directions. The kind of building up illustrated in worked cases will demonstrate how this pitfall can be avoided. |
The simplification and consistency of is-pure-lindy-trace(ob) tracing is introduced, with obap.sml and obap.check alignment
No, everything was, and still is very skeletal as I initiated development of the project. Thanks to your great questions, I have stitched together this much by way of explanation. Your questions about Lindies here and in Question #4 also inspired an important simplification. Thank you. |
|
Nice simplification! Now it makes sense. Minor: Pls fix typo Also, I am trying to find a paper, which presented minimum length universal combinator... If I remember correctly, it was about of length ~ 21. Could be good example for oMiser. Also there is an interesting article on combinators used in general AI: Universal Induction with Varying Sets of Combinators by Alexey Potapov, Sergey Rodionov. (in short: Genetic Programming with CL) This is near that what I tried to recall on search for algorithms. Maybe relevant for scope of Miser project. I will try to find "universal combinator machine" as well. At least here there is an interesting survey of minimalistic machines for Chaitin & Co AIT. So maybe self-interpreting example for oMiser can be of illustrative value. Also, https://en.wikipedia.org/wiki/Combinatory_logic#One-point_basis can be yet another cool example. |
There was a typo and incomplete replacement when obap.is-pure-lindy-trace was introduced as simplification of lindy-based traces.
|
While adding more to the "standard library" , I've found, that:
|
Well, you are using "lindy" notation, i.e., string format. That won't be used in oFrugal because there is the hope of having strings some day 😄 . Lindies are the closest there are, in oMiser, to LISP atoms. They are truly meant to be literals, and should be easy to use as/in obs representing data. It will also make lambda.lindy and rec.lindy be smooth (anticipating that the idioms will be for |
Yes, I have been using the right-to-left instead of left-to-right order for over 50 years, so it is automatic for me. It also avoids treating |
Well, after having gone around and around on that, the current conclusion is that after all. This is how established in the summary grammar in Question #14 and #8, and the resolution of Question #13. Whenever I doubt it, all I need to do is look at the above identity. The use of I think it is time to close this one too. |
This Question is Closed
After experimental confirmations carried out with Roman Susi (@rnd0101), the treatment of Individuals and Lindies has stabilized.
In obtheory.txt, all obs, x, such that ob.a(x) = ob.b(x) = x are classed as individuals.
ob.NILis established as such an ob, and it is indicated that there can be any number of additional distinct ones. At the theory, these are distinguished by difference in the lexical forms of the names given to them.In obaptheory.txt, as part of introducing universal functions obap.ap(p,x) and obap.ev(exp), a number of additional individuals are introduced. I.e., individuals such as
obap.A,obap.C,obap.SELF, andobap.EVare identified as distinct primitives along withob.NIL. In the reference notation for expression of obs in plaintext, these are designated as.A,.C,.SELF,.EV, and.NIL, respectively.Also, in obaptheory.txt, we learn that there are lindies (short for literal individuals) that are distinct from primitives and symbolized in the theory by notation Ʃs where s is a distinct alphanumeric spelling taken as the identifier of the lindy. In the reference notation, that lindy is simply written s.
Then, in the formulation of the universal function obap.ap in the theory language, Ot, there are some elaborate predicates concerning lindies.
The text was updated successfully, but these errors were encountered: