loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
On The Lambda Y Calculus
Copenhagen, Denmark
July 22-July 25
ISBN: 0-7695-1483-9
ASCII Text
x 
 
Rick Statman, "On The Lambda Y Calculus," Logic in Computer Science, Symposium on, pp. 159, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002.
 
 
BibTex
x
 
@article{ 10.1109/LICS.2002.1029825,
author = {Rick Statman},
title = {On The Lambda Y Calculus},
journal ={Logic in Computer Science, Symposium on},
volume = {0},
year = {2002},
issn = {1043-6871},
pages = {159},
doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029825},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Logic in Computer Science, Symposium on
TI - On The Lambda Y Calculus
SN - 1043-6871
SP
EP
A1 - Rick Statman,
PY - 2002
KW - null
VL - 0
JA - Logic in Computer Science, Symposium on
ER -
 
Rick Statman, Carnegie Mellon University

In this note we consider three problems concerning the lambda Y calculus obtained from the simply typed lambda calculus by the addition of fixed point combinators Y :(A → A ) → A.

The "paradoxical" combinator Y was first discussed in Curry & Feys Vol 1 [3]. It appears first in a typed context in Scott [7] and also in Richard Platek?s thesis [5], and forms the basis for L.C.F [6] and its descendants.
In this note we shall consider

  • (1) the question of whether higher type Y are "definable" from lower type Y. We shall show that it is not the case in this context, sharpening a result of ours from [8]. A similar result has been obtained by Warner Damm;
  • (2) the question of the decidability of termination. More precisely, we shall show that it is decidable whether a given term has a normal form. This extends results of Plotkin and Bercovicci. [2]. By similar methods we show that we show that it is decidable whether a term has a head normal form, and whether a term has a finite Bohm tree;
  • (3) the question of the decidability of the word problem. This question was first put to us by Albert Meyer 20 years ago. We shall show that it is in general undecidable whether two lambda Y terms convert. This is done by encoding the behavior of register machines. In addition we shall give a decision procedure for the special case of only Y?s of type (0 → 0) → 0.

    • Citation:
    Rick Statman, "On The Lambda Y Calculus," lics, pp.159, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002
    Usage of this product signifies your acceptance of the Terms of Use.