In a small-step semantics with a deterministic reduction strategy, refocusing is a transformation that connects a reduction-based normalization function (i.e., a normalization function that enumerates the successive terms in a reduction sequence -- the successive reducts) and a reduction-free normalization function (i.e., a normalization function that does not construct any reduct because all the reducts are deforested). This transformation was introduced by Nielsen and the author in the early 2000's with an informal correctness proof. Since then, it has been used in a variety of settings, starting with Biernacka and the author's syntactic correspondence between calculi and abstract machines, and several formal proofs of it have been put forward. This article presents a simple, if overdue, formal proof of refocusing that uses the Coq Proof Assistant and is aligned with the simplicity of the original idea.

翻译：在具有确定性约简策略的小步语义中，重聚焦是一种转换方法，它将基于约简的归一化函数（即枚举约简序列中连续项——即连续约简项——的归一化函数）与无约简的归一化函数（即不构造任何约简项的归一化函数，因为所有约简项均被消除）联系起来。该转换由Nielsen与作者于21世纪初提出，并附带非形式化的正确性证明。此后，该转换被广泛应用于多种场景，例如Biernacka与作者关于演算与抽象机之间的语法对应研究，且已提出若干形式化证明。本文给出一种简洁（尽管稍显迟来）的重聚焦形式化证明，该证明基于Coq证明助手，并与原始思想的简洁性保持一致。