Compactness via Pattern Stepping Bisimulation

TL;DR

This paper introduces a novel proof technique called pattern stepping bisimulation, which simplifies and generalizes the compactness lemma in programming language theory, enabling formal verification in more complex language settings.

Contribution

It develops a new bisimulation method indexed over step transitions with an intermediate pattern language, extending the compactness lemma to languages with control flow effects.

Findings

Successfully formalized the proof in Coq for languages with control flow.

Extended the applicability of the compactness lemma to a broader class of languages.

Provided a mechanized proof technique that simplifies recursive function simulation.

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.