Replies: 23 comments
-
Ok. I've realised my idea that scripts can be found automatically. See https://github.com/rnd0101/miser/blob/master/oMiser/mockups/python/solve.py for a proof of concept (randomized one). For example, it found the following script to swap pair's constituents:
Of course, sometimes there is infinite recursion, so Python limit get exceeded and I see this:
This is real joy! When I look at that script, it looks so logical. |
Beta Was this translation helpful? Give feedback.
-
Wow! Added to the library:
|
Beta Was this translation helpful? Give feedback.
-
It is interesting, that certain problems, which look simple, are not easy to solve, eg:
Also, solution can not be found to "unenclose" to arbitrary depth:
One more hard problem is to regroup the following pairs:
not quite sure why. (but using SELF causes problems to the solver, perhaps, it needs timeout, so maybe unenclosing can be solved using SELF) |
Beta Was this translation helpful? Give feedback.
-
This sounds like it fits with the cookbook idea. It is especially important to see how to construct recursive procedures, as in the There are idioms for manually abstracting from desired scripts. You saw that in the obapcheck.sml stages of cS, cK, There are patterns and we can use helpers to build them. In particular, there will be useful scripts ^lambda and ^rec that will be instrumental. It will be the case that manual abstraction can arrive at more efficient scripts, so we will study that to see why and how close the scripts can come to working as well. KEY OPEN ISSUES:
|
Beta Was this translation helpful? Give feedback.
-
Good point. Cookbook for now uses Python syntax to build obs, no eval applied until it is printed in the shell, where eval is applied implicitly, but I will change that. One small check: both for assignment and input, right? |
Beta Was this translation helpful? Give feedback.
-
This script needs to be defined when the argument is not a pair. I suggest that if it is a singleton, just return it unchanged, otherwise do the swap. This should do that job (with no eval added, just building the ob using ‵ and ::).
providing a script such that Notice how only one of the then or else arm is evaluated, as needed. That is also how |
Beta Was this translation helpful? Give feedback.
-
So now the shell has two modes: with explicit eval and without one (default). Assignments do not use eval:
Also I get rid of INPUT/OUTPUT because after implementing in-parser evals there is no parsed original input... |
Beta Was this translation helpful? Give feedback.
-
No assignment and input provided at oMiser. oFrugal needs an include statement. The idea, for now, is that oFrugal REPL works like the SML/NJ one. Just build up source code files that do the assignments (ob ^binding = ... ) in comparison with SML (val binding = ... ). Maybe |
Beta Was this translation helpful? Give feedback.
-
Yes, "assignment" (actually, binding) and input - those are oFrugal side. Should the prompt be 'oFrugal' also? The longer extension maybe better. |
Beta Was this translation helpful? Give feedback.
-
Yes, the default cases are exactly what is needed. The eval cases break the ^cS definition, for example. |
Beta Was this translation helpful? Give feedback.
-
Agreed. I think we are on the right track for this phase of development. |
Beta Was this translation helpful? Give feedback.
-
BTW, solver found shorter swap, which also handles enclosures:
and what I like in this variant, is that is pretty straightforward. |
Beta Was this translation helpful? Give feedback.
-
Sure, if you don't mind that
Is the solver hypothesizing that x in A singleton x is not of that form. See the second rule under Ob1 in the Primitive Notions of obtheory.txt. Also, I think the operand grouping in the applicative use of .C is not correct. The shorter swap should be
should yield |
Beta Was this translation helpful? Give feedback.
-
Solver is very simple. I give it an "equation" like (it's in Pythonish frugal, list is for arguments here):
and then it goes one to be roughly breadth-first search for all possible ob-trees out there. At the moment, no prior probabilities of ob-construction elements are used, they are applied with uniform distribution. The exact syntactical form is not optimized for the number of brackets as ob output procedure is very simple as well. But with the extra rule for individual (in the above), solver fails to find solution, at least so far on my computer. I need to rewrite it and oMiser in a more efficient language than Python to be able to handle more complex obs - their complexity grows exponentially. |
Beta Was this translation helpful? Give feedback.
-
I've added solver to the shell as well:
It's interesting, that sometimes scripts proposed by the solver looks more like hacks, which abuse some oMiser specific behavior. I do not know if it is a theoretical concern oMiser is so robust / forgiving, but it means that a lot of structures produce the same effect and still some looking-easy equations can't be solved:
|
Beta Was this translation helpful? Give feedback.
-
OK, I think that givng There is also something wrong with the derived script. If there is no .C in there, there is no way to produce a pair in the result. It looks like the .EV should be .C. And there are too many parentheses, so it should not work. I think it appears to work because you might be getting lindy traces in a way that is misleading. obap.ap( I still think it is
assuming no eval done following the evaluation of the ob-exp, and assuming that the argument is always a pair. If you want to preserve
Try it without post-eval. |
Beta Was this translation helpful? Give feedback.
-
Yes, solver finds precisely what is asked. I may have asked for example:
to cover more cases. The equation is just as it is: "find ^F, which when given these arguments produces these results". There may be more than one conditions, and solver can find your variant as well (I do not care about redundant parentheses) with more time/calculations:
BTW, do you think I can add
will be:
|
Beta Was this translation helpful? Give feedback.
-
I was also thinking if some kind of conversion function (for standard lib) for situations where one wants to convert a pair into arguments can be good addition to standard library:
that is, for "function" of two arguments construct a new equivalent function, where arguments are in the pair. |
Beta Was this translation helpful? Give feedback.
-
I am finding the following useful as an evaluation indicator:
2-3 different indicators are also useful:
(simpleSwap is that "buggy" naiive swap) |
Beta Was this translation helpful? Give feedback.
-
In this case, convertF = (`(F) :: (.A :: .ARG) ) :: .B :: ARG
The counterpart challenge is curry2(g) which, given a g that takes an argument pair, in g(x :: y), produces an f such that f(x) y yields g(x :: y). That would satisfy convert( curry2 g )(x :: y) = g(x :: y). I am reminded that we must not think of oFrugal ob-exp as a programming language. The ob-exp is an expression for calculating an ob. In that respect, it is more like an assembly language in which there are applicative expressions for intermediate computations. Those applicative expressions can be thought of as the counterparts of macros in assembly language, except it is all about computing/assembling obs. We go higher-level only after motivating it in conjunction with extensions beyond oMiser. And, because oMiser obap.ap is a universal function, we can have elaborate computations that, just-the-same, produce only obs. The ob-exp calculator is as powerful as we can ever have, at that level. |
Beta Was this translation helpful? Give feedback.
-
BTW, typos above: |
Beta Was this translation helpful? Give feedback.
-
I am trying to find some parallels with Python:
So, curry will have double lambda while convert (uncurry?) has double application - single lambda... But that |
Beta Was this translation helpful? Give feedback.
-
look like the right idea to me. Is |
Beta Was this translation helpful? Give feedback.
-
The following marvel implements "has" (taken from smlcheck). It would be interesting to know how to come up with my own scripts though. Like what are heuristics for composing scripts. Maybe, some useful intermediate "building blocks" need to be devised (like use of combinator here), but combining those into coherent program remains a mystery for me.
For simple example, given
ob ^t = "a"::"b"::"c"
, I need a script, which retrieves a second member ("b"
) from the ob t.Direct application is straightforward:
but it's encoding as a script could be challenging. With some trial-n-error I came up with:
This approach to A and B seem to scale well to access n-th item:
but I guess if I deal with a need to encode two-argument
C
andD
and mix withA
andB
, some other way is needed.There are some other interesting tricks:
Beta Was this translation helpful? Give feedback.
All reactions