Semantic Completeness for Correct Maintenance: A Strict Hierarchy of Typing and Inheritance
When typing or inheritance does not derive a required answer, correct code or tooling must supply it elsewhere. We count these semantic obligations, not source lines, and minimize them over every refactoring preserving declared identities, memberships, and independent implementations. Each restriction has an exact price. Structural typing needs retained names when edits erase distinctions. Contracts carry membership but no code, so required implementation-class connections remain outside ancestry. Whenever authoritative providers are comparable at each consumer, as under one parent, linearization, mixin sequencing, or trait resolution, the ancestry gap d_↓ is the fewest such connections any sound repair leaves outside. This minimum permits arbitrary reparenting, helper nodes, replication, delegation, forwarding, and tooling. It is zero exactly for tree-shaped provider groups; multiple parents realize every finite relation. The fixed-table deletion minimum is therefore the exact program-level floor. Static optima do not settle maintenance. We construct a history whose every snapshot is tree-shaped, yet each update forces a parent change, forwarding, or an endpoint blocker. Holding the original one-parent map fixed leaves exactly n(n + 1)/2 required connections outside ancestry after n updates. No algorithm identifies exactly which generated requirement streams remain tree-shaped forever. In pinned audits, 18 of 20 preselected Python source-owner maps have positive gaps. One SQLAlchemy component still has gap 520 after excluding order-sensitive lookups, leaving no lookup conflict. Its checked repair needs a minimum of 59 shared bundles of implementations to supply the missing connections. Lean 4 checks every numbered result's formal content and each certified optimum, including the halting reductions; standard complexity-class naming and source extraction remain external.
Authors
- Tristan Simas (ORCID: https://orcid.org/0000-0002-6526-3149)
Institutions
- McGill University (CA)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-09-17
- DOI
- https://doi.org/10.5281/zenodo.18123531
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 0.00