Closed rnd0101 closed 3 years ago
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:
oMiser> ((.B :: .ARG) :: (`(.A) :: .ARG)) "a"::"b"
INPUT: ("b" :: "a")
OUTPUT: ("b" :: "a")
Of course, sometimes there is infinite recursion, so Python limit get exceeded and I see this:
Infinite loop: ((`((.EV :: .ARG)) :: `(((.B :: .C) :: (.ARG :: .ARG)))) :: ((`(.ARG) :: .ARG) :: `((`((`(.D) :: `(.D))) :: (.B :: .B)))))
This is real joy! When I look at that script, it looks so logical.
Wow! Added to the library:
oMiser> .A ^bSAY
INPUT: "TRUE"
OUTPUT: "TRUE"
oMiser> .B ^bSAY
INPUT: "FALSE"
OUTPUT: "FALSE"
oMiser> (^bOR (^bTRUE, ^bFALSE)) ^bSAY
INPUT: "TRUE"
OUTPUT: "TRUE"
oMiser> (^bXOR (^bTRUE, ^bFALSE)) ^bSAY
INPUT: "TRUE"
OUTPUT: "TRUE"
oMiser> (^bXOR (^bTRUE, ^bTRUE )) ^bSAY
INPUT: "FALSE"
OUTPUT: "FALSE"
oMiser> (^bXOR (^bTRUE, ^bAND(^bTRUE, ^bFALSE) )) ^bSAY
INPUT: "TRUE"
OUTPUT: "TRUE"
oMiser> (^bXOR (^bTRUE, ^bAND(^bTRUE, ^bTRUE) )) ^bSAY
INPUT: "FALSE"
OUTPUT: "FALSE"
It is interesting, that certain problems, which look simple, are not easy to solve, eg:
swap(x :: y) -> y :: x
is easy, but if arguments may be enclosed - then there is no short solution.
Also, solution can not be found to "unenclose" to arbitrary depth:
``````````````x -> x
One more hard problem is to regroup the following pairs:
x :: (y :: z)
-> (x :: y) :: z
not quite sure why.
(but using SELF causes problems to the solver, perhaps, it needs timeout, so maybe unenclosing can be solved using SELF)
@rnd0101: t 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.
This sounds like it fits with the cookbook idea. It is especially important to see how to construct recursive procedures, as in the has
example.
There are idioms for manually abstracting from desired scripts. You saw that in the obapcheck.sml stages of cS, cK, has
, and hasX
checks. The derivation was the reverse. That is, SXYZ
was laid out first, as a pure-lindy-trace that would be the model for use of actual x, y, z obs as operands. Then lindy Z
was abstracted to derive SXY
, etc., until cS was obtained. Then the checks were used to confirm that the applications work. Finally, additional tests were used to confirm that well-known combinations, such as SKK, operate as expected using cS and cK, etc. Confirming has
is a little trickier because we need to confirm has(x) L with L having the idiomatic list form.
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:
^cS
= ...
; and this is pointed out here in #8. ::
infix operators. I am still pondering at #8 though.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?
@rnd0101: For example, it found the following script to swap pair's constituents:
oMiser> ((.B :: .ARG) :: (`(.A) :: .ARG)) "a"::"b" INPUT: ("b" :: "a") OUTPUT: ("b" :: "a")
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 ::).
ob ^swap = .EV :: (.D :: .ARG :: .B :: .ARG) :: ‵(.ARG :: .C :: (.B :: .ARG) :: .A :: .ARG);
providing a script such that ^swap x = if x = ob.b(x) then x else ob.c(ob.b(x), ob.a(x))
Notice how only one of the then or else arm is evaluated, as needed. That is also how has
always terminates on ^has(x) L.
So now the shell has two modes: with explicit eval and without one (default). Assignments do not use eval:
$ python shell.py
oMiser/Frugal syntax interpreter
Press Ctrl-D to leave.
oMiser> ^cS
(.C :: (`(.C) :: (.C :: ((.E :: (.C :: ((.E :: .ARG) :: `(.ARG)))) :: `((.C :: ((.E :: .ARG) :: `(.ARG))))))))
oMiser> ^cS .NIL
(.C :: (`((`(.NIL) :: .ARG)) :: (.C :: ((.E :: .ARG) :: `(.ARG)))))
oMiser> eval
Implicit eval now ON
oMiser> ^cS
(.C :: (`((`(.ARG) :: .ARG)) :: (.C :: ((.E :: .ARG) :: `(.ARG)))))
oMiser> ^cS .NIL
((`(.NIL) :: .ARG) :: (`(.ARG) :: .ARG))
Also I get rid of INPUT/OUTPUT because after implementing in-parser evals there is no parsed original input...
@rnd0101: One small check: both for assignment and input, right?
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 .of
or .ofrugal
for filename extension?
Yes, "assignment" (actually, binding) and input - those are oFrugal side. Should the prompt be 'oFrugal' also?
The longer extension maybe better.
@rnd0101: So now the shell has two modes: with explicit eval and without one (default). Assignments do not use eval:
Yes, the default cases are exactly what is needed. The eval cases break the ^cS definition, for example.
@rnd0101: Yes, "assignment" (actually, binding) and input - those are oFrugal side. Should the prompt be 'oFrugal' also? The longer extension maybe better.
Agreed. I think we are on the right track for this phase of development.
BTW, solver found shorter swap, which also handles enclosures:
oFrugal> ob ^swap = (.C :: ((.B :: .ARG) :: (.A :: .ARG)))
and what I like in this variant, is that is pretty straightforward.
Sure, if you don't mind that
^swap ob.NIL
yields ob.NIL :: ob.NIL
^swap lindy
yields lindy :: lindy
^swap ‵enc
yields ‵enc :: enc
Is the solver hypothesizing that x in ^swap(
x)
is of form t::
u`?.
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
ob ^swap = .C :: (.B :: .ARG) :: .A :: .ARG;
^swap (X :: Y)
should yield Y :: X
, and ^swap ^swap (X::Y)
should yield X :: Y
. It is that identity that suggest to me singletons should pass through unchanged.
Solver is very simple. I give it an "equation" like (it's in Pythonish frugal, list is for arguments here):
rules = [
(
[x],
(x)
),
(
[x ** y],
(y ** x)
),
(
[e(x) ** e(y)],
(e(y) ** e(x))
),
]
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. Then it spits all possible solutions with decreasing length, and stops at the depth it finds a solution. (ok, there is an optimization - solver "memoizes" up to millions of checked solutions plus all infinite loops solutions)
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.
I've added solver to the shell as well:
oFrugal> solve ^F(x::y) == y::x ;
Level: 3 Iters: 300000
(((.B :: .ARG) :: (.A :: .ARG)) :: (.NIL :: (.B :: .A)))
((.B :: (.B :: .ARG)) :: (.A :: (.ARG :: .C)))
(.EV :: ((.B :: .ARG) :: (.A :: .ARG)))
Inf: 2 Seen: 199682 Dups: 100318 Speed: 82179.0 IPS
oFrugal> ^F(a::b)
(b :: a)
oFrugal> ^F
(.EV :: ((.B :: .ARG) :: (.A :: .ARG)))
oFrugal> solve ^G(x, y) == x::y ;
Level: 3 Iters: 300000
.NIL
.A
Inf: 0 Seen: 200027 Dups: 99973 Speed: 102155.0 IPS
oFrugal> ^G(a, b)
(a :: b)
oFrugal> solve ^F(x, y, z) == x::z ; ^F(`x, `y, `z) == `x::`z ;
Level: 3 Iters: 300000
((.C :: `(.C)) :: (.E :: .ARG))
(.E :: ((.B :: .C) :: .ARG))
(`(.E) :: (.C :: .ARG))
(.E :: (.C :: .ARG))
Inf: 1 Seen: 199922 Dups: 100078 Speed: 84621.0 IPS
oFrugal> ^F(a,b,c)
(a :: c)
oFrugal> ^F(`a,`b,`c)
(`(a) :: `(c))
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:
oFrugal> solve ^F(x, y, z) == x::y::z ;
Level: 3 Iters: 300000
Inf: 2 Seen: 199820 Dups: 100180 Speed: 31272.0 IPS
Level: 4 Iters: 400000
Inf: 4 Seen: 466556 Dups: 233444 Speed: 32164.0 IPS
Level: 5 Iters: 500000
Inf: 11 Seen: 799366 Dups: 400634 Speed: 32523.0 IPS
Level: 6 Iters: 600000
Inf: 18 Seen: 1199573 Dups: 600427 Speed: 30989.0 IPS
Level: 7 Iters: 700000
Inf: 27 Seen: 1666171 Dups: 833829 Speed: 29022.0 IPS
Level: 8 Iters: 800000
^CAborted.
oFrugal>
oFrugal> solve ^F(x::y) == y::x ;
. . .
oFrugal> ^F
(.EV :: ((.B :: .ARG) :: (.A :: .ARG)))
OK, I think that givng ^F(x::y)
in the conditions to solve leads to a solution based on the assumption that the argument will be in form x::y
. The conditions for other forms of the argument are omitted. That is why it gets too simple of a solution.
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(^F
, x
) is going to produce eval( obap.ap(ob.b(x
), ob.a(x
)) ) and that obap.ap produces a pair only because you're running into the pure-lindy-trace rule. Then the eval simply reproduces the trace. The solver should not know about lindy-trace rules, and it should not assume that the variables are lindies. You want it to solve assuming arbitrary obs for x, y, z, etc.
I still think it is
ob ^swap = .C :: (.B :: .ARG) :: .A :: .ARG;
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 ^swap ^swap
x=
x, then you need to have ^swap
x=
x when x is a singleton instead of a pair. Hence
ob ^swap = .EV :: (.D :: .ARG :: .B :: .ARG) :: ‵( .ARG :: .C :: (.B :: .ARG) :: .A :: .ARG );
Try it without post-eval.
Yes, solver finds precisely what is asked. I may have asked for example:
oFrugal> solve ^F(x::y) == y::x ; ^F(
x::y) ==
y::x ;
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:
oFrugal> solve ^F(x::y) == y::x ; ^F(`x::`y) == `y::`x ;
Level: 3 Iters: 300000
Inf: 1 Seen: 199556 Dups: 100444 Speed: 71357.0 IPS
Level: 4 Iters: 400000
Inf: 4 Seen: 466306 Dups: 233694 Speed: 65708.0 IPS
Level: 5 Iters: 500000
Inf: 7 Seen: 799273 Dups: 400727 Speed: 51975.0 IPS
Level: 6 Iters: 600000
Inf: 15 Seen: 1199232 Dups: 600768 Speed: 39951.0 IPS
Level: 7 Iters: 700000
Inf: 29 Seen: 1665004 Dups: 834996 Speed: 36323.0 IPS
Level: 8 Iters: 800000
Inf: 39 Seen: 2000004 Dups: 1101607 Speed: 41301.0 IPS
Level: 9 Iters: 900000
Inf: 46 Seen: 2000011 Dups: 1401705 Speed: 53776.0 IPS
Level: 10 Iters: 1000000
Inf: 61 Seen: 2000026 Dups: 1735983 Speed: 51128.0 IPS
Level: 11 Iters: 1100000
Inf: 74 Seen: 2000039 Dups: 2102914 Speed: 46852.0 IPS
Level: 12 Iters: 1200000
Inf: 81 Seen: 2000046 Dups: 2502890 Speed: 45625.0 IPS
Level: 13 Iters: 1300000
Inf: 97 Seen: 2000062 Dups: 2935928 Speed: 43811.0 IPS
Level: 14 Iters: 1400000
Inf: 108 Seen: 2000073 Dups: 3401999 Speed: 41311.0 IPS
Level: 15 Iters: 1500000
(.C :: ((.B :: .ARG) :: (.A :: .ARG)))
Inf: 122 Seen: 2000087 Dups: 3901576 Speed: 39824.0 IPS
BTW, do you think I can add x == y
as equivalent for .D (x, y)
? What would be priority? (in PLs priority is usually quite low). Could be nice also to provide syntactic sugar for IF-THEN-ELSE
, what do you think? This way we will have some programming language.
oFrugal> (.D (^F(x::y), y::x)) ^bSAY
TRUE
will be:
oFrugal> (^F(x::y) == y::x) ^bSAY
TRUE
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:
f (x, y) === (convert f) (x::y)
that is, for "function" of two arguments construct a new equivalent function, where arguments are in the pair.
I am finding the following useful as an evaluation indicator:
oFrugal> ^indicator
(.NIL :: evaluated)
oFrugal> ^indicator .NIL
evaluated
2-3 different indicators are also useful:
oFrugal> ^swap (^indicator :: ^indicator2 )
((.NIL :: evaluated2) :: (.NIL :: evaluated))
oFrugal> ^simpleSwap (^indicator :: ^indicator2 )
evaluated2
(simpleSwap is that "buggy" naiive swap)
@rnd0101 I was also thinking if some kind of conversion function (for standard lib) for situations where one wants to convert a pair into arguments
In this case,
convertF = (`(F) :: (.A :: .ARG) ) :: .B :: ARG
convert = .C :: ( .C :: (.E :: .ARG) :: ‵ (.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.
BTW, typos above: (.E .ARG)
-> (.E :: .ARG)
, but I of course got the point, thanks!
I am trying to find some parallels with Python:
def g((x, y)):
return x + y
def curry2(gg):
def f(q):
def fq(z):
return gg((q, z))
return fq
return f
def convert(F):
def ff((a, b)):
return F(a)(b)
return ff
def lcurry2(gg):
return lambda q: lambda z: gg((q, z))
def lconvert(F):
return lambda (a, b): F(a)(b)
print (curry2(g))("a")("b")
f = curry2(g)
print (convert(f))(("a", "b")), f("a")("b")
print (lcurry2(g))("a")("b")
f = lcurry2(g)
print (lconvert(f))(("a", "b")), f("a")("b")
So, curry will have double lambda while convert (uncurry?) has double application - single lambda... But that gg
needs to be propagated through those lambdas (in Python, scopes do their job).
Please, do not spoil it yet.
def curry2(gg):
def f(q):
def fq(z):
return gg((q, z))
return fq
return f
def convert(F):
def ff((a, b)):
return F(a)(b)
return ff
look like the right idea to me. Is F(a)(b)
the same as (F(a))(b)
in python?
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: