PaperlayerView exact revision on arXiv

Source-linked AI summary

Typed Flexible-Arity Slotted E-Graphs: A Soundness Construction and an Alloy Case Study

Guanxuan Wu, Allison Sullivan

arXiv:2609.03998v2cs.PLcs.LO

TL;DR

Open terms with typed interfaces and algebraic operators with sequence, bag, or set children pose complementary representation needs. The paper specifies their composition with separate certificates and proves finite-unfolding soundness for abstract certified traces. In the Alloy study, the Certificate-Integrated IR recognized 4,088 correct equivalences versus 2,160 for De Bruijn baselines, alongside complete recovery of the constructed capability cases.

  • Problem

    Algebraic child carriers and open terms modulo consistent renaming are complementary representation needs, but neither alone covers an algebraic container holding a typed invocation of an open e-class.

    Source: §1 · p. 1

  • Method

    The paper specifies typed slot-mapped invocations in operator-declared ports, with separate certificates for sibling quotients, recursive flattening, and abstract obligation traces.

    Source: §1 · pp. 1–2

  • Results

    4,088 correct student–oracle equivalences were recognized by the Certificate-Integrated IR versus 2,160 for the De Bruijn baselines across 61,598 evaluated pairs, with no observed incorrect zero-distance matches.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The checked construction establishes exactness for a supplied finite quotient presentation and equates certified unfoldings that reach one leader and align by a recorded symmetry word.

    Source: §1 · p. 2, §6 · p. 20

    The trace theorem validates abstract obligation transformations, not concrete Java transition semantics, implementation evidence generation, unrestricted symmetry, saturation termination, or semantic completeness.

    Source: Theorem 1 (Certificate-Preserving… · p. 16

Abstract

from arXiv · show

Slotted e-graphs represent open terms modulo consistent renaming, while algebraic operators benefit from canonical sequence, bag, or set children. We compose the two at a specification level: typed slot-mapped invocations inhabit operator-declared ports whose sibling quotient and recursive flattening licenses are certified separately. A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision. For abstract obligation traces carrying local endpoint certificates, we prove finite-unfolding equational soundness. An Alloy case study compares seven related pipeline arms on a frozen corpus and a controlled transformation suite.

1 Introduction

The paper specifies a typed composition of slotted invocations and algebraic child quotients, with separate certificates for quotienting and flattening. It proves soundness for abstract certified traces and reports bounded Alloy evidence for seven pipeline arms.

1 Introduction

  • Typed flexible-arity ports compose slot-mapped invocations with operator-declared sequence, bag, or set children, while separate certificates license sibling quotients and recursive flattening.Equality-certified permutations act on exposed slots; descriptor-certified automorphisms act locally inside binder blocks.Source: §1 · p. 1
  • The quotient-first design extracts an exact-support leader kernel, minimizes local leader and binder orbits, then aggregates bags or deduplicates sets before free-slot renaming.Certified collision can create a parent edge only when the composed certificate has that edge’s exact directed type.Source: §1 · p. 2
  • Two abstract certified unfoldings that reach one leader and align by a recorded symmetry word are equal in every supplied model.The theorem consumes local obligation evidence; it does not verify operational rebuild implementation.Source: §1 · p. 2
  • 4,088 correct student–oracle equivalences were recognized by the Certificate-Integrated IR versus 2,160 for the De Bruijn baselines across 61,598 evaluated pairs.No zero-distance matches were observed among pairs labeled incorrect; slot-aware configurations also recognized all 5,500 constructed capability cases.Source: §1 · p. 2
  • The contributions comprise a typed port grammar, finite-orbit exactness and certified record interfaces, a finite-unfolding trace theorem, and a bounded Alloy study.The study’s evidence boundary is stated separately from the mathematical result.Source: §1 · p. 2

2 Background and Scope

The background motivates combining e-graph equality saturation, typed open-term interfaces, and algebraic child carriers. It distinguishes the construction’s certified scope from bounded Alloy checking and broader completeness or implementation claims.

2 Background and Scope

  • E-graphs retain equivalent alternatives in shared classes until an application-specific cost model selects a preferred expression.Rebuilding updates parent keys and merges newly identical parents after a merge.Source: §2 · pp. 2–4
  • Sequence children preserve order and multiplicity, bags forget order, and sets forget both; explicit AC saturation may materialize many parenthesizations and permutations.Open terms must retain their dependence on free variables, whereas consistently renamed bound variables are alpha-equivalent.Source: §2 · p. 4
  • Slotted E-Graphs represent open terms with finite slot interfaces and caller maps, while shapes quotient slot names and separately justified groups record symmetries.A coordinate may be removed only after independence is proved; De Bruijn indices do not express side-conditioned declaration-block permutations.Source: §2 · p. 4
  • Alloy equivalence checks search for predicate disagreement within specified object and trace bounds, so no disagreement is evidence only within those bounds.The evaluation inherits the dataset’s labels and reports its bounded checks separately.Source: §2 · p. 5
  • The construction covers declared Seq/Bag/Set ports containing typed slot-mapped invocations, and only visible same-type operator applications can be flattened.Carrier annotations alone introduce no semantic equation; the stated scope does not claim semantic completeness, unrestricted termination, parser correctness, full Java refinement, or full-corpus replay.Source: §2 · p. 5

3 Typed Flexible-Arity Slotted E-Graphs

The construction defines typed flexible-arity nodes and certified structural relations over finite contexts. Its checked results cover finite quotient presentations, graph-relative support and alignment, and abstract rebuild properties, while concrete producer procedures remain separate refinement obligations.

3.1 Typed contexts, embeddings, and ports

  • Complete binary AC closure has constructive finite codings of sizes 2^n − 1 and 3^n + 1 − 2^(n+1), with counting functions Θ(2^n) and Θ(3^n).This result motivates using flat carriers rather than materializing complete binary AC closure.Source: §3.1 · p. 5

3.2 Graph state and graph-relative structure

  • Typed embeddings preserve node output types and transport slots, while an invocation map embeds a class’s exposed interface into its caller.A proper parent embedding may contract invocation support; it is not itself a renaming or evidence of independence.Source: §3.1 · pp. 6, 8, §3.2 · p. 9

3.1 Typed contexts, embeddings, and ports

  • A checked port value is indexed by free context, typed bound scope, and schema; its schema distinguishes unary and block binders from arity-licensed Seq/Bag/Set containers.A Seq, Bag, or Set port requires respectively no sibling law, commutativity, or commutativity plus idempotence; flattening has a separate license.Source: §3.1 · p. 7

3.2 Graph state and graph-relative structure

  • The quotient-first normal form selects the least member of a finite generated orbit and preserves support, schema, leaf types, output, and idempotence.The exactness theorem is generic over a supplied finite quotient presentation; constructing that presentation with a particular recursive program remains a refinement obligation.Source: §3.2 · pp. 10–11
  • Effective-support canonical shapes are equal exactly when their extracted kernels admit a typed renaming, and this result does not assert renaming between larger ambient input contexts.The canonicalizer records a generally nonsurjective kernel-to-ambient inclusion rather than inverting ambient transport.Source: §3.2 · p. 11

3.3 Canonicalization and rebuilding

  • Finite rebuild traces reach quiescence when every step strictly decreases a natural-valued measure and every nonquiescent state admits a step.The reported budget is an accounting definition, not a proved asymptotic bound or Java runtime claim; the Lean development has no operational cost semantics.Source: §3.3 · p. 12

4 Certificate-Based Metatheory

The metatheory turns typed, locally certified obligations into equational certificates and proves their soundness in typed models. For abstract certified traces, it establishes coherent certificate families and finite-unfolding equality under specified leader and caller-alignment conditions.

4 Certificate-Based Metatheory

  • Typed equational certificates are finite derivation trees, and typed models evaluate certified structural alpha-equivalence and realization transport soundly.Block automorphisms require a supplied descriptor-local certificate rule; realization naturality is given by constructor-level equations.Source: §4 · p. 13
  • A proof-relevant direct structural derivation under a typed embedding yields an EqCert, which gives evaluation equality in every typed model.At the identity embedding, the equality is untransported.Source: §4 · p. 14
  • A coherent certificate family supplies endpoint certificates for stored cases, parent edges, and recorded symmetry generators.Identity, inverse, and composition derive certificates for represented symmetry words.Source: §4 · p. 14
  • Finite unfolding selects a stored case, extends its context, and replays a finite trace to a realization, preserving equational certificates.The related lemma also establishes certificate preservation along raw finite parent paths to a leader.Source: §4 · p. 14
  • A certified kernel-extraction record replays its finite provenance to produce an equational certificate from the original term to its exact kernel.The theorem validates a supplied record; constructing one from a concrete graph remains a refinement obligation.Source: §4 · pp. 14–15
  • For canonical records with matching typed context and shape, normalization replay and shape equality yield a directed kernel certificate that transports to a common context.The theorem requires equal output types and a common canonical context as premises, not as consequences of untagged payload equality.Source: §4 · p. 15

Theorem 1 (Certificate-Preserving Reachability and Finite-Unfolding

  • Certified traces preserve coherent obligations, and finite unfoldings reaching one leader are equal when a recorded symmetry word and caller-embedding equality align them.The result transports to a common typed context along equal caller embeddings; the nine trace-step families carry local certificates or typed endpoint bridges.Source: Theorem 1 (Certificate-Preserving… · pp. 15–16
  • The trace theorem validates abstract obligation transformations, not Java transition semantics, and does not establish implementation evidence, unrestricted symmetry, termination, or completeness.The formalization status treats abstract-kernel closure, Java refinement, and experimental replay as separate layers.Source: Theorem 1 (Certificate-Preserving… · p. 16

5 Implementation and Evaluation

The evaluation tests implementation observations, transformation capability, and cost on a frozen Alloy corpus and controlled suite, while distinguishing bounded implementation evidence from formal guarantees.

5 Implementation and Evaluation

  • Figure 2’s example reaches a common readable observation through certified implication elimination, type-preserving binder renaming, and ACI disjunction steps.The equality is relative to the declared certified rewrite theory, not a complete decision procedure for Alloy.Source: §5 · p. 16, Figure 2 · p. 17
  • The measurements do not establish Java-adapter refinement, semantic completeness for Alloy, or full-corpus replay by an independently verified checker.The corpus used in-process checks rather than complete exported-and-replayed traces.Source: §5 · pp. 17, 20
  • The frozen snapshot contains 61,598 AST-different student–oracle pairs: 19,212 labeled CORRECT and 42,386 labeled overconstrained, underconstrained, or both, across 181 invariant groups and 17 problem variants.The seven arms are controlled variants of the same Java pipeline, not executions of external e-graph systems.Source: §5 · p. 17
  • The repair projection compares temporal skeleton, binding view, and normalized matrix; its paired mean was 14.022 for Certificate-Integrated and 13.943 for Fast Rewrite.The coordinates use ordered dynamic programming, exact type-compatible binder-orbit matching, and carrier-specific child comparisons.Source: §5 · p. 18
  • On the 5,500-pair targeted suite, each slot-aware arm recognized every pair; for binder-block permutations, De Bruijn recognized 22/500 versus 500/500 for each slot-aware arm.These are in-vocabulary recognition results, not completeness or prevalence estimates.Source: §5 · p. 18
  • At radii 1, 2, 5, and 10, Certificate-Integrated IR coverage was 4.0%, 10.4%, 31.0%, and 59.3%, versus raw-AST coverage of 8.2%, 11.7%, 23.8%, and 43.0%.Each curve uses its own edit units, so the vertical difference is not an equal-budget improvement; the axis is capped at 50 while all 42,386 predicates remain in the denominator.Source: §5 · p. 18, Figure 3 · p. 19
  • 4,088 of 19,212 labeled-correct pairs received zero distance, while none of the 42,386 inherited incorrect pairs did.These are zeroes under the frozen implementation’s key, not a refinement proof or unbounded semantic soundness result.Source: §5 · p. 18, Table 1 · p. 19
  • Certificate-Integrated took 111.885 times Fast Rewrite’s process wall time and 593.026 times its engine CPU, consistent with an audit-heavy implementation rather than representation growth.The arm performs global validation, exact renaming and certificate work, rebuilds, and finite unfolding; its average pair-level representation-unit count was slightly smaller, 29.541 versus 30.001.Source: §5 · pp. 19–20

6 Conclusion

The conclusion combines typed flexible-arity ports and quotient-first canonicalization with a soundness result for abstract certified traces. Its Alloy study reports bounded corpus and capability outcomes, distinct from the mathematical guarantees.

6 Conclusion

  • The Alloy study recorded zero distance for 4,088 AST-distinct correct pairs across 61,598 evaluated pairs, with no observed incorrect zero-distance merges, and recovered all 5,500 capability cases.These implementation observations are bounded; the paper distinguishes them from the mathematical result.Source: §6 · p. 20
  • Typed flexible-arity ports combine certified sibling quotients, separately licensed flattening, bound-name alpha-renaming, and equality-certified slot symmetry.The quotient-first theorem is exact for a supplied finite quotient presentation, while certified records expose evidence for effective-support extraction and collision.Source: §6 · p. 20
  • For abstract local-obligation traces, two certified unfoldings reaching one leader and aligned by a recorded symmetry word are equal in every supplied typed model.The traces preserve a coherent witness family.Source: §6 · p. 20

A Formal Statement Index and Proof Details

The section indexes the paper’s formal units and compiled Lean declarations, recording their source locations and relationships while distinguishing the statement inventory from Java-facing artifacts and implementation claims. It also summarizes scoped results and edge-case assessments by layer without treating archived assessment or bounded replay as evidence of Java-to-Lean refinements.

A Formal Statement Index and Proof Details

A.1 Complete formal statement index

  • 146 active formal units have an exact 146-ID/146-declaration source-tag bijection, with each row naming one distinct Lean declaration.The suffix is the first twelve hexadecimal digits of the exact pretty-type SHA-256.Source: §A.1 · p. 24
  • The index includes typed-context, embedding, port-schema, and invocation declarations, including concrete embedding type preservation and invocation type safety.Source: §A.1 · p. 24
  • The inventory names both foundational definitions and proof units, including typed-embedding category laws, concrete slot-support invariance, and concrete invocation type safety.Source: §A.1 · p. 24
  • Normalization and canonicalization entries include ambient quotient normal-form exactness, effective-support canonicalization, and finite canonicalization and collision contracts.Source: §A.1 · p. 25
  • The indexed units also cover finite rebuild quiescence and typed equational certificates, models, evaluation, and binder-admissibility naturality.Source: §A.1 · p. 25
  • The index lists declarations for concrete typed alpha-semantic soundness, structural realization and naturality, and port-and-node congruence certificates.These entries are identified by Lean declaration names and source references.Source: §A.1 · p. 25
  • Certificate-related entries cover coherent certificate families, finite unfolding, preservation, certified leader-kernel extraction, shape collision, and finite-unfolding soundness.The index also names local certified traces and certificate-preserving reachability.Source: §A.1 · pp. 25–26
  • The listed counterexamples address parent equality without child symmetry and proper embedding without independence.A further entry names an overflow-reassociation counterexample.Source: §A.1 · p. 26
  • Algorithm contracts include kernel-trace replay, canonical records and occurrences, leader-port handling, abstract rebuild, and certified canonicalization pseudocode.The index names both pseudocode contracts and profile-rule contracts for these operations.Source: §A.1 · p. 26
  • The ordered rule-pipeline entries include parser normalization and cleanup, capture-avoiding let-beta, branch elimination, and Boolean-negation normalization.The index names these as contracts for rules in the pipeline.Source: §A.1 · p. 26
  • Further rule entries cover negation duals, quantifier transformations, descriptor-certified block permutation, operator-law boundaries, and local saturation.The listed rules include modular-integer AC profiling and Boolean, atomic-complement, relational, and implication saturation.Source: §A.1 · p. 26
  • Atomic and structural entries include binary AC class and node counts, typed-slot embedding and renaming, concrete port action, and flexible-arity e-node action.The index identifies these declarations alongside their source locations.Source: §A.1 · pp. 26–27
  • Concrete invocation declarations cover port and node support images, identity and composition, and unindexed alpha-port equivalence laws.Source: §A.1 · p. 27
  • The quotient normal form is indexed with soundness, an equivalence characterization, support and schema preservation, and idempotence.Source: §A.1 · p. 27
  • The index includes canonicalizer claims that shape equality characterizes effective-kernel typed renaming and that canonicalization preserves output.Source: §A.1 · p. 27
  • The statement index lists certified reachability coherence, collision certificates, and local steps for insertion, canonicalization, and collision.Other indexed local steps include union, symmetry, interface restriction, rebuild, and path compression.Source: §A.1 · pp. 27–28
  • The finite-unfolding declarations state equational and model soundness, including a common-context weakening result.The index also lists a finite-unfolding witness certificate.Source: §A.1 · pp. 27–28

A.4 Foundation and evidence boundary

  • Proof-bearing declarations use the standard-lean-explicit-tcb profile, with propext, Quot.sound, and Classical.choice as the only permitted foundational axioms.Each proof-bearing declaration receives a per-declaration axiom report; tests and corpus measurements do not establish a Lean refinement.Source: §A.4 · p. 32

A.5 Artifact-refinement boundary

  • No row in the archived artifact-refinement assessment has a Lean refinement proof or Lean-checked implementation trace.“Exact Lean specification” means a distinct compiled declaration for the paper-side contract, not that the listed Java producer refines it; newer bounded replay evidence is separate and does not establish full component refinements.Source: §A.5 · p. 32, Table 4 · p. 32
  • The artifact-boundary index includes exact Lean rule specifications and property/mutation tests, but the listed text does not establish their outcomes.Source: §A.5 · pp. 32–33
  • A bounded partial-repair row is marked PARTIAL, without a broader implementation-status claim in the supplied text.Source: §A.5 · p. 33
  • The index separately names an independent non-Lean checker and operator-law routing, without specifying their results here.Source: §A.5 · p. 33
  • The paper–Lean registry has 146 units, while the implementation bridge consists of eight Java-facing rows; closing the former does not upgrade the latter’s statuses.Source: §A.5 · p. 33
  • Pure Java/run-manifest evidence is listed as a distinct scope boundary from exact Lean specifications.Source: §A.5 · p. 33

A.6 Edge-case closure summary

  • Table 5 summarizes edge-case closure by layer; “proved narrow claim” denotes a scoped Lean result, not an end-to-end implementation fact.Source: §A.6 · p. 33, Table 5 · p. 33

A.2 Structural proofs

The structural proofs establish typed renaming laws and support properties, invocation-level transport, quotient-normal-form exactness, and rebuild quiescence under explicit assumptions. Their claims remain scoped: invocation support is not structural support, and the quotient theorem does not verify a recursive normalization program.

A.2 Structural proofs

  • Identity embeddings and composites of injective, type-preserving maps remain injective and type preserving, while stored inverse laws establish the renaming inverse directly.The inverse proof uses no finite-cardinality or surjective-injection argument.Source: §A.2 · pp. 28–29
  • The concrete renaming action preserves schema, output type, and support, while carrying bound indices separately and introducing no fresh free coordinate.Support after action is exactly the direct image of prior support for every target slot.Source: §A.2 · p. 29
  • Typed embeddings preserve invocation-image containment, but the leader-support result does not extend to arbitrary ports or nodes or establish independence from a missing coordinate.For an invocation image, the parent-path embedding supplies a witness that the slot lies in the caller-map image.Source: §A.2 · p. 29
  • The alpha-equivalence judgement has identity, inverse, and composition laws because it is defined as the reflexive–symmetric–transitive closure of direct structural generators.The container and binder clauses belong to the direct generator; F13 does not separately prove them closed under inversion.Source: §A.2 · p. 29
  • Graph-relative transport uses checked parent paths, a common leader, admitted symmetry, and an embedding equation to establish invocation-level transport.It does not assert recursive container or binder transport.Source: §A.2 · p. 29
  • For leader invocations, identity alignment reduces to an admitted typed permutation, yielding pointwise equivalence of the two invocation-image predicates.The proof uses the permutation in the forward direction and its stored inverse in the reverse direction; it is not a structural-support theorem.Source: §A.2 · p. 29
  • The least-orbit normal form is exact for a finite quotient presentation, and shape equality is characterized by a nonempty kernel correspondence under renaming.The shape theorem derives from quotient exactness and kernel-output equations; it constructs neither an ambient input-context renaming nor a least renaming witness.Source: §A.2 · p. 30
  • Rebuild reaches quiescence when every nonquiescent state has a decreasing successor under a natural-valued strict measure.Well-founded induction closes the proof with a reflexive trace at quiescent states; no particular worklist or lexicographic implementation measure is specified.Source: §A.2 · p. 30

A.3 Certificate and semantic proofs

The appendix builds soundness from certified local equations and endpoint evidence, then proves finite-unfolding evaluation equality for abstract certified traces. The results depend on supplied laws and certificates rather than establishing their concrete construction or implementation refinement.

F20: semantic alpha-soundness

  • F20 derives semantic alpha-soundness by induction on alpha-closure, using supplied structural laws and typed-certificate soundness to establish equality for every target environment.Descriptor automorphisms are usable only through the supplied policy and local certificate laws.Source: §A.3 · p. 30

F21: realization naturality

  • F21 proves realization commutes syntactically with renaming by constructor-level naturality, without fresh-name choices or sibling and flattening laws.The mutual recursor covers complete values and child forests.Source: §A.3 · p. 30

F22: certified congruence

  • F22 turns certified leaf endpoints and supplied one-constructor laws into node congruence, then obtains the model result through typed-certificate semantic soundness.The proof assumes licensed local constructor rules and per-leaf certificates rather than deriving them from graph metadata.Source: §A.3 · p. 31

F23: coherent certificate family

  • F23 specifies coherence by requiring (EC), (PC), and (SC) certificates for stored-case, parent-edge, and symmetry-generator endpoint families.It is a coherence specification, not an existence theorem; F27 supplies coherence for the final obligation family from a certified trace.Source: §A.3 · pp. 31–32

F24: find and finite unfolding

  • F24 combines certified parent-path finding with finite unfolding of one stored case and a compatible caller extension to produce endpoint certificates.It makes no redundant-coordinate-independence claim.Source: §A.3 · p. 31

F25: certified kernel extraction

  • F25 replays an explicit certified kernel-extraction record into an equational certificate, without claiming an algorithm constructs that record.The record includes the original term, exact kernel, typed inclusion, and finite replay.Source: §A.3 · p. 31

F26: certified collision

  • F26 derives an ambient source certificate from certified canonical records when their shapes are equal and their output and context indices are shared.The proof assumes those shared-index conditions and shape equality; it does not derive them.Source: §A.3 · p. 31

F27: trace preservation and finite-unfolding soundness

  • F27 preserves obligation coherence across nine abstract local-trace constructors, producing the coherent final endpoint state needed to establish F23.The preservation schemas cover adding, rekeying, composing, and removing obligations with checked endpoint bridges; they do not prove refinement of particular graph code.Source: §A.3 · p. 32

B Evaluation Detail

The appendix documents the measured pipeline, corpus views, and distance summaries while distinguishing implementation observations from formal guarantees. It reports bounded, manifest-bound measurements rather than implementation refinement or distributional timing evidence.

B Evaluation Detail

  • The Certificate-Integrated arm is an in-process certificate-checked observation, but its complete traces were not exported for independent replay and it establishes no Java–theory refinement.The recorded measurements are bound to a repository snapshot, run, source commit, dataset, and executable; those identifiers do not certify conformance to the formal model.Source: B Evaluation Detail · pp. 33–34

B.1 Arms and Representation Boundaries

  • The evaluation arms use different representation boundaries, and the front end records typed ports, supports, binder descriptors, witnesses, transition certificates, and bounded finite unfoldings.The repair projection removes proof and schema plumbing before measuring distance; runtime checks and empirical outputs do not prove conformance to the paper construction.Source: Table 6 · p. 34, §B.1 · p. 34

B.2 Corpus Views and Distance Summaries

  • Table 8 counts recorded truths within each invariant group, with Certificate-Integrated classes defined by CI equality and equivalent pairs counting AST-different pairs within those classes.Table 10's ten schema rows do not map one-to-one to the 17 variants because variants can share a base schema; its counts give model-size context.Source: Table 8 · p. 35, §B.2 · p. 35, Table 10 · p. 36
  • Corpus comparisons stay within invariant groups, while each repair coordinate chooses its own nearest reference and uses its own edit unit.The augmented truth pool removes raw-AST duplicates; canonical-representative tree edit distance is diagnostic, not the primary repair metric. Table 7 reports view-specific structural-unit counts, and Table 9 cautions that distance coordinates have different units.Source: §B.2 · p. 35, Table 7 · p. 35, Table 9 · p. 36

B.3 Full Ablation and Targeted Recognition

The evaluation reports a seven-arm ablation on a frozen corpus and a targeted transformation-recognition suite. The supplied evidence defines the suites' scope but does not support a winner or a cross-system performance ranking.

B.3 Full Ablation and Targeted Recognition

  • Table 11 records a seven-arm ablation on 61,598 AST-different pairs, with Fast Rewrite and Certificate-Integrated as its final two arms.The compact Table 12 aliases map Fix., F+DB, Var., V+DB, Slot, Leg., and Exact to Raw, Raw + De Bruijn, Java egglog, Java egglog + De Bruijn, Slotted, Fast Rewrite, and Certificate-Integrated.Source: Table 11 · p. 37, §B.3 · p. 38
  • The targeted suite tests historical representation and pipeline recognition, not semantic completeness or prevalence.Table 12 contains rows of 500 AST-different pairs for each named, side-conditioned transformation.Source: §B.3 · p. 37, Table 12 · p. 37
  • Each natural-corpus arm completed the recorded pairs, but one fresh-process run per arm supports neither distributional timing claims nor a cross-system performance ranking.Because arms combine normalization and representation boundaries, transitions are pipeline-level attributions rather than estimates for individual rewrite rules.Source: §B.3 · p. 38

B.4 Checker Boundary and Threats to Validity

The section bounds the checker evidence and states the canonicalization specification, including how typed slotted graph data and effective support are represented. Its proofs concern abstract interfaces and bounded checks, not full Java or parser refinement.

B.4 Checker Boundary and Threats to Validity

  • Bounded Alloy analysis found no counterexample or solver error for 4,088 labeled-correct identities and completed all 29 sampled capability checks without counterexample, error, or inconclusive result.Eight checks used bounded temporal solving at scope 4 with trace bounds 1–10; four invalid probes were rejected.Source: §B.4 · p. 38
  • The natural corpus contains short educational specifications with inherited labels, and excluding identical ASTs conditions the analysis on syntactic difference.Distances are not calibrated semantic-error probabilities, and the data do not establish industrial generalization, operational repair success, full semantic equivalence, or Java–theory refinement.Source: §B.4 · p. 39

C Canonicalization Algorithm and Rewrite Theory

  • The Alloy and Java names are refinement targets for the abstract rewrite theory, not a proved implementation correspondence.The Lean development proves finite-orbit normalization and specified Boolean, list, finite-function, and relation equations.Source: C Canonicalization Algorithm and… · p. 39

C.1 Notation and Preconditions

  • A typed slotted e-graph stores parent assignments, per-class type and slot data, canonical shapes, justified slot symmetries, and a shape-collision index.Finding composes parent links to return a leader invocation in caller context.Source: §C.1 · p. 39
  • Sequence, bag, and set ports respectively preserve order and multiplicity, quotient by permutation, and quotient by permutation plus idempotence.A binder block carries a complete descriptor, a fresh occurrence-local bound context, and its certified finite automorphism group.Source: §C.1 · p. 39
  • The indexed extraction theorem replays structural traces into equality between endpoint denotations for any two interpreters that supply equality for every trace label.It does not identify those equalities with EqCert or prove that Java extraction emits the required trace.Source: §C.1 · p. 40
  • The shape witness maps canonical slots bijectively to effective support, while ambient transport preserves the original context, including coordinates removed by find.Binder-block automorphisms act only on bound coordinates licensed by the full descriptor and remain separate from global free-slot renaming.Source: §C.1 · p. 40
  • In a strict-support case, a leader kernel can use a proper subset of the input slots, so the construction keeps its effective-support witness separate from ambient transport.The canonical context is built from the reduced support, with a proper embedding back into the original context.Source: §C.1 · p. 40

C.2 The Graph-Relative Canonicalizer

The appendix specifies a graph-relative canonicalizer and formal rewrite contracts, while distinguishing abstract proofs from implementation-refinement obligations. Its claims range from finite-presentation exactness to Boolean, quantifier, and flexible-arity equations.

C.2 The Graph-Relative Canonicalizer

  • For any finite presentation, least-orbit normalization is exact, but graph-relative and rebuild claims remain abstract contracts rather than a verified producer.The proposed design minimizes invocation and binder-block orbits before bag aggregation and set deduplication; the concrete Figure 4 procedure remains a refinement target.Source: Figure 4 · p. 41, §C.2 · p. 43

C.3 Ordered Application of Rules

  • Rule-001 lists nine formal stages, but its phase theorem only preserves the stored phase index and does not establish Java execution order.The listed stages run from parser cleanup through local saturation and rebuild.Source: §C.3 · pp. 43–44

C.4 Parser and Structural Normalization

  • Formal parser and substitution rules include singleton-list cleanup and scoped let substitution, without establishing Java parser or substitution behavior.Lifted substitution fixes the newly bound coordinate 0.Source: §C.4 · p. 44

C.5 Branch Connectives and Boolean NNF

  • Boolean NNF and atomic-dual equations are formal truth-function results, while Alloy conditional classification and parser-specific operator behavior remain refinement obligations.The dual theorem is conditional on the supplied atomic-dual lookup returning the reverse operator.Source: §C.5 · p. 45

C.6 Temporal Negation

  • Temporal-dual normalization is proved conditionally from the supplied dual lookup, not as a temporal-semantics or Java-handling result.The reverse lookup must return the original operator.Source: §C.6 · p. 45

C.7 Quantifier Rewrites and Prenexing

  • Quantifier results cover finite Boolean lists and formal empty-domain cases; binding-tuple and binder-permutation claims do not establish Alloy-body semantics.For an empty admissible-value list, the seven quantifier outcomes are proved by evaluation; accepted finite permutations are tied to a supplied descriptor list.Source: §C.7 · pp. 46–47

C.8 Flexible-Arity Structural Laws

  • Flexible-arity laws include formal finite-integer associativity and commutativity, but linking the models to Alloy or Java integer modes is outside the proofs.The modular profile sets both flat flags; the overflow-forbidding profile clears both.Source: §C.8 · p. 47, Table 15 · p. 47

C.9 Local Saturation Rules

  • Local saturation establishes Boolean identities, while recognizing concrete operator duals and equal canonical invocations remains an implementation premise.The formal rules also cover atomic polarity complement and abstract predicate reasoning, not typed Alloy AST or Java rewrites.Source: §C.9 · p. 48

C.10 Boundary and Implementation Correspondence

The section defines a discrete canonical distance from an arbitrary complete finite normalization presentation. Its zero-distance equivalence follows from normal-form exactness, without identifying the function with dataset AST edit distance or a concrete implementation.

C.10 Boundary and Implementation Correspondence

  • Canonical distance is defined as 0 when two inputs have equal normal forms and 1 otherwise.The definition applies to an arbitrary complete finite normalization presentation P.Source: §C.10 · p. 49
  • A distance of 0 is equivalent to the inputs being related by P.This equivalence follows from the presentation’s normal-form exactness.Source: §C.10 · p. 49
  • The theorem neither identifies this function with dataset AST edit distance nor proves that the appendix rules form one presentation or correspond to production behavior.Graph-relative enumeration, binder-group closure, permutation limits, and rewrite bounds remain artifact-only obligations.Source: §C.10 · p. 49
Loading 2609.03998v2…