Email Gateway (May 03 2024 at 17:38): Email Gateway (May 03 2024 at 17:38):From: Dmitriy Traytel <traytel@di.ku.dk>
Dear all,
a new entry by Vincent Trélat proving that the iterated self-composition of acyclic substitutions converges (yielding the so-called fixed-point substitution) on lambda-free higher-order terms:
Substitutions for Lambda-Free Higher-Order Terms
This theory provides a formalization of substitutions on lambda-free higher-order terms, establishing a structured framework with the expected algebraic properties. It introduces a type construction for the rigorous definition and manipulation of substitutions. The main theorem of this theory proves the existence of fixed-point substitutions under acyclicity, a theorem that is too often regarded as trivial in the literature.
https://www.isa-afp.org/entries/Substitutions_Lambda_Free.html
Enjoy!
Last updated: May 19 2024 at 08:18 UTC