The logic at my fingertips

Guile log is an exploration of logic programming where one can choose to maintain the state in a stack or on a translation list like in kanren. Actually guile-log contains an implementation of the kanren interface that are as fast or faster as the original kanren distribution compiled on chicken ( a scheme environment).

The bad thing is that one need to track the state in more advanced application for which a state which is a combination of a mutual structure and the old cons list. Also this means some overhead and makes things complicated!

The good part is that one can combine the speed of the stack based solution found for example in gprolog with the generality and thread friendly solution that kanren provides.

If one like to just stick to the kanren approach one can take advantage to the stack in many ways which makes the coding experience richer. The basic principle is that you get a notion of going back and forth in time between different states and this walk can be traced to understand more about the program and enable some features

One of the features is to code with meta global variables (my naming). They behave as global variables with respect to computation e.g. storing values over backtracking cycles which means that one can enter sub backtracking regions that need to store for example a list of all results and use that list
as a value. The meta comes from the fact that these variables will behave as normal stack variables / kanren variables in the higher level backtracking where the list of results are used. Also when storing the state and restoring the state these variables will follow and be restored correctly.

Guile log is therefor ideal to use in an interactive proof solver for example because you can work from the guile prompt all the time and have all of guile log and guile scheme at your fingertips and e.g. be able store states try a branch go back, go forth and so on.

maybe one day I will port the coq prover to guile-log or something similar.

Aschm! not a cold just a combination of assembler and scheme

But most of my current time has been on hacking on the internals of guile. Wingo has started coding on a new VM for guile based on a register layout e.g. using local variable index in stead of pop and push to get and set local variable data. I on the other hand have ported SBCL's assembler (see aschm on gitorious) and implemented translations of the original VM and the new RTL VM to native code. Quite fun indeed and can show the speed benefits and overhead of using this.

maybe you can by a factor of 2x going to the RTL VM and another 3x compiling to native. To note here is that much of the overhead comes from the fact that all operations usually have some overhead, for example trying looping around and summing an incrementor e.g. calculating 1 + 2 + 3 ... would mean maybe 250Million additions per seconds for nativly compiled version. This is adding guile fixnums and there is some overhead of managing these datatypes, also the RTL feature is transfered to the native one as well e.g. the natively compiled code does not use the registers as much as one can do.

native logically yours

Stefan