Abstract

We investigate the applicability of the classic eta-conversion in the type-theory of acyclic algorithms. While denotationally valid, classic eta-conversion is not algorithmically valid in the type theory of algorithms, with the exception of few limited cases. The paper shows how the restricted, algorithmic eta-rule can recover algorithmic eta-conversion in the reduction calculi of type-theory of algorithms.

Details

Title
Eta-Reduction in Type-Theory of Acyclic Recursion
Author
Loukanova, Roussanka
First page
e29199
Section
Articles
Publication year
2023
Publication date
2023
Publisher
Ediciones Universidad de Salamanca
e-ISSN
22552863
Source type
Scholarly Journal
Language of publication
English
ProQuest document ID
3065615677
Copyright
© 2023. This work is licensed under https://creativecommons.org/licenses/by-nc-nd/4.0 (the “License”). Notwithstanding the ProQuest Terms and conditions, you may use this content in accordance with the terms of the License.