Summary
The contribution of this paper is twofold.
First, we derive a complete characterization of all simply-typed fixed-point combinator (fpc) generators using Barendregt's Inhabitation Machines.
A fpc generator is a lambda term \( G \) such that \( Y G \) is a fpc whenever \( Y \) is.
The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan's Owl, is a famous fpc generator.
For instance, Turing's fpc \( Y_1 \) can be obtaind from Curry's fpc \( Y_0 \) by postfixing \( \delta \): \[ Y_1 = Y_0 \delta \]
Second, we present a conjecture that vastly generalises Richard Statman's question on the existance of double fixed-point combinators.
Statman asked whether there is a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \).
This question remains open as the proof by Benedetto Intrigila contains a gap.
We have the following conjecture about the relation of the \( \mu \)-opertator and fixed-point combinators:
Conjecture
We conjecture that for any fixed-point combinator \( Y \) and simply-typed \( \lambda\mu \)-terms \( s,t \) it holds that
\[ s =_{ \beta \mu } t \iff s_Y =_{ \beta } t_Y \]
where \(s_Y, t_Y\) are the untyped lambda terms obtained from \(s,t\), respectively, by replacing all occurrences of \( \mu \)-operators with the fixed-point combinator \( Y \).
This conjecture immediately implies a negative answer to Statman's question.
See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.
Bibtex
@inproceedings{lambda:clocks:functional:programs:2013,
author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
title = {{Clocks for Functional Programs}},
booktitle = {The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday},
pages = {97--126},
year = {2013},
doi = {10.1007/978-3-642-40355-2\_8},
series = {LNCS},
volume = {8106},
publisher = {Springer},
keywords = {rewriting, infinitary rewriting, lambda calculus},
type = {journal}
}