schememinikanren

How do I port code using `all` to minikanren-with-symbolic-constraints?


I am reading minirop.pdf and it seems to be written in a dialect of MiniKanren that is outdated. I am interested in how I can port this style of MiniKanren to miniKanren-with-symbolic-constraints, since that seems to be more widely used.

I have to make a couple of adjustments, like replacing exists, but the code seems to work with the current version of the CVS repo on https://kanren.sf.net. For example, all, which is used in common-ancestor:

~/kanren/mini $ scheme type-inference.scm
Chez Scheme Version 9.5.8
Copyright 1984-2022 Cisco Systems, Inc.
[... bunch of omitted test output ...]
> (define father
    (lambda (dad child)
      (conde
      ((== dad 'jon) (== child 'sam))
      ((== dad 'jon) (== child 'hal))
      ((== dad 'sam) (== child 'rob))
      ((== dad 'sam) (== child 'jay))
      ((== dad 'sam) (== child 'roz))
      ((== dad 'hal) (== child 'ted))
      ((== dad 'rob) (== child 'sal))
      ((== dad 'rob) (== child 'pat)))))
> (define child
    (lambda (child dad)
      (father dad child)))
> (define ancestor
    (lambda (anc desc)
      (conde
        (succeed (child desc anc))
        (succeed (fresh (paren)
        (child desc paren)
        (ancestor anc paren))))))
> (define common-ancestor
    (lambda (anc desc1 desc2)
      (all
        (ancestor anc desc1)
        (ancestor anc desc2)
        (project (desc1 desc2) (if (not (eqv? desc1 desc2)) succeed fail)))))
> (run 2 (a) (common-ancestor a 'sal 'jay)))
(sam jon)

This is the expected result. However, all isn't available in with-symbolic-constraints. Intuitively, I don't even understand why it should be necessary, since The Reasoned Schemer (2nd ed.) doesn't use it, it just puts consecutive conditions after each other. So I was thinking I could just remove it, and it should work in with-symbolic-constraints. But as you can see, that doesn't work:

~/with-symbolic-constraints $ scheme mk.scm
[... required definitions omitted, they are the same as above ...]
(define common-ancestor
  (lambda (anc desc1 desc2)
    (ancestor anc desc1)
    (ancestor anc desc2)
    (project (desc1 desc2) (if (not (eqv? desc1 desc2)) succeed fail))))
> (run 2 (a) (common-ancestor a 'sal 'jay)))
(_.0)

How do I write common-ancestor nowadays? Is the problem with all or is it with the projection?


Solution

  • The expression

    ((lambda ()
       a
       b
       c))
    

    will always return c, whatever a and b are (unless they do some non-local control flow such as using continuations). So unless a and b have side effects, you might as well have just written c instead of the whole lambda invocation. In particular, if a and b are goals, they are ignored, and your lambda just produces the goal c anyway.

    You need something to combine them into one compound goal, and all is a traditional name for a combinator that does this. But in the absence of all, observe that fresh does the same thing: all the goals under a fresh are combined. So you can just use (fresh () ...) as a substitute for (all ...), or indeed define all yourself as a function (or macro) that takes multiple goals and combines them with (fresh ()).