Stable abstraction: binding cost, K restrictions, and safety boundaries

This follows the adder/source-form investigation. The priority is now compiler investigation; arithmetic supplies a realistic workload, not a reason to weaken lazy or reflective semantics. No production compiler, reducer, or math-library changes have been made.

Trace through the existing compiler

sourceResolveLocal in lib/source/resolve.tri lowers a nonrecursive local to:

Apply (Lambda body) value

There is no separate let node in resolved core. stableCachedEliminate in lib/source/stable.tri eliminates the lambda before handling the application. The binding therefore creates an extra abstraction pass. The resulting residual then participates in elimination of enclosing binders.

stableCachedBracket has three relevant behaviors:

• literals and independent variables can become K applications;
• independent certified constructor applications can also be put under K;
• dependent applications, and independent applications not certified safe for K, are distributed recursively using the native application abstraction rule.

There is no general eta contraction. These restrictions are deliberate: closed computations must not be executed merely to construct a function tree.

An exact-tree diagnostic model

test/abstraction_binding_model.py is an independent finite Python model of the stable residual annotations, lowering, bracket abstraction, constructor folding, and final normalization. It counts abstraction-rule decisions by binder.

test/abstraction_bindings.py generates matching source from the same explicitly specified expression ASTs and compiles it with the accepted stable compiler. The model uses the actual compiled helper trees as opaque literals, then predicts the complete compiled tree for each target function. All 18 predicted trees match exactly, through canonical DAG interning, not merely by applying them to a few numeric arguments. The model does not model the parser or rebuild helper functions; its validated scope is the target expressions' abstraction.

The model's final normalization is eager and applies only to these finite compiled controls. It is not a substitute reducer or a performance model. Counts below are compiler rule firings, not measured runtime reduction counts.

Attribution: the original smell was useful, but not the whole diagnosis

The isolated full-adder expression binds neg = not carry and uses it in two mutually exclusive branches, or writes the negation directly in those branches. Both return the sum/carry Boolean pair. All eight total Boolean combinations were checked for both versions.

Target	Dependent application distributions	Independent computation distributions	Reachable compiled DAG nodes
Adder-shaped bound expression	119	8	196
Adder-shaped inline expression	60	1	154
Simple exclusive branches, bound	28	0	94
Simple exclusive branches, inline	11	0	82
Constructor-valued exclusive branches, bound	28	0	86
Constructor-valued exclusive branches, inline	11	0	74

For the adder-shaped example, all eight independent-computation distributions occur while eliminating the local binder. The expanded residual then entails more work under the remaining carry/bit binders. That supports the hypothesis that conservative K eligibility interacts with the extra abstraction layer.

But the simple branch example has no rejected independent-computation K opportunities, and still has substantial additional abstraction from the binding. Replacing its computed value with a known constructor gives the same rule counts. Therefore:

The extra let/beta abstraction layer is a real cost. Conservative K handling contributes in the adder-shaped case, but is not the sole cause. We have not identified an eta redex as the primary explanation.

Relaxing the K guard would target a deliberately protected boundary rather than cleanly eliminating this source-level overhead.

Nonnumeric performance controls

Recorded run: five fresh-process repetitions, first excluded, shuffled order, full-result forcing before rendering, unchanged single-capability Haskell host. The three branch/constructor/single-use workloads use every Boolean input combination repeatedly. These small workloads are not expected to reproduce whole multiplication speedups.

Workload	Bound allocation	Inline allocation	Bound / inline median time
Single use, batch 1024	11.488 MB	11.283 MB	3.366 / 3.367 ms
Exclusive branches, batch 1024	16.428 MB	15.593 MB	4.444 / 4.089 ms
Constructor-valued branches, batch 1024	14.124 MB	13.289 MB	4.028 / 3.925 ms
Shared traversal, 512 elements	5.474 MB	7.737 MB	3.601 / 4.253 ms

MB are cumulative decimal allocated bytes, not live/peak memory. Timing includes profiling collection overhead; small differences should not be overinterpreted. The isolated single-use workload shows essentially no time separation despite a smaller emitted tree.

Negative sharing control

The final row compares:

let z = copy xs in t z z

with:

t (copy xs) (copy xs)

Here copy traverses a list and wraps each element. Both result branches are fully observed. Inlining increases allocation by about 41% at 512 elements. Removing bindings indiscriminately is therefore an experimentally demonstrated regression, not merely a theoretical concern. The inline compiled function is slightly smaller, again showing that code-tree size alone is not a runtime cost model.

Negative semantic controls

Captured computation versus delayed function body

These source forms are not interchangeable under full tree observation:

closureBound x = let z = loop x in ignored : z
closureInline x = ignored : loop x

where loop x = loop x.

After supplying a finite x:

• Fully observing closureBound x exceeds the three-second limit. Its returned function contains a captured shared computation which full observation forces.
• closureInline x returns a finite function tree. Its exact 182-byte tree encoding agrees with the independent model's prediction.
• Applying either returned function to an ignored argument exceeds the limit.

This is a returned-function observation, not a claim that merely obtaining weak head normal form of the bound function must diverge. The benchmark observer fully traverses the returned tree.

Crucially, z occurs only once in the source. A single-use substitution rule alone is not enough to preserve this behavior. Escaping/nested function construction needs its own treatment. Three-second timeouts are bounded observations; the source explains the recurring computation they encounter.

The unused-binding and unselected-divergent-branch controls succeed in both forms. Selected-divergent-branch controls time out as expected. Thus the closure finding is not just a broken general implementation of lazy selection.

Eta changes an observable constructor

The controls:

etaExpanded f = arg : f arg
etaContracted f = f

both construct the same Stem result when supplied f = t and a subsequent argument. But after supplying only f = t, the expanded version is a Fork and the contracted version is Leaf. Complete returned trees are checked against the independent model, and the unequal outer tags are asserted.

Therefore general eta contraction can change a direct triage observation; this is stronger than merely producing a different opaque function hash. The existing no-general-eta policy is justified by a concrete control.

What this suggests for a compiler candidate

The first executable analysis-only binding classifier is now implemented and checked against an independent path-enumeration oracle. It recognizes the adder opportunity and rejects the sharing/closure controls; rewriting remains disabled.

The evidence supports investigating elimination or sinking of a binding before it incurs repeated bracket abstraction, rather than disabling K's safety checks. A candidate needs explicit certificates or conservative exclusions for:

1. Use multiplicity and real sharing: reject the duplicated-traversal case.
2. Escaping or nested function construction: reject the captured-computation counterexample even though it has one occurrence.
3. Proven branch exclusivity: a function named choose is not itself evidence that its arguments are mutually exclusive; aliases and arbitrary callers must not be guessed from spelling.
4. Structural observations and source diagnostics, as well as application results and finite-value arithmetic.

A useful next prototype is a narrowly scoped core/source transformation with explicit eligibility diagnostics, initially testing single-use non-escaping forms and then certified exclusive branches. Those conditions are a research plan, not a sufficiency proof or an implemented optimization. Existing stable function-construction and intensional controls must accompany any rebuilt compiler candidate. The accepted toolchain remains untouched.

Artifacts and checks

• Model: test/abstraction_binding_model.py
• Harness and source generator: test/abstraction_bindings.py
• Recorded result: bench/abstraction-binding-results.json
• Raw staged source, bundle, inputs, outputs, logs: /tmp/tricu-abstraction-bindings-recorded

The recorded run has 18 exact compiled-tree matches, 90 checked timed invocations, 16 total-Boolean adder checks, four eta tree/application checks, and 12 demand/closure checks (including five expected bounded timeouts). All data-producing checks match independent expectations. Reports bind the runtime, compiler, generated source, model, and harness hashes.

HOST=$(nix build .# --no-link --print-out-paths)/bin/tricu
python3 test/abstraction_bindings.py "$HOST" \
  --directory /tmp/abstraction-bindings-new --repeats 5

Use a fresh output directory and do not disable Python assertions. Each process has a 2 GiB heap limit; the whole job is bounded. No production artifacts are published by the harness.