Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Abstracting Denotational Interpreters

Sebastian Graf, Simon Peyton Jones, Sven Keidel

TL;DR

The paper targets the longstanding tension between compositional denotational semantics and operational detail needed for static analysis. It proposes a single, parametric denotational interpreter that outputs small-step traces and can be instantiated with different semantic domains to realize dynamic evaluation strategies (call-by-name, call-by-need, call-by-value) as well as static analyses (absence, usage, type, CFA). The key contributions include the first provably adequate denotational semantics for call-by-need, a guarded-type-theory-based total encoding, and a framework that derives various analyses from the same interpreter via abstract interpretation. It demonstrates the approach with concrete instantiations (absence/usage analyses, Algorithm J type analysis, 0CFA, and a Glasgow Haskell Demand Analysis case study), and argues that soundness proofs decompose into domain-level abstraction laws, yielding modular, reusable proofs. The framework promises scalable, modular static analyses tied to a unified semantic core, with practical impact for compiler analyses and verification of operational properties like variable usage counts and termination behavior. Overall, the work furnishes a principled, compositional pathway from operational semantics to static analyses, enabling rigorous, reusable proofs and real-world applicability such as GHc’s Demand Analyser.

Abstract

We explore denotational interpreters: denotational semantics that produce coinductive traces of a corresponding small-step operational semantics. By parameterising our denotational interpreter over the semantic domain and then varying it, we recover dynamic semantics with different evaluation strategies as well as summary-based static analyses such as type analysis, all from the same generic interpreter. Among our contributions is the first denotational semantics for call-by-need that is provably adequate in a strong, compositional sense. The generated traces lend themselves well to describe operational properties such as how often a variable is evaluated, and hence enable static analyses abstracting these operational properties. Since static analysis and dynamic semantics share the same generic interpreter definition, soundness proofs via abstract interpretation decompose into showing small abstraction laws about the abstract domain, thus obviating complicated ad-hoc preservation-style proof frameworks.

Abstracting Denotational Interpreters

TL;DR

The paper targets the longstanding tension between compositional denotational semantics and operational detail needed for static analysis. It proposes a single, parametric denotational interpreter that outputs small-step traces and can be instantiated with different semantic domains to realize dynamic evaluation strategies (call-by-name, call-by-need, call-by-value) as well as static analyses (absence, usage, type, CFA). The key contributions include the first provably adequate denotational semantics for call-by-need, a guarded-type-theory-based total encoding, and a framework that derives various analyses from the same interpreter via abstract interpretation. It demonstrates the approach with concrete instantiations (absence/usage analyses, Algorithm J type analysis, 0CFA, and a Glasgow Haskell Demand Analysis case study), and argues that soundness proofs decompose into domain-level abstraction laws, yielding modular, reusable proofs. The framework promises scalable, modular static analyses tied to a unified semantic core, with practical impact for compiler analyses and verification of operational properties like variable usage counts and termination behavior. Overall, the work furnishes a principled, compositional pathway from operational semantics to static analyses, enabling rigorous, reusable proofs and real-world applicability such as GHc’s Demand Analyser.

Abstract

We explore denotational interpreters: denotational semantics that produce coinductive traces of a corresponding small-step operational semantics. By parameterising our denotational interpreter over the semantic domain and then varying it, we recover dynamic semantics with different evaluation strategies as well as summary-based static analyses such as type analysis, all from the same generic interpreter. Among our contributions is the first denotational semantics for call-by-need that is provably adequate in a strong, compositional sense. The generated traces lend themselves well to describe operational properties such as how often a variable is evaluated, and hence enable static analyses abstracting these operational properties. Since static analysis and dynamic semantics share the same generic interpreter definition, soundness proofs via abstract interpretation decompose into showing small abstraction laws about the abstract domain, thus obviating complicated ad-hoc preservation-style proof frameworks.
Paper Structure (53 sections, 25 theorems, 83 equations, 25 figures)

This paper contains 53 sections, 25 theorems, 83 equations, 25 figures.

Table of Contents

  1. Introduction
  2. The Problem We Solve
  3. Object Language
  4. Absence Analysis
  5. Compositionality, Summaries and Modularity
  6. Summaries vs. Abstracting Abstract Machines
  7. Problem: Proving Soundness of Summary-Based Analyses
  8. Reference Semantics: Lazy Krivine Machine
  9. A Denotational Interpreter
  10. Semantic Domain
  11. The Interpreter
  12. More Evaluation Strategies
  13. Call-by-name
  14. Call-by-need
  15. Call-by-value
  16. ...and 38 more sections

Key Result

lemma 1

$\mathcal{A}\llbracket {(\mathbf{\bar{\lambdaup}} \mathsf{x}. \mathsf{e})~\mathsf{y}} \rrbracket_ρ = (\mathcal{A}\llbracket {\mathsf{e}} \rrbracket_{ρ[\mathsf{x}↦\langle [\mathsf{x}↦\mathrlap{\mathsf{U}}\space], \mathsf{Rep}~\mathrlap{\mathsf{U}}\space \rangle]})[\mathsf{x} \Mapsto ρ(\mathsf{y}).φ]$

Figures (25)

  • Figure 1: Absence analysis
  • Figure 2: Absence analysis extended to small-step configurations
  • Figure 3: Lazy Krivine transition semantics $\xhookrightarrow{\space}$
  • Figure 4: Syntax
  • Figure 5: Environments
  • ...and 20 more figures

Theorems & Definitions (72)

  • proof
  • definition 1: Abstract substitution
  • lemma 1
  • proof
  • lemma 2
  • proof
  • lemma 3
  • proof
  • lemma 4
  • proof
  • ...and 62 more