The Matcher and µKanren Libraries

Reference entries for the two case-study libraries of Part III. Both load into the session with the loop’s load, and both are ports of examples in namin/pink.

lib/matcher.naj

Two bindings:

• matcher-src — the matcher as open source: three functions (star_loop, match_here, match) with maybe-lift free.
• (matcher ml) — the closed program: maybe-lift bound to the source text ml, wrapped around matcher-src.

The regex language: a list of symbols; a literal matches itself, _ matches any symbol, a postfix * repeats the preceding element, and done terminates both regexes and inputs. Match results are 'yes and 'no.

Interpreting reading — '(lambda _ e e) as the maybe-lift:

(load lib/matcher.naj)
(define m ((interpret (matcher '(lambda _ e e))) nil-env))
((m '(a _ * done)) '(a b c done))
;=> 'yes
((m '(a _ * done)) '(b done))
;=> 'no

Compiling reading — '(lambda _ e (lift e)), with the application to the regex kept inside the run scope; the matcher case study has the full recipe and the residual-size discussion.

lib/mk.naj

One binding:

• (mk program) — program spliced into a let-chain binding the µKanren kernel around it. The result is closed Pink source for interpret or compile.

Names the wrapped program sees: =, assp, var, var?, var=?, walk, ext-s, mzero, unit, unify, ==, call/fresh, mplus, bind, disj, conj, empty-state.

Conventions, all curried:

• a goal applied to a state yields a stream of states: (g empty-state);
• ((== a) b) unifies two terms; (call/fresh (lambda _ q g)) introduces a variable; ((disj g1) g2) and ((conj g1) g2) combine;
• a state is (substitution . counter); a logic variable is ('var . n); a substitution is an association list from variables to terms.

(load lib/mk.naj)
((interpret (mk '(let p ((call/fresh (lambda _ q ((== q) 5))) empty-state) (car p)))) nil-env)
;=> (((('var . 0) . 5)) . 1)

Deviations from the reference mk.scm: $-prefixed stream names became st names ($ is not a symbol character here), and the empty list is written 'nil. Streams may suspend their tails behind zero-argument closures (mplus/bind), so forcing a stream position may require applying it — the case study shows both states of a disjunction being drawn out.