This script is an attempt at a mostly verbatim implementation of scheme microkanren.

• Trees are represented by nested boxed arrays.
  
• Variables are integers and are considered in scope if lying between zero and 1-length of the state array.
  
• Promises are boxed strings, and are forced by the execute verb (".).
  
• The indeterminate value (_.) was chosen as initial value in the state array because of its limited usefulness in the J language, and to allow unification with the empty array (''). _. is therefore a marker of the freshness of a variable.

CAUTION: there certainly are major bugs and misunderstandings in this, due to my inexpertise in both logic and J!

Definitions

apm (conjunction)

scheme: $append-map

Works similarly to app. apm is a conjunction only because it has to handle functions as arguments.

app (dyad)

scheme: $append

Test x, and if a promise makes a new promise with reversed arguments (line 4). Otherwise appends and recurs (line 5). The depth of recursion is usually not too great, so it seems ok.

cis (conjunction)

scheme: call/initial-state

Notice the initial state is a boxed indeterminate value, in our case. We ‘fold’ over the initial promise a user-defined number of times. Since this actually does not map over a sequence but only produces one as we go, this is more akin to a loop.

con (conjunction)

scheme: conj

Conjunction.

dis (conjunction)

scheme: disj

Disjunction.

equ (conjunction)

scheme: ==
example: 0 equ 'a' (<_.)

The equivalence constraint. u and v are values to be unified. y is the state array. All constraints must define an optional default rank in x.

ext (dyad)

scheme: ext-s
example: (<_.) ext 0;'a'

Replaces the values of y by their substitutions according to x, and stores that in a. For unification to occur, the pair must 1.pass the occurs check and 2.the substituted values must be either identical to themselves (i.e. fresh variables) or identical to the values pointed to in the substitution. Unification then occurs by amending the positions pointed to in x by those in a.

fsh (adverb)

scheme: call/fresh
example: ] fsh ''

Introduces a new variable by extending the state array y with an indeterminate value.

get (dyad)

scheme: find
example: (_.;'a') get 1

Walks the state x to find the substitution of y.
Tests whether the position y in x is <_.. If <_. is found or the verb fails, y is returned. Otherwise the y-th element is returned. Walking the state is done by executing until the result stops changing.

occ (dyad)

scheme: occurs?
example: (<2) occ <<2

Tests x & y for identity, and returns zero in that case. If x & y are different, we flatten the tree y to a list of leaves and check for x membership in the flattened tree.

uni (conjunction)

scheme: unify
example: (_ _) 0 uni 'a' (<_.)

We test u & v for identity, and return the substitution y unchanged if true. We then check that all variables in the terms to be unified are in scope by flattening the tree and comparing to the length of y. Rank polymorphism is then achieved by splitting the terms according to the desired left and right ranks given in x. We map the tree in paths to obtain a list of paths, and then filter the variable paths into vp. Substitution paths are obtained in vs by negating the first element of each variable path. We check that all substitution paths are present in the paths in fp by checking for membership in all prefixes of the path list. We rearrange into 2 columns with variables on the left, and values to be unified on the right. Rows of the table t are then filtered to eliminate identical values and cycles in ft. Finally, the state is updated.

var (monad)

scheme: var?
example: var 3

This predicate test whether y is of type integer and is not a vector.