4
$\begingroup$

I just read the definition of lambda calculus. Apparently it's Turing complete, but I tried writing a very simple function and I couldn't:

f(a)=b
f(b)=a
f(x)=x otherwise

so it just swaps the variables a and b.

Functional languages already have conditions which makes it easy, but how do you do it using only abstraction and application?

$\endgroup$

1 Answer 1

6
$\begingroup$

It's impossible. And this doesn't contradict Turing completeness.

To say that a computation system is Turing-complete doesn't mean that you can express every computation you might like to express inside the system. It means that there is an encoding of Turing machines and their computation rule. If you perform the system's computation on encodings of Turing machines, it does the same thing as Turing machine computation. This doesn't imply anything about how the system behaves on objects that are not encodings of Turing machines.

An equivalent definition is that a computation system is Turing-complete if there is an encoding of natural integers such that every computable function corresponds to a computation on the encodings of the integers. Once again, this doesn't imply anything about how the system behaves on objects that are not encodings of integers.

In mathematical notation, the lambda calculus is Turing-complete because there is a function $E : \mathbb{N} \to \Lambda$, where $\Lambda$ is the set of all lambda terms, such that if $f : \mathbb{N} \to \mathbb{N}$ is computable then there is a lambda-term $F_f$ such that $\forall n \in \mathbb{N}, F_f E(n) \equiv_\beta E(f(n))$. If $M$ is a lambda term that cannot be expressed as $E(n)$, there is no particular reason why $F_f M$ would reduce to anything remarkable.

An example of encoding of integers into the lambda calculus, which does demonstrate the lambda calculus's Turing completeness, is the Church numerals, which encode a natural number as the function that maps an integer $n$ to the $n$-times repetition function: the function that maps every function $f$ to $f$ iterated $n$ times. That is, $E(0) = \lambda x. \lambda f. x$, $E(1) = \lambda x. \lambda f. f(x)$, $E(2) = \lambda x. \lambda f. f(f(x))$, etc. The lambda terms that are of the form $E(n)$ are called Church numerals. I'll write $\mathscr{C}$ for the set of Church numerals.

If $A$ and $B$ are two Church numerals, there is indeed a lambda term $S_{A,B}$ such that $S_{A,B} A \equiv_\beta B$, $S_{A,B} B \equiv_\beta A$, and $\forall X \in \mathscr{C} \setminus \{A,B\}, S_{A,B} X \equiv_\beta X$. I will leave finding an expression for $S_{A,B}$ as an exercise. It's tedious, but not difficult once you've played a bit with Church encodings.

If $X$ is not a Church numeral, there is no particular reason why $S_{A,B} X$ would be beta-equivalent to $X$. And there is no particular reason to believe that the construction of $S_{A,B}$ can be generalized to the case where $A$ and $B$ are arbitrary lambda terms. I will prove that the second property in fact cannot be generalized to variables at all. I believe that the first property also cannot be true of any encoding, but this requires non-elementary theorems.

Suppose that $M a \equiv_\beta b$ and $M b \equiv_\beta a$. Since $M a$ is not a normal form, $M$ must reduce to an abstraction: $M \to_\beta^* \lambda x. N$. Then $M a \equiv_\beta (\lambda x. N) a \to_\beta N[x \leftarrow a]$. Since we assumed $M a \equiv_\beta b$, we have $N[x \leftarrow a] \equiv_\beta b$. Now apply another renaming substitution: $N = N[x \leftarrow a][a \leftarrow x] \equiv_\beta b[a \leftarrow x] = b$. But we also have the assumption $M b \equiv_\beta a$, hence $N[x \leftarrow b] \equiv_\beta a$ and $N = N[x \leftarrow b][b \leftarrow x] \equiv_\beta a[b \leftarrow x] = a$. So $a \equiv_\beta N \equiv_\beta b$, which is impossible since $a$ and $b$ are distinct normal forms.

Intuitively speaking, in the lambda calculus, all variables are indistinguishable. This is an indirect consequence of alpha conversion and of the fact that variables can be substituted by arbitrary terms through abstraction and beta reduction: to make the “identity” of a variable disappear, put it under a lambda, and it becomes a bound, renamable variable.

Programming languages based on the lambda calculus are different because they have objects other than functions. As soon as you add constants, and rules to calculate on those constants (called delta rules), the shape of the possible computations changes. To start with, in the lambda calculus, the normal forms (i.e. values) have a simple characteristic: they're all functions applying a variable, i.e. $\lambda x_1. \cdots \lambda x_n. y M_1 \cdots M_m$ for some $(n,m) \in \mathbb{N}^2$. As soon as you add constants, the shape of values is much more complicated, since an application of a constant to a term may or may not be reducible depending on what delta rules involve this constant. It is trivial in virtually every programming language to define a function $f$ such that $f(c_1) = c_2$ and $f(c_2) = c_1$ for two constants $c_1$ and $c_2$. But if you apply this function to variables ($f(x)$), you won't get another variable: you'll get at most a partially evaluated term still involving the variable.

$\endgroup$
1
  • $\begingroup$ Thanks it has cleared my doubts ! $\endgroup$
    – hehehe
    Dec 30, 2021 at 5:19

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.