Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compactness via Pattern Stepping Bisimulation

Matias Scharager

TL;DR

This work addresses proving the compactness lemma in languages with control flow by introducing pattern stepping bisimulation, which indexes the relation over execution steps and uses a pattern language to track where a recursive function occurs. The core idea is to relate a term to its finite unrollings through an indexed relation $\mathbf{of}^n$, enabling a generalized compactness result $[F_\omega/x]e\downarrow \iff \exists n.\ [F_n/x]e\downarrow$ and a Coq-verified formalization with continuations. The main contributions are the pattern language construction, the indexed bisimulation strategy, and the demonstrated Coq formalization that extends compactness to explicit control flow and polymorphism, reducing reliance on contextual approximation. This approach broadens the applicability of compactness in logical relations and type theories, providing a robust, machine-checked foundation for reasoning about recursive functions in complex languages.

Abstract

The compactness lemma in programming language theory states that any recursive function can be simulated by a finite unrolling of the function. One important use case it has is in the logical relations proof technique for proving properties of typed programs, such as strong normalization. The relation between recursive functions and their finite counterparts is a special variant of the class of bisimulation relations. However, standard bisimulation proof approaches do not apply to the compactness lemma as properties of the relation vary over execution. As a result, the proof of compactness is often messy because the multiple copies made of the recursive function during execution can be unrolled an inconsistent number of times. We present a new proof technique by indexing the bisimulation relation over the step transitions and utilizing an intermediate "pattern" language to mechanize bookkeeping. This generalization of "pattern stepping bisimulation" obviates the need for contextual approximation within the compactness lemma, and thus extends the compactness lemma to a wider range of programming languages, including those that incorporate control flow effects. We demonstrate this approach by formally verifying the compactness lemma within the Coq theorem prover in the setting of explicit control flow and polymorphism.

Compactness via Pattern Stepping Bisimulation

TL;DR

This work addresses proving the compactness lemma in languages with control flow by introducing pattern stepping bisimulation, which indexes the relation over execution steps and uses a pattern language to track where a recursive function occurs. The core idea is to relate a term to its finite unrollings through an indexed relation , enabling a generalized compactness result and a Coq-verified formalization with continuations. The main contributions are the pattern language construction, the indexed bisimulation strategy, and the demonstrated Coq formalization that extends compactness to explicit control flow and polymorphism, reducing reliance on contextual approximation. This approach broadens the applicability of compactness in logical relations and type theories, providing a robust, machine-checked foundation for reasoning about recursive functions in complex languages.

Abstract

The compactness lemma in programming language theory states that any recursive function can be simulated by a finite unrolling of the function. One important use case it has is in the logical relations proof technique for proving properties of typed programs, such as strong normalization. The relation between recursive functions and their finite counterparts is a special variant of the class of bisimulation relations. However, standard bisimulation proof approaches do not apply to the compactness lemma as properties of the relation vary over execution. As a result, the proof of compactness is often messy because the multiple copies made of the recursive function during execution can be unrolled an inconsistent number of times. We present a new proof technique by indexing the bisimulation relation over the step transitions and utilizing an intermediate "pattern" language to mechanize bookkeeping. This generalization of "pattern stepping bisimulation" obviates the need for contextual approximation within the compactness lemma, and thus extends the compactness lemma to a wider range of programming languages, including those that incorporate control flow effects. We demonstrate this approach by formally verifying the compactness lemma within the Coq theorem prover in the setting of explicit control flow and polymorphism.
Paper Structure (19 sections, 20 theorems, 5 equations, 7 figures)

This paper contains 19 sections, 20 theorems, 5 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Compactness as a Bisimulation
  3. Practical Application of Compactness
  4. Formally Expressing Compactness
  5. Pattern Language Definition
  6. Relating Terms to Patterns
  7. Proof Strategy
  8. Coq Formalization with Continuations
  9. Language Specification
  10. Formalizing Pattern Language
  11. Compactness
  12. Necessity of Pattern Stepping
  13. Generality of Pattern Stepping
  14. Dependent and Polymorphic Types
  15. Mutual Recursive Functions
  16. ...and 4 more sections

Key Result

Theorem 1

If for all $n$, $F_n\in R[A\to B]$, then we have $F\in R[A\to B]$.

Figures (7)

  • Figure 1: Relevant components of the programming language
  • Figure 2: Function unrollings
  • Figure 3: Pattern stepping extension under $\mathtt{fun}\ f(x:\tau_1):\tau_2 \ \mathtt{is}\ e_f$
  • Figure 4: Combination of \ref{['lemma:step_stepf']} and \ref{['lemma:stepf_step']} assuming $e\downarrow$
  • Figure 5: Full grammar of language
  • ...and 2 more figures

Theorems & Definitions (24)

  • Theorem 1: Admissibility
  • Lemma 2: Determinism
  • Lemma 3: Safety
  • Lemma 4: Bottom
  • Lemma 5: Compactness
  • Lemma 6: Decrement Pattern
  • Lemma 7: Value Pattern
  • proof
  • Lemma 8: $\longmapsto$ to $\longmapsto_\omega$
  • proof
  • ...and 14 more