binding-analysis-prototype.md (8916B)
Binding transformation: analysis-only prototype
This implements the first step proposed by the stable abstraction investigation. It is executable tricu compiler-analysis code, not a source-text heuristic. It does not rewrite programs, change the stable backend, or publish a compiler.
Implementation and interface
bench/binding-analysis.tri consumes the existing resolved-core node schema:
(kind, (payload, (start, end)))
The input body is scoped under the binding being considered. Index 0 denotes that binder; when traversing a nested lambda the target index increases. Inner parameters which shadow names therefore are not mistaken for captured uses. There is no source-name lookup in the analyzer.
The standalone probe interface is:
inspect (certifiedSelectorTree, bodyCore)
-> (classification, summary)
The summary contains:
- total syntactic occurrences;
- maximum uses along an evaluated path;
- occurrence below a lambda;
- occurrence passed through an unknown consumer;
- occurrence in a partial selector application;
- an unsupported-kind/malformed-list flag.
The analyzer assumes trusted, well-formed resolved core from the compiler. It is not a validator for arbitrary hostile core encodings; the last flag catches unsupported kinds and certain unexpected list shapes, not every malformed payload. It leaves the input and its source spans untouched.
Certificates are explicit identities, not names
The integration harness compiles a small, known selector with the accepted compiler. It records its source hash, bundle hash, exact literal-tree hash, arity, and the explicit harness assertion of its selector contract:
- three arguments;
- arguments 0 and 1 are alternatives;
- argument 2 is the selector.
The tricu analyzer compares a resolved external literal against that exact tree.
An alias of the same literal is recognized. A parameter shadowing choose, or
a different literal with the same suggested source name, is not recognized.
Partial and oversaturated applications are not treated as certified selection.
The contract is trusted input to this prototype. Hash identity establishes which compiled tree is being discussed; it does not independently prove that an arbitrary tree satisfies a selector contract. There is no production certificate registry or automatic inference from an unfamiliar helper yet. A caller cannot legitimately obtain an optimization by merely claiming its function is a selector.
Likewise, only explicit Leaf construction or literal Leaf/Stem heads within their constructor arity are recognized as construction. Literal Fork application is an unknown computation. Proper list nodes are treated as data construction.
Path accounting
For ordinary construction, the analyzer adds child path-use bounds: both fields may eventually be inspected. For a certified selector it uses:
conditionUses + max(yesBranchUses, noBranchUses)
It still sums both branches when reporting syntactic occurrences. These are conservative occurrence bounds, not measured reduction or allocation counts. Repeated condition values are not assumed to have been evaluated already.
Unknown consumers involving the binder are rejected. For example, an opaque function could duplicate or retain its argument; one textual occurrence is not sufficient evidence of one dynamic use. Occurrences below a lambda are rejected regardless of the path-use bound.
Diagnostic categories
| Code | Meaning | Prototype action |
|---|---|---|
| 0 | No uses | Leave unchanged |
| 1 | Passes this candidate screen | Record for further verification; do not rewrite |
| 2 | More than one use on a path | Reject |
| 3 | Crosses a lambda boundary | Reject |
| 4 | Unknown consumer | Reject |
| 5 | Partial selector application | Reject |
| 6 | Unsupported core kind / detected malformed list | Reject |
The summary keeps multiple flags even when the primary diagnostic reports only one. Lambda and partial-selector diagnostics take precedence over the generic unknown-consumer diagnostic.
Results on the motivating examples
| Example | Syntactic uses | Maximum path uses | Classification |
|---|---|---|---|
| Single-use binding | 1 | 1 | Candidate |
| Exclusive branch binding | 2 | 1 | Candidate |
| Constructor-valued exclusive branches | 2 | 1 | Candidate |
| Adder-shaped negation binding | 2 | 1 | Candidate |
| Duplicated shared traversal | 2 | 2 | Reject: multiple path uses |
| Captured computation in returned lambda | 1 | 1 | Reject: lambda boundary |
| Unused divergent value | 0 | 0 | Leave unchanged |
| Binding used in both condition and selected branch | 2 | 2 | Reject: multiple path uses |
| Alias of certified literal | 1 | 1 | Candidate |
| Shadowed/different selector | 1 | 1 | Reject: unknown consumer |
| Partially applied selector | 1 | 1 | Reject: partial selector |
The important separation is preserved: the adder opportunity survives, while both concrete counterexamples from the previous stage are rejected.
Independent validation
test/binding_analysis.py generates actual resolved-core trees and executes the
compiled tricu analyzer. Its Python oracle independently enumerates the sets of
possible path-use counts; it does not merely implement the same max-propagation
recurrence. It compares the complete output trees, including all summary flags.
The recorded run checked 277 bodies:
- binding bodies extracted from the earlier explicit expression fixtures;
- selector identity/alias/shadow/arity controls;
- constructor, unknown-call, list, nested-scope, and unsupported-kind controls;
- 256 deterministic generated core expressions.
All decisions and summaries match the oracle. The corpus yields 26 candidates, 15 multiple-path-use rejections, 87 lambda-boundary rejections, 59 unknown-consumer rejections, five partial-selector rejections, one unsupported-kind rejection, and 84 unused bindings left alone.
test/binding_analysis_test.py supplies four additional intent tests, including
explicit expected classifications for the named controls, condition-use
accounting, and nested de Bruijn shadowing/capture. These prevent agreement
between implementations from being the only statement of intended behavior.
The recorded source, runtime, compiler and certificate hashes are in
bench/binding-analysis-results.json. Raw source snapshots, bundles, core input
files, result trees and command logs are in /tmp/tricu-binding-analysis-first.
No performance improvement is claimed for this pass yet; it currently adds
analysis work and changes no emitted program.
What “candidate” does not establish
This first pass analyzes uses of the binder in the body. It does not analyze the RHS, prove all function-tree observations equivalent, establish a cost model, or perform capture-avoiding substitution. It also does not prove a general rule for consumers beyond the explicitly trusted selector/constructor contracts.
In particular, passing this screen is not enough to enable an optimization. The current output is useful eligibility evidence and a rejection reason, not a completed safety certificate. The prototype is intentionally outside the production compiler, with no rewrite switch hidden behind its classification.
Next implementation boundary
An isolated Boolean-binding substitution candidate now implements the next stage with a stricter RHS/body gate, independent named substitution oracles, and compilation through the exact shipped stable core worker. This analysis module itself remains analysis-only; production rewriting is still disabled.
Before constructing an unpublished compiler candidate:
- Specify the additional RHS and structural-observation obligations for the narrow subset that will actually be rewritten.
- Implement capture-avoiding resolved-core substitution with explicit handling of source spans, outer indices, and nested scopes; test it independently.
- Test original and transformed programs with finite values, partial inputs, returned-function observations, and sharing controls. Keep rejected core byte-for-byte unchanged.
- Connect the pass only to an isolated backend/toolchain build, run existing stable construction and intensional controls, and measure compilation overhead as well as runtime savings.
No eta contraction or weakening of the stable K guard is part of this direction. The accepted compiler and all public numeric encodings remain unchanged.
Reproduce
HOST=$(nix build .# --no-link --print-out-paths)/bin/tricu
python3 test/binding_analysis_test.py
python3 test/binding_analysis.py "$HOST" \
--directory /tmp/binding-analysis-new
Use a fresh directory and normal assertion settings. The harness explicitly selects the shipped stable compiler and applies process/whole-run resource bounds.