How can we ensure computations continue indefinitely when needed? This paper studies perpetuality in the calculus of explicit substitutions λx, where a reduction is considered perpetual if it maintains the possibility of infinite reduction sequences.
The study explores applications of perpetuality, including an inductive characterization of λx-strongly normalizing terms, two perpetual reduction strategies for λx, and a proof of strong normalization for a polymorphic lambda calculus with explicit substitutions *F*
Published in Mathematical Structures in Computer Science, this paper aligns with the journal's focus on theoretical foundations and mathematical tools relevant to computer science. By exploring perpetuality in lambda calculus, it contributes to the development of more powerful and predictable computational models, which is of interest to the journal's readership.
| Category | Category Repetition |
|---|---|
| Science: Mathematics: Instruments and machines: Electronic computers. Computer science | 1 |