1
$\begingroup$

I am trying to construct a lambda expression which works in the following way: assume you have a function $f$ and an argument $x$. The lambda expression I'm trying to build is of the form $P f x$ and evaluates to $P f f(x)$. It would then endlessly evaluates to $P f f^n(x)$ for $n \in \mathbb{N}$ (the infinite loop is not a problem for me).

The lambda expression I have found so far uses the following expression for $P$:

$P=(\lambda g.\lambda f.\lambda x.((g g) f) (f x)) (\lambda g.\lambda f.\lambda x.((g g) f) (f x))$

The problem I'm having is that whereas it seems to me that this should work in theory, passing it to an actual lambda-calculus interpreter either gets me an infinite loop of developing $P$ without $f(x),f^2(x),...$ being evaluated, or I get an infinite loop of expressions with $f(f(f(....(f x))))$ expressions but never the actual value $f^n(x)$, depending on the evaluation method.

Therefore I'm asking here if my solution is sound and it is only a problem of lambda-calculus interpreters, or if there is a better solution to this problem.

$\endgroup$
3
  • 1
    $\begingroup$ It is not clear what results the interpreters give you, maybe you should copy them here. $\endgroup$ Commented May 20 at 8:30
  • 3
    $\begingroup$ Anyways, your term seems to do the job. I think the "problem" is that you expect it to be run according to a specific reduction strategy (if I understand well, reduce three outermost redexes, then fully reduce all the $f^n(x)$ parts, then start again?), which is not the one implemented by the interpreters you're using. $\endgroup$ Commented May 20 at 8:33
  • $\begingroup$ You're quite right ! Of the interpreters I have found, innermost reduction getsme infinite Ps, and outermost reduction gives me f(f(f(...x))) but never the actual value $f^n(x)$. I was struggling to find another lambda expression which would force interpreters to first compute $f(f^{n-1}(x))$, then develop again, but this has been hard. Otherwise I'll have to find a way to tweak interpreters. $\endgroup$ Commented May 20 at 14:02

1 Answer 1

Reset to default
3
$\begingroup$

Your build does as you wish.

Your interpreter is just not abbreviating the functional iterations when it generates them, but it does seem to be generating them.

Let $\mathsf Q:=(\lambda g.\lambda f.\lambda x.ggf(fx))$ so that $\mathsf P:=\mathsf {QQ}$.

Now since $\mathsf Qgfx\equiv ggf(fx)$ then, by hand we find:

$\qquad\begin{align}\mathsf Pfx &\equiv \mathsf {QQ}fx\\&\equiv \mathsf{ QQ}f(fx)\\&\equiv \mathsf {QQ}f(f(fx))&&\equiv\mathsf {QQ}f(f^2(x))\\&~~\vdots \\&\equiv \mathsf {QQ}f(f(f(\ldots (f( fx))\ldots)))&&\equiv\mathsf {QQ}f(f^n(x)) \end{align}$

$\endgroup$
1
  • $\begingroup$ Thanks ! I was wondering if my expression was wrong. Finding an alternate expression for which interpreters would be forced to compute $f^n(x)$ first is hard though. I'll have to see if there's a way to tweak interpreters.... $\endgroup$ Commented May 20 at 14:04

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.