¿Existe un cálculo lambda mecanografiado que sea consistente y Turing completo?

¿Existe un cálculo lambda tipificado donde la lógica correspondiente bajo la correspondencia de Curry-Howard es consistente y donde hay expresiones lambda tipificables para cada función computable?

Esta es ciertamente una pregunta imprecisa, que carece de una definición precisa de "cálculo lambda mecanografiado". Básicamente me pregunto si hay (a) ejemplos conocidos de esto, o (b) pruebas de imposibilidad conocidas para algo en esta área.

Editar: @cody da una versión precisa de esta pregunta en su respuesta a continuación: ¿existe un sistema de tipo puro lógico (LPTS) que sea consistente y Turing completo (en el sentido que se define a continuación)?

type-theory lambda-calculus typed-lambda-calculus curry-howard Morgan Thomas
fuente

No existe un cálculo recursivamente axiomatizable (lambda o de otro tipo) cuyas funciones recursivas probables totales sean todas funciones recursivas, por lo que su cálculo tendría que implicar términos sin terminación.

Emil Jeřábek apoya a Monica el

Esta respuesta tiene un teorema que dice que no puedes tener ningún tipo de cálculo que sea Turing completo y total.

Andrej Bauer

Es probable que responda su pregunta una vez que la haga lo suficientemente precisa. Creo que la prueba de Andrej es innecesariamente complicada (pero muestra más): el punto es simplemente que si hubiera un sistema efectivamente descrito donde todas las funciones recursivas fueran representables de tal manera que pueda certificar sintácticamente que una expresión es una representación honesta de un función recursiva (por ejemplo, comprobando que está correctamente escrita en el sistema), obtendría una función recursiva total universal, que es imposible.

Emil Jeřábek apoya a Monica el

Por supuesto, una respuesta clásica a este tipo de preguntas podría ser: cálculo de

con tipos de intersección , ya que escribe todos (y solo aquellos) términos que se están normalizando fuertemente. Sin embargo, es más una pregunta filosófica preguntar si el cálculo admite o no una "interpretación de Curry-Howard".

λ

$\lambda$

cody

Es difícil ser más preciso aquí porque la pregunta no es precisa.

Andrej Bauer

Respuestas:

Muy bien, le diré algo: en general, para un sistema de tipo dado , lo siguiente es cierto: $T$

Si todos los términos de tipo de pozo en el cálculo están normalizando, entonces es consistente cuando se ve como una lógica. $T$ $T$

La prueba generalmente procede asumiendo que tiene un término de tipo , utilizando la reducción de sujeto para obtener una forma normal, y luego procediendo por inducción en la estructura de dicho término para obtener una contradicción. $\mathrm{absurd}$ $\mathrm{False}$

Es natural preguntarse si lo contrario es válido, es decir

Para cualquier sistema de tipo , si es lógicamente consistente , entonces cada término bien tipado en está normalizando. $T$ $T$ $T$

El problema con esto es que no existe una noción real más general de "sistema de tipos", y aún menos acuerdo sobre el significado de consistencia lógica para tales sistemas. Sin embargo, podemos verificar empíricamente que

Para los sistemas de tipos más conocidos que tienen una interpretación lógica, lo contrario es válido.

¿Cómo se relaciona esto con la integridad de Turing? Bueno, por un lado, si la verificación de tipo es decidible , entonces el argumento de Andrej muestra que uno de los siguientes debe ser válido:

El conjunto de todos los programas bien escritos no es Turing Complete.
Hay un programa bien escrito que no termina.

Esto tiende a sugerir que:

Los sistemas de tipos que tienen una interpretación lógica y son consistentes y recursivamente enumerables no son Turing Complete.

Dar un teorema real en lugar de una sugerencia requiere hacer que la noción de sistemas de tipos e interpretaciones lógicas sea matemáticamente precisa.

Ahora me vienen a la mente dos comentarios:

Hay un sistema de tipos indecidible , el sistema de tipos de intersección que tiene una interpretación lógica y puede representar cada término normalizador . Como observa, esto no es lo mismo que ser Turing completo, ya que el tipo de una función total puede necesitar actualizarse (refinarse, de hecho) antes de aplicarlo al argumento deseado. El cálculo es un cálculo de "estilo curry" y es igual a STLC + $\lambda$ y
$\frac{Γ ⊢ M : τ Γ ⊢ M : σ}{Γ ⊢ M : τ \cap σ}$ $\frac{\Gamma\vdash M:\tau\quad \Gamma\vdash M:\sigma}{\Gamma\vdash M:\tau\cap\sigma}$ Está claro que la "interpretación"conduce a una interpretación lógica consistente. $\frac{Γ ⊢ M : τ \cap σ}{Γ ⊢ M : τ} \frac{Γ ⊢ M : τ \cap σ}{Γ ⊢ M : σ}$ $\frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\tau}\quad \frac{\Gamma\vdash M:\tau\cap\sigma}{\Gamma\vdash M:\sigma}$ $\cap=\wedge$
Hay una clase de sistemas de tipos, los Sistemas de Tipos Puros , en los que tal pregunta podría hacerse precisa. En este marco, sin embargo, la interpretación lógica es menos clara. Uno podría estar tentado a decir: "un PTS es consistente si tiene un tipo deshabitado". Pero esto no funciona, ya que los tipos pueden vivir en diferentes "universos", donde algunos pueden ser consistentes y otros no. Coquand y Herbelin definen una noción de sistemas lógicos de tipo puro , en la que la pregunta tiene sentido y muestran

Cada LPTS inconsistente y no dependiente tiene un combinador de bucles (y también lo está Turing Complete)

Lo que responde a la pregunta en una dirección (inconsistente TC) en este caso. Hasta donde sé, la pregunta para LPTS general todavía está abierta y es bastante difícil. $\Rightarrow$

Editar: ¡ Lo contrario del resultado Coquand-Herbelin no es tan fácil como pensaba! Esto es lo que se me ocurrió hasta ahora.

Un sistema lógico de tipo puro es un PTS con (al menos) los tipos y , (al menos) el axioma y (al menos) la regla , con el requisito adicional de que no hay ningún tipo de tipo . $\mathrm{Prop}$ $\mathrm{Type}$ $\mathrm{Prop}:\mathrm{Type}$ $(\mathrm{Prop},\mathrm{Prop},\mathrm{Prop})$ $\mathrm{Prop}$

Ahora voy a asumir una declaración particular de integridad de Turing: arreglar un LPTS y dejar que sea el contexto $L$ $\Gamma$

Γ = n a t : P r o p, 0 : n a t, S : n a t \to n a t

$\Gamma = \mathrm{nat}:\mathrm{Prop},\ 0:\mathrm{nat},\ S:\mathrm{nat}\rightarrow \mathrm{nat}$

esTuring Completoiff para cada función computable total hay un término tal que y para cada $L$ $f:\mathbb{N}\rightarrow\mathbb{N}$ $t_f$

Γ ⊢ t_{f} : n a t \to n a t

$\Gamma \vdash t_f : \mathrm{nat}\rightarrow \mathrm{nat}$

n \in N

$n\in\mathbb{N}$

t_{f} (S^{n} 0) \to_{β}^{*} S^{f (n)} 0

$t_f\ (S^n\ 0)\rightarrow^*_{\beta} S^{f(n)}\ 0$

Ahora, el argumento de diagonalización de Andrej muestra que hay no terminantes de tipo . $t$ $\mathrm{nat}$

¡Ahora parece que estamos a medio camino! Dado un término que no termina , queremos reemplazar las ocurrencias de por algún tipo genérico y deshacernos de y en , y tendremos nuestra inconsistencia ( está habitada en el contexto )! $\Gamma \vdash \mathrm{loop}:\mathrm{nat}$ $\mathrm{nat}$ $A$ $0$ $S$ $\Gamma$ $A$ $A:\mathrm{Prop}$

Desafortunadamente, aquí es donde me quedo atascado, ya que es fácil reemplazar por la identidad, pero el es mucho más difícil de eliminar. Idealmente, nos gustaría usar algún teorema de recursión de Kleene, pero aún no lo he descubierto. $S$ $0$

cody
fuente

Bien, entonces las dos primeras aclaraciones sobre su comentario (1). ¿Qué quiere decir cuando dice que este sistema de tipos de intersección no es recursivamente enumerable? Ciertamente, el conjunto de teoremas del sistema es re, porque lo has dado como un cálculo secuencial directo. Además, el resultado que veo probado en el documento que vinculó es que los términos que se pueden escribir en el sistema son exactamente los términos fuertemente normalizadores; ¿Pero no es tan diferente de decir que puede escribir exactamente las funciones computables totales? Por ejemplo, no es

fuertemente normalizado, pero no total?

λ x . x x

$\lambda x. xx$

Morgan Thomas

Ahora una pregunta sobre su comentario (2). Me parece que el teorema que usted cita no es lo que nos interesa. Dice que para cada LPTS no dependiente, si es inconsistente, entonces es Turing completo. Pero nos gustaría saber si para cada LPTS, si es Turing completo, entonces es inconsistente. ¿Estoy malinterpretando algo aquí?

Morgan Thomas

Γ, t, A

$\Gamma, t, A$

Γ ⊢ t : A

$\Gamma\vdash t:A$

El segundo punto: también tiene razón en que uno puede tener una función no total que está bien tipada (aunque no necesariamente se puede aplicar a un argumento dado). Enmendaré la respuesta.

cody

Tercer punto Estás en lo correcto otra vez! Sin embargo, lo contrario (en el caso especial de LPTS) es bastante trivial. Voy a esbozar el argumento.

cody

$\beta$

$\lambda$ $\text{nat}, 0, S$

⊢ nat : *

$\vdash \text{nat} : \ast$

⊢ 0 : nat

$\vdash 0 : \text{nat}$

⊢ S : nat \to nat

$\vdash S : \text{nat} \to \text{nat}$

$e$ $f_e$ $f_e : \text{nat} \to \text{nat}$ $e,x \in \mathbb{N}$ $\beta$

f_{e} (x) \to_{β} Φ_{e} (x),

$f_e(x) \to_\beta \Phi_e(x),$

$\Phi_e(x)$ $e$ $x$ $\Phi_e(x)$ $\beta$ $\beta$

Ahora, esta teoría es claramente completa en un sentido aproximado de @ cody, solo por la fuerza bruta; pero la afirmación es que también es consistente. Construyamos un modelo de ello.

$U_1 \in U_2 \in U_3$

$\emptyset, \mathbb{N}, 0, S \in U_1$ $S$
$a \in b \in U_i$ $a \in U_i$
$A, B \in U_i$ $B^A \in U_i$
$A \in U_i$ $f : A \to U_i$ $\prod_{a \in A} f(a) \in U_i$

$U_i$

$v$ $U_2$ $v$ $I_v$

$I_v(x) = v(x)$ $x$
$I_v(\ast) = U_1, I_v(\Box) = U_2$
$I_v(\text{nat}) = \mathbb{N}, I_v(0) = 0, I_v(S) = S$
$I_v(f_e) = \Phi_e$ $\mathbb{N} \to \mathbb{N}$ $e$
$I_v(AB) = I_v(A)(I_v(B))$ $I_v(A)$ $I_v(B)$ $I_v(AB) = 0$
$I_v(\lambda x : A. B)$ $a \in I_v(A)$ $I_{v[x:=a]}(B)$
$I_v(\Pi x : A. B) = \prod_{a \in I_v(A)} I_{v[x:=a]}(B)$

Tenemos eso para todos los términos , $A$ $I_v(A) \in U_3$ $v$ $A : B$ $v \models A : B$ $I_v(A) \in I_v(B)$ $\Gamma \models A : B$ $v$ $v \models x : C$ $(x : C) \in \Gamma$ $v \models A : B$

$\Gamma \vdash A : B$ $\Gamma \models A : B$ $x,y$ $y : \ast \models x : y$ $y$ $\emptyset$

$\beta$

Morgan Thomas
fuente

A

$A$

f_{e} (x) \to Φ_{e} (x)

$f_e(x)\rightarrow \Phi_e(x)$ $\iota$

β

$\beta$

β

$\beta$

f_{e} (x)

$f_e(x)$

ι

$\iota$

β

$\beta$

Creo que tienes razón. Este no es mi campo, así que soy un poco torpe haciendo cosas. :-) Creo que su prueba funciona, y una consecuencia interesante, si tengo razón, es que esta teoría no tiene mucha fuerza de consistencia. Parece una teoría potencialmente muy poderosa, ya que tiene tipos y números naturales, que deberían permitirle interpretar la teoría de conjuntos; pero aparentemente no puedes, ¡porque puedes demostrar que es consistente sin usar la poderosa teoría de conjuntos!

Morgan Thomas