English Wikipedia @ Freddythechick

Scott–Curry theorem

In mathematical logic, the Scott–Curry theorem is a result in lambda calculus stating that if two non-empty sets of lambda terms A and B are closed under beta-convertibility then they are recursively inseparable.[1]

Explanation

A set A of lambda terms is closed under beta-convertibility if for any lambda terms X and Y, if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X \in A} and X is β-equivalent to Y then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Y \in A} . Two sets A and B of natural numbers are recursively separable if there exists a computable function   such that   if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a \in A} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f(b) = 1} if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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.

Proof

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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle fx = 0} if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x \in A} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle fx = 1} if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x \in B} (where equality is β-equality). Then define Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle G \equiv \lambda x.\text{if}\ (\text{zero?} \ (fx)) a b} . Here, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \text{zero?}} is true if its argument is zero and false otherwise, and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \text{if}} is the identity so that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \text{if}\ b x y} is equal to x if b is true and y if b is false.

Then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x \in C \implies Gx = a} and similarly, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X \in C} implies that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X = G(X') = b} so in fact Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X \notin C} . The reverse assumption Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X \notin C} gives Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X = G(X') = a} so Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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.

History

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]

References

  1. ^ Hindley, J.R.; Seldin, J.P. (1986). Introduction to Combinators and (lambda) Calculus. Cambridge Monographs on Mathematical Physics. Cambridge University Press. ISBN 9780521268967. LCCN lc85029908.
  2. ^ Barendregt, H.P. (1985). The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. 103 (3rd ed.). Elsevier Science. ISBN 0444875085.
  3. ^ Gabbay, D.M.; Woods, J. (2009). Logic from Russell to Church. Handbook of the History of Logic. Elsevier Science. ISBN 9780080885476.
  4. ^ Curry, Haskell B. (1969). "The undecidability of λK-conversion". Journal of Symbolic Logic. January 1969: 10–14.
Retrieved from "https://enwiki.freddythechick.net/index.php?title=Scott–Curry_theorem&oldid=16138668"