Teorema de Scott-Curry

En lógica matemática , el teorema de Scott-Curry es un resultado del cálculo lambda que establece que si dos conjuntos no vacíos de términos lambda A y B están cerrados bajo convertibilidad beta, entonces son recursivamente inseparables . ^[1]

Explicación

Un conjunto A de términos lambda es cerrado bajo beta-convertibilidad si para cualesquiera términos lambda X e Y, si y X es β-equivalente a Y entonces . Dos conjuntos A y B de números naturales son recursivamente separables si existe una función computable tal que si y si . Dos conjuntos de términos lambda son recursivamente separables si sus conjuntos correspondientes bajo una numeración de Gödel son recursivamente separables, y recursivamente inseparables en caso contrario. ${\displaystyle X\in A}$ ${\displaystyle Y\in A}$ ${\displaystyle f:\mathbb {N} \rightarrow \{0,1\}}$ ${\displaystyle f(a)=0}$ ${\displaystyle a\in A}$ ${\displaystyle f(b)=1}$ ${\displaystyle b\in B}$

El teorema de Scott-Curry se aplica igualmente a conjuntos de términos en lógica combinatoria con igualdad débil. Tiene paralelismos con el teorema de Rice en el teorema de computabilidad, que establece que todas las propiedades semánticas no triviales de los programas son indecidibles.

El teorema tiene como consecuencia inmediata que es un problema indecidible determinar si dos términos lambda son β-equivalentes.

Prueba

La prueba está adaptada de Barendregt en The Lambda Calculus . ^[2]

Sean A y B cerrados bajo la beta-convertibilidad y sean a y b representaciones de términos lambda de elementos de A y B respectivamente. Supóngase para una contradicción que f es un término lambda que representa una función computable tal que si y si (donde la igualdad es β-igualdad). Luego defina . Aquí, es verdadero si su argumento es cero y falso en caso contrario, y es la identidad tal que es igual a x si b es verdadero e y si b es falso. ${\displaystyle fx=0}$ ${\displaystyle x\in A}$ ${\displaystyle fx=1}$ ${\displaystyle x\in B}$ ${\displaystyle G\equiv \lambda x.{\text{if}}\ ({\text{zero?}}\ (fx))ab}$ ${\displaystyle {\text{zero?}}}$ ${\displaystyle {\text{if}}}$ ${\displaystyle {\text{if}}\ bxy}$

De manera similar, entonces , . Por el segundo teorema de recursión, hay un término X que es igual a f aplicado al numeral de Church de su numeración de Gödel, X ' . Entonces implica que, de hecho , . La suposición inversa da como resultado . De cualquier manera, llegamos a una contradicción, y por lo tanto, f no puede ser una función que separe a A y B . Por lo tanto, A y B son recursivamente inseparables. ${\displaystyle x\in C\implies Gx=a}$ ${\displaystyle x\notin C\implies Gx=b}$ ${\displaystyle X\in C}$ ${\displaystyle X=G(X')=b}$ ${\displaystyle X\notin C}$ ${\displaystyle X\notin C}$ ${\displaystyle X=G(X')=a}$ ${\displaystyle X\in C}$

Historia

Dana Scott demostró por primera vez el teorema en 1963. El teorema, en una forma ligeramente menos general, fue demostrado independientemente por Haskell Curry . ^[3] Fue publicado en el artículo de Curry de 1969 "La indecidibilidad de la conversión λK". ^[4]

Referencias

1. Hindley, JR ; Seldin, JP (1986). Introducción a los combinadores y al cálculo (lambda) . Cambridge Monographs on Mathematical Physics. Cambridge University Press . ISBN 9780521268967Código de artículo LCCN  lc85029908 .
2. Barendregt, HP (1985). El cálculo lambda: su sintaxis y semántica . Estudios de lógica y fundamentos de las matemáticas. Vol. 103 (3.ª ed.). Elsevier Science . ISBN 0444875085.
3. Gabbay, DM; Woods, J. (2009). Lógica desde Russell hasta Church . Manual de historia de la lógica. Elsevier Science . ISBN 9780080885476.
4. Curry, Haskell B. (1969). "La indecidibilidad de la conversión λK". Journal of Symbolic Logic . Enero de 1969: 10–14.