Content area

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

1009240
Business indexing term
Identifier / keyword
Title
Eta-Reduction in Type-Theory of Acyclic Recursion
Volume
12
First page
e29199
Publication year
2023
Publication date
2023
Section
Articles
Publisher
Ediciones Universidad de Salamanca
Place of publication
Salamanca
Country of publication
Spain
e-ISSN
22552863
Source type
Scholarly Journal
Language of publication
English
Document type
Journal Article
Publication history
 
 
Online publication date
2023-07-18
Milestone dates
2022-05-22 (Submitted); 2023-07-18 (Issued); 2023-07-18 (Modified)
Publication history
 
 
   First posting date
18 Jul 2023
ProQuest document ID
3065615677
Document URL
https://www.proquest.com/scholarly-journals/eta-reduction-type-theory-acyclic-recursion/docview/3065615677/se-2?accountid=208611
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.
Last updated
2024-06-17
Database
ProQuest One Academic