3
$\begingroup$

I am trying to understand the distinction between the relations

$$ \to_\beta \qquad\text{and}\qquad \twoheadrightarrow_\beta $$

in lambda calculus notation.

By $M \to_\beta N$, I mean that $N$ is obtained from $M$ by exactly one $\beta$-reduction step.

By $M \twoheadrightarrow_\beta N$, I mean that $N$ is obtained from $M$ by zero or more $\beta$-reduction steps.

I am looking for an explicit example of a lambda term $M$ such that

$$ M \twoheadrightarrow_\beta M $$

via a nontrivial reduction sequence.

More precisely, I want a sequence

$$ M \to_\beta M_1 \to_\beta \cdots \to_\beta M $$

with at least two $\beta$-reduction steps and such that at least one intermediate term $M_i$ is syntactically different from $M$.

I do not want the trivial repetition

$$ \Omega \to_\beta \Omega \to_\beta \Omega $$

where every term in the sequence is identical.

Does such an example exist in pure $\beta$-reduction?

Improve this question
$\endgroup$
1

2 Answers 2

Reset to default
3
$\begingroup$

Arguably the most immediate solution is $\Theta \, I$, where $\Theta$ is Turing's fixpoint combinator. As is well known, unlike $Y f$ which is only $\beta$-equivalent to $f\,(Y\,f)$, $\Theta\,f$ literally $\beta$-reduces to $f\,(\Theta\,f)$:

$\begin{align*}\Theta\,f & \equiv \, (\lambda x y. y\,(xxy))\, (\lambda x y. y\,(xxy))\, f \\ {} & \to_{_{\beta}} {} (\lambda y. y\,((\lambda x y. y\,(xxy))\,(\lambda x y. y\,(xxy))\,y))\, f \\ {} & \to_{_{\beta}} {} f\ ((\lambda x y. y\,(xxy))\, (\lambda x y. y\,(xxy))\, f)\ \equiv \ f\ (\Theta\,f) \end{align*}$

Thus

$\begin{align*}\Theta\, (\lambda x. x) & \twoheadrightarrow_{_{\beta}} {} (\lambda x. x) (\Theta\, (\lambda x. x)) \\ {} & \to_{_{\beta}} {} \Theta\, (\lambda x. x) \end{align*}$

Improve this answer
$\endgroup$
2
$\begingroup$

One approach is to do some (trivial) beta-expansions in $\Omega$.

$\begin{align*}\Omega' = {} & (\lambda x. (\lambda y. y)xx)(\lambda x. (\lambda y. y)xx) \\ {} \to {} & (\lambda y.y)(\lambda x. (\lambda y. y)xx)(\lambda x. (\lambda y. y)xx) \\ {} \to{} & (\lambda x. (\lambda y. y)xx)(\lambda x. (\lambda y. y)xx) = \Omega'\end{align*}$

Another idea is to tweak the combinator $\lambda x. xx$ to receive more arguments and produce a permutation of them.

$\begin{align*}& (\lambda xyz. xxzy)(\lambda xyz. xxzy)(\lambda x y.x)(\lambda xy.y) \\ {}\to{} & (\lambda xyz. xxzy)(\lambda xyz. xxzy)(\lambda xy.y)(\lambda x y.x) \\ {}\to{} & (\lambda xyz. xxzy)(\lambda xyz. xxzy)(\lambda x y.x)(\lambda xy.y)\end{align*}$

One last idea is to use a fixpoint combinator to write a recursive function that composes itself with a permutation. For example, a function $f$ taking a boolean such that $f b \to^\star f (\neg b)$ (the boolean negation $\neg$ is a permutation on two elements). Here it is in full:

Let $\Theta = (\lambda xf. f(xxf))(\lambda xf. f(xxf))$.

$\begin{align*}& \Theta(\lambda f b. b(f(\lambda xy.y))(f(\lambda xy.x)))(\lambda xy.x) \\ {}\to^\star{} & \Theta(\lambda f b. b(f(\lambda xy.y))(f(\lambda xy.x)))(\lambda xy.y) \\ {}\to^\star{} & \Theta(\lambda f b. b(f(\lambda xy.y))(f(\lambda xy.x)))(\lambda xy.x)\end{align*}$

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.