Functional objects, recursive self, and representation

The first calculus is weak, call-by-value, functional, and store-free: object literals bind self separately in every method; invocation substitutes the current literal; override constructs a new literal. The second adds only Top, width subtyping with invariant shared method results, subsumption, and the runtime minimum-type reannotation in (Override-Sub). Imperative state, primitive Self, matching, F-bounds, and binary methods are absent.

Weakening, substitution, canonical forms for receivers and objects, preservation, progress, and finite safety are established first without subtyping. Receiver narrowing and source substitution with subsumption support the subtyped proof. Minimum typing is unique, sound, and below every declarative type; it supplies the exact runtime annotation required by subtyped preservation. The chapter also gives explicit countermodels to covariant shared method components and detached method extraction. These are failures of the proposed rules, not failures of the invariant calculus.

The Point development imports only chapter 12’ iso-recursive formation, fold/unfold typing, fold–unfold contraction, substitution, and folded canonical forms. It proves the corresponding object safety cases locally. No equi-recursive conversion, normalization, or semantic domain theorem is used. Point/ColorPoint is left as the extension obstruction that motivates the next chapter.

The explicitly fixed target has bounded existentials, covariant records, arrows, iso-recursive types with the Amber subtyping rule, and functional letrec with full compatible closure. Local proofs cover type- and term-context narrowing, type and term substitution, existential subtype inversion, and preservation of the generalized open root after package subsumption. The root always substitutes the actual witness and payload.

Type translation preserves width. The visible bound, recursive record family $C_A(X)$, and recursive function $r_{D_A}$ are well formed. Environment invariance under receiver-context narrowing, translation substitution, scoped typing, and one-root operational simulation are proved. In the override case the actual runtime package may have a smaller bound; target narrowing and generalized opening justify it, while environment invariance identifies the reannotated replacement body up to alpha equality. The stored self and the separately translated literal are literally the same application $r_{D_A}(\overline{f})$. Consequently invocation and override give direct reductions from a source translation to the translation of its reduct; the proof uses no reverse target step.

The representation theorem is scoped to the nonrecursive source calculus; the separate fluent Point example is not silently included. The source paper proves computational adequacy for its interpretation, but neither it nor this chapter claims full abstraction. The executable companion is finite implementation evidence, not a proof of source safety or representation.