Current integration is a stable compiler change, not a third backend. See binding elimination; separate-backend stages below are superseded historical experiments.

Isolated Boolean-binding substitution candidate

This extends the analysis-only classifier with capture-avoiding substitution and a deliberately narrower experimental rewrite. It is implemented in tricu, exercised on resolved core, and compiled through the accepted stable core compiler. It is not installed into the production source compiler, and no default compilation behavior has changed.

Implemented pieces

bench/binding-substitution.tri supplies:

• positive de Bruijn index shifting with a cutoff;
• capture-avoiding removal of one binder;
• a guarded immediate-binding rewrite;
• a conservative one-pass traversal over a complete core tree.

The input schema is the existing located core (kind, (payload, (start, end))). Inputs must be trusted well-formed core. These functions do not replace frontend validation or diagnose every malformed payload.

Substitution and source origins

To remove a binder, substitution tracks its depth under nested lambdas:

• indices below that depth remain local to the nested scope;
• the matching index is replaced by the RHS, shifted to avoid capture;
• indices above it decrease by one to account for the removed binder.

Literal trees remain opaque, including trees that happen to resemble syntax. Application, lambda and proper-list core payloads are traversed structurally.

Unchanged nodes retain their spans. Inserted RHS syntax retains its definition's spans, rather than pretending to originate at the variable use. The final root of a rewritten binding receives the original binding's outer span. This policy is explicitly tested; it is not an accidental side effect of substitution.

Independent oracle

test/binding_substitution.py does not validate the tricu implementation by copying its index arithmetic. It converts indices into globally fresh binder names, performs named substitution, and resolves names back to indices. Its shift oracle similarly inserts a gap in the outer environment. Body and RHS local names occupy separate fresh namespaces.

The recorded run compares complete located core trees for 195 substitutions and 128 shifts, including generated nested lambdas/lists and explicit capture, shadowing, outer-index, zero-shift, and span-origin cases.

Narrow rewrite gate

The rewrite considers only an immediate core application:

Apply (Lambda body) rhs

It requires all of the following:

1. The previous use/path analysis classifies the body as a candidate.
2. The RHS is either a literal Boolean tree, or a fully applied certified Boolean negation whose argument is a bound variable or literal Boolean.
3. The body contains no nested lambda at all, even one not mentioning the eliminated variable. This is deliberately stricter than the first screen.

The Boolean-result contract is trusted and bound to an exact compiled literal identity, like the selector certificate. It is not inferred from a name such as not. The integration harness compiles the known selector and negation with the accepted compiler and records their exact tree and source identities.

The candidate does not yet admit arbitrary computations which might return a Boolean, arbitrary constructor-valued RHSs, lambda RHSs, or negation applied to an unknown computation. This leaves the motivating not carry case available without using a broad function-valued substitution rule.

New diagnostics supplement the original analysis categories:

Code	Meaning
7	RHS does not meet the narrow Boolean gate
8	Nested lambda anywhere in the body
9	Node is not an immediate binding

Only code 1 rewrites. Every other decision returns the original core exactly. The whole-tree traversal treats an immediate binding as one decision unit: if it is rejected, none of its descendants are rewritten. Accepted bindings are substituted once; there is no fixed-point optimization loop. Other enclosing applications, lambdas and lists are traversed normally to find bindings.

This conservative policy avoids claiming that a rejected parent remains unchanged while silently optimizing code underneath it.

Isolated compiled pipeline

The harness stages the analyzer and substitution sources in a private workspace. It obtains a retained stableCompileCore worker from authenticated fixtures and checks two facts:

• its source snapshot matches the inspected stable abstraction source;
• its entire exact function tree occurs in the reachable closure of the shipped sourceBuildGraph compiler.

This second check binds the retained worker to the actual accepted compiler, not merely to a matching source filename. Original and transformed core are then separately compiled using that worker and executed on the unchanged Haskell reducer.

There is no replacement parser, no host numeric implementation, and no reducer modification. The Python named-variable implementation supplies independent expectations; the actual candidate transformation is performed by compiled tricu code.

Results

Structural transformation checks

There are 142 immediate-binding decisions checked against complete expected outputs, including all source spans. Eight are rewritten; every rejected node is byte-for-byte unchanged. Generated raw-core tests establish manipulation and gating behavior, not semantic equivalence of every possible open core program.

The whole-program corpus contains 18 earlier controls. Only three change:

Program	Decision
Single-use Boolean binding	Rewrite
Exclusive-branch Boolean binding	Rewrite
Adder-shaped negation binding	Rewrite
Constructor-valued binding	Reject: RHS outside narrow gate
Duplicated traversal	Reject: multiple path uses
Captured computation in returned lambda	Reject: lambda crossing
Unused divergent binding	Leave unchanged
Closed divergent branch binding	Reject: uncertified RHS
Eta controls and already-inline programs	Unchanged

For the three admitted programs, the candidate's emitted function tree is exactly equal to the corresponding manually inlined control's tree. The remaining 15 whole-program cores and their emitted function trees remain exact. This connects the new transformation to the previously measured source-form change without claiming a new runtime benchmark result.

Application, demand, and sharing controls

Independent concrete results include all Boolean combinations for branch and isolated-adder functions, actual list traversal outputs, unused divergent values, and unselected divergent branches.

Ten additional original/candidate partial-result checks cover:

• an ignored divergent flag;
• negation of a known Stem whose child diverges, observing only the known result;
• a known zero carry despite an unknown operand bit;
• a known one carry despite an unknown incoming carry.

All return the expected results for both original and transformed programs. This includes the demand shape that exposed the earlier incorrect mux adder.

The captured-closure and selected-divergent-branch controls are rejected by the pass, remain exact compiled trees, and retain their expected three-second full-observation timeouts in both versions. Four such bounded failures are recorded separately from successful value checks. A timeout is experimental bounded evidence, not a general proof of divergence.

The sharing control is not rewritten and retains its exact core and function tree, rather than merely returning the same duplicated list by a more expensive implementation.

test/binding_substitution_test.py adds seven intent tests for index handling, source origins, outer-span restoration, RHS/lambda rejection, and the rule that a rejected binding's descendants are left alone. The prior four classifier intent tests also pass.

What is and is not established

This is now an executable isolated rewrite candidate, not only an occurrence classifier. Its substitution mechanics, rejection behavior, known emitted trees, and selected runtime observations have been checked.

It is still not a universal equivalence proof for all reflective source contexts. The three transformed functions intentionally have different code trees from the originals. As with other compiler/backend changes, inspecting those function representations can distinguish the toolchains. The tests do not promise that an arbitrary intensional comparison involving a rewritten function is unchanged. The narrower obligations checked here include preserving the rejected closure hazard, ordinary data results, and explicitly tested partial-input demand.

No new performance percentage is claimed. The previous adder benchmark motivates the pass, and these controls prove correspondence to selected inline trees, but the candidate has not yet been integrated into a source compiler or measured on whole compilation workloads. It adds analysis work whose compile-time cost must also be measured.

Next acceptance boundary

The broader semantic and unpublished source-compiler investigation records the next stage and its initial cold-compilation timeout. A subsequent failure investigation completed unchanged retries, full arithmetic measurements and existing regression checks without reproducing that timeout. None of the adoption gates below has been waived.

Before considering adoption:

1. Broaden generated closed-program semantic/demand tests beyond raw-core manipulation, including reflective contexts with explicit expected outcomes.
2. Integrate only into an unpublished compiler candidate, with a defined certificate authority and eligibility diagnostics; do not trust source names.
3. Run the existing stable function-construction, local-scope, diagnostics, sharing, and intensional test suites.
4. Measure compile-time overhead and runtime effects on the original recursive arithmetic workload and unrelated real programs.
5. Decide and document the intended function-representation changes at the toolchain boundary before any promotion.

K eligibility and eta policy remain untouched. Public numeric encodings remain uncommitted, and the accepted compiler remains byte-for-byte unchanged.

Artifacts and reproduction

• Tricu candidate: bench/binding-substitution.tri
• Integration/oracle harness: test/binding_substitution.py
• Intent tests: test/binding_substitution_test.py
• Recorded evidence: bench/binding-substitution-results.json
• Raw run: /tmp/tricu-binding-substitution-final

The report records 114 successful invocation checks plus the four expected bounded demand failures, source/certificate/compiler/runtime hashes, 18 program comparisons, and the exact shipped-core-worker identity check.

HOST=$(nix build .# --no-link --print-out-paths)/bin/tricu
python3 test/binding_analysis_test.py
python3 test/binding_substitution_test.py
python3 test/binding_substitution.py "$HOST" \
  --directory /tmp/binding-substitution-new

Use a fresh directory and normal assertion settings. Compilation and execution have explicit memory and time bounds. No accepted artifacts are published.