Demo: the CLRS red-black tree with Python selectors

[sidprasad]

Stacked on #152. Base is python-selectors — review that one first; this diff is one notebook.

What this is

spytial-clrs's trees.ipynb declares its red-black constraints in sgq, which runs over the relationalized instance. Skipping the NIL sentinel reads:

left & (RBNode -> (RBNode - NoneType.~key))

This is the same CLRS chapter 13 structure with the selectors written as Python functions over the objects themselves:

def real(n):
    return isinstance(n, RBNode) and n is not NIL

def left_edges(values):
    return [(n, n.left) for n in values if real(n) and real(n.left)]

def red_nodes(values):
    return [n for n in values if real(n) and n.color == RED]

Constraint	sgq (trees.ipynb)	Python (this notebook)
Left edges, skipping NIL	left & (RBNode -> (RBNode - NoneType.~key))	[(n, n.left) for n in values if real(n) and real(n.left)]
Red nodes	{ x : RBNode | @:(x.color) = "red" }	[n for n in values if real(n) and n.color == RED]
Scaffolding to hide	{ x : RBNode | (x.key in NoneType) } + RBTree + int + NoneType + {s : str | @:s = "red" or @:s = "black"}	[v for v in values if v is NIL or isinstance(v, (RBTree, int)) or v is None or v in (RED, BLACK)]

Worth noting on the first row: NIL is a single object, so Python says n is NIL. sgq has no way to say "this object", so trees.ipynb identifies it by a property that happens to hold only of it — its key is None. That works, and it stops working the moment a real node is given a None key.

It is honest about the boundary

The notebook ends by pointing at disjoint-sets.ipynb's ^(~parent) — transitive closure of the inverted parent relation. There is no comprehension for that; the Python version is a hand-written fixpoint. The rule it offers: Python selectors for conditions about a value (n.color == RED, n is NIL), sgq for conditions about the shape of the graph (^parent, ~next, iden).

It found a bug

Porting this surfaced a real defect in #152, now fixed there: a str was emitted as a quoted literal, but a quoted string is a value in sgq and not a member of univ ("black" & univ is empty). So hideAtom on the colour strings silently drew them anyway — visible as two stray red/black boxes in the diagram. Strings are now emitted as {s : str | @:s = "..."}, which is exactly how the sgq notebooks spell it, and now I know why.

Verification

The notebook is executed and its output committed. The tree is CLRS figure 13.4, checked as a valid red-black tree — BST order, no red child of a red node, uniform black-height 3 — and the rendered diagram was inspected in a browser: six nodes, five edges matching the tree's shape, red borders on exactly the two red nodes, no scaffolding atoms drawn.

🤖 Generated with Claude Code