The “naturally-recursive” macro-based implementations we came up with
go the wrong direction. They nest the goals unfortunately, in ways
that we can see in e.g. my redex model, and in Michael’s graffle
depiction.
I will it turns out need to discuss the difficulty of the conjunction.
We should be able to see from the derivation how a clean definition brings us to right behavior.
Just working with var-args functions isn’t enough; we could define the logic operators associating the “right way” just as easily as defining them the “wrong way”. So we need some more subtle categorization.
It seemed like conda had forced our hand into including the
zero-ary base case. If we wanted to build out of earlier primitives,
we had needed the zero-ary version for conda. Bracket that concern for
a second, and let’s otherwise say we don’t need that additional case.
We can implement the 2+-ary versions, using conj2/disj2 as primitives, in either the tail recursive or the natl. recursive versions, with either macros or varargs, either forwards or backwards. So that’s a nice place to start. Note, that left or right association and left or right fold are the same, because the operator is binary conj2/disj2—association is fold. Selecting a starting operator conj2 v. disj2 is not an axis of variation; any successful approach must work for both.
Why would you want to do that? Macros, for instance. The (C g) case
matters b/c, say, some conde macro, or fresh if you wanted. Maybe
it would suck if the user had to think about whether their fresh
body had 1 or 2+ goals in it. But suppose you didn’t care about that,
either, and that you didn’t need the singleton conjunction case
either. Then we can pick from a smörgåsbord of options.
The basic steps seem to be
- I mean, honestly. That 0-ary base case needs to go. We gotta get rid of that.
- To get rid of macro, start with 2-ary versions. These blend easily.
- To avoid
apply, use variadic to make a help function, and just use list recursion - We should be able to simplify by substituting through the old
xyzj/2definition - We ought to be able to reduce the base case
So, which one is this?—~varargs-2+-left-assoc~
#lang racket
(define ((C g1 g2 . gs) s)
(cond
((null? gs) ((conj2 g1 g2) s))
(else ((apply C (cons (conj2 g1 g2) gs)) s))))We can start by breaking the function up into a recursive variant and
an external-facing help function. Unlike the earlier recursive variant
above, this inner recursive function does not require apply since it
uses ordinary list recursion.
#lang racket
(define ((C g1 g2 . gs) s)
(C-rec g1 g2 gs s))
(define (C-rec g1 g2 gs s)
(cond
((null? gs) ((conj2 g1 g2) s))
(else
(C-rec (conj2 g1 g2) (car gs) (cdr gs) s))))If we substitute through in the definition of conj2, we get:
#lang racket
(define ((C g1 g2 . gs) s)
(C-rec g1 g2 gs s))
(define (C-rec g1 g2 gs s)
(cond
((null? gs) ((lambda (s) ($append-map g2 (g1 s))) s))
(else
(C-rec (lambda (s) ($append-map g2 (g1 s))) (car gs) (cdr gs) s))))Here is the important piece; since we only need s to build the
stream, we can assemble the stream on the way in, and accumulate
along it—instead of passing in g1 and s separately, we pass in their
combination as a stream. The function is tail recursive, we can change
the signature in the one and only external call and the recursive
call.
We had to combine and hand substitute through, as in ((lambda (s)
($append-map g2 (g1 s))) s)
#lang racket
(define ((C g1 g2 . gs) s)
(C-rec g2 gs (g1 s)))
(define (C-rec g2 gs s-inf)
(cond
((null? gs) ($append-map g2 s-inf))
(else (C-rec (car gs) (cdr gs) ($append-map g2 s-inf)))))The recursion and the base case share a lot in common. We can exploit
that. If we pass back the stream in the base case, and split gs in
the recursive case, we can get rid of g2 and turn this into a 1+ary
version.
#lang racket
(define ((C g1 . gs) s)
(C-rec gs (g1 s)))
(define (C-rec gs s-inf)
(cond
((null? gs) s-inf)
(else (C-rec (cdr gs) ($append-map (car gs) s-inf)))))And there you have it. We can derive this answer from the original
version. Both the first version and this final version have their
virtues and drawbacks; one uses explicit car and cdr, while the
other uses apply. I think we prefer this last one, because it’s
strictly more general.
This “derivation sequence” is essentially a three step operation: 1. take an operation based on conj2/disj2 and then go beneath that level 2. some simple clean-up optimizations 3. reduce the demanded arity so that it operates on 1+ arguments.
It could be nice to avoid having to specialize our macros to the two different cases and keep our users from needing to worry adding and removing a combinator when moving from one to more than one goal.
#lang racket
(define-syntax fresh
(syntax-rules ()
[(fresh () g) <do something on this one>]
[(fresh () g g1 g* ...) <do something on this one>]
[(fresh (x ...) g ...) <recur here down to base case>]))To illustrate just how superfluous the 0-arity version is, see that we can add that back in as a separate case of the interface function.
#lang racket
(define ((C . gs) s)
(cond
((null? gs) S)
(else (C-rec (cdr gs) ((car gs) s)))))
(define (C-rec gs s-inf)
(cond
((null? gs) s-inf)
(else (C-rec (cdr gs) ($append-map (car gs) s-inf)))))Is this transformation sequence (or some analogous version of it) equally applicable across all of the 4 varags versions?
To recapitulate, our initial motivation was to remove some macros. This led to using variadic functions to combine arbitrary-length goal sequences. I want to tell a story where many, if not all, of the decisions fell out as a consequence of this choice. Can we do that?
I want to try one of the more interesting variants. I’m actually
interested in all four versions, because I want to know whether we can
get tail recursive disj taking its arguments the right way, and
ensuring that we cannot do a similar derivation for the natl.
recursive variants, and for good reason. If we can do that, everything
is aces and this is a good paper. If we are stuck with the
backward-disj, then that’s okay but not great.
#lang racket
(define ((conj g g1 . gs) s)
(cond
((null? gs) ((conj2 g g1) s))
(else ((conj2 g (apply conj (cons g1 gs))) s))))So, alright. We’ll try it this way. Break it apart into two mutually recursive functions.
#lang racket
(define ((conj g g1 . gs) s)
(C-rec g g1 gs s))
(define (C-rec g g1 gs s)
(cond
((null? gs) ((conj2 g g1) s))
(else ((conj2 g (apply conj (cons g1 gs))) s))))Okay, now this must be where things get different. We cannot (easily)
replace the subsequent line by a recursive call to C-rec, because we
are still waiting on an s. So the best we can do is this,
abstracting over s and waiting.
#lang racket
(define ((conj g g1 . gs) s)
(C-rec g g1 gs s))
(define (C-rec g g1 gs s)
(cond
((null? gs) ((conj2 g g1) s))
(else ((conj2 g (λ (s) (C-rec g1 (car gs) (cdr gs) s))) s))))From here we can try and substitute through the definition of conj2.
#lang racket
(define ((conj g g1 . gs) s)
(C-rec g g1 gs s))
(define (C-rec g g1 gs s)
(cond
((null? gs) ((lambda (s) ($append-map g1 (g s))) s))
(else ((lambda (s) ($append-map (λ (s) (C-rec g1 (car gs) (cdr gs) s)) (g s))) s))))In the earlier version, we could construct the stream on the way
down. We cannot do that here. We can β-reduce here, since the
lambdas weren’t doing anything for us.
#lang racket
(define ((conj g g1 . gs) s)
(C-rec g g1 gs s))
(define (C-rec g g1 gs s)
(cond
((null? gs) ($append-map g1 (g s)))
(else ($append-map (λ (s) (C-rec g1 (car gs) (cdr gs) s)) (g s)))))In the earlier derivation we were able to turn the stream itself into a parameter, and change the recursive function’s arity. We can do that here, although again this abstraction makes the results a little less pleasant.
#lang racket
(define ((conj g g1 . gs) s)
(C-rec g1 gs (g s)))
(define (C-rec g1 gs s-inf)
(cond
((null? gs) ($append-map g1 s-inf))
(else ($append-map (λ (s) (C-rec (car gs) (cdr gs) (g1 s))) s-inf))))We can try and loosen the 2+ requirement, a bit at least.
#lang racket
(define ((conj g . gs) s)
(C-rec gs (g s)))
(define (C-rec gs s-inf)
(cond
((null? gs) s-inf)
(else ($append-map (λ (s) (C-rec (cdr gs) ((car gs) s))) s-inf))))It’s not totally clear that there’s some optimization we’re prevented from performing, but needing to construct a closure for every recursive call is expensive, I guess compared to doing not-that.
But I’m having trouble understanding how one is so obviously a worse definition, or how one permits an optimization the other clearly forbids, in a way that leads to the thesis “basic programming skills get us to the clever definition” and that we can see from horse sense.
Maybe the nested lambdas there is it. However.
If you treat the list as accumulatively, then you’ll get the result you want.
This one wound up with a nested lambda, and does a non-trivial amount of work to it. Is the alternative nicer?
#lang racket
(define ((disj g g1 . gs) s)
(cond
((null? gs) ((disj2 g g1) s))
(else ((disj2 g (apply disj (cons g1 gs))) s))))
Mutual recursion
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((disj2 g g1) s))
(else ((disj2 g (apply disj (cons g1 gs))) s))))But since unlike the earlier version we don’t have all the parts yet,
we cannot build the recursive function right now. Instead we have to
λ abstract.
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((disj2 g g1) s))
(else ((disj2 g (λ (s) ((apply disj (cons g1 gs)) s))) s))))… and then we can build the recursion
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((disj2 g g1) s))
(else ((disj2 g (λ (s) (D-rec g1 (car gs) (cdr gs) s))) s))))Now seems like a nice time to unfold the definitions of disj2.
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((λ (s) ($append (g s) (g1 s))) s))
(else ((λ (s) ($append (g s) ((λ (s) (D-rec g1 (car gs) (cdr gs) s)) s))) s))))This makes the β reductions come out very nice.
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ($append (g s) (g1 s)))
(else ($append (g s) (D-rec g1 (car gs) (cdr gs) s)))))And this is a nice time to reduce the arity.
#lang racket
(define ((disj g . gs) s)
(D-rec g gs s))
(define (D-rec g gs s)
(cond
((null? gs) (g s))
(else ($append (g s) (D-rec (car gs) (cdr gs) s)))))This approach has to be the right solution. It might be that this doesn’t take the conjuncts in the correct order or something, in which case we have to switch which goal goes in which position, but I have a real hard time believing that this isn’t the correct answer.
I worry the other disj implementation we’re after ends up with those same sadly-nested lambdas. And I suspect that performance wise that’s a bad thing.
I thought the straightforward left-associative, left recursion
disj implementation you get that great performance, the same with
conjunction. The fact that the above is so nice makes me suspect that
the other implementation has to be incorrect. Or, maybe with
disjunction it just doesn’t matter? Let’s see anyway.
#lang racket
(define ((disj g g1 . gs) s)
(cond
((null? gs) ((disj2 g g1) s))
(else (let ((res (apply disj (cons (disj2 g g1) gs))))
(res s)))))
and split
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((disj2 g g1) s))
(else ((apply disj (cons (disj2 g g1) gs)) s))))
and apply through
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((disj2 g g1) s))
(else (D-rec (disj2 g g1) (car gs) (cdr gs) s))))We have to abstract over s here, which is probably going to be sub-optimal.
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((λ (s) ($append (g s) (g1 s))) s))
(else (D-rec (λ (s) ($append (g s) (g1 s))) (car gs) (cdr gs) s))))I guess we can β in the base case.
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ($append (g s) (g1 s)))
(else (D-rec (λ (s) ($append (g s) (g1 s))) (car gs) (cdr gs) s))))And finish up with the arity reduction again.
#lang racket
(define ((disj g . gs) s)
(D-rec g gs s))
(define (D-rec g gs s)
(cond
((null? gs) (g s))
(else (D-rec (λ (s) ($append (g s) (g1 s))) (cdr gs) s))))This variant builds up one giant big honkin’ goal, and then applies that dude all over creation. I assume that’s sub-optimal. But I don’t know it.
At some point, one of the problems that we saw, that Greg Rosenblatt also pointed out, was that the mK search heuristic was flipped for one of these implementations—that is to say, the rightmost goal ended up getting I think 1/2 of the search rather than the leftmost, as per usual. However, we saw also that alternate implementations flip the order that the arguments execute. And there’s no problem switching them as we recur down. This is the same derivation we just saw, but instead using the left-associated flipped args version.
#lang racket
(define ((disj g g1 . gs) s)
(cond
((null? gs) ((disj2 g1 g) s))
(else ((apply disj (cons (disj2 g1 g) gs)) s))))So, the by-now standard practice.
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((disj2 g1 g) s))
(else ((apply disj (cons (disj2 g1 g) gs)) s))))We can directly substitute the call ((apply disj (cons (disj2 g1 g)
gs)) s) through for the recursion.
#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((disj2 g1 g) s))
(else (D-rec (disj2 g1 g) (car gs) (cdr gs) s))))#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ((lambda (s) ($append (g1 s) (g s))) s))
(else (D-rec (lambda (s) ($append (g1 s) (g s))) (car gs) (cdr gs) s))))#lang racket
(define ((disj g g1 . gs) s)
(D-rec g g1 gs s))
(define (D-rec g g1 gs s)
(cond
((null? gs) ($append (g1 s) (g s)))
(else (D-rec (lambda (s) ($append (g1 s) (g s))) (car gs) (cdr gs) s))))#lang racket
(define ((disj g . gs) s)
(D-rec g gs s))
(define (D-rec g gs s)
(cond
((null? gs) (g s))
(else (D-rec (lambda (s) ($append ((car gs) s) (g s))) (cdr gs) s))))(define ((D . gs) s) …)
Since \rackinline|gs| could be empty, as with the macro based implementation we introduce a base-case for the zero-length list.
(define ((D . gs) s) (cond ((null? gs) (list)) …))
But it’s also unfortunate to force an extra failing recursion onto every call, so we add the length-one arguments list to short-circuit that.
(define ((D . gs) s) (cond ((null? gs) ‘()) ((null? (cdr gs)) (g s)) …))
;; These assume 2+ goals; and we don’t write or work w/ “silly conjunctions.”
(define-syntax conj (syntax-rules () ((conj g0 g1) (conj₂ g0 g1)) ((conj g0 g1 g …) (conj (conj₂ g0 g1) g …))))
(define-syntax disj (syntax-rules () ((disj g0 g1) (disj₂ g0 g1)) ((disj g0 g1 g …) (disj (disj₂ g0 g1) g …))))
;; These next two are from the paper, as written. ;; As they’re written, they are 0-or-more-ary. ;; But they likewise shouldn’t require silly arities.
(define-syntax conj (syntax-rules () ((conj) S) ((conj g) g) ((conj g0 g …) (conj₂ g0 (conj g …)))))
(define-syntax disj (syntax-rules () ((disj) F) ((disj g) g) ((disj g0 g …) (disj₂ g0 (disj g …)))))
;; So we first remove the zero arity, conda be damned.
(define-syntax conj (syntax-rules () ((conj g) g) ((conj g0 g …) (conj₂ g0 (conj g …)))))
(define-syntax disj (syntax-rules () ((disj g) g) ((disj g0 g …) (disj₂ g0 (disj g …)))))
;; Then, we try again and unfold the recursion once more
(define-syntax conj (syntax-rules () ((conj g) g) ((conj g0 g1) (conj₂ g0 (conj g1))) ((conj g0 g1 g …) (conj₂ g0 (conj g1 g …)))))
(define-syntax disj (syntax-rules () ((disj g) g) ((disj g0 g1) (disj₂ g0 (disj g1))) ((disj g0 g1 g …) (disj₂ g0 (disj g1 g …)))))
;; Then, substitute through, and specialize away
(define-syntax conj (syntax-rules () ((conj g0 g1) (conj₂ g0 g1)) ((conj g0 g1 g …) (conj₂ g0 (conj g1 g …)))))
(define-syntax disj (syntax-rules () ((disj g0 g1) (disj₂ g0 g1)) ((disj g0 g1 g …) (disj₂ g0 (disj g1 g …)))))
(define-syntax conj (syntax-rules () ((conj g0 g1) (conj₂ g0 g1)) ((conj g0 g1 g …) (conj (conj₂ g0 g1) g …))))
(define-syntax disj (syntax-rules () ((disj g0 g1) (disj₂ g0 g1)) ((disj g0 g1 g …) (disj (disj₂ g0 g1) g …))))
Then there’s this janky reimplementation of fresh. It’s hacky and
non-portable. That procedure-arity is very implementation specific
and only partially works (case-lambda, procedure-arity doesn’t really
always work, etc, see failed SRFI discussion), and at least Racket’s
assert mechanism is not the same as the Scheme error handling
mechanism. But build-list is AFAIK Racket only.
#lang racket
(define (fresh f)
(let ((n (procedure-arity f)))
(assert (number? n))
(λ (s/c)
(let ((c (cdr s/c)))
((apply f (build-list n (curry + c)))
(cons (car s/c) (+ n c)))))))