In
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
, the Scott–Curry theorem is a result in
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation th ...
stating that if two non-empty sets of lambda terms ''A'' and ''B'' are closed under beta-convertibility then they are
recursively inseparable In computability theory, two disjoint sets of natural numbers are called computably inseparable or recursively inseparable if they cannot be "separated" with a computable set.Monk 1976, p. 100 These sets arise in the study of computability the ...
.
Explanation
A set ''A'' of lambda terms is closed under beta-convertibility if for any lambda terms X and Y, if
and X is
β-equivalent to Y then
. Two sets ''A'' and ''B'' of natural numbers are recursively separable if there exists a
computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...
such that
if
and
if
. Two sets of lambda terms are recursively separable if their corresponding sets under a
Gödel numbering
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was developed by Kurt Gödel for the proof of h ...
are recursively separable, and recursively inseparable otherwise.
The Scott–Curry theorem applies equally to sets of terms in
combinatory logic
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of com ...
with weak equality. It has parallels to
Rice's theorem
In computability theory, Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior (for instance, does the program terminate for all inputs), unlike a synta ...
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
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an ...
to determine if two lambda terms are β-equivalent.
Proof
The proof is adapted from Barendregt in ''The Lambda Calculus''.
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
if
and
if
(where equality is β-equality). Then define
. Here,
is true if its argument is zero and false otherwise, and
is the identity so that
is equal to ''x'' if ''b'' is true and ''y'' if ''b'' is false.
Then
and similarly,
. 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
implies that
so in fact
. The reverse assumption
gives
so
. 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.
History
Dana Scott
Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
first proved the theorem in 1963. The theorem, in a slightly less general form, was independently proven by
Haskell Curry
Haskell Brooks Curry (; September 12, 1900 – September 1, 1982) was an American mathematician and logician. Curry is best known for his work in combinatory logic. While the initial concept of combinatory logic was based on a single paper by ...
. It was published in Curry's 1969 paper "The undecidability of λK-conversion".
References
{{reflist
Lambda calculus
Undecidable problems