What is apint of arbitrary individual ob?

[rnd0101]

Can't find any formal definition for the case when ob is missing apint in the theories, so for example my REPL implementation breaks on the following input:

ob.c(ob.c(Ob('x'), Lindy('ImLindy')), ob.e(Ob('NIL')))

That is Ob('x') does not have an interpretation.

Is the program above incorrect, or should all extra obs come with apint? Or have I overlooked something in the theories? (there is that trace-related comment I have not understood in terms of interpreter pragmatics.)

(for now I've added ValueError: Ob individual Ob('x') can't be interpreted. to provide better error message)

Thanks!

PS. In SML implementation, it seems there are no other individuals at all. Is this right?

[orcmid]

Issue Closed

There is some useful experimentation covered here, and the question has been answered.

The resolution statement identifies where there might be more related explanations.

---

Please enable issues on your rnd0101/miser fork and we can talk about these things better there.

In obaptheory, there are no missing apints. A computational realization must satisfy that.

I have some observations about your current Python mockup. This is mostly thinking out loud and speculative on my part. I have not run your Python script.

1. For a runtime representation of obap.eval(exp) there are only "concrete" obs. So Ob('x') must produce the representation of a canonical ob. It looks like you should be using Lindy('x') for this. Or if you are using Ob(x) to introduce primitives, as with Ob('NIL'), you should fail if there is no such defined primitive. Raising an exception in the case of Ob('x') is appropriate, in that case.

2. In the python representation, it should never be the case that an Ob can be instantiated with either a or b set to none. You probably need a constructor for individuals and then functions c(x,y) and e(x) that are constructors of obs from their ob arguments. If setting a and b to self for an Ob instance, x has x.a == x and x.b == x work properly, you have what you need.

3. You will need to make Ob instances comparable though, to determine when two obs are the same or different. For example, if you have two instances of Lindy('myFirstLindy') they must compare as identical. You probably can't use "==" for that unless there is some overloading. I would define a comparison function or method and save any overloading for another time.

4. You do need an isLindy() method, but you don't need the others. The other forms of ob can be determined by inspection. If you want helper functions for that, fine But you don't need methods for all of those.

Of course, you can have discrimination predicates as individual methods on an Ob if you want that much encapsulation. In that case, the methods must work as defined in obtheory. E.g., it is sufficient to have

def is_individual(self):
      return self.a == self

(The use of self.a == self.b is incorrect, since ob.c(x,x) would satisfy that.)

5. Since your initialization constructor is with Ob(name), I think that must distinguish whether "name" is for a lindy or not. You could differentiate using the name convention given in ob.txt, so names beginning with "." are for primitives and alphanumeric names beginning with a letter are for lindies. For the primitives, you could have a list/dictionary of the defined primitive names. That is probably where the exception could be thrown if the name is not of a defined form.

6. In the manner of (5), obs determined via ob.e(x) and ob.c(x,y) are anonymous These could be defined as constructors perhaps? It might be useful if Ob( ) produced the ob for ob.NIL as the default constructor. Then ObE(x) and ObC(x,y) could inherit from Ob( ) and alter the a, b, and name settings appropriately. I am speculating that there is some Python idiom that provides the equivalent of single inheritance in this context.

I don't follow Python that closely and have not used it much, so I don't have anything else to say at a high level here.

Oh. I would not call the python runtime for oMiser operation a REPL, although a REPL would use this for the Eval part.

[orcmid]

PS. In SML implementation, it seems there are no other individuals at all. Is this right?

Yes, that is correct. There are only lindies and the identified primitives.

[rnd0101]

Thank you for input! For the Python runtime my goal is to have, well, oMiser runtime in the programming language I know best, so I can do experiments and understand what is it all about better.

I want to rewrite the whole module using OOP. This will make a change to ev function signature, as it will be a method of the last argument instead (not sure if this is constitute oMiser compliance violation, hopefully, not). ADTs are not good match for Python, and so far I do not see any obstacles for OOP rewrite.

I am still haunted by ob/obaptheory predicates and classes. And SML code seems to agree with that: code in the ap function is not very readable. As for classes, I thought there are three of them as per totality axiom but during python (and earlier with RDF) implementation I had gut feeling like classification is very hairy in a sense that there possibly is a simpler way without any sacrifices. Unfortunately, my intuition did not produce anything at conscience level yet. In such cases I usually wait.

Also, in Python code I had a desire to bring the syntax as near as possible. So the code is not pythonic, as I tried to follow ob.something / obap.somethingelse syntax. So I most probably rewrite it totally, and make beautiful code with the following principles:

• all ADT constructors will be Python classes, where top level class will be abstract
• NIL and other primitives will have their own classes.
• moving ev, ap, apint into those classes

I've enabled issues, good hint!

[rnd0101]

I've reworked miser.py, thanks for your simplification to lindy logic. However, I would like to add tests and "cookbook" when I have more time. In cookbook, I intend to present combinators (S, K, I, ...) and also see how basic combinator operation ("concatenating" combinators) is reflected in oMiser notation. Like, is it as well "concatenation" or more complex operation.

[orcmid]

I intend to present combinators (S, K, I, ...) and also see how basic combinator operation ("concatenating" combinators) is reflected in oMiser notation. Like, is it as well "concatenation" or more complex operation.

It is by applicative interpretation, so more complex. I had been thinking of this important next step (separate from getting some oFrugal in place) so I have gone ahead and started Question #7 on this.

I like the "cookbook" idea. I was thinking of narrative that describe the combinator representations, but also a narrative that describes handy oMiser expressions that are usable as a kind of catalog of useful macros for easier construction of applicative-expression obs, working up to having scripts for lambda and rec. To have this be usable in making oMiser "programs," a running oFrugal, even as a mockup, is indispensable.

[orcmid]

The topic question and some related concerns have been addressed to the extent that they apply to oMiser as intended. The presentation on Combinators will be tied to Question #7. Looking for a Cookbook is held open in Question #12 for now.