miniKanren — Brief ☧

Deep version → | Back to Unification →

Q: Suppose you want to learn something from Scripture. How do you begin?

A: You state what you already know, and you ask about what you do not.

For example: "Who was the father of Solomon?" — you know Solomon, and you seek the father.

Q: Could a computer do the same thing — state what it knows and ask about the rest?

A: That is exactly what miniKanren does. You describe relationships as facts,

then ask questions by leaving blanks for the things you want to discover:
(run* (father_chirho)
  (parent_chirho father_chirho "Solomon"))
In plain language: "Find every value of father_chirho such that parent_chirho holds between father_chirho and Solomon."

The answer comes back: ("David").

Q: So it is like a search engine for logical facts?

A: A good way to think about it. But unlike a web search engine, miniKanren does not just match keywords — it reasons about relationships. It can work backward, forward, or sideways through the facts you give it, using a process called unification.

Q: How much machinery does this require? It sounds like it could be complicated.

A: Remarkably little. The entire language is built from just five operators:

The Five Core Operators

Operator	What it does	Everyday sense
`==`	Assert two things are the same	"This IS that" — identifying a match
`fresh`	Introduce a new unknown	"Let there be a question" — naming what we seek
`conde`	Try multiple possibilities	"Search ALL the Scriptures" — exploring branches
`run*`	Find ALL answers	"Seek and you shall find" — exhaustive search
`run N`	Find first N answers	"Show me N witnesses" — bounded search

That is it. Five building blocks, and from them you can express any logical query. The simplicity is not a limitation — it is by design. Each operator does one thing well, and their combinations cover the full range of logical reasoning. Compare this to a typical programming language with dozens of control flow constructs; miniKanren achieves comparable expressiveness with just five.

Let us see each operator in action.

Quick Examples

# 1. == (unification): "David is the father of Solomon"
(== father_chirho "David")

# 2. fresh: introduce an unknown
(fresh (x_chirho)
  (== x_chirho "David"))

# 3. conde: try alternatives
(conde
  [(== tribe_chirho "Judah")]     # either Judah
  [(== tribe_chirho "Benjamin")]) # or Benjamin

# 4. run*: find all answers
(run* (q_chirho)
  (conde
    [(== q_chirho "Judah")]
    [(== q_chirho "Benjamin")]))
# → ("Judah" "Benjamin")

# 5. run 1: find just the first answer
(run 1 (q_chirho)
  (parent_chirho q_chirho "Solomon"))
# → ("David")

Notice that conde is like branching in a tree: each branch is an alternative possibility, and the system explores them all. The run* operator collects every answer that survives — every branch where the logic holds.

How It Maps to Hardware

Each operator has a direct hardware counterpart. This one-to-one mapping is what makes miniKanren so well-suited to FPGA acceleration — there is no "translation gap" between the language semantics and the hardware implementation:

== (unify)  →  AND two bitmasks         →  1 cycle on FPGA
fresh       →  allocate a new domain    →  1 register
conde       →  duplicate search state   →  parallel lanes
run*        →  exhaust all branches     →  ring FSM drains queue
run N       →  stop after N results     →  early termination flag

The algorithm that run* uses is essentially a breadth-first traversal of a search tree. Each conde branch creates new leaves to explore, and unification prunes the branches where contradictions appear.

graph TD
    Q["run* (q) ..."] --> F["fresh variables → domains"]
    F --> E["== constraints → AND bitmasks"]
    E --> C["conde branches → parallel states"]
    C --> R["Results: all surviving (non-zero) states"]

Learn more about miniKanren internals

Next: appendo | Related: streams

Soli Deo Gloria