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.

翻译：编程语言理论中的紧致性引理断言，任何递归函数都可以通过该函数的有限展开来模拟。该引理的一个重要应用场景是用于证明类型化程序性质（如强规范化）的逻辑关系证明技术。递归函数与其有限副本之间的关系是互模拟关系类的一种特殊变体。然而，由于该关系的性质随执行过程动态变化，标准的互模拟证明方法无法应用于紧致性引理。因此，紧致性的证明往往因执行过程中生成的多个递归函数副本可能被不一致次数的展开而显得混乱。我们提出一种新的证明技术：通过索引步进转移上的互模拟关系，并利用中间“模式”语言实现机械化记账。这种“模式步进互模拟”的推广消除了紧致性引理中对语境近似的需求，从而将紧致性引理扩展到更广泛的编程语言，包括包含控制流效应的语言。我们通过在Coq定理证明器中显式控制流与多态性设定下形式化验证紧致性引理来演示该方法。