Preserve Beta-Normal Eta-Long Form

[mlb2251]

Beta-normal eta-long form

This is the form that dreamcoder programs are in.

• beta-normal: there are no redexes aka no unapplied lambdas aka nothing of the form (lambda body) arg
• eta-long:
  • All arrow-type subterms are either the left hand side of an application (ie they're immediately applied to some argument) or they're a lambda term.
  • This mainly comes up when passing functions into higher order functions. map double xs isn't allowed because double has an arrow type yet is not syntactically lambda and is not syntactically immediately applied to any arguments. Instead this should be eta-expanded to become map (lambda (double $0)) xs. Specifically the eta-expansion of e is (lambda (upshift(e) $0)). For an arity-2 expression eta-expansion would look like (lambda (lambda (e $1 $0))) which you can get by just applying eta expansion twice in a row, specifically look for a term thats an arrow type but isnt applied to anything and eta-expand it. So we get foo -> (lambda (foo $0)) -> (lambda (lambda (foo $1 $0))) where in the second eta expansion we didnt do another eta expansion of foo since it was already applied to an arg, but we saw that foo $0 is itself an arrow type so we eta expanded it.

If you're familiar with dreamcoders topdown search that's an easy way to think about this. Since it never produces unapplied lambdas it is clearly maintains beta-normal form, and since it autofills lambdas whenever it encounters an arrow-typed hole this maintains eta-long form.

Maintaining eta-long form during compression

• Rewriting a set of programs with a new primitive can break the eta-long form of dreamcoder if you aren't careful.
• Specifically, if you abstract an arrow-type term to use as an argument to your invention, you can break eta-normal form because you've created a HOF argument.
• For example if (double 5) showed up in the original set of programs and we abstracted double we'd end up with double as an invention argument, but since double is an arrow type it should be written like (lambda (double $0)) when used as an argument
• Stitch is not type-aware at compression-time, however if we assume that the input set of programs is in beta-normal eta-long form then we can actually detect arrow-types.
  • Since in eta-long form a function primitive is always immediately applied to all of its arguments, and non-functions are of course never applied to arguments, we can just look at chains of applications to whether a term is an arrow type and what its arity is.
• So whenever we do abstraction (which is the only way we modify the program and thus the only way we break eta-expansion) we can use this to check the arity of the term we're abstracting and eta-expand it that many times. In short, just look at how many Apps are directly above you (where you are always the function argument) and add that many apps + lambdas above you when you move into the argument position

Todo think about:

• [ ] What happens when you have (lam (lam foo $1 $0)) and you abstract it at various points?
  • abstracting the whole thing is fine bc your HOF input has its lambdas and all is well
  • abstracting just the inner lambda will create a term with free variables that will need 1 lambda before it's closed
  • abstracting foo $1 $0 will create a term with free variables that will need 2 lambdas before it's closed
  • note that in the above two cases i think the auto-adding of lambdas would end up looking realllly gross in the way it affects the invention body? Or maybe it wouldnt idk I have to do it out
  • abstracting foo $1
  • abstracting foo
  • gotta think about all these cases, arent they all ultimately going to be rebuilt into the same lam lam foo $1 $0 as an argument? I guess if you actually had something like foo 5 7 instead though the abstractions would have to be different. I don't know exactly but worth thinking this all through
• [ ] what exactly will this arity-checker look like, in both the abstraction case and the rewriting case? Should we do it top down or do it with an on-the-spot check? Can we precompute every terms arity beforehand for simplicity and if so exactly what will that look like?
• [ ] we should preserve all this eta-long beta-normal stuff in a readme somewhere for the future!

[mlb2251]

Not urgent since Gabe is doing eta-expansion on their end, however we absolutely do want this for dreamcoder-identicalness

[mlb2251]

Studying the current cases where dreamcoder fails in EtaLongVisitor:

Here's a crash example:

from dreamcoder.program import Program
from dreamcoder.domains.logo.logoPrimitives import turtle
from dreamcoder.type import arrow
from dreamcoder.program import EtaLongVisitor
EtaLongVisitor(request=arrow(turtle,turtle)).execute(Program.parse('(lambda (#(lambda (lambda ($1 (lambda (#(lambda (logo_PT (lambda (logo_FWRT $1 logo_ZA $0)))) logo_UL ($1 (#(lambda (logo_PT (lambda (logo_FWRT $1 logo_ZA $0)))) logo_UL (#(logo_FWRT logo_UL logo_ZA) $0)))))))) (#(lambda (lambda (logo_forLoop $1 (lambda (lambda (logo_GETSET $2 (logo_FWRT logo_ZL (logo_DIVA logo_UA $3) $0))))))) 6) (#(lambda (#(lambda (lambda (logo_forLoop $1 (lambda (lambda (logo_FWRT (logo_MULL logo_UL $2) (logo_DIVA logo_UA $3) $0)))))) $0 1)) 5) $0))'))

It turns out the line self.context.unify(request, ft.returns()) in EtaLongVisitor is to blame. This is because ft actually returns a t0 which can (and should in this case) actually become an arrow type turtle -> turtle which effectively adds one extra argument. However, this line unifies t0 with the request (which at this point in the recursion is just turtle) forcing t0=turtle.

So more generally I believe that this means when you try to unify some function type with its list of arguments you should from left to right across the arguments because things like t0 can expand into arrow types that actually add more arguments as you go! So unifying directly with the return type instead of traversing across the list of arguments can fail in these cases.

The solution is to add some code right before self.context.unify(request, ft.returns()) that does:

for i,x in enumerate(xs):
    self.context.unify(
        ft.functionArguments()[i],
        x.infer().instantiateMutable(self.context))
    ft = ft.applyMutable(self.context)

I'd love someone to review this because I have not actually worked with applyMutable() instantiateMutable() or unify() before.

I'll push this to the laps repo

[mlb2251]

de-escalating from critical. Might be nice to add but is nontrivialded

[mlb2251]

So more generally I believe that this means when you try to unify some function type with its list of arguments you should from left to right across the arguments because things like t0 can expand into arrow types that actually add more arguments as you go! So unifying directly with the return type instead of traversing across the list of arguments can fail in these cases.

Actually this is not correct. Well, it's correct except that if you think about how top down synthesis works you always unify the RETURN type of each primitive with your hole, so you DO always unify the return type and you never go left to right across the arguments.

[mlb2251]

This should be considerably easier now that we have types :) we just need to include the types in compression ofc

[mlb2251]

see also my notes 2023-01-09 adding eta expansion to stitch