1637 LABEL:LastPageOct. 05, 2018Jul. 23, 2020

# Fixed point combinators as fixed points of higher-order fixed point
generators

Andrew Polonsky  Appalachian State University
Boone NC 28608-2133, USA<EMAIL_ADDRESS>
###### Abstract.

Corrado Böhm once observed that if $Y$ is any fixed point combinator (fpc),
then $Y(\lambda yx.x(yx))$ is again fpc. He thus discovered the first “fpc
generating scheme” – a generic way to build new fpcs from old. Continuing this
idea, define an _fpc generator_ to be any sequence of terms
$G_{1},\dots,G_{n}$ such that

$Y\text{ is fpc }\;\Longrightarrow\;YG_{1}\cdots G_{n}\text{ is fpc}.$

In this contribution, we take first steps in studying the structure of (weak)
fpc generators. We isolate several robust classes of such generators, by
examining their elementary properties like injectivity and (weak) constancy.
We provide sufficient conditions for existence of fixed points of a given
generator $(G_{1},\cdots,G_{n})$: an fpc $Y$ such that $Y=YG_{1}\cdots G_{n}$.
We conjecture that weak constancy is a necessary condition for existence of
such (higher-order) fixed points. This statement generalizes Statman’s
conjecture on non-existence of “double fpcs”: fixed points of the generator
$(G)=(\lambda yx.x(yx))$ discovered by Böhm.

Finally, we define and make a few observations about the monoid of (weak) fpc
generators. This enables us to formulate new conjectures about their
structure.

###### Key words and phrases:

Fixed point combinator, Lambda Calculus, Bohm tree, FPC generator

Dedicated to Corrado Böhm, a pioneer of the Lambda Calculus

##  1\. Introduction

Fixed point combinators (fpcs) are a fascinating class of lambda terms.
Arising in the proof of the Fixed Point Theorem, their dynamical character
affects the global structure of the Lambda Calculus in a fundamental way.
Being a mechanism of unrestricted recursion, they are directly responsible for
the Turing-completeness of the lambda calculus as a programming language.111
In fact, the very notion of Turing-completeness traces back to Church’s bold
suggestion that lambda calculus can encode arbitrary computational processes.
Yet the idea was only accepted after Kleene and Turing, using fixed point
constructions, showed equivalence between Church’s formalism and their own
ones. And when lambda terms are used as the computational basis of a logical
system
.— whether based on the Curry–Howard isomorphism or illative combinatory
logic — fixed point combinators appear unexpectedly as the untyped skeletons
of paradoxes, heralding inconsistency of the logic lying over the
computational calculus. [2] [9] [4] [8] [5] [13]

It is an elementary fact that a term $Y$ is a fixed point combinator if and
only if $Y$ is itself a fixed point of the combinator $\delta=\lambda
yx.x(yx)$. [1, 6.5.3] This can even be taken as the definition of fpcs:
$Y\in\Lambda$ is fpc iff $Y=\delta Y$. Corrado Böhm noticed that also
$Y\delta$ is fpc whenever $Y$ is. [1, 6.5.4] For example, if $Y=\mathtt{Y}$ is
Curry’s fpc, then $Y\delta=\Theta$ is Turing’s fpc. A major open problem in
the Lambda Calculus asks whether there exists a “double fpc” $Y$ satisfying
$\delta Y=Y=Y\delta$. Statman [15] conjectures that no such $Y$ exists. An
early attack on this problem was undertaken by Intrigila [10]. Unfortunately,
Endrullis discovered a gap in the argument which seems difficult to overcome.
As of this writing, the conjecture remains open. For recent developments, see
[6], [12]. We will also discuss the conjecture in Section 4.

Böhm’s observations revealed that fpcs themselves have a compositional
structure, where one constructs new fpcs from old by applying them to
$\delta$. Since then, other “fpc generating schemes” have been discovered and
investigated by several authors. [14] [6] These contributions have confirmed
that fpcs have a rich mathematical structure indeed.

In this paper, we will explore such fpc generators “in the abstract”, studying
their general properties and providing a basic taxonomy. We formulate several
new problems, including a significant strengthening of Statman’s conjecture.

##  2\. Notations and definitions

We assume the reader is familiar with the basic notions of lambda calculus:
$\lambda$-terms, free variables, substitution, and beta-conversion. We refer
to [1] for background on these matters. Here we shall employ the following
symbols and notions.

  * •

$\Lambda$ is the set of $\lambda$-terms.
$\Lambda^{0}=\\{{M\in\Lambda\mid\mathsf{FV}(M)=\emptyset}\\}$ is the set of
_closed_ $\lambda$-terms.

  * •

$\mathsf{FV}(M)$ is the set of free variables of $M\in\Lambda$.

  * •

$M[x:=N]$ is the result of capture-avoiding substitution of $N$ for $x$ in
$M$.

  * •

If $\vec{N}=(N_{1},\dots,N_{k})$ is a sequence of $\lambda$-terms, then
$M\vec{N}=MN_{1}\cdots{}N_{k}$.

  * •

$F^{k}(z):=F(F(\cdots F(z)\cdots))$, with $k$ $F$s.

  * •

$\mathtt{I}=\lambda x.x$, $\mathtt{K}=\lambda xy.x$, $\mathtt{c}_{k}=\lambda
xy.x^{k}(y)$, $\delta=\lambda yx.x(yx)$.

  * •

$M=N$ denotes beta conversion between $M$ and $N$.

  * •

$M\twoheadrightarrow N$ denotes beta reduction from $M$ to $N$.

  * •

$M$ is _solvable_ , if $M\vec{N}=\mathtt{I}$ for some $\vec{N}$. Otherwise,
$M$ is _unsolvable_.

  * •

$M\mathbin{=^{\infty}}N$ if $M$ and $N$ have the same Böhm tree.
We note without proof that this relation can be defined using one axiom and
one inference rule, the latter to be understood _coinductively_ (see [11],[7],
and especially [3, Def. 5.6]):

$M,N\\!\phantom{\vec{M}}\\!\text{unsolvable}$ $M\mathbin{=^{\infty}}N$
$M=\lambda\vec{x}.y\vec{M}\quad N=\lambda\vec{x}.y\vec{N}$
$M_{1}\mathbin{=^{\infty}}N_{1}\quad\cdots\quad
M_{k}\mathbin{=^{\infty}}N_{k}$ $M\mathbin{=^{\infty}}N$

  * •

$z\\#M$ means $z\notin\mathsf{FV}(M)$. For $S\subseteq\Lambda$, $z\\#S$ means
$z\\#M$ for each $M\in S$.

  * •

$z\notin M$ if there exists $N=M$ such that $z\\#N$. $z\in M$ if
$z\in\mathsf{FV}(N)$ for all $N=M$.

  * •

$z\notin^{\infty}M$ if there exists $N=^{\infty}M$ such that $z\\#N$.
Otherwise, $z\in^{\infty}M$.

$Y\in\Lambda$ is a _fixed point combinator (fpc)_ if $Yx=x(Yx)$ for $x\\#Y$.

$Y\in\Lambda$ is a _weak fixed point combinator (wfpc)_ if
$Yx\mathbin{=^{\infty}}x(Yx)$ for $x\\#Y$.

Notice that every fpc is a wfpc. See Examples 3 for both types of terms.

All (w)fpcs have the same Böhm tree, so $Y\in\Lambda$ is wfpc iff
$Y\mathbin{=^{\infty}}Y_{0}$ for some fpc $Y_{0}$.

A wfpc $Y$ can equivalently be given by a sequence of terms $(Y_{n})$ with
$Y=Y_{0}$ and $Y_{n}x=x(Y_{n+1}x)$, with $x\\#\\{Y_{n},Y_{n+1}\\}$. [12, Prop.
3.9] If $Y$ is fpc, then $Y_{n}=Y_{0}$ for all $n$.

We write $\mathsf{FPC}$ ($\mathsf{WFPC}$) for the set of fpcs (weak fpcs).

Henceforth, we shall often write $\mathsf{(W)FPC}$ in a sentence that is meant
to apply to both $\mathsf{FPC}$ and $\mathsf{WFPC}$. Such a statement should
always be read as a conjunction of two statements: one, in which parentheses
are ignored together with their contents, and another, where parentheses are
removed but their contents remain.

A _(weak) fpc generating vector_ , or _(w)fgv_ , is a sequence of terms
$\vec{G}$ satisfying

$Y\in\mathsf{(W)FPC}\;\Longrightarrow\;Y\vec{G}\in\mathsf{(W)FPC}.$

######  Proposition 1.

TFAE:
$(i)\quad\ \ \vec{G}$ is wfgv.
$(ii)\quad\ Y\in\mathsf{FPC}\;\Longrightarrow\;Y\vec{G}\in\mathsf{WFPC}$.
$(iii)\quad Y\vec{G}\in\mathsf{WFPC}$ for some $Y\in\mathsf{FPC}$.

######  Proof 2.1.

$(i)\Rightarrow(ii)$. Let $\vec{G}$ be wfgv, $Y$ be fpc. Then $Y$ is wfpc, and
$Y\vec{G}$ is wfpc.

$(ii)\Rightarrow(iii)$. Trivial.

$(iii)\Rightarrow(i)$. Let $Z$ be wfpc. Then $Z=^{\infty}Y$. Also
$Z\vec{G}=^{\infty}Y\vec{G}$ is wfpc.

######  Corollary 2.

Every fpc generator is wfpc generator.

######  Proof 2.2.

Let $\vec{G}$ be fpc generator. Pick $Y\in\mathsf{FPC}$. Then $Y\vec{G}$ is
fpc, hence $\vec{G}$ is wfgv.

######  Proposition 3.

Consider the following conditions on $\vec{G}$.

$\displaystyle\begin{array}[]{l r l}(i)&Y\phantom{j}\quad\text{ fpc
}&\;\Longrightarrow\;Y\vec{G}\quad\text{ fpc }\\\ (ii)&Y\,\quad\text{wfpc
}&\;\Longrightarrow\;Y\vec{G}\quad\text{wfpc }\\\
(iii)&Y\phantom{j}\quad\text{ fpc }&\;\Longrightarrow\;Y\vec{G}\quad\text{wfpc
}\\\ (iv)&Y\,\quad\text{wfpc }&\;\Longrightarrow\;Y\vec{G}\quad\text{ fpc }\\\
\end{array}$

The following relations are valid:

$(iv)\;\Longrightarrow\;(i)\;\Longrightarrow\;(ii)\iff(iii)$

######  Proof 2.3.

These relations simply summarize the facts noted above.

##  3\. Examples and first observations

  * •

_Turing’s fpc._ Let $\Theta x=VVx$, where $V=\lambda vx.x(vvx)$. Then
$\Theta\in\mathsf{FPC}$.

  * •

_Parametrized Turing’s fpc._ For $M\in\Lambda$, let $\Theta_{M}x=VVMx$, where
$V=\lambda vmx.x(vvmx)$. Then $\Theta_{M}\in\mathsf{FPC}$. (This example can
be generalized to have multiple parameters.)

  * •

Let $z$ be a variable. Put $\Psi_{z}=W_{z}W_{z}\mathtt{I}$, where
$W_{z}=\lambda wpx.x(ww(zp)x)$. Then
$\Psi_{z}\in\mathsf{WFPC}\setminus\mathsf{FPC}$.

  * •

A slight variant of the above will play a central role in the proof of our
main result. Let $c$ be a variable. Put $\Upsilon=\lambda
x.V_{x}\mathtt{I}V_{x}$, where $V_{x}=\lambda pv.x(v(cp)v)$. Then
$\Upsilon\in\mathsf{WFPC}\setminus\mathsf{FPC}$.

A nice feature of this wfpc is that it has a very simple reduction graph.

######  Proposition 4.

$\Theta_{M}=\Theta_{N}\;\Longrightarrow\;M=N$.

######  Proof 3.1.

This is manifest upon inspecting the reduction graph of $\Theta_{z}$ — the set
of reducts of $\Theta_{z}$. For a precise proof, see [12, Lemma 4.1].

  * •

Let $\vec{G}=()$, the empty vector. Obviously,
$Y\in\mathsf{(W)FPC}\;\Longrightarrow\;Y\vec{G}=Y\in\mathsf{(W)FPC}$.
We call this generator _trivial_. In subsequent sections, we will tacitly
assume all generators to be non-trivial.

  * •

Fix a (w)fpc $Y$, and let $\vec{G}=(\mathtt{K}Y)$. Then $(\mathtt{K}Y)$ yields
the same (w)fpc on every input:

$Z=(Z_{0},Z_{1},\dots)\in\mathsf{WFPC}\;\Longrightarrow\;Z_{0}(\mathtt{K}Y)=\mathtt{K}Y(Z_{1}(\mathtt{K}Y))=Y\in\mathsf{(W)FPC}.$

We call such generators _constant_. Their only interesting feature is the
fixed point $Y=Y\vec{G}$.

  * •

Recall that $\delta yx=x(yx)$. It is easy to verify the following:

    * –

$\delta^{k}(z)x=x^{k}(zx)$.

    * –

If $Y$ is fpc, then $Y=\delta Y=\delta^{k}(Y)$.

    * –

If $Y=(Y_{n})$ is wfpc, then $Y_{0}=\delta^{k}(Y_{k})$.

Let $\vec{G}=(\delta)$. Then $Y\in\mathsf{FPC}\;\Longrightarrow\;Y\delta
x=\delta(Y\delta)x=x(Y\delta x)\;\Longrightarrow\;Y\delta\in\mathsf{FPC}$.
As noted in the introduction, it is open whether there exists
$Y{\in}\,\mathsf{(W)FPC}$ such that $Y{=}\,Y\delta$.

  * •

Let $\vec{G}=(\lambda y.\Theta_{y})$. Then

$Y\in\mathsf{FPC}\;\Longrightarrow\;Y\vec{G}=Y(\lambda y.\Theta_{y})=(\lambda
y.\Theta_{y})(Y(\lambda y.\Theta_{y}))=\Theta_{Y\vec{G}}\in\mathsf{FPC}.$

Furthermore, there exists fpc $Y$ such that $Y=Y\vec{G}$.
Indeed, take $Y=\Theta(\lambda x.\Theta_{x(\lambda
y.\Theta_{y})})=\Theta_{Y(\lambda y.\Theta_{y})}$. Then $Y\in\mathsf{FPC}$,
and

$Y(\lambda y.\Theta_{y})=(\lambda y.\Theta_{y})(Y(\lambda
y.\Theta_{y}))=\Theta_{Y(\lambda y.\Theta_{y})}=Y.$

  * •

Yet another single-term fgv is given by $\vec{G}=(\lambda
yx.x(y(\mathtt{K}[y,x])\mathtt{I}))$, where $[P,Q]=\lambda z.zPQ$:

$\displaystyle Y\in\mathsf{FPC}\;\Longrightarrow\;YG_{0}x=G_{0}(YG_{0})x$
$\displaystyle=x(YG_{0}(\mathtt{K}[YG_{0},x])\mathtt{I})$
$\displaystyle=x(G_{0}(YG_{0})(\mathtt{K}[YG_{0},x])\mathtt{I})$
$\displaystyle=x(\mathtt{K}[YG_{0},x](\cdots)\mathtt{I})$
$\displaystyle=x([YG_{0},x]\mathtt{I})=x(\mathtt{I}(YG_{0})x)=x(YG_{0}x)$

  * •

The set of (w)fgvs is closed under composition: if $\vec{G}$ and
$\vec{G}^{\prime}$ are fgvs, then

$Y\in\mathsf{FPC}\;\Longrightarrow\;Y\vec{G}\in\mathsf{FPC}\;\Longrightarrow\;Y\vec{G}\vec{G}^{\prime}\in\mathsf{FPC}.$

Thus, $(\delta,\lambda y.\Theta_{y})$ and $(\lambda y.\Theta_{y},\delta)$ are
both fgvs.

  * •

Many other examples of fpcs and fgvs can be found in [6] and [12].

A (w)fgv $\vec{G}$ is _injective_ if for all (w)fpcs $Y,Y^{\prime}$,
$Y\vec{G}=Y^{\prime}\vec{G}$ implies $Y=Y^{\prime}$.

######  Proposition 5.

No non-trivial (w)fgv is injective.

######  Proof 3.2.

Suppose $\vec{G}=(G_{0},\dots,G_{n})$, for $n\geq 0$, is injective. Since
$\Theta\vec{G}=G_{0}(\Theta G_{0})G_{1}\cdots G_{n}$ is (w)fpc, $G_{0}$ must
be solvable. That is, $G_{0}\vec{P}=\mathtt{I}$ for some closed $\vec{P}$. Put
$Y=\Theta_{x\vec{P}}$, $Y^{\prime}=\Theta_{x\vec{P}\mathtt{I}}$. By
Proposition 4, $Y\neq Y^{\prime}$. Yet

$\displaystyle
Y\vec{G}=\Theta_{G_{0}\vec{P}}\vec{G}=\Theta_{\mathtt{I}}\vec{G}=\Theta_{G_{0}\vec{P}\mathtt{I}}\vec{G}=Y^{\prime}\vec{G}.$

It follows that $\vec{G}$ is not injective.

(Notice that in the above proof both $Y$ and $Y^{\prime}$ are closed, so even
restricting injectivity hypothesis to closed terms, no non-trivial wfpc
generator is injective.)

######  Corollary 6.

Suppose wfgv $\vec{G}$ fixes every fpc: $Y\vec{G}=Y$ for all fpc $Y$. Then
$\vec{G}$ is trivial.

An interesting consequence of these observations is that there is no uniform
way to “Böhm out” an inner level of a wfpc.

######  Proposition 7.

For $m>0$, it is not possible to find terms $(M_{0},\dots,M_{n})$ such that

$Z=(Z_{n})\text{ wfpc}\quad\;\Longrightarrow\;\quad Z_{0}\vec{M}=Z_{m}.$ (1)

######  Proof 3.3.

Suppose such $\vec{M}=(M_{0},\dots,M_{n})$ exists. Then $\vec{M}$ is a wfgv.
For every fpc $Y$, we have $Y\vec{M}=Y$, so every fpc is fixed by $\vec{M}$.
(In particular, $\vec{M}$ is a fgv.) By Corollary 6, $\vec{M}$ is trivial:
$\vec{M}=()$. But then $\vec{M}$ fixes every wfpc as well, and thus cannot
satisfy the hypothesis in (1).

##  4\. The four main classes of generators

Let us consider again Statman’s conjecture on the non-existence of fixed
points of the generator $\vec{G}=(\delta)$. This conjecture is intuitively
compelling, because applying any fpc $Y$ to $\delta$ leads to a slowdown of
head reductions that seems impossible to remove:

$\displaystyle Yx$ $\displaystyle\twoheadrightarrow_{w}x(Y^{\prime})$
$\displaystyle=_{\beta}x(Yx)$ $\displaystyle Y\delta x$
$\displaystyle\twoheadrightarrow_{w}\delta(Y^{\prime}[x:=\delta])x\twoheadrightarrow_{w}x(Y^{\prime}[x:=\delta]x)$
$\displaystyle=_{\beta}x(Y\delta x)$

Upon closer inspection, the central property of the generator $(\delta)$ that
this reasoning depends on is that $\delta(Y\delta)x$ _adds to_ the reduction
length needed for the Böhm tree to develop, while still using the given fpc
$Y$ in constructing this Böhm tree infinitely often. Since any conversion
between the two will synchronize their Böhm reductions, no such conversion can
be possible.

If this reasoning proves to be correct for $\delta$, it should remain valid
for any generator possessing the same property. This leads us to the following
definition and conjecture.

Recall, for any wfpc $(Y_{n})$, $Y_{0}=\lambda
x.x^{k}(Y_{k}x)=\delta^{k}(Y_{k})=\delta^{k}(z)[z:=Y_{k}]$.

A generator $\vec{G}$ is _accretive_ if, for each $k$,
$z\in^{\infty}\delta^{k}(z)\vec{G}$.

That is, $\vec{G}$ is accretive if it actually uses every level of the input
fpc in constructing the output fpc, so that replacing $Y$ with any approximant
will also cut the Böhm tree of $Y\vec{G}$.

######  Conjecture 8.

If $\vec{G}$ is accretive, then there exists no $Y\in\mathsf{WFPC}$ such that
$Y=Y\vec{G}$.

######  Remark 9.

Conjecture 8 generalizes Statman’s conjecture. Indeed,

$\delta^{k}(z)\delta=(\lambda x.x^{k}(zx))\delta=\delta^{k}(z\delta)=\lambda
x.x^{k}(z\delta x)$

Thus, $z\in^{\infty}\delta^{k}(z)\delta$ for all $k$, and the fgv
$\vec{G}=(\delta)$ is accretive.

Conjecture 8 is as sharp as possible: later in this section, we will show that
every $\vec{G}$ which is _not_ accretive possesses a fixed point among the
wfpcs.

The non-accretive generators can be naturally divided into several classes
given below. (We eschew the (W)FPC notation in the next definition to
emphasize that there are actually four properties of generators that are being
defined.)

From the earlier equality $Y_{0}=\delta^{k}(Y_{k})$, note that for each (w)fpc
$Y$, $k\geq 0$, we can write

$Y\vec{G}=\delta^{k}(Y^{\prime})\vec{G}=G_{0}^{k}(Y^{\prime}G_{0})G_{1}\cdots
G_{n}.$

Let $\vec{G}$ be a wfgv. Fix $z\\#\vec{G}$.

  * •

$\vec{G}$ is _constant_ if there is a $k$ such that $\,z\notin
G_{0}^{k}(z)G_{1}\cdots G_{n}$.

  * •

$\vec{G}$ is _weakly constant_ if there is a $k$ s.t.
$z\notin^{\infty}G_{0}^{k}(z)G_{1}\cdots G_{n}$.

  * •

$\vec{G}$ is _compact_ if there is a $k$ such that $\;G_{0}^{k}(z)G_{1}\cdots
G_{n}\in\mathsf{FPC}$.

  * •

$\vec{G}$ is _weakly compact_ if there is a $k$ s.t. $G_{0}^{k}(z)G_{1}\cdots
G_{n}\in\mathsf{WFPC}$.

The least $k$ satisfying one of these conditions is then called the _modulus
of constancy_ , or _modulus of compactness_ , accordingly. Note that $\vec{G}$
is accretive iff $\vec{G}$ is not weakly compact.

From now on, let $\vec{G}$ be a possibly weak fgv. We will omit freshness
conditions $x\\#Y$, $z\\#\vec{G}$ etc., as they will always be obvious from
the context.

######  Proposition 10.

Let $\vec{G}$ be a constant (w)fgv. There is a term $Z$ such that

$Y\vec{G}=Z$

for all wfpc $Y$. Hence $Z$ is (w)fpc.

######  Proof 4.1.

Let $\vec{G}$ be constant, and let $k$ be such that $z\notin
G_{0}^{k}(z)G_{1}\cdots G_{n}$.

That is, $z\notin\mathsf{FV}(Z)$ for some $Z\in\Lambda$ convertible to
$G_{0}^{k}(z)G_{1}\cdots G_{n}$.

Then for any wfpc $Y=(Y_{0},Y_{1},\dots)$, we have

$\displaystyle Y\vec{G}=Y_{0}\vec{G}$ $\displaystyle=Y_{0}G_{0}\cdots G_{n}$
$\displaystyle=G_{0}(Y_{1}G_{0})G_{1}\cdots G_{n}$
$\displaystyle=\qquad\vdots$ $\displaystyle=G_{0}^{k}(Y_{k}G_{0})G_{1}\cdots
G_{n}$ $\displaystyle=G_{0}^{k}(z)G_{1}\cdots G_{n}[z:=Y_{k}G_{0}]$
$\displaystyle=Z[z:=Y_{k}G_{0}]$ $\displaystyle=Z\hskip 99.58464pt$

######  Proposition 11.

The following observations are immediate.

  1. (1)

Every constant fgv is compact.

  2. (2)

Every constant (w)fgv is weakly constant.

  3. (3)

Every compact (w)fgv is weakly compact.

######  Proposition 12.

$\vec{G}$ is weakly constant iff $\vec{G}$ is weakly compact.

######  Proof 4.2.

Let $\vec{G}$ be a wfgv. Then

$\displaystyle z\notin^{\infty}G_{0}^{k}(z)G_{1}\cdots G_{n}$
$\displaystyle\;\Longrightarrow\;G_{0}^{k}(z)G_{1}\cdots
G_{n}=^{\infty}G_{0}^{k}(\Theta G_{0})G_{1}\cdots
G_{n}=\Theta\vec{G}\in\mathsf{WFPC},$ $\displaystyle G_{0}^{k}(z)G_{1}\cdots
G_{n}\in\mathsf{WFPC}$
$\displaystyle\;\Longrightarrow\;G_{0}^{k}(z)G_{1}\cdots
G_{n}=^{\infty}\Theta\;\Longrightarrow\;z\notin^{\infty}G_{0}^{k}(z)G_{1}\cdots
G_{n}.$

######  Proposition 13.

Every (weakly) compact generator has a fixed point:

  1. (1)

If $\vec{G}$ is compact fgv, there exists fpc $Y$ with $Y\vec{G}=Y$.

  2. (2)

If $\vec{G}$ is weakly compact wfgv, there exists wfpc $Y$ with $Y\vec{G}=Y$.

######  Proof 4.3.

The construction is the same for both claims. We will first treat the weak
case, and then specialize the proof to the first claim as well.

Let $\vec{G}$ be a weakly compact wfgv. Let $k$ be the modulus of weak
compactness, so that $G^{k}_{0}(z)G_{1}\cdots G_{n}\in\mathsf{WFPC}$. Put
$F_{0}[z]:=G^{k}_{0}(z)G_{1}\cdots G_{n}$. Since $F_{0}[z]$ is wfpc, write

$F_{0}[z]x=x(F_{1}[z]x)=x^{2}(F_{2}[z]x)=\cdots=x^{k}(F_{k}[z]x)=\cdots$ (2)

Define $Y:=\Theta(\lambda y.F_{k}[yG_{0}])=F_{k}[YG_{0}]$, and
$X:=F_{0}[YG_{0}]$. Now compute

$\displaystyle X\vec{G}$ $\displaystyle=XG_{0}\cdots G_{n}$
$\displaystyle=F_{0}[YG_{0}]G_{0}\cdots G_{n}$ by definition of $X$
$\displaystyle=G_{0}^{k}(F_{k}[YG_{0}]G_{0})G_{1}\cdots G_{n}$
$\displaystyle\text{by \eqref{e:fk} with\ \ }[x:=G_{0},z:=YG_{0}]$
$\displaystyle=G_{0}^{k}(YG_{0})G_{1}\cdots G_{n}$ by definition of $Y$
$\displaystyle=F_{0}[YG_{0}]$ by definition of $F_{0}$ $\displaystyle=X$ by
definition of $X$

Since $F_{0}[z]$ is wfpc, so is $X=F_{0}[YG_{0}]$, proving the second claim.

Now suppose that $\vec{G}$ was actually compact fgv. Then $F_{0}[z]$ would be
fpc, while all of the steps above would remain valid, with $F_{0}[z]=F_{k}[z]$
for each $k$. Then $X=F_{0}[YG_{0}]$ would be fpc as well, proving the first
claim.

######  Remark 14.

The reader will recognize the converse to Proposition 13(2) as the
contrapositive of Conjecture 8. The converse to Proposition 13(1) seems
plausible, but we do not have sufficient evidence to assert it as a formal
conjecture.

##  5\. Rectifying generators

A vector $\vec{G}$ is _rectifying_ if it satisfies condition $(iv)$ of
Proposition 3:

$Y\in\mathsf{WFPC}\;\Longrightarrow\;Y\vec{G}\in\mathsf{FPC}$

$\vec{G}=(\lambda y.\Theta_{y})$ is rectifying:

$(Y_{n})\in\mathsf{WFPC}\;\Longrightarrow\;Y_{0}(\lambda
y.\Theta_{y})=(\lambda y.\Theta_{y})(Y_{1}(\lambda
y.\Theta_{y}))=\Theta_{Y_{1}(\lambda y.\Theta_{y})}\in\mathsf{FPC}$

In Example 3, we saw that $(\lambda y.\Theta_{y})$ has a fpc fixed point. We
shall presently see that so does every rectifying fgv.

Our original proof of this fact first showed that if $\vec{G}$ is rectifying,
then $\vec{G}$ is weakly constant, and thus has a wfpc fixed point $Y$. But
then $Y=Y\vec{G}\in\mathsf{FPC}$ because $\vec{G}$ is rectifying, hence $Y$ is
fpc.

Considering that compactness provides another sufficient condition for
existence of fpc fixed points, it was natural to wonder whether rectifying and
compact fgvs are related. This led us to the following result.

######  Theorem 15.

A fgv $\vec{G}$ is compact iff it is rectifying.

######  Proof 5.1.

$(\Rightarrow)$:

Suppose $G^{k}_{0}(z)G_{1}\cdots G_{n}\in\mathsf{FPC}$. Then

$\displaystyle Y=(Y_{0},Y_{1},\dots)\in\mathsf{WFPC}$
$\displaystyle\quad\Longrightarrow\quad$ $\displaystyle
Y\vec{G}=Y_{0}G_{0}\cdots G_{n}=G_{0}^{k}(Y_{k}G_{0})G_{1}\cdots
G_{n}=G_{0}^{k}(z)G_{1}\cdots G_{n}[z:=Y_{k}G_{0}]\in\mathsf{FPC}.$

$(\Leftarrow)$:

The intuition for this direction is that, although the Böhm tree of a wfpc $Y$
is infinite, only a finite part of it can be used in any conversion
$\rho:Y\vec{G}x=x(Y\vec{G}x)$. Thus, writing
$Yx=x^{k}(Y_{k}x)=\delta^{k}(Y_{k})x$ for large enough $k$ will ensure that
$Y_{k}$ is not touched by any redex contractions. Then the whole conversion
$\rho$ could be lifted to $\rho=\sigma[z:=Y_{k}]$, where

$\sigma:\delta^{k}(z)\vec{G}x=x(\delta^{k}(z)\vec{G}x).$

To formalize this intuition, suppose $\vec{G}$ is rectifying. Fix
$c\\#\vec{G}$. Recall the wfpc $\Upsilon$ from Examples 3:

$\displaystyle W_{x,p}$ $\displaystyle=\lambda v.x(v(cp)v)$ $\displaystyle
V_{x}$ $\displaystyle=\lambda p.W_{x,p}$ $\displaystyle\Upsilon$
$\displaystyle=\lambda x.V_{x}\mathtt{I}V_{x}$

That is, $V_{x}=\lambda pv.x(v(cp)v)$. Note that $W_{x,p}$ and $V_{x}$ are
normal forms. Let $\Upsilon^{k}_{x}=V_{x}c^{k}(\mathtt{I})V_{x}$. The term
$\Upsilon x$ reduces as follows:

$\displaystyle\Upsilon x\to\Upsilon^{0}_{x}\equiv V_{x}\mathtt{I}V_{x}$
$\displaystyle\to W_{x,\mathtt{I}}V_{x}\to x(V_{x}(c\mathtt{I})V_{x})\equiv
x(\Upsilon^{1}_{x})$ $\displaystyle\to x(W_{x,c\mathtt{I}}V_{x})\to
x(x(V_{x}c^{2}(\mathtt{I})V_{x}))\equiv x^{2}(\Upsilon^{2}_{x})$
$\displaystyle\to\cdots$ $\displaystyle\to x^{k}(\Upsilon^{k}_{x})$
$\displaystyle\to\cdots$

Since each term appearing in the above reduction sequence has a unique redex,
the reduction is completely deterministic. That is — the above sequence
actually comprises the entire reduction graph of $\Upsilon^{0}_{x}$. The
sequence also shows that $\Upsilon$ is a wfpc. It is not a fpc however, since
$\Upsilon^{0}_{x}$ obviously has no reducts in common with $\Upsilon^{1}_{x}$.
But $\vec{G}$ is rectifying, so $\Upsilon\vec{G}$ is fpc. By the Church–Rosser
theorem, let $X$ be a common reduct

$\Upsilon\vec{G}x\twoheadrightarrow X\twoheadleftarrow x(\Upsilon\vec{G}x).$
(3)

We will use these reductions to show that
$\delta^{k}(z)\vec{G}\in\mathsf{FPC}$ for large enough $k$.

The main idea behind the construction is as follows. Any finite reduction
$\Upsilon M\twoheadrightarrow X$ can be continued until all the descendants of
$\Upsilon$ project the same number of steps from $\Upsilon^{0}_{M}$ in the
sequence above. Afterwards, all descendants of $M$ can be further synchronized
by confluence.

For example, if $M=\lambda y.[y\mathtt{K},y]$, then

$\displaystyle\Upsilon(\mathtt{I}M)\twoheadrightarrow(\mathtt{I}M)(\Upsilon^{1}_{\mathtt{I}M})$
$\displaystyle\twoheadrightarrow(\lambda
y.[y\mathtt{K},y])(V_{\mathtt{I}M}c^{1}(\mathtt{I})V_{\mathtt{I}M})$
$\displaystyle\twoheadrightarrow[V_{\mathtt{I}M}c^{1}(\mathtt{I})V_{\mathtt{I}M}\mathtt{K},V_{\mathtt{I}M}c^{1}(\mathtt{I})V_{\mathtt{I}M}]$
$\displaystyle\twoheadrightarrow[W_{\mathtt{I}M,c^{1}(\mathtt{I})}V_{\mathtt{I}M}\mathtt{K},\mathtt{I}M(V_{\mathtt{I}M}c^{2}(\mathtt{I})V_{M})]$

and this reduction can be further continued to

$\displaystyle[W_{\mathtt{I}M,c^{1}(\mathtt{I})}V_{\mathtt{I}M}\mathtt{K},\mathtt{I}M(V_{\mathtt{I}M}c^{2}(\mathtt{I})V_{M})]$
$\displaystyle\twoheadrightarrow[M(V_{M}c^{2}(\mathtt{I})V_{M})\mathtt{K},
M(V_{M}c^{2}(\mathtt{I})V_{M})]$
$\displaystyle\;\equiv\;[M(\Upsilon^{2}_{M}),M(\Upsilon^{2}_{M})].$

We proceed with the following sequence of claims, which are hopefully
sufficiently clear not to warrant additional elaboration.

  1. (1):

If $\Upsilon M\twoheadrightarrow X$, then $X\twoheadrightarrow
X^{\prime}\equiv
C[V_{M_{1}}c^{k_{1}}(\mathtt{I})V_{M^{\prime}_{1}},\cdots,V_{M_{k}}c^{k_{m}}(\mathtt{I})V_{M^{\prime}_{m}}]$,
with $M\twoheadrightarrow M_{i}$, $M\twoheadrightarrow M^{\prime}_{i}$, and
every occurrence of $c$ in $X^{\prime}$ being displayed in the subterm
$c^{k_{i}}(\mathtt{I})$ in one of the holes in $C[]$.

  2. (2):

If $\Upsilon M\twoheadrightarrow X$, then $X\twoheadrightarrow
X^{\prime}\equiv C[\Upsilon^{k_{1}}_{M_{1}},\dots,\Upsilon^{k_{m}}_{M_{m}}]$,
with $M\twoheadrightarrow M_{i}$ and every occurrence of $c$ being uniquely
determined by its occurrence in some $\Upsilon^{k_{i}}_{M_{i}}$. This is
obtained from above by finding a common reduct for each
$M_{i}$,$M_{i}^{\prime}$.

  3. (3):

If $C[\Upsilon M]\twoheadrightarrow X$, then $X\twoheadrightarrow
C^{\prime}[\Upsilon^{k_{1}}_{M_{1}},\cdots,\Upsilon^{k_{m}}_{M_{m}}]$, with
the same conditions on $M_{i}$ and occurrences of $c$ as before. This is
obtained from the previous point by factoring the reduction into a part that
does not depend on $\Upsilon M$, $C[x]\twoheadrightarrow
D[x\vec{P}_{1},\dots,x\vec{P}_{k}]$, followed by reductions inside $D[\cdots]$
which are treated separately via 2. (See “Barendregt’s Lemma” in [1, Exercise
15.4.8])

  4. (4):

If $C[\Upsilon M]\twoheadrightarrow X$, then $X\twoheadrightarrow
C^{\prime}[\Upsilon^{k}_{N},\cdots,\Upsilon^{k}_{N}]$, where
$M\twoheadrightarrow N$ and each occurrence of $c$ being uniquely determined
by its occurrence in some $\Upsilon^{k}_{N}$. This is obtained from the
previous claim by “bumping all $\Upsilon^{k_{i}}$s along” to stage
$k\geq\max\\{{k_{i}}\\}$, and letting $N$ be a common reduct of all the
$M_{i}$s.

  5. (5):

If the reduction $\rho:C[\Upsilon M]\twoheadrightarrow
C^{\prime}[\Upsilon^{k}_{N},\cdots,\Upsilon^{k}_{N}]$ is obtained by the
algorithm given in the previous steps, then $\rho$ lifts to the instance
$\rho=\sigma[ux:=\Upsilon^{k}_{x}]$, where

$\sigma:C[\delta^{k}(u)M]\twoheadrightarrow C^{\prime}[uN,\cdots,uN].$

And now we are done! The common reductions in (3) can be both continued to

$\Upsilon\vec{G}x\twoheadrightarrow
C^{\prime}[\Upsilon^{k}_{N},\cdots,\Upsilon^{k}_{N}]\twoheadleftarrow
x(\Upsilon\vec{G}x)$

so that all of the descendants of $\Upsilon$ (under _both_ reductions) are
displayed in the context. (This follows from the fact that every occurrence of
$c$ is witnessed in some $\Upsilon^{k}_{N}$, and $c$ was chosen to be fresh.
The variable $c$ acts as a “label” for the unfolding depth of $\Upsilon$.)

The conclusion of the last step therefore holds for both of these reductions,
and so

$C[\delta^{k}(u)M]:=[\delta^{k}(u)G_{0}]G_{1}\cdots G_{n}\twoheadrightarrow
C^{\prime}[uN,\dots,uN]\twoheadleftarrow x(\delta^{k}(u)G_{0}\cdots G_{n}).$

That is, $G_{0}^{k}(uG_{0})G_{1}\cdots G_{n}\in\mathsf{FPC}$. Applying the
substitution $[u:=\mathtt{K}u]$, we find that $G_{0}^{k}(u)G_{1}\cdots
G_{n}\in\mathsf{FPC}$ as well.

######  Corollary 16.

Every rectifying fgv has a fixed point in $\mathsf{FPC}$.

######  Remark 17.

The proof of the nontrivial direction of Theorem 15 suggests a deeper
connection between uniform properties (finite conversions) and terms obeying a
coinductive pattern (such as wfpcs). In the next section, we will see a
different application of the same type of argument. There seems to be a more
general “continuity principle” at work here that could be worthwhile to
isolate.

We finish this section with an example of a weakly constant fgv which is not
rectifying. It follows that, even restricting to fgvs, compactness is indeed
stronger than weak compactness.

This gives the full picture of the relationships between various classes of
wfgvs we defined here. These relationships are summarized in Figure 1.

######  Proposition 18.

There exist weakly constant fpc generators which are not rectifying.

######  Proof 5.2.

Consider the following combinators:

$\displaystyle Pxy$ $\displaystyle=yx$ $\displaystyle Qyz$
$\displaystyle=z(yQz)$ $\displaystyle Wwpz$ $\displaystyle=z(ww(zp)z)$
$\displaystyle Ryz$ $\displaystyle=WW(yQz)z$

First we observe that $(P,Q)$ is an fgv: for $Y$ fpc, we have

$YPQx=P(YP)Qx=Q(YP)x=x(YPQx).$ (4)

We claim that $(P,Q)$ is not rectifying. If it was, then by the previous
theorem, it would be compact, hence weakly compact. To the contrary, (4) shows
that $(P,Q)$ is accretive. So it cannot be rectifying.

Next, we verify that $(P,R)$ is again fgv:

$\displaystyle YPRx=P(YP)Rx=R(YP)x$ $\displaystyle=WW(YP\,Q\,x)\,x$
$\displaystyle=x(WW(x(YP\,Q\,x))\,x)$
$\displaystyle=_{\eqref{ypqx}}x(WW(YP\,Q\,x)\,x)=x(YPR\ \\!x)$

At the same time, we claim $(P,R)$ is weakly constant with modulus $1$:

$\displaystyle P^{1}(z)Rx=PzRx=Rzx$ $\displaystyle=WW(zQx)x$
$\displaystyle=x(WW(\cdots)x)$ $\displaystyle=x^{2}(WW(\cdots)x)$
$\displaystyle=\cdots$ $\displaystyle=x^{n}(\cdots)$

The variable $z$ is being pushed to infinity, and does not appear in the Böhm
tree of $PzRx$—nor in the Böhm tree of $PzR=\lambda x.PzRx$. That is,
$z\notin^{\infty}P^{1}(z)R$. Indeed, $\vec{G}=(P,R)$ is weakly constant. We
claim it is not rectifying.

For a wfpc $Z$, the term $ZPR$ reduces as follows:

$\displaystyle ZPRx\twoheadrightarrow P(ZP)Rx\to^{2}R(ZP)x$
$\displaystyle\to^{2}WW(ZPQx)x$ $\displaystyle\to^{3}x(WW(x(ZPQx))x)$
$\displaystyle\to^{3}x^{2}(WW(x^{2}(ZPQx))x)$ $\displaystyle\to\qquad\vdots$
$\displaystyle ZPRx\quad\twoheadrightarrow^{z_{0}+2+2+3n}$
$\displaystyle\quad\ \ x^{n}(WW(x^{n}(ZPQx))x)$

From this analysis, it is manifest that any common reduction

$ZPRx\ \ \twoheadrightarrow\ \ \cdot\ \ \twoheadleftarrow\ \ x(ZPRx)$

must contain a common reduction between

$x^{n}(ZPQx)\ \ \twoheadrightarrow\ \ \cdot\ \ \twoheadleftarrow\ \
x^{n+1}(ZPQx).$

As we observed earlier, $(P,Q)$ is not rectifying, so there exist wfpcs $Z$
for which such conversion is not possible. Thus $(P,R)$ is not rectifying
either. This completes the proof.

(Note that the modulus of constancy can be adjusted to any $k>0$ by passing
the argument of the generator into the head position $k$ times before pushing
it to infinity.)

Figure 1. The hierarchy of (weak) fpc generators

##  6\. The monoid of wfgvs

The wfpc and fpc generators have an obvious monoid structure:

$(G_{0},\dots,G_{n})\odot(G_{0}^{\prime},\dots,G_{m}^{\prime})\quad:=\quad(G_{0},\dots,G_{n},G_{0}^{\prime},\dots,G_{m}^{\prime})$

The identity is the trivial generator $()$. The concatenation operation is
associative, and satisfies the identity laws. We thus have a monoid
$(\mathcal{G},\odot,())$ of wfgvs, containing a submonoid
$(\mathcal{F},\odot,())$ of fgvs.

Neither of these monoids is finitely generated, as there are infinitely many
constant fgvs of the form $\mathtt{K}\Theta_{M}$ that cannot be obtained by
composition of more elementary ones.

### Extensional equality

Since the primary interest in (w)fgvs is in their ability to generate new
(w)fpcs from old, it is natural to identify generators having the same
functional behavior.

We say a fgv or wfgv $\vec{G}$ is _extensionally equal_ to $\vec{G}^{\prime}$,
written $G\simeq G^{\prime}$, if for every _fpc_ $Y$,
$Y\vec{G}=Y\vec{G}^{\prime}$. (Note that this is an equivalence relation on
$\mathcal{G}$, preserved by $\odot$.)

  * •

If $\vec{G}$ is a constant generator, say, $Y\vec{G}=Z$ for all $Y$, then
$\vec{G}\simeq(\mathtt{K}Z)$:

$Y(\mathtt{K}Z)=\mathtt{K}Z(Y^{\prime}(\mathtt{K}Z))=Z=Y\vec{G}$

  * •

Recall the combinator $\mathtt{C}=\lambda fxy.fyx$. Note that
$\mathtt{C}\mathtt{K}=\mathtt{K}\mathtt{I}$, and
$\mathtt{C}(\mathtt{C}\mathtt{K})=\mathtt{C}(\mathtt{K}\mathtt{I})=\mathtt{K}$.
Let $Gyz=z(y(\mathtt{C}z))(\delta(y(\mathtt{C}z)))$. Then $(G,\mathtt{K})$,
and $(G,\mathtt{C}\mathtt{K})$ are fgvs, and
$(G,\mathtt{K})\simeq(G,\mathtt{C}\mathtt{K})$:

$\displaystyle Y\in\mathsf{FPC}\quad\Longrightarrow\quad YG\mathtt{K}$
$\displaystyle=G(YG)\mathtt{K}=\mathtt{K}(YG(\mathtt{C}\mathtt{K}))(\delta(YG(\mathtt{C}\mathtt{K})))=YG(\mathtt{C}\mathtt{K})$
$\displaystyle=G(YG)(\mathtt{C}\mathtt{K})=(\mathtt{C}\mathtt{K})(YG(\mathtt{C}(\mathtt{C}\mathtt{K})))(\delta(YG(\mathtt{C}(\mathtt{C}\mathtt{K}))))$
$\displaystyle\hskip
68.71321pt=(\mathtt{K}\mathtt{I})(YG\mathtt{K})(\delta(YG\mathtt{K}))=\delta(YG\mathtt{K})\in\mathsf{FPC}$

The reason that in the definition of $\simeq$ the quantifier ranges over fpcs
both in the case of fgvs as well as wfgvs is that, when the quantifier is
taken over all wfpcs, it makes the resulting notion of equality much more
restrictive, as we shall now demonstrate.

Because we obviously want equal fgvs to remain equal as wfgvs, the definition
of extensional equality is expressed in terms of behavior on fpcs in both
contexts.

######  Proposition 19.

If $Y\vec{G}=Y\vec{G}^{\prime}$ for every wfpc $Y$, then for some $k$,
$\delta^{k}(z)\vec{G}=\delta^{k}(z)\vec{G}^{\prime}$.

######  Proof 6.1.

This statement follows by the same reasoning as used in Theorem 15. Take
$z\\#\vec{G},\vec{G}^{\prime}$, and let $\Upsilon=\Upsilon_{z}$ be the
canonical wfpc defined there with a deterministic reduction graph that uses
the variable $z$ to track its unfolding history. The argument subsequently
showed how every conversion $C[\Upsilon M]\twoheadrightarrow
X\twoheadleftarrow C^{\prime}[\Upsilon M]$ can be extended through
$X\twoheadrightarrow X^{\prime}$, such that
$X^{\prime}=D[\Upsilon^{k}_{N},\cdots,\Upsilon^{k}_{N}]$, with
$M\twoheadrightarrow N$ and every occurrence of $z$ in $X^{\prime}$ to be
found among the displayed $\Upsilon^{k}_{N}$. We could then conclude that the
common reduction may be lifted to a finite truncation of $\Upsilon$. In the
present case, our starting conversion has the form

$C[\Upsilon G_{0}]:=[\Upsilon G_{0}]G_{1}\cdots G_{n}=[\Upsilon
G_{0}^{\prime}]G_{1}^{\prime}\cdots
G_{n^{\prime}}^{\prime}=:C^{\prime}[\Upsilon G_{0}^{\prime}]$ (5)

To justify application of the same argument, we should thus argue why
$G_{0}=G_{0}^{\prime}$. Let $X$ be a reduct of $C[\Upsilon G_{0}]$. By
recalling the reduction graph of $\Upsilon$, it is evident that every
innermost occurrence of $z$ in $X$ is applied to a reduct of $G_{0}$. If $X$
is also a reduct of $C^{\prime}[\Upsilon G_{0}^{\prime}]$, then the same
conclusion will hold, with $G_{0}^{\prime}$ in place of $G_{0}$. Thus, the
very fact of occurrence of $z$ in $X$ forces $G_{0}$ and $G_{0}^{\prime}$ to
be convertible. Of course, if $z$ does not occur in $X$ at all, that only
means that all descendants of $\Upsilon$ have already been erased, in which
case there is nothing left to prove. So $G_{0}=G_{0}^{\prime}$. We can thus
adjust conversion in (5) to

$C[\Upsilon G_{0}]\equiv[\Upsilon G_{0}]G_{1}\cdots G_{n}=[\Upsilon
G_{0}]G_{1}^{\prime}\cdots G_{n^{\prime}}^{\prime}\equiv C^{\prime}[\Upsilon
G_{0}]=C^{\prime}[\Upsilon G_{0}^{\prime}]$

where the conversion on the right takes place inside the subterm that
$\Upsilon$ is applied to.

Now we extend the other conversion to a common reduct

$[\Upsilon G_{0}]G_{1}\cdots G_{n}\twoheadrightarrow
D[\Upsilon^{k}_{N},\cdots,\Upsilon^{k}_{N}]\twoheadleftarrow[\Upsilon
G_{0}]G_{1}^{\prime}\cdots G_{n^{\prime}}^{\prime}$

and proceed, as in the proof of Theorem 15, to lift these reductions to

$[\delta^{k}(u)G_{0}]G_{1}\cdots G_{n}\twoheadrightarrow
D[uN,\dots,uN]\twoheadleftarrow[\delta^{k}(u)G_{0}]G_{1}^{\prime}\cdots
G_{n^{\prime}}^{\prime}.$

Converting $G_{0}$ in the right term to $G_{0}^{\prime}$, we obtain the
desired result.

From now on, we will consider the monoid $\mathcal{G}$ up to extensional
equality. We will also write concatenation of vectors by juxtaposition:
$\vec{F}\vec{G}=\vec{F}\odot\vec{G}$.

### Ideals

A _two-sided ideal_ in a monoid $(M,\cdot)$ is a set $I\subseteq M$ such that

$i\in I,\,m\in M\quad\Longrightarrow\quad i\cdot m,\,m\cdot i\,\in\,I.$

######  Proposition 20.

  1. (1)

The constant generators form the minimal ideal in both monoids.

  2. (2)

The weakly constant/weakly compact wfgvs form a two-sided ideal in
$\mathcal{G}$.

  3. (3)

The compact fgvs form a two-sided ideal in $\mathcal{F}$ (and a right ideal in
$\mathcal{G}$).

######  Proof 6.2.

  1. (1)

Let $\vec{G}$ be constant, so that $Y\vec{G}=Z$ for all (w)fpc $Y$. Let
$\vec{G}^{\prime}$ be arbitrary. Then
$Y\vec{G}\vec{G}^{\prime}=Z\vec{G}^{\prime}$ for all $Y$, and
$Y\vec{G}^{\prime}\vec{G}=Z$ for all $Y$. Thus $\vec{G}\vec{G}^{\prime}$ and
$\vec{G}^{\prime}\vec{G}$ are constant. Moreover, since any ideal includes the
constant generators by composition on the right, these generators together
constitute the minimal ideal.

  2. (2)

Let $\vec{G}\in\mathcal{G}$ be weakly constant, so that
$z\notin^{\infty}G_{0}^{k}(z)G_{1}\cdots G_{n}$. Let
$\vec{G}^{\prime}\in\mathcal{G}$ be arbitrary. Clearly,
$z\notin^{\infty}G_{0}^{k}(z)G_{1}\cdots G_{n}G_{0}^{\prime}\cdots
G_{m}^{\prime}$. That is, $\vec{G}\vec{G}^{\prime}$ is weakly constant. On the
other hand, we know that $\vec{G}^{\prime}$ maps wfpcs to themselves:

$(\lambda y.y\vec{G}^{\prime}):\mathsf{WFPC}\to\mathsf{WFPC}$

All wfpcs have the same Böhm tree, and in the tree topology, its neighborhood
basis consists of the set $\\{{\lambda x.x^{n}(\Omega)\mid n\geq 0}\\}$. By
Continuity Theorem [1, 14.3.22], there exists $l\geq 0$ such that

$\displaystyle(\lambda x.x^{l}(z))\vec{G}^{\prime}=(\lambda
y.y\vec{G}^{\prime})(\lambda x.x^{l}(z))$ $\displaystyle=\lambda x.x^{k}(X)$

for some $X$, possibly containing $z$. And yet,

$\displaystyle z\notin^{\infty}G_{0}^{k}(X)G_{1}\cdots G_{n}=(\lambda
x.x^{k}(X))\vec{G}=(\lambda
x.x^{l}(z))\vec{G}^{\prime}\vec{G}=(G^{\prime}_{0})^{l}(z)G^{\prime}_{1}\cdots{}G^{\prime}_{m}\vec{G}.$

Indeed, $\vec{G}^{\prime}\vec{G}$ is weakly constant.

  3. (3)

It is immediate that the rectifying fgvs form a two-sided ideal in
$\mathcal{F}$. By Theorem 15, so do the compact ones. Also, for
$\vec{G},\vec{G}^{\prime}\in\mathcal{G}$, $\vec{G}^{\prime}$ rectifying
clealry implies $\vec{G}\vec{G}^{\prime}$ rectifying.

### Green’s relations

The structure of many monoids can be characterized in terms of Green’s
relations. Here we record several observations about these relations in
$\mathcal{G}$, which could be useful for future study of this monoid. For
$\vec{G},\vec{G}^{\prime}\in\mathcal{G}$, put

$\displaystyle\mathpzc{L}(\vec{G})$
$\displaystyle\\!\quad=\quad\\{{\vec{H}\vec{G}\mid\vec{H}\in\mathcal{G}}\\}$
$\displaystyle\mathpzc{R}(\vec{G})$
$\displaystyle\\!\quad=\quad\\{{\vec{G}\vec{H}\mid\vec{H}\in\mathcal{G}}\\}$
$\displaystyle\vec{G}\preccurlyeq_{\mathpzc{L}}\vec{G}^{\prime}$
$\displaystyle\iff\,\mathpzc{L}(\vec{G})\subseteq\mathpzc{L}(\vec{G}^{\prime})\,\iff\vec{G}\in\mathpzc{L}(\vec{G}^{\prime})$
$\displaystyle\vec{G}\preccurlyeq_{\mathpzc{R}}\vec{G}^{\prime}$
$\displaystyle\iff\mathpzc{R}(\vec{G})\subseteq\mathpzc{R}(\vec{G}^{\prime})\iff\vec{G}\in\mathpzc{R}(\vec{G}^{\prime})$
$\displaystyle\vec{G}\sim_{\mathpzc{L}}\vec{G}^{\prime}$
$\displaystyle\iff\,\mathpzc{L}(\vec{G})=\mathpzc{L}(\vec{G}^{\prime})$
$\displaystyle\vec{G}\sim_{\mathpzc{R}}\vec{G}^{\prime}$
$\displaystyle\iff\mathpzc{R}(\vec{G})=\mathpzc{R}(\vec{G}^{\prime}).$

  1. (1)

If $\vec{G}\simeq(\mathtt{K}Z)$ is a constant generator, then
$\mathpzc{L}(\vec{G})=\\{{\mathtt{K}Z}\\}$, so all constant generators are
each in their own left class. That is, $\vec{G}\in\mathpzc{L}(\mathtt{K}Z)$
implies $\vec{G}\simeq(\mathtt{K}Z)$.

  2. (2)

On the other hand,
$(\mathtt{K}Z,\mathtt{K}Z^{\prime})\simeq(\mathtt{K}Z^{\prime})$, thus
$\mathtt{K}Z^{\prime}\in\mathpzc{R}(\mathtt{K}Z)$. Since the choice of
$Z,Z^{\prime}$ was arbitrary,
$\mathtt{K}Z\sim_{\mathpzc{R}}\mathtt{K}Z^{\prime}$ for all $Z$ and
$Z^{\prime}$. That is, constant generators are all in the same right class.
Since constant generators form an ideal, $\vec{G}{\sim{R}}(\mathtt{K}Z)$ or
$\vec{G}\preccurlyeq{R}(\mathtt{K}Z)$ imply
$\vec{G}\simeq(\mathtt{K}Z^{\prime})$ for some $Z^{\prime}$. So
$\mathpzc{R}(\mathtt{K}Z)=\\{{(\mathtt{K}Z^{\prime})\mid
Z^{\prime}\in\mathsf{WFPC}}\\}$ is the ideal of all constant generators.

  3. (3)

Similarly, if $\vec{G}$ is weakly constant, then so is every element of
$\mathpzc{L}(\vec{G})$ and $\mathpzc{R}(\vec{G})$. That is, the only (w)fgvs
that can be congruent to $\vec{G}$ modulo $\sim{L}$ or $\sim{R}$ are again
weakly constant.

  4. (4)

If $\vec{G}$ is compact, then so is every element of $\mathpzc{L}(\vec{G})$.
When restricted to $\mathcal{F}$, both $\mathpzc{L}(\vec{G})$ and
$\mathpzc{R}(\vec{G})$ consist of compact generators.

  5. (5)

Suppose $\vec{G}\sim{R}\vec{G}^{\prime}$. Then we can find
$\vec{F},\vec{F}^{\prime}\in\mathcal{G}$ such that
$\vec{G}\simeq\vec{G}^{\prime}\vec{F}$, and
$\vec{G}^{\prime}\simeq\vec{G}\vec{F}^{\prime}$. But then
$\vec{G}\simeq\vec{G}\vec{F}^{\prime}\vec{F}$, and
$\vec{G}^{\prime}\simeq\vec{G}^{\prime}\vec{F}\vec{F}^{\prime}$. If
$\vec{G}\simeq\vec{G}\vec{F}^{\prime}\vec{F}$, then for every $Y$,
$Y\vec{G}=Y\vec{G}\vec{F}^{\prime}\vec{F}$ is a fixed point of
$\vec{F}^{\prime}\vec{F}$. By Conjecture 8, $\vec{F}^{\prime}\vec{F}$ is
weakly constant. By Proposition 20, so is $\vec{G}\vec{F}^{\prime}\vec{F}$.
But $\vec{G}\vec{F}^{\prime}\vec{F}\simeq\vec{G}$. So $\vec{G}$ is weakly
constant. Of course, everything we just said applies to $\vec{G}^{\prime}$ as
well. We conclude that, modulo Conjecture 8, nontrivial $\sim{R}$-relations
can only exist between weakly constant wfgvs.

In fact, we believe that for accretive $\vec{G},\vec{G}^{\prime}$, either
$\vec{G}\sim{R}\vec{G}^{\prime}$ or $\vec{G}\sim{L}\vec{G}^{\prime}$ implies
$\vec{G}\simeq\vec{G}^{\prime}$. Indeed, this is a consequence of the
“freeness” conjecture we formulate next.

### Unique factorization of accretive generators

An accretive generator $\vec{G}$ is _prime_ if
$\vec{G}=\vec{G}_{1}\vec{G}_{2}$ implies
$\\{{\vec{G}_{1},\vec{G}_{2}}\\}=\\{{\vec{G},()}\\}$. The following “unique
factorization conjecture” states that the accretive generators are freely
generated by the prime ones.

######  Conjecture 21.

If $\vec{G}\in\mathcal{G}$ is accretive, then
$\vec{G}=\vec{G}_{1}\cdots\vec{G}_{k}$, where each $\vec{G}_{i}$ is prime.

Furthermore, this decomposition is unique up to extensional equality. That is,
for all prime $\vec{G}^{\prime}_{1},\dots,\vec{G}^{\prime}_{k^{\prime}}$, if
$\vec{G}=\vec{G}^{\prime}_{1}\cdots\vec{G}^{\prime}_{k^{\prime}}$, then
$k=k^{\prime}$ and $\vec{G}_{i}\simeq\vec{G}^{\prime}_{i}$ for all
$i\in\\{{1,\dots,k}\\}$.

The conjecture implies that any relations in the monoid of wfpc generators
under composition can only arise between non-accretive i.e., weakly compact
generators. In particular, the equations

$\displaystyle\vec{F}\vec{G}$ $\displaystyle=\vec{F}$ (6)
$\displaystyle\vec{F}\vec{G}$ $\displaystyle=\vec{G}$ (7)

admit no (non-trivial) solutions among the accretive generators. As a result,
the left and right classes of accretive generators would indeed all be
distinct if Conjecture 21 was to be validated.

And what about the solutions to (6) or (7) among the rest of $\mathcal{G}$?
The following examples show that there indeed exist solutions to these
equations under certain conditions. In all cases, (weak) compactness plays an
essential role.

######  Proposition 22.

For $\vec{G}$ weakly constant, there exists non-constant $\vec{F}$ with
$\vec{F}\vec{G}\simeq\vec{F}$. (In particular,
$\vec{F}\preccurlyeq{L}\vec{G}$.)

######  Proof 6.3.

The idea is to make $\vec{F}$ generate the fixed points of $\vec{G}$ according
to the scheme in Proposition 13. Let $k$, $F_{0}$, $F_{k}$ be chosen as in the
proof of that proposition. Put $A=\lambda yb.b(y\delta)$, $B=\lambda
y.F_{0}[y(\lambda u.F_{k}[uG_{0}])G_{0}]$, and $\vec{F}=(A,B)$. Observe that

$\displaystyle Y\in\mathsf{FPC}\quad\Longrightarrow\quad Y\\!A\delta$
$\displaystyle=A(Y\\!A)\delta=\delta(Y\\!A\delta)$ $\displaystyle Y\\!AB$
$\displaystyle=A(Y\\!A)B=B(Y\\!A\delta)=F_{0}[(Y\\!A\delta)(\lambda
u.F_{k}[uG_{0}])G_{0}].$

Since $Y\\!A\delta$ is thereby forced to be fpc, it follows that
$Y\\!AB=F_{0}[UG_{0}]$, where $U=F_{k}[UG_{0}]$. This allows us to calculate
as in the proof of Proposition 13 that $Y\\!AB$ is a fixed point of $\vec{G}$:

$Y\vec{F}\vec{G}=Y\\!AB\vec{G}=Y\\!AB$

Note however, that $\vec{F}$ will not be constant in general, because it uses
its fpc argument to define $U$.

######  Proposition 23.

Let $\vec{F}=(F_{0},\cdots,F_{n})$ be wfgv with $n\geq 1$. There exists a
compact fgv $\vec{G}$ such that $\vec{F}\vec{G}\simeq\vec{G}$. (In particular,
$\vec{G}\preccurlyeq{R}\vec{F}$.)

######  Proof 6.4.

First, recall that $F_{0}=\lambda v_{0}..v_{l}.v_{m}\vec{P}$ is solvable.
Since $Y\vec{F}=F_{0}(Y^{\prime}F_{0})F_{1}\cdots F_{n}$, we also know that
the head variable $v_{m}$ cannot be $v_{0}$, for otherwise the result would be
unsolvable, while it must be a wfpc.

We let $\vec{G}=(F_{0},G_{1},\cdots,G_{n+1})$. We will only need to specify a
couple of $G_{i}$s. Set $G_{m}=\lambda\vec{p}.\lambda
g_{l+1},...,g_{n+1}.\Theta_{g_{n+1}(F_{0}v_{0}F_{1}\cdots F_{n})}$,
$G_{n+1}y=\Theta(\lambda gy.g(y\vec{F}))=G_{n+1}(y\vec{F})$.

$\displaystyle Y\vec{G}$ $\displaystyle=G_{0}(Y^{\prime}G_{0})G_{1}\cdots
G_{n+1}$ $\displaystyle=F_{0}(Y^{\prime}F_{0})G_{1}\cdots G_{n+1}$
$\displaystyle=G_{m}\vec{P}[v_{0}:=Y^{\prime}F_{0}][v_{i}:=G_{i}]_{1\leq i\leq
l}G_{l+1}\cdots G_{n+1}$
$\displaystyle=\Theta_{G_{n+1}(F_{0}(Y^{\prime}F_{0})F_{1}\cdots F_{n})}$
$\displaystyle=\Theta_{G_{n+1}(YF_{0}\cdots F_{n})}$
$\displaystyle=\Theta_{G_{n+1}(Y\vec{F})}$ ($\star$)
$\displaystyle=\Theta_{G_{n+1}(Y\vec{F}\vec{F})}$
$\displaystyle=\Theta_{G_{n+1}((Y\vec{F})\vec{F})}$
$\displaystyle=(Y\vec{F})\vec{G}\quad\textrm{by ($\star$), with
$Y:=Y\vec{F}$}$

Our final observation is a corollary to one of the first ones.

######  Proposition 24.

The monoid $\mathcal{G}$ is _zerosum-free_ : If $\vec{F}\vec{G}\simeq()$, then
$\vec{F}\simeq()\simeq\vec{G}$.

######  Proof 6.5.

Suppose $\vec{F}\vec{G}\simeq()$. Then, considered as endofunctions on
$\mathsf{WFPC}/{=_{\beta}}$, $\vec{G}$ acts as a left inverse of $\vec{F}$,
making $\vec{F}$ a split mono (modulo beta). But we have seen in Proposition 5
that no wfgv is injective, so no wfgv can be monic. Specifically, take $Y\neq
Y^{\prime}$ such that $Y\vec{F}=Y^{\prime}\vec{F}$. Since
$()\simeq\vec{F}\vec{G}$, we have
$Y=Y\vec{F}\vec{G}=Y^{\prime}\vec{F}\vec{G}=Y^{\prime}$, a contradiction.

##  7\. Concluding remarks

In this paper,we have broached the topic of abstract fpc generators. Our first
investigations revealed that these operators naturally fall into a few robust
classes. We established elementary relationships between these classes.

What becomes clear from our investigations is that there is yet much to be
uncovered about the structure of fixed point combinators. Some of the possible
future research directions include the following.

  1. (1)

The most pressing issue is the status of Conjecture 8. All the evidence
available points to this conjecture being true, yet current techniques in
untyped lambda calculus decidedly come up short in settling the question.
However it will be decided, the insights to be gathered from the new
approaches will greatly deepen our understanding of lambda terms.

  2. (2)

Of course, one could take the next step and ask whether the converse to the
first claim in Proposition 13 is also valid. Considering how difficult the
former question is, this one will likely remain out of reach for the
foreseeable future.

  3. (3)

What else can be said about the structure of the monoid $\mathcal{G}$? Is the
submonoid of accretive generators freely generated by the prime generators, as
Conjecture 21 asserts? What about the (weakly) compact generators? How can
their compositional structure be characterized?

  4. (4)

Since the monoid of (w)fgvs naturally acts on the set of (w)fpcs, how much of
the structure of fpcs is captured by this monoidal action? Does every fpc have
a representation in terms of the prime elements of the monoid — again, modulo
extensional equality, and the ideal of compact generators?

  5. (5)

Finally, while not directly relevant to the earier discussion, an answer to
the following question could also shed light on recursion-theoretic properties
of FPCs:

Let $\mathtt{Y}$ be Curry’s simplest fpc. Is $\\{{\\#M\mid M=\mathtt{Y}}\\}$ a
decidable subset of $\mathsf{FPC}$? Specifically, does there exist a term
$\Delta_{\mathtt{Y}}$ satisfying, for all _closed $Y\in\mathsf{FPC}$_, the
following:

$\displaystyle\Delta_{\mathtt{Y}}\ulcorner Y\urcorner
xy=\begin{cases}x&\mathtt{Y}=_{\beta}Y\\\
y&\mathtt{Y}\neq_{\beta}Y\end{cases}$

Notice that Scott’s theorem does not apply here because $\mathsf{FPC}$ is not
all of $\Lambda$, but is only a computably enumerable subset of it.
$\Delta_{\mathtt{Y}}$ is allowed to diverge outside of this set.

The recent paper [12] proposes another approach to Statman’s conjecture based
on simple types. We note that the generalization of the conjecture stated
there is consistent with ours, since every simply-typed generator is accretive
thanks to strong normalization of ($\mathtt{Y}$-free) typed terms.

I would like to thank Jan Willem Klop, Joerg Endrullis, Dimitri Hendriks,
Giulio Manzonetto, and Stefano Guerrini for wonderful discussions about fpc
generators.

I would also like to extend my gratitude to the anonymous referees whose many
suggestions have significantly improved this paper.

## References

  * [1] H. P. Barendregt.  The lambda calculus, its syntax and semantics.  Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1984.
  * [2] H. P. Barendregt.  Lambda calculi with types.  In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 2), pages 117–309. Oxford University Press, Inc., New York, NY, USA, 1992.
  * [3] L. Czajka.  A new coinductive confluence proof for infinitary lambda calculus.  Logical Methods in Computer Science, 16(1), 2020.
  * [4] Thierry Coquand and Hugo Herbelin.  A-translation and looping combinators in pure type systems.  Journal of Functional Programming, 4(1):77–88, 1994.
  * [5] Haskell B. Curry.  The inconsistency of certain formal logics.  Journal of Symbolic Logic, 7(3):115–117, 1942.
  * [6] Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky.  Discriminating lambda-terms using clocked Böhm trees.  Logical Methods in Computer Science, 10(2), 2014.
  * [7] Jörg Endrullis and Andrew Polonsky.  Infinitary rewriting coinductively.  In Nils Anders Danielsson and Bengt Nordström, editors, 18th International Workshop on Types for Proofs and Programs, TYPES 2011, September 8-11, 2011, Bergen, Norway, volume 19 of LIPIcs, pages 16–27. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
  * [8] Herman Geuvers and Joep Verkoelen.  On fixed point and looping combinators in type theory.  http://www.cs.ru.nl/~herman/PUBS/TLCApaper.pdf.
  * [9] Douglas J. Howe.  The computational behaviour of Girard’s paradox.  In Proceedings of the Symposium on Logic in Computer Science (LICS ’87), Ithaca, New York, USA, June 22-25, 1987, pages 205–214. IEEE Computer Society, 1987.
  * [10] Benedetto Intrigila.  Non-existent Statman’s double fixedpoint combinator does not exist, indeed.  Inf. Comput., 137(1):35–40, 1997.
  * [11] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries.  Infinitary lambda calculus.  Theor. Comput. Sci., 175(1):93–125, 1997.
  * [12] Giulio Manzonetto, Andrew Polonsky, Alexis Saurin, and Jakob Grue Simonsen.  The Fixed Point Property and a Technique to Harness Double Fixed Point Combinators.  Journal of Language and Computation, 29(5):831–880, 2019.
  * [13] Albert R. Meyer and Mark B. Reinhold.  ”type” is not a type.  In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986, pages 287–295. ACM Press, 1986.
  * [14] Dana S. Scott.  Some philosophical issues concerning theories of combinators.  In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, Italy, March 25-27, 1975, volume 37 of Lecture Notes in Computer Science, pages 346–366. Springer, 1975.
  * [15] Richard Statman.  Some examples of non-existent combinators.  Theoretical Computer Science, 121(1&2):441–448, 1993.