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和作者在2000年初以非正式的正确性证明引入的。从那时起,这种转变就被用于各种环境,从Biernacka和作者的计算器和抽象机器之间的合成通信开始,并提出了若干这方面的正式证据。如果逾期,这篇文章提供了使用 Coq 校准助理并符合原始概念的简单化的简单化的正式证据。