Content area
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
Key topics Powered by Web of Science® Description for Powered by Web of Science
Subject
Business indexing term
Identifier / keyword
Title
Eta-Reduction in Type-Theory of Acyclic Recursion
Author
Volume
12
Issue
1
First page
e29199
Publication year
2023
Publication date
2023
Section
Articles
Place of publication
Salamanca
Country of publication
Spain
Publication subject
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
2881161077
Document URL
https://www.proquest.com/scholarly-journals/eta-reduction-type-theory-acyclic-recursion/docview/2881161077/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-08-26
Database
ProQuest One Academic