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
- Pairs, such as
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
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
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
Here is an example:
(conj (= x a) (= y b) )
This goal asserts that
a, and also that
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
(disj (= x a) (= x b) (= x c) )
This goal asserts that
x is either equals to
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
(y z). Execution will try to find terms
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
(succ (succ zero)) (2):
(fresh x y (addo x y (succ (succ zero))) )
Note that functions can be defined recursively.