Reasoning about fexprs through abstract interpretation

[Andres Navarro]

Sorry I wasn't paying much attention to klisp this last semester.  I was concentrating of finishing my bachelor degree and had to take a break, but I'm back now.  My idea is to resume work on klisp (continue the thread branch) in februrary.

In the meantime, I just made public a project I've been working on for the last couple of weeks: https://bitbucket.org/AndresNavarro/fklisp.  I had this idea a while ago, but I couldn't work on it until now (see http://lambda-the-ultimate.org/node/4346#comment-66884).

fklisp (as the project is currently named) takes a stab at the problem of analyzing in which environments the symbols of a Kernel expression are evaluated.  It tries to do this through abstract interpretation of the expression.

Only a functional (pure) dialect of Kernel is supported in order to simplify this problem, but maybe in the future we can try to lift that restriction, although it probably won't be an easy task.

I'll write about the details in another mail some of these days, but I wanted to announce this as I am starting to get some encouraging results.

The idea is that after analyzing the environment in which the symbols of the expression are evaluated, it replaces some of them with either primitive combiners or direct accesses to the environment (to avoid looking for the correct bindings at run time).  There is still no support for executing the resulting expression (no way in klisp to access the environment directly), but you can see the result (the symbols are marked with angle brackets for visualization (e.g. 'cons' becomes '<cons>' because it is a primitive applicative and 'ls' may become '<ls><0,1>', i.e. a direct access to the current environment for the first binding).

As far as I can see, the results are correct (i.e. the algorithm is conservative in the symbols it replaces, if it can't prove that a symbol always evaluates to some primitive combiner or is in a specific position in the environment it leaves it intact).  Details of how it manages to do this are to follow soon.

It is currently able to replace all symbols correctly (it doesn't miss any opportunity) in a bunch of derived combiners for the fklisp dialect.  That file (derived.k) contains about 50 combiners in around 100 lines of fklisp code.  While many of the combiners are one liners (like car, cdr, caar, etc) there are also recursive combiners (like list?, $cond, $or?) and higher order applicatives like map, which are themselves used to define other combiners there (like $let). All of this takes under 4 seconds in an Intel i7 (pretty neat considering it is written in Kernel and running in klisp).

The code needs a lot of cleaning, but once the debug code is removed it's about 1500 lines of code.

I would love some feedback on this, if anyone wants to give it a spin.  You just need to load the file fklisp.k in klisp (you may need to copy the klisp executable to the fklisp folder or set the KLISP_PATH variable  in order to run it, ask me if you have any problems).

There is no documentation for now, but I intend to clean this up and add some by next weekend.

Regards,

Andres

[Oto Havle]

Hi Andres,

it is quite impressive.

On 22.1.2013 08:22, Andres Navarro wrote:
> [...]

> The idea is that after analyzing the environment in which the symbols of
> the expression are evaluated, it replaces some of them with either
> primitive combiners or direct accesses to the environment (to avoid
> looking for the correct bindings at run time). There is still no
> support for executing the resulting expression (no way in klisp to
> access the environment directly), but you can see the result (the
> symbols are marked with angle brackets for visualization (e.g. 'cons'
> becomes '<cons>' because it is a primitive applicative and 'ls' may
> become '<ls><0,1>', i.e. a direct access to the current environment for
> the first binding).
>

I may be mistaken, but is it related to alpha-conversion? Could fklisp,
with some changes, do transformations like this:

($let ((a #t)) ($let ((a ($lambda (a) a))) a))
=>
($let ((x #t)) ($let ((y ($lambda (z) z))) y))

?

> [..] All of this takes under 4

> seconds in an Intel i7 (pretty neat considering it is written in Kernel
> and running in klisp).
>

It takes about 20s on an old Pentium 4, with these definitions added:

($quote (x) #ignore x)
(vv () (eval ($quote ww) (get-current-environment)))
(ww () (eval ($quote vv) (get-current-environment)))
=>
($quote (x) #ignore <x><0.0>)
(vv () (<eval> (<$quote><1.48> <ww><1.51>) (<get-current-environment><1.32>)))
(ww () (<eval> (<$quote><1.48> <vv><1.50>) (<get-current-environment><1.32>)))

Defining mutually recursive functions, while looking under $quote. Cool.

This takes somewhat more time:

($quote (x) #ignore x)
(dl (x e) (eval (list $lambda (list $quote a) x ($quote a) ($quote b)) e))
(f (a x) (dl x (get-current-environment)))
=>
($quote (x) #ignore <x><0.0>)
(dl
(x e)
(<eval>
(<list><1.0>
<$lambda><1.33>
(<list><1.0> <$quote><1.48> a)
<x><0.0>
(<$quote><1.48> a)
(<$quote><1.48> b))
<e><0.1>))
(f (a x) (<dl><1.49> <x><0.1> (<get-current-environment><1.32>))))

Why is the symbol "a" in (list $lambda ...) not solved here?

> [..]

Oto Havle.

[Andres Navarro]

On Tue, Jan 22, 2013 at 8:01 PM, Oto Havle <havl...@gmail.com> wrote:

I may be mistaken, but is it related to alpha-conversion? Could fklisp,
with some changes, do transformations like this:

($let ((a #t)) ($let ((a ($lambda (a) a))) a))
=>
($let ((x #t)) ($let ((y ($lambda (z) z))) y))

While the mechanism used by klisp it's not directly related to alpha conversion, it is certainly possible to implement something like this.  I put something there in the TODO file about separating the basic engine of the rest, I think mozilla implemented something like that for their javascript partial evaluator.

Currently klisp only register for each symbol in the original expressions the result of the evaluations (to see if it's always the same primitive combiners) and the position in the environment chain of bindings, to see if a direct access is possible.  You could certainly add to this by registering the bindings present in each environment that the symbol is evaluated, to be able to do alpha conversion without collisions.

 

It takes about 20s on an old Pentium 4, with these definitions added:

Tell me about it.  I actually developed this on an Atom based netbook... It took about 30 secs with just the code in derived.k...  

There's certainly some low hanging fruit to optimize (e.g. there's a cache that records the result of evaluating combiners in different environments which is used to find fixpoints for recursive and mutually recursive combiners in the presence of uncertainty.  This cache is actually a list and a check in the cache is a worst case O(n*m) lineal search in a list of pairs (expression environment), where n is the length of such list and m is the number of pairs in the expression.  This can be easily replaced by a hashtable which precalculated hashcodes for all tagged objects, since they are immutable).

Of course it could also be written in another language too (either a low level one like C, or why not ML or Haskell, it could also run faster if ported to scheme, which is a much easier port).  However my plan is to actually run it on itself so I went with kernel first with an intention of eventually rewriting it if fk-lisp itself (I will have to do some additions like numbers, etc)

 

This takes somewhat more time:

  ($quote (x) #ignore x)
  (dl (x e) (eval (list $lambda (list $quote a) x ($quote a) ($quote b)) e))
  (f (a x) (dl x (get-current-environment)))
=>
  ($quote (x) #ignore <x><0.0>)
  (dl
   (x e)
   (<eval>
    (<list><1.0>
     <$lambda><1.33>
     (<list><1.0> <$quote><1.48> a)
     <x><0.0>
     (<$quote><1.48> a)
     (<$quote><1.48> b))
    <e><0.1>))
  (f (a x) (<dl><1.49> <x><0.1> (<get-current-environment><1.32>))))

Why is the symbol "a" in (list $lambda ...) not solved here?

I may be missing something... do you intend 'a' to be evaluated in which environment? The environment of f, that is passed to dl in argument e?  That's not what the above code does.  It evaluates 'a' in the environment of dl which doesn't have such binding.  If you wanted to include a quoted 'a' as argument to $lambda maybe you meant (list $lambda ($quote (a)) ... The abstract interpreter could certainly issue a warning in this case, it has all the info needed for that..

Please also note that in fklisp $lambda only takes two arguments (i.e. the body is just one expression).  This is because as there is no mutation, there's no need for multiple expressions in the body.  I'm not sure what you are trying to do here, but maybe you want to do inside the body (list ...) to eval various expressions.

 

I hope this was helpful, feel free to ask anything else about this, 

I'll try to write a piece with some implementation details in the near future,

Regards