Questions

[rnd0101]

The project interested me since circa 2001 ( https://mail.python.org/pipermail/python-list/2001-July/116910.html ) and I am glad it is continued. Now I'm being a bit more versed in type theory, so would be interesting to know the purpose and specialization of the project.

My understanding always was it's a way to embed algorithms in documents, but in the current form it's very low-level for that to be practical.

If it's a new model of computation, better lambda calculus or better LISP-machine, then what are highlights? For example, what is it's place on the lambda cube, any example on introducing types? How to attach semantics, and which kind of semantics better suits here?

Nowadays it's fashionable to prove properties of the new languages, for example, with systems like Coq, and current description (and current theory files are almost ready for that, though, more "constructivistic" formulation of some axioms/theorems would not hurt).

In other words, why people can be interested in this yet another representation of algorithms? I guess, it may be answered somewhere, but I have not found. (yes, I've seen Golden Geek in facebook)

Happy New Year 2018!

[orcmid]

Thank you for your great question(s). They deserve several responses.

First, it needs to be understood that oMiser is a single-/simple-type system. That puts it as closer to the original level of LISP as portrayed in McCarthy's "Part 1" paper. I intend to sneak up on types eventually, but not at the oMIser level. That's my thinking at this time.

It is intentional that ideas of LISP are revisited with the Miser Project. The difference is that oMiser is applicative, in operational terms, and doesn't have lambda as primitive. Lambda is definable though and that's one interesting feature of oMiser as fronted by oFrugal. Combinators are similarly representable by oMiser scripts. So this is more primitive than starting with lambda calculus or CUCH, etc. It is not about "better." I think it is important to start with something that is so low level because of the assurances of operating within denumerability and extensional equality. I'm hoping this makes it easier to comprehend the limitations of computing and appreciate the power that is achievable regardless.

Finally, there is no binding in the way smarter systems work. It is all done by a copying/rewriting mechanism. This copying is not literal, but by reference, and that is sound because obs are immutable.

One thing we know already is that there are many ways to optimize such a system's operation in a way that does not alter its fidelity to the mathematical theory/model that is honored. I intend to rely on, and celebrate, that.

I have several motivations starting with oMiser/oFrugal as the bottom level of abstraction. I agree that the materials, as presently organized are sketchy and don't connect the dots very well.

I forgot the discussion about Eternal Programming. Consider the connection to be this one,

I believe, that there is some set of operations which is as general as Turing machine BUT is easily evolutionable into something practical. The above means you need to implement only one operation and library will create: AND, OR, XOR, NOT, ... whatever.

In oMiser there are more operations to have the ap function be sufficient for represetation of all computable functions f: Ob -> Ob via ap: Ob x Ob -> Ob. I want to motivate this with minimal machinery. Not only are combinators and lambda representable, so are (short-circuit) AND, OR, etc.

This is like machine-language programming though. having higher-levels of operation and abstraction remains to be demonstrated in a way that reveals how the stored-program principle permits this.

Better primitive data types are needed for practical work, although there are already nice idioms one can put together at the ob-as-script level.

Thank you for your abiding interest. I will look deeper into your questions as I look for more that needs to be motivated.

Question for you. I think the "axioms" that I offer are constructive enough for representation of computable functions, especially obs being individually finite and denumerable. Although I use FOL=, I am thinking that, within that domain of discourse, there is not any significant difference. For me, it is a matter of using the most-straightforward already-known logical system as the basis for Ot. Do you see any non-constructive pitfall in the axiomatizations that are provided?

[rnd0101]

Thank you for the answer! I have not done anything practical towards Eternal Programming goal (well, reminding myself lead me here), but it's true it needs "machine language" of some sort. I myself started to learn programming as a kid from primitive machine language of programming calculator (reverse Polish notation, very limited memory, etc), but even back then there were very nice visualizations of both command set, stack operations, etc, that low-levelness was no problem.

In other words, if it can be explained to kids, it has potential.

Question for you. I think the "axioms" that I offer are constructive enough for representation of computable functions, especially obs being individually finite and denumerable. Although I use FOL=, I am thinking that, within that domain of discourse, there is not any significant difference. For me, it is a matter of using the most-straightforward already-known logical system as the basis for Ot. Do you see any non-constructive pitfall in the axiomatizations that are provided?

My gut feeling is not-equal signs (≠) in the theory make proving anything about ob/obap theories more difficult as the universe (or universes?) of the obs are not part of the definitions (only totality says obs belong to three categories). Ok, to be honest, when I saw theory files with such clear definitions, I wanted to type them right away into Coq and see what can be proven, but non-equals stopped me... I wonder if some kind of axiom is needed, that there always can be found something else to be, eg, a pair. In other words, intuitionistic formulation would make it more straightforward. But I guess there should be no fundamental problems, formulation is more a matter of convenience.

One more observation: "... x ¶ y is only partial ordering. When x ≠ y is determined, it need not be determined which of x ¶ y or y ¶ x holds.". If ¶ is a partial order, but not total order, then not all elements are comparable, so it may be neither x ¶ y nor y ¶ x holds. So I wonder Ob8.d "x = y ⇔ ¬ (x ¶ y) ∧ ¬ (y ¶ x) " actually saying ¬ F ∧ ¬ F ⇔ T ∧ T ⇔ T ⇔ x = y , that is, all incomparable obs are equal? This is strange.

[orcmid]

Thank you for your observations. You are inspiring me to see what additional narrative I can provide to have things be more understandable. My son (who is a musician with no software-developer experience) asks me questions about the value of this that are also helpful.

My gut feeling is not-equal signs (≠) in the theory make proving anything about ob/obap theories more difficult as the universe (or universes?) of the obs are not part of the definitions (only totality says obs belong to three categories).

Basically, the obs are all that can be generated from individuals and the functions e(x) and c(x,y). Individuals are problematic so their identity is handled based on spelling of their identifiers. Then lindies (which look like atoms but have no binding to anything) are also distinguished by their names.

If ¶ is a partial order, but not total order, then not all elements are comparable, so it may be neither x ¶ y nor y ¶ x holds

All canonical obs are comparable. Those are the elements of Ob, the domain of discourse. So x = y or x ≠ y is determined in those cases. The only way neither x ¶ y nor y ¶ x holds is when x = y. That follows from ob8(d). Would it help to state that differently?

There are many cases where neither x ¶ y nor y ¶ x is deducible, when one of x = y or x ≠ y is.

This bothers another correspondent of mine who has a background working on the FP system of John Backus.

Another question for you: The use of x ¶ y is sufficient to ensure that there can be no construction of cycles. I haven't worked through it, though I wonder if this is required for there to be some sort of structural induction. Have you seen this limitation against cycles accomplished another way that you find appealing? I suspect that Coq treatment of the Ob datatype might have that be intrinsic without requiring use of ¶ at all. I know that is true for the datatype in SML.

[orcmid]

So I wonder Ob8.d "x = y ⇔ ¬ (x ¶ y) ∧ ¬ (y ¶ x) " actually saying ¬ F ∧ ¬ F ⇔ T ∧ T ⇔ T ⇔ x = y , that is, all incomparable obs are equal? This is strange.

Great question. Let me take it apart. Ob8(d) essentially asserts two implications:

   x = y  ⇒ ¬ (x ¶ y) ∧ ¬ (y ¶ x)          (d.1)
   ¬ (x ¶ y) ∧ ¬ (y ¶ x)  ⇒ x = y          (d.2)

So, given x = y, one may deduce ¬ (x ¶ y) ∧ ¬ (y ¶ x) given (d.1)

And given ¬ (x ¶ y) ∧ ¬ (y ¶ x) one may deduce x = y given (d.2)

Basically, it is the case that x = y ∨ x ¶ y ∨ y ¶ x. When x ≠ y, we know it must be one of the other two, but we might not know which, because of the partial ordering.

Rather than saying x and y might be incomparable (which is not the case), I would say that there is always an ordering but it is only partially-determined. In the case where x ≠ y that's basically all we need know.

I think this always comes down to individuals. For the ones introduced so far, we can presume they are ordered but we don't care, since we know they are different by their definitions. The theory/model is indifferent.

Does this help, or should I find a better way to assure the extensional/structural identity of obs?

[rnd0101]

I see no problems in opaque nature of individuals, wrapped in e and c. I'd said, this is the most interesting aspect of Miser.

Ok, so comparing, say ob.e(x) and ob.e(y) is up to individuals' x and y theory. Then probably stating partial order is confusing. It's a total order, which is partially defined by the structure and partially by "theory of individuals"? (and this is exactly what looked like violation of constructivism, because one can't state "either-or": the proof is always one or another.)

[orcmid]

Thank you. That is very helpful. I will see if there is a better way to handle this in obtheory.txt.

Having ¶ not strictly determined is valuable in that an interpretation of the theory is required to satisfy only the stated constraints. Identifying an ordering of individuals and non-overlapping constructions is not relevant to validity of interpretation. In particular, no defined ¶ relation is to be exposed.

I suppose one could come up with a quasi-¶determined script ob-precedes(x,y) in oMiser that returns one of four values corresponding to definitely x ¶ y, definitely x = y, definitely y ¶ x , and not-determined (by Ob8). That's an interesting challenge. It looks like it will be computationally hard.

PS: A means for extension of oMiser is with (primitive) operations that determine unique individuals from given obs. This will require extensions to ¶ (i.e., Ob8).

[rnd0101]

FYI, I've added my (amateurish) attempt to feed Coq with obtheory to my fork here. I am not an expert in Coq, so I left Lemma without proof. What I really liked, is that the result is almost literary the obtheory. I only needed to do some renamings. Also I am not quite sure in defining ob.c as Cartesian product to Ob. Alternative for ob.c type is:

ob_c : Ob -> Ob -> Ob.

But the former allowed me to do minimal syntactical changes with your original theory (replaced dot to underscore and dash to underscore, plus added "foralls").

[orcmid]

Wonderful!

It is ob.c: Ob * Ob -> Ob

in obtheory.

That's also the case for ob.d: Ob * Ob -> {obap.A, obap.B}, although ob.d as a function is not defined separately. It is essentially buried in obaptheory.txt as part of the applicative interpretation of obap.D.

In obtheory, we have "=" so we don't need ob.d.

In obaptheory, we only have obs so predicates are represented as functions In the "standard" oMiser representation, predicate functions (dare I say predicatives?) are defined to be ones that have range {obap.A, obap.B}.

One can Curry pairing and distinction (equality/inequality) in obap.ap and obap.eval although I have established obap.C and obap.D as special binary-operation syntactic cases. We'll have to see if that notational convenience holds up or becomes too confusing.

There are two insights I have had in this area.

• For years, I thought it necessary to have special forms in script obs to handle ob.c(x,y) and x = y. When I was defining the applicative interpretations of obap.C and obap.D I saw that I didn't have to do that, although I kept the special-form cases anyhow. The primitives obap.C and obap.D can be used either way and there is no ambiguity. It is necessary to be a little careful though. I desire your perspective on this when you look into obap.ap(p,x) and obap.ev(p,x,exp).

• This comes at what does it mean to have truth (values) in a single-type system. The answer seems to be that it is whatever is defined as the computational result of the relational, x = y, in oMiser. In, LISP, it is whatever causes COND to choose one branch or the other. In C (and Java) it is what has conditionals choose one case or another. Because of Boolean duality, deciding which is true and which is false is contextual even though language specifications tend to be specific. In oMiser, all of those are built up as idioms based on restriction to {obap.A, obap.B}. Which of the duo serve to represent truth and falsity is context-dependent. For example, ob.d(x,y) is usable as either x = y or x ≠ y depending on how one chooses to identify one of the ob.A or the ob.B result as the then case. It appears that much of the labelling around true and false is mainly idiomatic. And very useful for us.

[orcmid]

I've added my (amateurish) attempt to feed Coq with obtheory to my fork here.

Your use of miser/oMiser/mockups/Coq/ is perfect. That's a great addition. I have no experience with Coq at all, so I bow to your results. Just reading obtheory.v, I think the lemma is necessary and cannot be proven. Assertion that the totality cases are distinct has to be turned into formalism somehow. Do you see another way?

[orcmid]

For example, what is it's place on the lambda cube, any example on introducing types? How to attach semantics, and which kind of semantics better suits here?

I had to look up lambda cube.

oMiser isn't exactly anywhere on the cube, but its affinity is closest to λ→. Since obap.ap: Ob * Ob -> Ob and obap.eval: Ob -> Ob, there is no such thing as λ-calculus at that level. The way it works is that there is an interpretation-preserving representation of combinators (S, K, and I are easy and the rest except Y are straight-forward). One can then arrive at representations of lambda (and recursion) abstraction that provide representations of lambda expressions slightly above the level of combinators.

Types have to be folded into this, but there is another level to be mastered first. There is likely overlap with single-type idioms and motivation of distinguished types.

What is worrisome for me is conditional evaluation. Since oMiser is greedy, one tends to program something like if p then e1 else e2 as the idiomatic ev ( (p_s) ‵(e1_s :: e2_s) ). That is, one applies the result of the scriptlet for p to the pair of e1, e2 scriptlets and then evaluates (ev) the one that is selected as the continuation, exp, in the current environment: obap.ev(p,x,exp). Abstraction via application of lambda.x (or rec.f) needs to dig inside of enclosures in recognition that the enclosed pair represents the alternatives. The only cue is the occurrence of operator ev (that is, obap.EV) and some clue that scriptlet p is predicative. So abstraction requires some constraints on idiomatic forms in which the appropriate abstraction of a to-be-bound "free variable" can be discerned.

Non-conditional expressions are easy. The conditional stuff that ev signals is trickier with respect to lambda-abstraction (i.e., currying). I have to get to that rather quickly.

[rnd0101]

I will try to finish Coq mockup first (pushed some new definitions yesterday, plus "tests" for syntax sugar - btw, found mixed backticks - two different unicode chars - in your text, so at first one test was failing). I have not yet deeply looked at ap / eval functions, but in my humble opinion, you depicted the right approach above ("digging inside enclosures ..."). There possibly could be even some optimizer, which deals with interpretable enclosures, but with current ev I do not see where to plug it in naturally plus how to mark the boundaries of interpretation? Nested quotes (`)?. Different programming languages add "laziness" differently. A lot of ideas can be applied here. For example, first which came to me now is to have primitive pattern-matching. Eval will need some kind of associative array to choose next enclosure to interpret given a key. In case of if-then-else, it will be boolean individual as a key, but it can be more generic. (this is like primitive version of pattern matching or guard expressions in Ocaml, or in SML or Erlang and I guess most FP languages out there). In Erlang, for example, whole function definition my consist of several parts, which "react" to different input patterns, so usage of IFs there is limited. This is similar to object-oriented programming, where IFs are better be replaced with one or another way of polymorphism, i.e. choice is done by having instance of one or another class. (ok, it does not work that well: Usually one IF is still needed somewhere in the factory, which chooses the class).

As for variables, I have not yet understood how these are handled in Miser (after reading comment in obaptheory, the one pointing to similarities with LISP). Rewriting application, as I understood, is one way to deal with variables, but this precludes some important applications beyond von Neumann architectures: sometimes part of the program is in read-only memory (for whatever reason), sometimes the program is distributed and served from shared memory. (and then there is a case when there is no shared parts, everything distributed, but Miser as it is does not have any notions of input/output or channels, this is probably by design not of concern).

[rnd0101]

Actually, finished and renamed the file to ob_obap_theory. Will take another look later. This is my first attempt at modeling whole new language in Coq, so I bet it's not optimal.

Also, if I understand it correctly, there is some way to really run it now in Coq, not only proof theorems about it - one example are those Test theorems at the bottom, which proofs are trivial to Coq as it knows how to unify structures, meaning, if I am not mistaken, equivalent Miser programs should be easily compared... But I need to figure out how. Plus lindies are not implemented as I did not want to model them with richer structure.

To be open, I see my part of the effort as learning. I am not yet sure how useful Miser approach would be in my Eternal Programming undertaking. I certainly like LISP-ness, but I want to see how it can be part of the "full stack" and things like compiler (?) bootstrapping. (but this same can be said to any other approach as well.) Plus I want some conceptual leverage from math, so axioms can be higher-level, like, stating lindies are monoid (aren't they?). Because if anything, math is truly eternal...

[rnd0101]

All that said, it's gigantic work you did, Dennis! Theory files were almost typo-free and Coq digested them as is, I only did minor string-replace operations to accommodate Coq syntax. I wish I could make formal verification for the whole thing, but it's probably to big task for me.

[orcmid]

btw, found mixed backticks - two different unicode chars - in your text, so at first one test was failing).

Yes, the official backtick is actually the prefix prime Unicode, but the acute accent will also be accepted in oFrugal. To do in-line examples and avoid backtick recognition in MarkDown, the prime (or an escape) must be used. (I made that mistake in a long comment yeseterday.)

update 2018-01-01: I am going to get rid of back ticks. The apostrophe (') will be accepted in place of reversed-prime, but reversed-prime is the official/reference-language character.

[orcmid]

I have not yet deeply looked at ap / eval functions, but in my humble opinion, you depicted the right approach above ("digging inside enclosures ..."). There possibly could be even some optimizer, which deals with interpretable enclosures, but with current ev I do not see where to plug it in naturally plus how to mark the boundaries of interpretation?

If you look at obap.ap and obap.ev, the two mutually-recursive functions that handle applicative interpretation, there is no problem about nested quotation, etc. The obapcheck.sml file illustrates this.

The problem I mixed into my comment is about lambda-abstraction. Afterwards, I realized it is not a problem. Briefly put, it is not necessary that every Ob be amenable to abstraction (i.e., currying). The representation of lambda.x (and rec.f) will make this clear when those scripts are devised. There will be a restriction of those applicative scripts to forms of ob where the exposure of "free variables" subject to abstraction is always clear. That does have to be devised carefully and I have worked it out before, wth an earlier formulation.

It comes down to having idioms that are used in scripts to have this work. What I had not noticed until the recent work was that I require primitive obap.EV for conditional evaluation and now I need a good idiom for the lambda-abstraction to detect and transform conditionals properly. And yes, definition of lambda/rec as transformations on obs involves pattern matching and rewriting.

Here are two markers about this.

• Dana Scott introduced ( s -> a,b ) as a conditional in a 1969 paper that he finally published in 1993 and that I recently tracked down because it is about what is now called LCF (Logic for Computable Functions). He's operating at the lambda-calculus level, but there may be something there in how he transformed between combinatory-algebra and lambda-calculus. There are remarkable parallels with oMiser that I had no awareness of, beyond recently learning that both Scott and I were inspired by Rosenbloom's treatment in the 1950 Dover book,"The Elements of Mathematical Logic." I am not the theoretician that Scott is and I need to work diligently to understand all that Scott worked through enough to see what I can apply. That, starting from different places, I arrive at similarities with Scott is both startling and encouraging.

• Conal Elliott has described Semantic Editors in an old blog post. This is essentially about recursive-descent into structures, modifying points in it, and then putting the structure back together (in a functional way). A compiler to Obs has to produce this kind of thing, and so does lambda-abstraction, since it is essentially compiling new obs from given ones.

[orcmid]

As for variables, I have not yet understood how these are handled in Miser (after reading comment in obaptheory, the one pointing to similarities with LISP). Rewriting application, as I understood, is one way to deal with variables, but this precludes some important applications beyond von Neumann architectures: sometimes part of the program is in read-only memory (for whatever reason), sometimes the program is distributed and served from shared memory. (and then there is a case when there is no shared parts, everything distributed, but Miser as it is does not have any notions of input/output or channels, this is probably by design not of concern).

Yes, there are no variables in oMiser. It is like combinatory logic in that respect. Also, obs are immutable so there is no problem about read-only and shared cases. That's critical at the oMiser level. The trick in oMiser is that obap.ev(p,x,exp) evaluates exp in a way that certain/free occurrences of obap.SELF are replaced by p and free occurrences of obap.ARG are replaced by x in the course of the evaluation. Note that, depending on the form of p, obap.ap(p,x) is reduced to evaluation of obap.ev(p,x,p).

The rewriting that goes on is not a replacement but derivation of a new ob. There is no assignment operation. In a conventional storage system, obs are typically list structures and copying parts of an ob into another is by pointing. That's not evident in the theory because ob.theory does not say anything about a computer-storage representation. Also, the abstract data type in SML doesn't reveal that either.

Finally, what lambda.x exp does, given x a lindy, is rewrite exp into one that abstracts x so that ap(lambda.x exp, y) is effectively eval(exp) with y in place of the abstracted x occurrences. I am oversimplifying, but that is the essential idea.

[orcmid]

To be open, I see my part of the effort as learning. I am not yet sure how useful Miser approach would be in my Eternal Programming undertaking. I certainly like LISP-ness, but I want to see how it can be part of the "full stack" and things like compiler (?) bootstrapping. (but this same can be said to any other approach as well.) Plus I want some conceptual leverage from math, so axioms can be higher-level, like, stating lindies are monoid (aren't they?). Because if anything, math is truly eternal...

I will avoid any commitment to Platonism. I agree that these are all important matters to work toward in achieving levels higher than oMiser. That's part of the challenge. I am taking it on faith that it can be done and it remains to be demonstrated in concrete, operational terms.

I appreciate everything that you have brought up. It inspires me to narrate more of my thinking. Your questions and observations are great ones. I am grateful for all further discussion that has value for you.

PS: I hesitate to answer the monoid question. I am still unclear what those actually are although I understand about the operational cases and lifting. I suspect that lindies have nothing to do with monoids, though.

[rnd0101]

Now that I put almost everything (except for lindies) into Coq format, I am trying to prove some checks you have in SML form. The first check was trivial, but i cant prove second at all, so asked for help on SO ( https://stackoverflow.com/questions/48048374/coq-how-to-apply-axioms-deeper-in-the-goal )

Definition ob_logo := ob_NIL :: ` ob_NIL.
Definition nob_logo := ` ob_logo.

Lemma ckOb1a :
  ∀ z: Ob, z = (` ob_logo :: ob_NIL) ⇒ (ob_a z = ` ob_logo) ∧ (ob_b z = ob_NIL).
Proof.
  intros.
  apply Ob1PairsA.
  trivial.
Qed.

Lemma ckOb1b :
  ∀ x: Ob, x = ob_a (ob_logo :: ob_b ob_logo) ⇒ x = ob_logo ∧ ob_a x ≠ x ∧ ob_b x ≠ x.
Proof.

There is already an answer on SO.

[rnd0101]

Regarding monoid. My bad, I meant even more specifically semigroup. I understood lindies at first as some kind of strings. And semigroup is quite natural for strings and concatenation operation. My point was that abstract algebra maybe more familiar in some circles. For example, in generic programming some/many data types are build around algebraic structures. The plus of this is that usually those structures do have a lot of theoretic results available, so foundations for data types are very solid, and certain properties we are interested in were proven one century ago or so.

But it's only my opinion. Successful experimentation is not dependent on this. It's more about communicating ideas to the audience.

[rnd0101]

One small observation. ob_c and obap_d are quite similar, so maybe both should be in ob?

Axiom Obap6EvI:   
  ∀ e1 e2 p x: Ob, obap_ev(p,x,obap_C::e1::e2) = ob_c(obap_ev(p,x,e1), obap_ev(p,x,e2)).
Axiom Obap6EvJ:          
  ∀ e1 e2 p x: Ob, obap_ev(p,x,obap_D::e1::e2) = obap_d(obap_ev(p,x,e1), obap_ev(p,x,e2)) 

[rnd0101]

One more interesting note is that oMiser's treatment of individuals reminds me Erlang convention of tagging: Each message should have an atom as first element so receiver's pattern matching will make it straightforward to process the case.

I mean this part:

        obap.apint(obap.C, x) = obap.C :: ob.e(x) :: obap.ARG
        obap.apint(obap.D, x) = obap.D :: ob.e(x) :: obap.ARG
        obap.apint(obap.E, x) = ob.e(x)
        
        obap.apint(obap.SELF, x) = ob.e(obap.SELF) :: ob.e(x)
        obap.apint(obap.ARG, x) = ob.e(obap.ARG) :: ob.e(x)
        obap.apint(obap.EV, x) = ob.e(obap.EV) :: ob.e(x)

If this is indeed the idea, then probably standardizing on the approach will reduce the complexity of the theory by using more regular structures. Now my impression is that there are some overlaps between numerous is-functions and obap individuals, which somewhat obscures the logic and intentions.

Maybe unrelated, but I have hard time understanding why there are so many variants of is-functions for lindies:

        obap.is-pure-lindy(p) ∧ obap.is-lindy-everywhere(x)
                => ob.is-pair(p) ⇒ obap.ap(p,x) = p :: x           
        ¬ ( obap.is-pure-lindy(p) ∧ obap.is-lindy-everywhere(x) )
=> ob.is-pair(p) ⇒ obap.ap(p,x) = obap.ev(p,x,p)

Just lindy, pure lindy, lindy-everywhere... help! IMHO, reformulation in positive notation (that is, without use of ¬ (not)), might clarify matters a lot. My usual programmer's sense of code smells says in situation like this that there is some new concept hiding here, and if it were made explicit, formulation would be clearer.

Maybe, this is purely cognition problem, but direct statements on kinds of lindies may be better (there are similar situation in theories, IMHO, there is an antipattern).

[rnd0101]

I am thankful you answered my questions regarding theories, and hopefully my notes make at least some sense. Now my understanding of theories is better, and I want to see if I can answer some of the questions above and if I can make REPL from Coq representation.

[orcmid]

I want to see if I can answer some of the questions above and if I can make REPL from Coq representation.

That's an interesting notion. I will clarify what I can for you. I think it will be helpful to break things down into separate Question issues. (I suppose this is the ultimate Socratic dialog when it is with oneself. Perhaps that is what Plato did, though making Socrates the responder.)

[rnd0101]

Yes, this thread is too big. I was referring to question you asked way up there, eg " I desire your perspective on this when you look into obap.ap(p,x) and obap.ev(p,x,exp)." ... I have not yet got around to it.