Intereting Posts

Why is convexity more important than quasi-convexity in optimization?
Why does the harmonic series diverge but the p-harmonic series converge
Prove that $ x_1+ \dotsb + x_k=n, \frac1{x_1}+ \dotsb + \frac1{x_k}=1$
T-invariant sub-sigma algebra
Sufficient and necessary condition for strictly monotone differentiable functions
Proving tautologies using semantic definitions
Locally bounded Family
How far can one get in analysis without leaving $\mathbb{Q}$?
How do you remember theorems?
point which minimises the sum of the distances from the sides in a triangle
Eigen Values Proof
Continuous function that is only differentiable on irrationals
How to show that the circle group T is isomorphic to $\mathbb R/ \mathbb Z$
Quotient of a local ring at a point is a finite dimensional vector space
Conformal mapping of a doubly connected domain onto an annulus

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states:

In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$

can be solved for $x$. That is, there is a term $X$ such that $$Xy_1..y_n =_{\beta,w} [X/x]Z$$

I dont understand how to even think about it. I was thinking that $y_1…y_n$ could be thought of as a function on which $X$ acts so $X$ is the fixed point I would like to find. Is that right?

And I dont even understand the proof a little bit, which is – Choose $X = \mathbf{Y}(\lambda x y_1…y_n.Z)$ What does it mean? How is it a solution? Can someone explain?

Note that $\mathbf{Y}$ here means any fixed-point combinator, i.e. $\mathbf{Y}X =_{\beta, w}X$ for any expression $X$.

- Prove that intervals of the form $(a,b]$, $$, $[a,\infty)$ do not have the fixed point property.
- A general result : Fixed point on finited sets?
- To prove : If $f^n$ has a unique fixed point $b$ then $f(b)=b$
- Convergence of fixed point iteration for polynomial equations
- If $f: \mathbb R^n \to \mathbb R^n$ is a contraction, then $x-f(x)$ is a homeomorphism
- Minimax Theorems V.S. Fixed Point Theorems.
- Question about fixpoints and zero's on the complex plane.
- Periodic orbits
- Continuous bijections from the open unit disc to itself - existence of fixed points
- Generalization of “easy” 1-D proof of Brouwer fixed point theorem

Just apply equational reasoning starting from the provided solution

$$ X = \mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) $$

Recall that $\mathbf{Y}F = F(\mathbf{Y}F)$ for any $\lambda$-term $F$, since $\mathbf{Y}$ is a fixed point combinator. In particular

$$

\mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) =

(\lambda x y_1 \ldots y_n.Z ) (\mathbf{Y}(\lambda x y_1 \ldots y_n.Z ))

$$

Then we just compute:

$$

\begin{array}{ll}

& X y_1 \ldots y_n \\

= & \mbox{\{definition of $X$\}} \\

& \mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) y_1 \ldots y_n \\

= & \mbox{\{fixed point property\}} \\

& (\lambda x y_1 \ldots y_n.Z ) (\mathbf{Y}(\lambda x y_1 \ldots y_n.Z )) y_1 \ldots y_n \\

= & \mbox{\{definition of $X$\}} \\

& (\lambda x y_1 \ldots y_n.Z ) X y_1 \ldots y_n \\

= & \mbox{\{$\beta$ reduction, applied $n+1$ times\}} \\

& [y_n / y_n] \ldots [ y_1 / y_1 ] [X/x] Z \\

= & \mbox{\{substituting a variable for itself has no effect\}} \\

& [X/x] Z \\

\end{array}

$$

Q.E.D.

Let me add some intuition about how one can find the proposed solution. Recall the equation

$$ x y_1 \ldots y_n = Z $$

and consider the easy case where $x \notin {\sf free}(Z)$. In this case there’s a trivial solution: $x$ can just take $n$ arguments $y_1 \ldots y_n$ and output $Z$:

$$

x = \lambda y_1 \ldots y_n. Z

$$

Hence, the above solves the easy case. What about the general one? There, the above equation does not provide a solution, since $x$ is present in the right hand side. However, we can apply a “reverse $\beta$ reduction step” to isolate such $x$:

$$

x = (\lambda x y_1 \ldots y_n. Z) x

$$

We can rewrite the above as

$$

x = F x \qquad\mbox{where } F = (\lambda x y_1 \ldots y_n. Z)

$$

Now, $F$ is a well-defined $\lambda$-term not involving $x$ as a free variable. All that is left is to solve the equation $x = F x$, but this is a fixed point equation so we can simply take $x = \mathbf{Y} F$ for this. Hence, we obtain the proposed solution.

- $n$ Lines in the Plane
- How do I show that this curve has a nonsingular model of genus 1?
- In category theory: What is a fibration and why should I care about them?
- Finding Weak Solutions to ODEs
- Poisson random variable with parameter $\lambda>0$
- Solving a non-linear Partial differential equation $px^5-4q^3x^2+6x^2z-2=0$
- For which $n$ is it “feasible” to classify groups of order $n$?
- Cheap proof that the Sorgenfrey line is normal?
- What do polynomials look like in the complex plane?
- When do the Freshman's dream product and quotient rules for differentiation hold?
- Techniques for showing an ideal in $k$ is prime
- If one side of $\int f\ d\lambda = \int f\ d\mu – \int f\ d\nu$ exists, does the other one exist as well?
- Characteristic polynomial of a matrix with zeros on its diagonal
- Exterior Derivative vs. Covariant Derivative vs. Lie Derivative
- $\epsilon$-$\delta$ proof that $f(x) = x^3 /(x^2+y^2)$, $(x,y) \ne (0,0)$, is continuous at $(0,0)$