appendo — Brief ☧
Deep version → | Back to miniKanren →
Q: Matthew's genealogy of Jesus divides the lineage into three parts:
Abraham to David (14 generations), David to the exile (14 generations),
and the exile to Christ (14 generations). If you wanted to join those three
segments into one continuous lineage, how would you do it?
A: You would append them — place the three lists end to end:
abraham_to_david_chirho ++ david_to_exile_chirho ++ exile_to_christ_chirho = full_lineage_chirhoIn most programming languages, appending is a function: you feed in the parts, you get back the whole.
Q: Alright, that gives me the joined list. But what if I have the full lineage and I want to find where to split it? For instance, "what prefix ends at David?"
A: Now you are asking the question in reverse. A normal append function cannot do that — it only goes forward (parts in, whole out). You would need to write a completely different function to search for a split point.
Q: That seems like the same problem we saw with relations vs functions. Is there a relational version of append?
A: Yes — that is
appendo. It is a relation, not a function. It describes the relationship "list L followed by list S equals list Out," and you can query it in any direction:Direction 1 (FORWARD — join): Given: abraham_to_david ++ david_to_exile = ? Find: the full lineage Direction 2 (BACKWARD — split): Given: ? ++ ? = [Abraham, Isaac, Jacob, Judah, ...] Find: ALL ways to split the lineage into two parts Direction 3 (FIND SUFFIX): Given: [Abraham, Isaac] ++ ? = [Abraham, Isaac, Jacob, Judah] Find: [Jacob, Judah]One definition. Three directions. Zero extra code.
Three Directions, One Definition
The definition uses recursion — the relation calls itself on a smaller piece of the list, just as a genealogy can be understood one generation at a time:
def appendo_chirho(l_chirho, s_chirho, out_chirho):
"""l_chirho ++ s_chirho == out_chirho — works in ANY direction."""
return conde_chirho(
# Base case: [] ++ s == s
[eq_chirho(l_chirho, []),
eq_chirho(s_chirho, out_chirho)],
# Recursive: [head|tail] ++ s == [head|rest]
# where tail ++ s == rest
[fresh_chirho(lambda head_chirho:
fresh_chirho(lambda tail_chirho:
fresh_chirho(lambda rest_chirho:
conj_all_chirho(
eq_chirho(l_chirho, [head_chirho, tail_chirho]), # l = [head|tail]
eq_chirho(out_chirho, [head_chirho, rest_chirho]), # out = [head|rest]
appendo_chirho(tail_chirho, s_chirho, rest_chirho) # tail++s = rest
))))]
)The base case says: an empty list followed by S is just S.
The recursive case says: peel off the first element (the head), and the rest follows the same pattern. This is the same idea as peeling one generation off a genealogy and asking about the remainder.
All Splits of a Lineage
When you leave both inputs unknown, appendo finds every possible split:
appendo(?, ?, [Abraham, Isaac, Jacob, Judah])
Answer 1: [] ++ [Abraham, Isaac, Jacob, Judah]
Answer 2: [Abraham] ++ [Isaac, Jacob, Judah]
Answer 3: [Abraham, Isaac] ++ [Jacob, Judah]
Answer 4: [Abraham, Isaac, Jacob] ++ [Judah]
Answer 5: [Abraham, Isaac, Jacob, Judah] ++ []Five ways to split a 4-element list. The relation finds them ALL. Notice there are always N+1 ways to split a list of length N — including the two "trivial" splits where one part is empty. This kind of complete enumeration is what makes relational programming powerful for search and analysis.
On the FPGA
appendo becomes a 3D sparse Boolean tensor:
Dimension 0: l (prefix)
Dimension 1: s (suffix)
Dimension 2: out (result)
Each valid tuple (l, s, out) where l++s=out is a 1-bit in the tensor.
Fix any dimension → slice the tensor → get all matching pairs.This is the same idea from relations: a binary relation is a matrix; a ternary relation like appendo is a 3D tensor. Fixing one dimension and reading the others is the hardware equivalent of running the relation in a particular direction.
The tensor representation is what makes the FPGA so efficient at appendo queries. Instead of recursively walking cons cells (which requires following pointers through memory), the FPGA loads the relevant slice of the tensor and scans it with bitmask AND operations. For the forward direction (known prefix and suffix, find the result), this is a single lookup. For the backward direction (known result, find all splits), it is a scan over the relevant slice — but the scan is pipelined and parallel across 8 lanes. The recursion that makes appendo elegant in software becomes a data structure that makes it fast in hardware.
Soli Deo Gloria