On the \(\lambda Y\) calculus
type: Item
instance of: scholarly article
title: On the \(\lambda Y\) calculus
zbMATH Open document ID: 1068.03013
published in: Annals of Pure and Applied Logic
publication date: 2004-11-18T00:00:00Z
review text: In this short and elegant article, the \(\lambda Y\) calculus, which extends the simply typed \(\lambda\)-calculus by the fixed-point combinator \(Y\) of type \((A \to A) \to A\) for any type \(A\), is investigated. The following theorems are shown: (1) Higher-type fixed-point combinators are not definable from lower-type fixed-point combinators. This result was obtained as well by Werner and Damm using a different method. (2) It is decidable whether a given term has a normal form and whether a term has a head normal form. (3) It is undecidable whether two \(\lambda Y\) terms convert. This is done by encoding register machines in the \(\lambda Y\)-calculus. Furthermore, a decision procedure is given for the special case of two \(\lambda Y\) terms containing only \(Y\) of type \((0 \to 0) \to 0\).
reviewed by: Anton Setzer
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 68N18
zbMATH DE Number: 2116242
zbMATH Keywords: \(\lambda\)-calculus
zbMATH Keywords: \(Y\)-combinator
zbMATH Keywords: fixed-point operator
zbMATH Keywords: word problem
zbMATH Keywords: decidability
zbMATH Keywords: weak normalisability
zbMATH Keywords: higher-type fixed-point operators
zbMATH Keywords: Böhm trees
zbMATH Keywords: register machines
author: Richard Statman
MaRDI profile type: Publication
full work available at URL: j.apal.2004.04.004
OpenAlex ID: W2078285934
cites work: The lambda calculus, its syntax and semantics
cites work: Q3702504
cites work: Q5565113
cites work: The IO- and OI-hierarchies
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q4513619
cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY
cites work: Completeness, invariance and λ-definability
cites work: Q4263805
cites work: Q5585417
DOI: 10.1016/J.APAL.2004.04.004
description: scientific article; zbMATH DE number 2116242