Scott–Curry theorem

A set A of lambda terms is closed under beta-convertibility if for any lambda terms X and Y, if ${\displaystyle X\in A}$ and X is β-equivalent to Y then ${\displaystyle Y\in A}$. Two sets A and B of natural numbers are recursively separable if there exists a computable function ${\displaystyle f:\mathbb {N} \rightarrow \{0,1\}}$ such that ${\displaystyle f(a)=0}$ if ${\displaystyle a\in A}$ and ${\displaystyle f(b)=1}$ if ${\displaystyle b\in B}$. Two sets of lambda terms are recursively separable if their corresponding sets under a Gödel numbering are recursively separable, and recursively inseparable otherwise.

The Scott–Curry theorem applies equally to sets of terms in combinatory logic with weak equality. It has parallels to Rice's theorem in computability theorem, which states that all non-trivial semantic properties of programs are undecidable.

The theorem has the immediate consequence that it is an undecidable problem to determine if two lambda terms are β-equivalent.

The proof is adapted from Barendregt in The Lambda Calculus.[2]

Let A and B be closed under beta-convertibility and let a and b be lambda term representations of elements from A and B respectively. Suppose for a contradiction that f is a lambda term representing a computable function such that ${\displaystyle fx=0}$ if ${\displaystyle x\in A}$ and ${\displaystyle fx=1}$ if ${\displaystyle x\in B}$ (where equality is β-equality). Then define ${\displaystyle G\equiv \lambda x.{\text{if}}\ ({\text{zero?}}\ (fx))ab}$. Here, ${\displaystyle {\text{zero?}}}$ is true if its argument is zero and false otherwise, and ${\displaystyle {\text{if}}}$ is the identity so that ${\displaystyle {\text{if}}\ bxy}$ is equal to x if b is true and y if b is false.

Then ${\displaystyle x\in C\implies Gx=a}$ and similarly, ${\displaystyle x\notin C\implies Gx=b}$. By the Second Recursion Theorem, there is a term X which is equal to f applied to the Church numeral of its Gödel numbering, X'. Then ${\displaystyle X\in C}$ implies that ${\displaystyle X=G(X')=b}$ so in fact ${\displaystyle X\notin C}$. The reverse assumption ${\displaystyle X\notin C}$ gives ${\displaystyle X=G(X')=a}$ so ${\displaystyle X\in C}$. Either way we arise at a contradiction, and so f cannot be a function which separates A and B. Hence A and B are recursively inseparable.

Dana Scott first proved the theorem in 1963. The theorem, in a slightly less general form, was independently proven by Haskell Curry.[3] It was published in Curry's 1969 paper "The undecidability of λK-conversion".[4]