Re: unification

Re: unification

[stefan]

Hi,

This will give some ideas of how I prefere to handle
unification. I add a few extra instructions. And I do not
expect you to swallow that. But at least it is a beutiful 
idea.

Consider an example of a unifing matcher e.g.

(def f ((a _) a) 
       ((c b) b))

currently this compiles to

,x f

Disassembly of #<procedure f (arg121)>:

   0    (assert-nargs-ee/locals 25)
   2    (unify-init)
   3    (br :L142)                      ;; -> 19
   7    (local-ref 0)                   ;; `arg121'
   9    (unify-cons)
  10    (local-set 1)                   ;; `a'
  12    (unify-cons)
  13    (drop)
  14    (make-eol)                      ;; ()
  15    (unify-eq)
  16    (local-ref 1)                   ;; `a'
  18    (return)
  19    (br :L143)                      ;; -> 36
  23    (local-ref 0)                   ;; `arg121'
  25    (unify-cons)
  26    (local-set 3)                   ;; `c'
  28    (unify-cons)
  29    (local-set 2)                   ;; `b'
  31    (make-eol)                      ;; ()
  32    (unify-eq)
  33    (local-ref 2)                   ;; `b'
  35    (return)
  36    (toplevel-ref 1)                ;; `error'
  38    (object-ref 2)                  ;; "no match in f"
  40    (tail-call 1)

2 initiates and stors the (br :L142) location if we need to jump to the 
next match, then executes 7  (this can be made better)

7.  pushes argument
9.  do a unifying cons. essentially (push cdr) (push car)
    but the unifying flavor. if not a cons go to L142 and initiate
10. set a to the pushed car and pop the car
12. do another cons sequence
13. pop
14. push '() and then check if eq? with the cdr
then the resulting code is executed.

if there is a failure we jump to 19, initiates the new next jump as :L143
and continue as before.

here is the code for unify-cons in c.


#define UNIFY_MODDED				\
  {						\
  if(!unify_modded)				\
    unify_modded = (int) SCM_UNPACK(gp_newframe());	\
  }

#define UNIFY_FAIL				\
  {						\
    if(!unify_modded)				\
      gp_unwind(FI_TO_SCM(unify_modded));	\
    ip = match_next;				\
    sp = stack_next;				\
    NEXT;					\
  }

VM_DEFINE_INSTRUCTION(123, unify_cons, "unify-cons",0,0,0)
{
  gp_lookup(GP_GETREF(*sp));
  sp--;
  if(GP_CONS(gp_ret.ref))
    {
      PUSH(GP_UNREF(gp_ret.id + 3));
      PUSH(GP_UNREF(gp_ret.id + 1));
      NEXT;
    }	  
  if(gp_ret.val == 0) //variable
    {
      SCM *ref;
      UNIFY_MODDED;
      ref = GP_GETREF(gp_mk_cons());
      gp_set_ref(gp_ret.id,GP_UNREF(ref));
      PUSH(GP_UNREF(ref + 3));
      PUSH(GP_UNREF(ref + 1));	    
      NEXT;
    }
  
  UNIFY_FAIL;
}

Have fun
/Stefan

unification

[stefan]

Hi,

I did a small try to extend guile to handle unification. The result is in

http:///c-lambda.se/gp.tar.gz

In there is an example of a unification solution of the Einstein riddle.
The solution takes 150ms on my PC. Gnu prolog execute it in about 16ms.
I'm using a c-extension linked in which is a fun play with the tagging system 
in guile (ducks!)

So not so bad. But there is a nice abstraction that lies behind this code that 
can be useful. So I would like to snow in and try to make this abstraction 
solid (You may be scared of the code) and perhaps even faster. What options
do I have to make it as fast and, if you are interested, please reply.

By the way. I can help out as well. My main interest now is in type theory but 
I start to dig into guile now and I would probably be able to help out if you 
like in a short time, as my knowledge matures.

 Are there any suitable tickets to close?

Regards
Stefan

Re: unification

[Ludovic Courtès]

Hello!

stefan <stefan.tampe@spray.se> writes:

> I did a small try to extend guile to handle unification. The result is in
>
> http:///c-lambda.se/gp.tar.gz
>
> In there is an example of a unification solution of the Einstein riddle.
> The solution takes 150ms on my PC. Gnu prolog execute it in about 16ms.
> I'm using a c-extension linked in which is a fun play with the tagging system 
> in guile (ducks!)

I haven’t looked at the code but that sounds like an interesting and
useful project!

If I were you I would write the unification code in Scheme, at least as
a starting point, esp. since I would expect most optimizations to be
done at an algorithmic level.

Then you could implement the hot spots in C, if that turns out to be a
real advantage, or simply wait until Guile gets a native compilation
back-end, JIT, or both.  :-)

> By the way. I can help out as well. My main interest now is in type theory but 
> I start to dig into guile now and I would probably be able to help out if you 
> like in a short time, as my knowledge matures.
>
>  Are there any suitable tickets to close?

You could look at the bugs in
<http://savannah.gnu.org/bugs/?group=guile>, along with posts on
<bug-guile@gnu.org> left unanswered.  And of course, you could do
testing under all possible conditions, or look at the code and improve
the bits that please you.  :-)

Besides, there’s an informal to-do list in the minds of some of us for
2.0, and that list is getting small.

Thanks,
Ludo’.

Re: unification

[Andy Wingo]

Hi Stefan,

On Tue 13 Apr 2010 13:55, ludo@gnu.org (Ludovic Courtès) writes:

> stefan <stefan.tampe@spray.se> writes:
>
>> I did a small try to extend guile to handle unification. The result is in
>>
>> http:///c-lambda.se/gp.tar.gz
>>
>> In there is an example of a unification solution of the Einstein riddle.
>> The solution takes 150ms on my PC. Gnu prolog execute it in about 16ms.
>> I'm using a c-extension linked in which is a fun play with the tagging system 
>> in guile (ducks!)
>
> I haven’t looked at the code but that sounds like an interesting and
> useful project!

Agreed! I looked briefly at the code, but this is one of my many
ignorant areas.

I would also suggest implementing this in Scheme, as a macro. That way
you program as in prog.scm, but when it's expanded, it expands out to
the exact thing you need to do the job. A macro extends the compiler
with support for a mini-language -- something like prolog in your case.

>> By the way. I can help out as well. My main interest now is in type theory but 
>> I start to dig into guile now and I would probably be able to help out if you 
>> like in a short time, as my knowledge matures.
>>
>>  Are there any suitable tickets to close?

Besides the points Ludovic mentioned, if you are interested you could
try writing a type inferencer for tree-il. Do it as a weak map from
tree-il to some type representation, then propagate down to the leaves
and back. At least, that will work for many cases -- you might know a
better implementation strategy.

Have fun with Guile,

Andy
-- 
http://wingolog.org/

Re: unification

[stefan]

I did a reference implementation of unification code in pure 
scheme. It is just 185 lines of code (the rest is the test case)

see http://c-lambda.se/unify.scm

Some timings for the example
============================
scheme-version     > 2100 ms
c-initial-guile    > ~150 ms
current-best-guile >   73 ms 
sbcl               >   25 ms
gprolog            >  ~20 ms

So I've been able to tweak out 2x in guile + c

So what next?

This is what I will be playing with.
one need apart from a unification primitive also
be able to destruct a pattern into variable references
this can be done in a vm on a stack machine. And I will
now go on to let this vm be the guile vm itself. Later 
on when we the compiler starts to shine, I could hook into
that as well and generate target code. So this litle play will
spill over into being useful for the compiler later.
/Stefan