docs: mutual recursion lowering prereq + bootstrap.dag dissolution scope

[briansrls]

Summary

Follow-up to #464. Two doc additions:

1. §2.4 in SELF_HOSTING.md — mutual recursion lowering as a named prereq for the complexity port and general language completeness. v3's lower.rs already detects cycles (compute_mutually_recursive) but currently rejects them. The bounded-descend lowering (SCC-ordered, bounded by |SCC| × |children|) is the missing step. Once lowering produces bounded Loop nodes, complexity reads Loop.bound from the substrate — no Tarjan's in complexity, no SCC reconstruction. Testing scope: SCC sizes 2-5.

2. v3 ROADMAP.md M2 — expanded "Recursive functions → Loop lowering" with n-way mutual recursion details and prereq linkage to complexity port and general language completeness.

Supersedes #465 which had merge conflicts from #464's squash merge.

Test plan

• No code changes to test

🤖 Generated with Claude Code

[briansrls]

ChatGPT Review

I only had the uploaded patch for src/v3/ROADMAP.md and src/v3/SELF_HOSTING.md, so I’m grounding this on those hunks plus the current thesis/discipline/roadmap docs.

Principle audit.

1. Fail-closed. Mostly satisfied. The new text is directionally good because it explicitly says current v3 still rejects mutual recursion and treats the missing lowering as the gap, which is consistent with the fail-closed rule in the lowering table (INVARIANTS.md:477-509, 592-598; diff:35-48). My only small comment is that the new testing bullets are all positive fixtures; I’d also want one sentence calling out negative SCC fixtures so the doc preserves the “reject when the shared measure is missing” side of the contract.

2. Illegal states unrepresentable. Satisfied. The doc does the right high-level thing by routing mutual recursion back into existing bounded primitives (Loop/descend) instead of inventing a new “mutual recursion” substrate kind (diff:50-72; INVARIANTS.md:477-495, 592-598). That keeps the representation aligned with the thesis’s “recursive syntax is sugar” claim rather than adding another durable state shape.

3. Facts flow forward. This is the one place I have a real concern. In SELF_HOSTING.md, step 2/3 says to pick an arbitrary deterministic SCC order and then rewrite recursive calls to “the next function in the SCC order” (diff:56-64). That appears to drop the actual intra-SCC call topology and replace it with a ring walk. The SCC membership is a fact, but the original edge structure is also a fact; if lowering keeps only membership/order, later consumers may get a bound while execution/equivalence lose the real program. Under the discipline doc, that is a boundary-shape problem, not an implementation detail (modeling-discipline.md:51-68; INVARIANTS.md “design commitments must name the substrate target”). BLOCKING.

4. Coproduct dissolution. Satisfied. I don’t see the diff introducing a new substrate coproduct or a new special-case enum family; it is trying to dissolve mutual recursion into existing bounded forms, which is the right lens (modeling-discipline.md:70-128; THESIS.md / INVARIANTS.md lowering table). On the bootstrap side, the direction also stays narrow rather than re-inflating bootstrap.dag into a second stage-contract authority.

5. Single-authority metadata. Satisfied. The mutual-recursion note is good where it says complexity should read the lowered structure instead of reconstructing SCCs itself (diff:66-78). And the broader bootstrap-authority story remains aligned with the current roadmap note that pipeline signatures are the stage-contract authority, while only schema-migration vocabulary survives in bootstrap.dag (ROADMAP.md:366-372, 1108-1120). That is the right single-authority direction.

6. API-level enforcement over convention. Mostly satisfied, but the same structural gap from principle 3 leaks here too. “Lower to Loop nodes” is a good target, but “replace calls with the next function in SCC order” is still prose-level convention unless the doc names the exact substrate fact that preserves original call targets. As written, two implementers could both “follow the doc” and produce different semantics. For a design doc, that is too loose on the one place that matters (INVARIANTS.md design-commitments rule; diff:56-64). BLOCKING for the same reason as #3.

7. LOOP HEALTH. This round is making real forward progress: the ROADMAP hunk usefully promotes mutual-recursion lowering from an implicit thesis consequence to an explicit prerequisite for the complexity port, and the current roadmap’s bootstrap note keeps dissolution scope narrower instead of reopening a second authority (diff:9-23; ROADMAP.md:366-372, 1108-1120). LOOP HEALTH: converging — the docs are getting clearer about prerequisite order and authority boundaries, but SELF_HOSTING.md should stop short of committing to an SCC-as-ring rewrite before the substrate fact that preserves real intra-SCC edges is named.

Design question.

What exact substrate fact preserves the original intra-SCC call graph after lowering?

That is the structural crux here. The thesis only commits that mutual recursion lowers to a bounded form; it does not license throwing away the actual call topology. If the implementation keeps only “SCC membership + deterministic order + next-function link,” complexity may get a cheap bound, but execution, equivalence, and any later lens that cares about branch shape will be forced to reconstruct or will silently compute over a different program. I’d keep the “this is a prereq” claim, but rewrite the algorithm sketch so it commits only to preserving SCC structure in substrate form, not to a ring-walk encoding unless that encoding is proved semantics-preserving for nontrivial SCCs.

Verdict.

REQUEST_CHANGES

The ROADMAP clarification looks good, and the bootstrap-authority direction is consistent with the current roadmap note. But SELF_HOSTING.md §2.4 overcommits to a specific SCC lowering that appears to lose real call-topology facts; I’d fix that before merge. Also, the patch appears to corrupt the ## §3. Stage 1 — emit.dag heading into replacement characters at the end of the diff, which should be cleaned up too.

---

View conversation

[briansrls]

codex · gpt-5.4 · 2befd9f1

⚠️ Review (blocking: 2, non-blocking: 0+/1-)

BLOCKING (2)

Root Cause

• src/v3/ROADMAP.md The current reject-only helper throws away SCC structure as soon as it detects a cycle -> track a structured SCC-lowering prerequisite, not just "replace rejection with Loop nodes."
• src/v3/SELF_HOSTING.md The new self-hosting rationale blurs stage-internal helper recursion with pipeline-stage composition -> scope mutual recursion to user programs or stage-local helpers, not stage boundaries.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• src/v3/SELF_HOSTING.md The replacement line for "## Section 3. Stage 1 - emit.dag" is mojibaked in the diff; restore the dash before merge.

⚠️ The mutual-recursion prerequisite is worth documenting, but the current wording both underspecifies the SCC facts lowering must preserve and contradicts the self-hosting stage model.

[briansrls]

BLOCKING: This roadmap item understates the missing work: compute_mutually_recursive only yields a flat membership set, so the SCC partition/order fact still gets dropped before the lowering->complexity boundary (FACTS FLOW FORWARD).

[briansrls]

BLOCKING: Treating lower<->infer as a likely mutual-recursion case contradicts Section 2.1's pipeline-as-DAG contract and the thesis's explicit dependency flow; stage composition should stay acyclic.

[briansrls]

codex · gpt-5.4 · 2befd9f1

⚠️ Review (blocking: 2, non-blocking: 0+/1-)

BLOCKING (2)

Root Cause

• src/v3/ROADMAP.md The current reject-only helper throws away SCC structure as soon as it detects a cycle -> track a structured SCC-lowering prerequisite, not just "replace rejection with Loop nodes."
• src/v3/SELF_HOSTING.md The new self-hosting rationale blurs stage-internal helper recursion with pipeline-stage composition -> scope mutual recursion to user programs or stage-local helpers, not stage boundaries.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• src/v3/SELF_HOSTING.md The replacement line for "## Section 3. Stage 1 - emit.dag" is mojibaked in the diff; restore the dash before merge.

⚠️ The mutual-recursion prerequisite is worth documenting, but the current wording both underspecifies the SCC facts lowering must preserve and contradicts the self-hosting stage model.