¿Explicación simple de por qué ciertas funciones computables no pueden ser representadas por un término escrito?

8

Al leer el documento Una Introducción al Cálculo Lambda , me encontré con un párrafo que realmente no entendía, en la página 34 (mi cursiva):

Dentro de cada uno de los dos paradigmas hay varias versiones de cálculo lambda mecanografiado. En muchos sistemas importantes, especialmente aquellos a la Iglesia, los términos que tienen un tipo siempre poseen una forma normal. Por la insolubilidad del problema de detención, esto implica que no todas las funciones computables pueden ser representadas por un término mecanografiado, ver Barendregt (1990), Teorema 4.2.15. Esto no es tan malo como parece, porque para encontrar funciones computables que no puedan representarse, uno tiene que pararse sobre la cabeza. Por ejemplo, en 2, el cálculo de lambda tipificado de segundo orden, solo aquellas funciones recursivas parciales no pueden representarse como sumas totales, pero no de manera demostrable en el análisis matemático (aritmética de segundo orden).

Estoy familiarizado con la mayoría de estos conceptos, pero no el concepto de una función recursiva parcial, ni el concepto de una función demostrablemente total. Sin embargo, esto no es lo que me interesa aprender.

Estoy buscando una explicación simple de por qué ciertas funciones computables no pueden ser representadas por un término tipeado, así como por qué tales funciones solo se pueden encontrar 'de pie sobre la cabeza'.

magnetar
fuente

Respuestas:

9

Dado que no desea aprender conceptos precisos, aquí hay una explicación intuitiva. En la discusión a continuación, "función" siempre se refiere a una función que asigna números naturales a números naturales (posiblemente no definidos en algunos argumentos).

Cualquier lenguaje de programación que tenga

  1. sintaxis computable y reglas de evaluación, y
  2. implementa cada función computable total

necesariamente implementa algunas funciones parciales .

Para ver esto, supongamos que todas las funciones definibles en este lenguaje fueran totales. Debido a que el lenguaje tiene una sintaxis computable, podemos enumerar todas las definiciones de funciones (solo enumere todas las cadenas y filtre las que causan errores sintácticos). Debido a que las reglas de evaluación son computables, la segunda suposición nos permite concluir que en nuestro lenguaje podemos definir la función total eval(n,m)que evalúa la nenésima función definible m(esencialmente este es un mini-intérprete escrito en el lenguaje mismo). Pero entonces la función

λ k . (1 + eval(k,k))

es una función definible total que es diferente de cada función definible total, una contradicción.

El cálculo simplemente escrito satisface la primera condición y define solo funciones totales. Por lo tanto, no cumple la segunda condición.λ

En lo que respecta a "pararse sobre su cabeza", para un cálculo de fuertemente normalizado es bastante fácil proporcionar una función total que no es definible en el cálculo, es decir, el procedimiento de normalización en sí mismo. No es muy importante cuán elegante sea su cálculo fuertemente normalizador, podría ser el cálculo polimórfico , o la teoría del tipo Martin-Lof, o el cálculo de las construcciones. (Ejercicio: si pudiera implementar el procedimiento de normalización, podría implementar más arriba).λλeval

Andrej Bauer
fuente
Me temo que no puedo analizar su segunda oración explicativa: ¿Cualquier lenguaje de programación con 1. y 2. verifica qué? Asumo que quería decir que no puede existir ningún tipo de lenguaje ...
Cody
Lo siento, estropeé el texto. Debería leer bien ahora.
Andrej Bauer
Genial, no pensé en esto. Vea aquí los antecedentes de esta respuesta.
Raphael
4

Creo que la respuesta de Merijn maneja la primera parte de su pregunta bastante bien. Trataré de responder la segunda parte: por qué encontrar funciones que son computables pero no representables en el cálculo polimórfico requiere "pararse sobre la cabeza".λ

Me temo que requiere una explicación de los conceptos que no le interesan. Una función recusiva parcial es un -term que representa una función de a . A -term aplica al representante de un número natural es enviado a si y sólo si qué no tener una forma normal. Si no se envía ningún número a , decimos que la función es total . Ahora la idea es que ninguna teoría lógica puede probar que un términoλNN{}λtnt nTtrepresenta una función total para cada función total , siempre hay "puntos ciegos" donde termina en todas las entradas , pero la instrucciónttn

n,t n terminates

es indecidible en . Si la afirmación anterior es demostrable en , decimos que la función representada por es demostrablemente total . Eso no todas las funciones totales son demostrablemente total en el es una consecuencia de (una variante de) la Godel incompletitud teorema para .TTtTT

Ahora el punto es que el programa de gran mayoría que deseamos escribir concretamente (clasificación de listas, recorrido de gráficos, sistemas operativos) no son solo funciones totales, sino que son demostrablemente totales en sistemas lógicos razonables, como Peano Arithmetic.

Ahora para el cálculo polimórfico . Se puede demostrar que los términos que se pueden escribir en este cálculo son exactamente los términos que representan las funciones demostrablemente totales en la aritmética de Peano de segundo orden. La aritmética de Peano de segundo orden es mucho, mucho más poderosa que la aritmética de Peano ordinaria.λ

Esto significa por las explicaciones anteriores que hay términos que son totales pero no demostrablemente totales, pero tales funciones son extremadamente raras, ya que ya son raras para la Aritmética de Peano (y mucho más raras en la teoría del segundo orden). De ahí la declaración de "pararse de cabeza".

cody
fuente
2
Le faltan condiciones en su teoría , es decir, la coherencia y que el conjunto de axiomas es recursivo, de lo contrario podemos tomar como una teoría cuyo conjunto de axiomas incluye " termina" para cada que termina. TTff
Andrej Bauer
Gracias por esas precisiones, Andrej. Una explicación más completa probablemente también detallaría lo que requerimos de nuestra teoría, a saber, que la teoría al menos puede expresar lo que significa terminar (la aritmética con multiplicación es suficiente, pero tiendo a favorecer sistemas un poco más expresivos).
cody
Bien, creo que es justo señalar que faltan algunas condiciones técnicas, por lo que los lectores interesados ​​pueden ir a buscarlas.
Andrej Bauer
3

Me resulta un poco difícil escribir de forma concisa la prueba, pero espero que esta explicación le brinde suficiente intuición para ver por qué los términos simples escritos no pueden representar todos los términos sin tipo.

El cálculo lambda simplemente tipado se está normalizando fuertemente. Cada reducción nos acercará a la forma normal. Cuando la función se aplica a un valor de tipo , reducirá a una función de tipo . Dado un número finito de argumentos, se necesita un número finito de pasos de reducción para alcanzar la forma -normal, en la que no hay más reducciones posibles.βf::αβγαββγβ

Para contrastar esto con el cálculo lambda sin tipo. Uno de los combinadores UTLC más famosos es el combinador :Y

Y=λf.(λx.f(xx))(λx.f(xx))

Cuando intentamos reducir el combinador sucede lo siguiente:Y

λf.(λx.f(xx))(λx.f(xx))g
(λx.g(xx))(λx.g(xx))
g((λx.g(xx))(λx.g(xx)))
g(g((λx.g(xx))(λx.g(xx))))

¡No importa qué funciones pasemos, nos quedamos atrapados en una secuencia infinita de reducciones! Si intentamos anclar un tipo STLC en el combinador UTLC, rápidamente lo encontramos imposible, porque la aplicación de función no reduce el tipo como se requiere en el STLC. El combinador es claramente computable (representa, usando la recursividad, el concepto de un bucle infinito), sin embargo, no puede representarse en el STLC, ya que todos los términos de STLC se están normalizando fuertemente.YY

Merijn
fuente
Este argumento tiene muy poco que ver con el hecho de que no todas las funciones teóricas de los números totales son representables en el tipo cálculo, que es de lo que se trata la pregunta. ¿En qué sentido el combinador una función total? λY
Andrej Bauer
@AndrejBauer La pregunta termina con "Estoy buscando una explicación simple de por qué ciertas funciones computables no pueden ser representadas por un término escrito". ¿Cómo mi respuesta no cubre esto? El combinador es un ejemplo de una función computable que no puede ser representada por un término simplemente tipado, y espero que mi explicación sea lo suficientemente coherente como para explicar por qué no puede representarse por un término simplemente tipado. Y
merijn
Bueno, si va a interpretar la pregunta como si pidiera un ejemplo de una función parcial que no se puede definir en el cálculo simple de , entonces cualquier función servirá (y la pregunta no tiene sentido). Por ejemplo, el que no está definido en todas partes. Tampoco es definible en el cálculo simple de . La pregunta es sobre las funciones totales, tal como lo leí. λλ
Andrej Bauer