This application is a step-by-step evaluator for a dialect of microKanren.

Programs define goals, and execution finds solutions to those goals if solutions exist. Run the program by clicking the Run button at the top of the page.

The execution path is chosen by clicking on subgoals of the current goal. Possible paths are highlighted, and can be clicked to continue execution.

The language consists of two types of terms:

• Symbols, such as a, b, c, and nil.
• Pairs, such as (a b).

Pairs can be nested to generate more interesting terms, such as (a (b (c nil))).

During evaluation, terms may also contain unknowns, indicated by a hash symbol: #1, #2, etc.

There are three basic types of goals - equality, conjunctions and disjunctions:

An equality goal asserts that two terms should be equal. Here is an example:

(= x (y z))

This goal asserts that the term x is equal to the pair (y z).

If the current goal is an equality, then it can be clicked, and this will expand the current substitution.

A conjunction asserts that two or more goals are satisfied simultaneously. A conjunction is introduced using the conj keyword. Here is an example:

(conj (= x a)
      (= y b)
)

This goal asserts that x equals a, and also that y equals b.

If the current goal is a conjunction, any of the subgoals can be clicked. Execution will proceed for the selected subgoal and the remaining subgoals will be added to the list of remaining goals. When execution of the current goal completes, the first remaining goal will be executed.

A disjunction asserts that at least one of a set of goals is satisfied. A disjunction is introduced using the disj keyword. Here is an example:

(disj (= x a)
      (= x b)
      (= x c)
)

This goal asserts that x is either equals to a, b or c.

If the current goal is a disjunction, any of the subgoals can be clicked. Execution will proceed only for the selected subgoal.

To generate fresh names, use the fresh keyword with one or more names, and a goal as the last argument:

(fresh x y z (= x (y z)))

This goal generates three fresh names, and asserts that x is equal to the pair (y z). Execution will try to find terms x, y and z such that this relation holds.

The defines pane can be used to define functions which can be used in the goal. A function is defined using the define keyword, which takes a list of arguments and the defined goal. For example, to define the addo relation on natural numbers:

(define addo x y z
  (disj (conj (= x zero)
              (= y z)
        )
        (fresh p r
          (conj (= x (succ p))
                (addo p y r)
                (= z (succ r))
          )
        )
  )
)

This function can then be used in the goal, to search for numbers which sum to (succ (succ zero)) (2):

(fresh x y
  (addo x y (succ (succ zero)))
)

Note that functions can be defined recursively.