miniKanren in V

A small, general-purpose miniKanren-style relational programming library implemented in V, plus an example that solves the Zebra (Einstein’s) puzzle.

Project layout

• minikanren/minikanren.v — the library module (public API)
• examples/zebra/ — example that models and solves the Zebra puzzle using the library
• tests/ — unit tests for core functionality
• main.v — minimal stub (points to examples)

Requirements

• V 0.4+ installed and available on PATH

Install / Build

No external dependencies. Use V directly.

• Run tests:

  v test .

• Run the Zebra example:

  v run examples/zebra

Library API

Module: minikanren

Types:

• Var { id int } — logic variable identifier (usually created via var_term)
• Term — a logic term; either a variable or an atom
• Subst — substitution mapping from variable id to term
• Stream = []Subst — stream of substitutions
• Goal = fn(Subst) Stream — a goal transforms a substitution into a stream of substitutions

Constructors and accessors:

• var_term(id int) Term — create a variable term with a fixed id
• atom(value string) Term — create a ground atom term
• reify(s Subst, t Term) Term — walk a term under a substitution
• value_of(s Subst, t Term) !string — get a concrete value or error if unbound

Core goals and combinators:

• unify_goal(t1 Term, t2 Term) Goal — unify two terms
• conde(goals ...Goal) Goal — logical OR (disjunction) of goals
• both(g1 Goal, g2 Goal) Goal — logical AND (conjunction)
• conjoin_goals(goals []Goal) Goal — AND over a list
• conde_from_list(goals []Goal) Goal — OR over a list
• run(n int, g Goal) []Subst — run a goal, returning up to n answers

General helper relations:

• nth_goal(l []Term, n int, result Term) Goal — enforce l[n] == result
• next_to_goal(x, y Term, l []Term) Goal — x and y are adjacent in list l (either order)
• right_of_goal(x, y Term, l []Term) Goal — x is immediately to the right of y in l
• same_position_goal(a []Term, aval Term, b []Term, bval Term) Goal — exists i with a[i]==aval and b[i]==bval
• next_to_cross_goal(a []Term, aval Term, b []Term, bval Term) Goal — exists i with a[i]==aval and b[i±1]==bval
• not_equal_goal(t1, t2 Term) Goal — disequality
• all_different_goals(terms []Term) []Goal — pairwise disequality goals
• one_of_goal(x Term, values []Term) Goal — x is one of the given values
• exists_in_list_goal(l []Term, v Term) Goal — some l[i] == v
• permute_goal(vars []Term, values []Term) Goal — assign a permutation of values to vars (injective mapping)

Usage examples

Simple unification

import minikanren { var_term, atom, run, unify_goal }

fn main() {
    x := var_term(0)
    results := run(1, unify_goal(x, atom('hello')))
    println(results.len) // 1
}

All-different from a small domain

import minikanren { var_term, atom, run, conjoin_goals, all_different_goals, one_of_goal }

fn main() {
    x := var_term(0)
    y := var_term(1)
    vals := [atom('a'), atom('b')]
    g := conjoin_goals([
        one_of_goal(x, vals),
        one_of_goal(y, vals),
        conjoin_goals(all_different_goals([x, y]))
    ])
    results := run(3, g)
    println(results.len) // >= 2
}

Zebra example

v run examples/zebra

The example builds five categories (colors, nationalities, pets, drinks, hobbies), encodes the clues with the helper goals, and uses permute_goal to enforce all-different across each category.

Notes

• This library focuses on pure miniKanren-style search via unification and goal composition.

License

This project is licensed under the MIT License - see the LICENSE file for details.

Disclaimer: This software is provided "as is", without warranty of any kind, express or implied, including but not limited to the warranties of merchantability, fitness for a particular purpose, and noninfringement. In no event shall the authors or copyright holders be liable for any claim, damages, or other liability, whether in an action of contract, tort, or otherwise, arising from, out of, or in connection with the software or the use or other dealings in the software.