einstein riddle

[snorgers]

Hi,

I've been busy coding for some time. I now have a working basic
framework. This framework can be used to combine backtracking and
unifications to builed prolog like features. E.g. in my view a natural
building block to spark Shen from.

The last couple of week's I've been focusing in understanding how to
get the prolog part and hence also
the type-checking to be fast.

For the einstein ridle I get 19ms (SBCL). Using gnu prolog I get
16-20ms. This ends my worry that Shen would be too slow on the java
virtual machine. QiII runs this program in about 260ms.

/Stefan

[Raoul Duke]

> For the einstein ridle I get 19ms (SBCL). Using gnu prolog I get
> 16-20ms. This ends my worry that Shen would be too slow on the java
> virtual machine. QiII runs this program in about 260ms.

that is pretty exciting news! congratulations :)

sincerely.

[snorgers]

Hi,

The previous result was for manually cleaned lisp code aka proof of
method. Now
after making this cleaning as part of the compilation auto-generated
lisp takes 21ms
to solve the Einstein riddle. In the process code has been tested and
bugs squashed.

I also prepared the code in a state so that it can experimented with
(if you feel so) follow
the instructions in the BoopCore directory on the Shen project on
github.

Beware that the code is under constant flux.

/Stefan

[stever]

Hi Stefan,

I'm new to Qi and I get the impression that you are porting Qi to
Clojure.
I haven't seen any description of the plans for Shen and was wondering
if you are considering the Clojure work the basis of Shen?

I've been away from Lisp and functional programming for quite a while,
but I really like what Mark has done with Qi. When I get up to speed
more I may try to help.

Steve

[snorgers]

The idea is that Shen will be a version of QI that work on "any" lisp
like platform.

The approach is to write a set of core libs in qi and then make a
compilation
to selected platforms like clojure and CL.

The conclusion I draw from that was that the prolog engine in qi had
to be
rewritten. As a consequence the code is
more then 10x faster on the test case above. This code will be brought
over to the java environment and there will be a loss of performance
but I don't think
that the penalty will be too much so that the type checking will
suffer.

I sieved out these core part and called it BoopCore. (It was the first
name that struck my
mind) I believe that this core part should live it's own "life" and
will probably try to focus to
make that part really good. On top of this you can attach the classic
prolog part of Qi, you can
build a corresponding Qi-Yacc part, Reader, Writer etc and then you
will have Shen.

So is there task to be taken. Well one of the design decisions I took
was to work with a classic CL labels construct
in stead of a nested if's, this has the advantage that you can very
easy transform a pattern matcher and make it a state
machine. And there should not be a loss of performance. Actually SBCL
is quite good at seeing these simplifications e.g.
tail call optimizations, and I would like to have a corresponding
notion in clojure. Now it is trivial to translate the common cases
to a tagbody but clojure doesn't have them either, so you need to
simulate those with quite a significant overhead. As Mark pointed out
you can leave out some optimizations and translate it back to a cond
construct or a nested if construct.
doing this transformation is not difficult and could be the way to go.
Of cause you could stick with a classic translation
to lambdas but again the performance will not be good. On the other
hand there looks like there is a notion of goto in the languish spec
for the virtual machine so it would actually be possible to implement
tagbodies in the java environment suitable to handle our case. with
our simple structure of tail calls. The problem is that tagbodies need
to handle the scope of dynamic variables and exceptions correctly. I
actually made a compilation step that did this work last week for a
similar task in the Boop code handling the unification and
backtracking. So it's not that difficult to do.

Anyway It would be nice to have a discussion about such a feature and
maybe the clojure people would appriciate such a feature so that they
included it in the clojure itself.

I would welcome you help and insights.

Regards
Stefan

[snorgers]

OK, I've replaced define with def in the Lambda.qi file and called it
Lambda.boop.qi
It now can compile itself. The next step is to spend a week writing
tests for it.

The plan is then to start write a typechecker that is turned on all
time that use type driven code
generation to generate target code e.g. lisp and clojure ... it will
have the option to run under
different modes aka (tc -) and (tc +)

/Stefan

[stever]

Thanks for the explanation.
I had a different impression from Mark's original Shen proposal.
It really clears up the approach you are taking.
I've got a lot to learn before I will have any insights ;-)

[Mark Tarver]

Just dropped in; looked at the code for Shen. Interesting; some
questions to reflect on though.

1. The 10X speedup sounds great but some details would be good. How
is the speedup gained? What does the generated Lisp code look like?

2. What is the declarative meaning of u? I guess it means 'unifies'.

(define foo [X | Y] -> Y) can be interpreted equationally as forall
X, Y foo(cons(X, Y)) = Y. This is important in formal methods since
it provides (modulo ordering) a transcription of a Qi program into an
axiomatic semantics (equations) for the program. But (define foo (u
[X | Y]) C -> Y means forall X, Y foo (u (cons X Y)) C = Y meaning
what? unification is a two place function not a 1 place.

The u is really a *procedural* tag saying 'Do unification here' but
its construction looks a little orthogonal to the rest of Qi. What is
the declarative reading of this construction?

3. How is this u construction to be type checked and how are the
math'l proofs in FPQi to be extended to guarantee this construction?

No need for a fast reply to all this. This is really for the developer
(s) to think on. I'm doing other things and drop in only occasionally.

Mark

[snorgers]

Hi Mark,

Good to see you back and great questions

On 1 Nov, 18:35, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:
> Just dropped in; looked at the code for Shen.  Interesting; some
> questions to reflect on though.
>
> 1. The 10X speedup sounds great but some details would be good.  How
> is the speedup gained? What does the generated Lisp code look like?

i) I decided to manage the stack explicitly with a simple array,

ii) I decided to see the impact of an array of cons cells and
allocations of cons cells for
many operations that is done from this stack hence there is a lot
less consing going on

ii) I try to manage stack frames intelligently and make use of these
stack frames. I also keep
track of the changes and two changes (Iookup may reset value pointers
hence there might be many changes)
in one stack frame will result in just one resetting (the first one)
when we undo the stack frame.

iii) A variable is a fixnum e.g. an index in a variable stack, numbers
will be translated to other a special
object and managed internalle. Therefore there is a need to translate
data in and from this unifcation and
match environment, this has to be done either way because symbol is
not as well handled as in CL in other platforms
also integers have usually fast tests on all platforms and numbers is
not that common in the type declarations.

iv) The generated code for all part of the def is factorizing meaning
that the same prefix in the pattern matcher will mean
that the code share the prefix logic, actually this is used for
segments and Yacc like features as well, but then the sharing
have a semantic meaning as well e.g. more powerfull and faster but
more difficult because of possible buggs - this is a feature that we
need to discuss.

v) I stared at the generated ASSEMBLER for two weeks.

> 2. What is the declarative meaning of u? I guess it means 'unifies'.

yep (u X) means unify argument

> (define foo [X | Y] -> Y)  can be interpreted equationally as forall
> X, Y foo(cons(X, Y)) = Y.  This is important in formal methods since
> it provides (modulo ordering) a transcription of a Qi program into an
> axiomatic semantics (equations) for the program.  But (define foo (u
> [X | Y]) C -> Y means forall X, Y foo (u (cons X Y)) C = Y meaning
> what?  unification is a two place function not a 1 place.

You can skip (u) and segment parts. The reason not to separate a tool
for
segmentation, a tool for unification, a tool for yacc a tool for
define is that a lot
of logic carries over in one way or the other to the other parts and
you can
separate those part in the higher level routines. But logically you
should combine
them at the wizard level. By the way have you though about trying to
unify segmentation constructs?

> The u is really a *procedural* tag saying 'Do unification here' but
> its construction looks a little orthogonal to the rest of Qi.  What is
> the declarative reading of this construction?

There is three modes of operation
- good old define world segmentation tiny yacc etc.
u unifies data in the unification world
m matches data in the unification world

so
(def (u U) (u [U|Y]) ....
will try to unify the first argument with the car of the second
argument.

> 3. How is this u construction to be type checked and how are the
> math'l proofs in FPQi to be extended to guarantee this construction?

Again you can perhaps in the final product separate out constructs
that are pure, But the
idea is to generate valid qi code that can to be type-checked in the
various modes. so I would
consider looking at the output qi code to decide on this.

Oh, please have a look at the reader.qi file in the BoopCore
directory, I did that code just as a
test.

[snorgers]

Here is generated lisp for "member"


(DEFUN member (V1466 V1467 V1468)
(LABELS ((g285 ()
(LET ((X1430 (lookup V1467)))
(IF (CONSP X1430)
(LABELS ((g287 ()
(IF
(EQ (PROGN (newframe) (unify V1466 (CAR
X1430)))
'true)
(IF (EQ (FUNCALL V1468) 'false)
(PROGN (unwind) (g286))
(PROGN (unwind) 'true))
(PROGN (unwind) (g286))))
(g286 ()
(LET ((L (CDR X1430)))
(member V1466 L V1468))))
(g287))
(IF (var? X1430)
(LABELS ((g287 ()
(LET ((L (var!)))
(LET ((K1464 (mycons V1466 L)))
(IF (EQ (circular? X1430 K1464)
'true)
(g286)
(PROGN
(PROGN
(newframe)
(setvc *wrap* X1430
K1464))
(IF (EQ (FUNCALL V1468)
'false)
(PROGN (unwind) (g286))
(PROGN (unwind)
'true)))))))
(g286 ()
(LET ((Y (var!)))
(LET ((L (var!)))
(LET ((K1465 (mycons Y L)))
(IF (EQ (circular? X1430
K1465) 'true)
(g284)
(PROGN
(setvc *wrap* X1430
K1465)
(member V1466 L
V1468))))))))
(g287))
(g284)))))
(g284 ()
'false)
(g283 ()
(error "partial function member")))
(g285)))

On 1 Nov, 18:35, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:

[snorgers]

> The u is really a *procedural* tag saying 'Do unification here' but
> its construction looks a little orthogonal to the rest of Qi. What is
> the declarative reading of this construction?

This is actually an interesting question (maybe I'm missing the point
but oh well)

consider
def f (u [(m X) Y]) Cont -> ...

now if the input to the function is unbound it will be bound to [X Y]
but this is not enough.
you should bind it to (u [(m X) Y]) and then in the unifications done
later one needs to make
sure the meaning of u and m is preserved

I guess something like this logic has to be used

(u X) ~ (m Y) -> Y <- X
(u X) ~ (u Y) -> X <- Y or Y -> X
(m X) ~ (m Y) -> backtrack if not equal bounded values
(m X) ~ (u Y) -> X <- Y

I'm not convinced that we need to implement this logic though, because
the use cases I've seen
(help me here) work quite ok with a weaker but faster version where if
somethings get the mode u,
then every dependents is under the u mode as well.

/Stefan

On 1 Nov, 18:35, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:

[Mark Tarver]

OK; the timing improvements to the Prolog are very good.

Now regarding your answers to my questions about the new features you
were introducing; these questions were as you recall, how to provide a
formal semantics and to prove type correctness for these
constructions. It seems that you are attempting to answer these
questions by a reductionist analysis i.e. by statically reducing these
constructions to familiar Qi. In that way you short-circuit these
difficult questions which would require changing the formal semantics
to something complex and a lot of dense math’l proofs.

Your approach, IMO, is the right one. By mapping these constructions
into familiar Qi, you avoid all these troubles. However if you really
provide a static analysis of this kind, then all these constructions
are doable through sugar functions and there is no real need to extend
the language standard. The type checker will not need any extension
or reprogramming.

Another reason for not extending that standard is that the matching
algorithms you are experimenting with are only a subset of a fairly
large set that includes unification, commutative unification,
associative unification, AC unification, sorted unification, higher-
order unification, segment matching, sorted segment matching etc. You
cannot reasonably build them all in and the proper place for this
stuff is in the library which is where sugar functions would place
them.

The challenging thing for Shen, is to identify within CL, the subset
of commands needed to make it computationally adequate. CL includes
(e.g.) streams; Qi does not. What out of all the CL stream commands
does Shen really need? What commands in your carrier (Clojure or
Python) can carry your chosen primitives? This means that you begin
to flesh out, in detail, what computational adequacy (circa early C21)
really means.

Mark

> > > /Stefan- Hide quoted text -
>
> - Show quoted text -

[snorgers]

Yep, the define is a pure library function, you should have a basic
DEFUN
as the standard element.

The idea though is to be able to push in functionality in a standard
define construct
very much of the extension mechanism we discussed previously. So there
will be a refactoring
in the end that pushes a lot of the extensions of the def construct
out to a library

/Stefan