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.