Checking fn : Nat -> Nat with one run instead of a stream
A walkthrough of CHECK.disp. In disp a type is just a program that says yes or no to a tree. So a claim like "fn turns naturals into naturals" is a claim about every member of an infinite stream. This page explains the stream way of checking it, why that can only ever refute, and how CHECK.disp turns the infinite stream into one run on a placeholder. Everything below is computed live by a small in-page reimplementation.
1. What is being claimed
Everything in disp is a binary tree grown from one leaf t. A tree is a leaf, a stem (one child), or a fork (two children). Numbers are trees too: zero is the leaf, and succ n is a fork whose left child is a leaf and whose right child is n.
A type is a recognizer: a function from trees to booleans. The type of naturals is the recognizer NatR:
rec NatR :: {v : Tree} -> Bool :=> if (is_leaf v) { true } else { (is_fork v) && ((v.fst == t) && NatR v.snd) }So "fn : Nat -> Nat" unpacks to: for every tree n that NatR accepts, NatR also accepts fn n. There are infinitely many such n. That is the whole difficulty.
2. The stream way: enumerate, filter, map, check
The companion file IDEAS.disp takes the claim literally. It enumerates every tree in size order (a stream called Trees), keeps the ones the domain recognizer accepts, applies fn to each, and asks whether the codomain recognizer accepts every output:
Arrow :: {Dom : Tree -> Bool, Cod : Tree -> Bool, fuel : Nat, fn : Tree} -> Bool :=> {
let members := Trees.bounded(fuel).s_filter(Dom)
let outputs := members.s_map({arg} => fn arg)
outputs.s_all(Cod)
}This is honest and simple, but for an infinite domain it has a built-in asymmetry. If some member misbehaves, the stream eventually reaches it and answers false with a concrete counterexample: a real refutation. If nothing misbehaves, the stream never ends. The only way to get true is to cap it with a budget (bounded(fuel)), and then true only means "no counterexample among the first few thousand trees". That is evidence, not proof. The stream side is a refuter.
Try the refuter
3. The idea: run fn once, on a placeholder
Look at what the stream is doing when fn is succ. Every member n goes through the same motions: succ wraps a fork around it and never looks inside. All the runs are the same run with a different thing pasted in. So do that run once, with a placeholder pasted in, and read the answer off the shape that comes out.
CHECK.disp calls a tree with placeholders in it a partly-known value (Val). There are five forms:
The important one is member_of T. It means "any item the stream Trees.s_filter(T) would ever yield", but it stores only the recognizer's name. Every rule we are allowed to fire on it needs just the name, and the name is the key back to the stream if the shortcut fails and we have to enumerate after all.
The rules, and the one place they look inside
The substrate has five rewrite rules. Applying a tree f to an argument x either grows the tree (leaf and stem heads) or, for a fork head t a b, dispatches on the shape of a. The key question for each rule: does it need to look inside the argument x?
Only the triage rule inspects its argument. That line in sapply is the whole abstraction wall: if a triage lands on a placeholder, the run is stuck. Stuck is never a verdict. It just means this shortcut does not apply and the stream is still there.
Here is the same thing as pictures. Under the orange cloud is something we know only by the name of its type. Substituting any concrete member for the cloud must give a valid concrete run.
4. Why one run is enough: substitution commutes with the run
Here is the argument in one square. Take a concrete member n. You can either substitute n for the cloud first and then run fn concretely (bottom path), or run fn on the cloud once and substitute n into the partly-known result (top path). If the symbolic run never got stuck, both paths give the same tree, for every n.
Why does it commute? Each of the five rules is decided by the shape of the head and, for triage, the shape of the argument. When the run never triages a placeholder, every rule fired on the top path fires identically after substitution, because substitution only changes what is under the clouds and the rules never looked there. Category-minded readers will recognize the shape: the placeholder is a generic element, and a computation that never inspects it is natural in it, so its value at the generic element determines its value everywhere. The stream is the set of elements; the symbol is the identity arrow standing in for all of them.
The last step is reading a verdict off V. judge_nat does not run NatR on V (that would triage the clouds and get stuck). It walks V by Nat's shape certificate: a leaf is a Nat, a fork with a leaf on the left is a Nat if the right side is, a stem is never a Nat, and a cloud labelled Nat is a Nat by its own name. If that walk says Yes, then every substitution instance is a Nat, so the bottom-right corner is a Nat for every n. That is the proof. If it says No for a shape no substitution can fix (a stem, or a concrete non-Nat), that is a refutation, and the same square says the stream would have found the same counterexample. That is why Proved may never meet the refuter's false: they are two paths around one commuting square.
Try the confirmer: check_by_structure
Same function as chosen above. One symbolic run of fn on Member Nat, then the judge. Pick an n to see the square commute live.
symbolic trace (every sapply call)
Notice which functions get Open. Anything that looks at its argument, including every recursive function on Nat (recursion on a number starts by asking "is it zero?"), triages the cloud and stops. That is where the second optimization comes in.
5. Splitting the stream by its own equation: induction
The stream of naturals satisfies an equation about itself: it is zero followed by the successor of everything in it.
E(Nat) = [zero] ++ E(Nat).s_map(succ)That means every member is either the leaf or a fork with a leaf on the left and another member on the right. So instead of one placeholder for "any Nat", use two runs that together cover the stream: one on zero (which is concrete, so just run it), and one on succ ⟨∈Nat⟩. The second run knows the outermost shape of its argument, which is exactly what is_leaf and .snd needed. The shape-shortcut table in sapply answers those directly: is_leaf of a half-fork is false, pair_snd of a half-fork is its right child.
But the step run has a problem: a recursive function calls itself on the right child. fn is fix step_fn, and in the step run the recursive call is step_fn's first argument. CHECK.disp binds that argument to the fifth placeholder form, assumed_fn Nat: a call that we may assume returns a member of Nat. Applying it to anything answers Member Nat. That is the induction hypothesis as a value.
check_by_induction :: {step_fn : Tree} -> Tree :=> {
let base_output := (fix step_fn) zero // concrete run
if (not (NatR base_output)) { "Refuted" }
else {
let with_ih := sapply (known step_fn) (assumed_fn NatR) 400 // bind the recursion to the IH token
...
let step_output := sapply with_ih.answer (half_fork (known t) (member_of NatR)) 400 // run on succ ⟨∈Nat⟩
... judge_nat step_output.answer ...Structurally this is the initial-algebra square. Nat is the least solution of X = 1 + X, with the two constructors [zero, succ] as the algebra. Proving something about all of Nat means proving it for the two constructors, assuming it for the recursive slot. The link between the step function and the real function is the single line test tree_eq dbl (fix dbl_step) = true: the real recursive function is the fixed point of the step, so what holds for one unrolled layer under the hypothesis holds for the whole fixed point.
Try the confirmer: check_by_induction
Each example also has a step-function form (a first argument for the recursive call, even if unused). Base runs concretely on zero; the step runs symbolically on succ ⟨∈Nat⟩ with the recursion bound to the IH token.
symbolic trace of the step run
6. What the three verdicts mean
| verdict | what happened | relation to the stream |
|---|---|---|
| Proved | the symbolic run finished and the judge said Yes on the output's known shell | every substitution instance is a Nat, so the stream's s_all would never find a counterexample |
| Refuted | the base case, or the run's output, has a shape no member can fix (a stem, a concrete non-Nat) | the stream would reach the same counterexample; the two paths agree |
| Open | stuck: some rule needed to look under a cloud, or the judge could not decide | not a verdict. The stored name NatR is the key back to Trees.s_filter(NatR), so we enumerate after all |
The cost difference is the whole point. The stream checks succ by running it on as many members as the budget allows and can still only say "no counterexample so far". The confirmer runs succ once, on a cloud, in a handful of rule firings, and says Proved.
7. Known debts in the v1 confirmer
No decreasing-measure check. The induction hypothesis token answers Member Nat for any argument. Nothing checks that the recursive call happens on something smaller. The example loop_step above recurses on n itself. It passes its base case, and its step run is Proved (confirmed against the real CHECK.disp), yet fix loop_step never returns on any n ≥ 1. The claim "returns a Nat" is vacuously fine for a function that never returns, but a checker that says Proved there has not shown termination. Fixing it means making the IH token accept only arguments that are structurally below the step's argument: in the step run, exactly the right child of the half-fork.
The judge is conservative on half-forks. judge_nat answers Stuck for a fork whose left child is not a known leaf. For {_d, n} => pair n n the step output is a fork whose left child is succ ⟨∈Nat⟩, itself a fork, so it can never equal the leaf: a sound answer would be No, hence Refuted. Today it says Open, which is honest but weaker than it could be.
Source: CHECK.disp, IDEAS.disp, lib/stream.disp, lib/prelude.disp. The in-page evaluator implements the five substrate rules with the same convention as src/core/tree.ts, and the checker is a line-for-line port of sapply, judge_nat, check_by_structure, and check_by_induction. Compiled trees for the example functions are produced by a small bracket-abstraction compiler, so their exact shapes differ from disp's elaborator output while their behaviour is the same.