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.
> 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.
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
On 11 Oct, 23:00, Raoul Duke <rao...@gmail.com> wrote:
> > 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 :)
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
On Oct 10, 5:27 pm, snorgers <stefan.ta...@spray.se> wrote:
> 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.
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
On 26 Oct, 04:17, stever <st...@keptprivate.com> wrote:
> 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
> On Oct 10, 5:27 pm, snorgers <stefan.ta...@spray.se> wrote:
> > 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.
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
On 26 Oct, 22:30, snorgers <stefan.ta...@spray.se> wrote:
> 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
> On 26 Oct, 04:17, stever <st...@keptprivate.com> wrote:
> > 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
> > On Oct 10, 5:27 pm, snorgers <stefan.ta...@spray.se> wrote:
> > > 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.
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 ;-)
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
On 10 Oct, 21:27, snorgers <stefan.ta...@spray.se> wrote:
> 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.
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.
> 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
> On 10 Oct, 21:27, snorgers <stefan.ta...@spray.se> wrote:
> > 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.
> 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
> On 10 Oct, 21:27, snorgers <stefan.ta...@spray.se> wrote:
> > 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.
> 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:
> 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
> On 10 Oct, 21:27, snorgers <stefan.ta...@spray.se> wrote:
> > 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.
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
On Nov 5, 3:28 am, snorgers <stefan.ta...@spray.se> wrote:
> > 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:
> > 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
> > On 10 Oct, 21:27, snorgers <stefan.ta...@spray.se> wrote:
> > > 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.
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
On 25 Nov, 07:02, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:
> 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
> On Nov 5, 3:28 am, snorgers <stefan.ta...@spray.se> wrote:
> > > 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:
> > > 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
> > > On 10 Oct, 21:27, snorgers <stefan.ta...@spray.se> wrote:
> > > > 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.
|
