Lambda calculus without free variables is as strong as lambda calculus?

Question

First question: How would one prove that by removing free (unbound) variables from lambda calculus, and allowing only bound variables, its power is not reduced (it is still Turing-complete) ?

Second question: Is the proposition given above really true? Is lambda calculus sans free variables really Turing-complete?

Answer 1

I'm assuming you are referring to the untyped lambda calculus.

If so, write $\newcommand{\num}[1]{\ulcorner #1 \urcorner}\num{n}$ for the Church numeral of the natural unmber $n$.

It is known that there exists a closed term (i.e., without free variables) $TM$ such that $$ TM\ \num{i}\ \num{n}\ =_{\beta\eta}\ \num{m} $$ if, and only if, the $i$-th Turing machine (in some standard enumeration) run with input $n\in\mathbb N$ (encoded as usual) halts returning $m$ as output.

Indeed, writing $TM$ is a standard "programming" exercise in the lambda calculus. For that, one can represent the tape as a pair-or-pairs-of-pairs-of... (AKA a cons list) of symbols. Then a "stepping" subroutine to advance the tape and the TM state can be written. Finally, the stepping subroutine is invoked until a halting state is reached. This last step can be achieved using a fixed point combinator such as $Y$.

Since we can simulate any Turing machine, we get Turing completeness.

---

Alternative proof, which is (in my opinion) easier to actually perform in full detail: prove that any general recursive function can be $\lambda$-defined using a closed lambda term. For that, proceed by induction on the definition of general recursive function.

Indeed, even if you do not aim for closed terms, in this programming exercise you will obtain a closed one in a natural way. After all, when programming one never needs a variable which was not declared beforehand.

Since the general recursive functions are exactly those which can be computed by a Turing machine, we get Turing completeness for the closed lambda calculus.