Table of Contents
Fetching ...

A Calculus of Overlays

Bo Yang

TL;DR

This work introduces Overlay-Calculus, a minimal declarative programming model built from three primitives: records, definitions, and inheritance, and demonstrates that the $λ$-calculus embeds into it while the semantics remains fully abstract w.r.t Böhm trees. It replaces traditional reduction with a purely observational, set-theoretic framework based on powerset lattices and the Knaster–Tarski fixed-point theorem, enabling a CPS-agnostic, memory-like RAM representation via records. A five-rule translation from the ANF form of the $λ$-calculus establishes adequacy and full abstraction, showing that convergence behavior matches Böhm-tree semantics without domain-theoretic machinery. The Case Study on the Expression Problem illustrates how Overlay-Calculus dissolves classic inheritance concerns, and the discussion connects the approach to configuration languages, effect systems, and union-file-system concepts, while outlining future work on a typed variant and standard libraries.

Abstract

Just as the $λ$-calculus uses three primitives (abstraction, application, variable) as the foundation of functional programming, Overlay-Calculus uses three primitives (record, definition, inheritance) as the foundation of declarative programming. It trivially embeds the $λ$-calculus, although the entire semantics builds on only naive set theory; as a consequence, all constructs including inheritance are inherently commutative, idempotent, and associative; the linearization problem of multiple inheritance simply does not arise. This induces a fully abstract semantics of the lazy $λ$-calculus with respect to Böhm tree equivalence. Overlay-Calculus is distilled from the Overlay language, a practical implementation in which we observed further emergent phenomena: the Expression Problem dissolves, programs are CPS-agnostic, records natively encode random-access memory, and self-reference resolves to multiple targets. These properties suggest applications to configuration languages, dependency injection, object-oriented programming, composable effect systems, modular software architectures, file-system-as-compiler, general-purpose programming, and no-code development.

A Calculus of Overlays

TL;DR

This work introduces Overlay-Calculus, a minimal declarative programming model built from three primitives: records, definitions, and inheritance, and demonstrates that the -calculus embeds into it while the semantics remains fully abstract w.r.t Böhm trees. It replaces traditional reduction with a purely observational, set-theoretic framework based on powerset lattices and the Knaster–Tarski fixed-point theorem, enabling a CPS-agnostic, memory-like RAM representation via records. A five-rule translation from the ANF form of the -calculus establishes adequacy and full abstraction, showing that convergence behavior matches Böhm-tree semantics without domain-theoretic machinery. The Case Study on the Expression Problem illustrates how Overlay-Calculus dissolves classic inheritance concerns, and the discussion connects the approach to configuration languages, effect systems, and union-file-system concepts, while outlining future work on a typed variant and standard libraries.

Abstract

Just as the -calculus uses three primitives (abstraction, application, variable) as the foundation of functional programming, Overlay-Calculus uses three primitives (record, definition, inheritance) as the foundation of declarative programming. It trivially embeds the -calculus, although the entire semantics builds on only naive set theory; as a consequence, all constructs including inheritance are inherently commutative, idempotent, and associative; the linearization problem of multiple inheritance simply does not arise. This induces a fully abstract semantics of the lazy -calculus with respect to Böhm tree equivalence. Overlay-Calculus is distilled from the Overlay language, a practical implementation in which we observed further emergent phenomena: the Expression Problem dissolves, programs are CPS-agnostic, records natively encode random-access memory, and self-reference resolves to multiple targets. These properties suggest applications to configuration languages, dependency injection, object-oriented programming, composable effect systems, modular software architectures, file-system-as-compiler, general-purpose programming, and no-code development.
Paper Structure (82 sections, 8 theorems, 39 equations)

This paper contains 82 sections, 8 theorems, 39 equations.

Key Result

theorem 1

A closed ANF $\lambda$-term $M$ has a head normal form if and only if $\mathcal{T}(M){\Downarrow}$.

Theorems & Definitions (10)

  • definition 1: Overlay-convergence
  • theorem 1: Adequacy
  • theorem 2: Full Abstraction
  • proposition 1
  • theorem 3
  • lemma 1: Single Path
  • lemma 2: Substitution
  • lemma 3: Result-step
  • theorem 4: Convergence preservation
  • definition 2: Overlay-contextual equivalence