¿Pueden los cálculos lambda escritos expresar * todos * los algoritmos por debajo de una complejidad dada?

Sé que la complejidad de la mayoría de las variedades de cálculos lambda mecanografiados sin la primitiva combinatoria Y está limitada, es decir, solo se pueden expresar funciones de complejidad limitada, con el límite cada vez mayor a medida que crece la expresividad del sistema de tipos. Recuerdo que, por ejemplo, el cálculo de construcciones puede expresar como máximo una complejidad doblemente exponencial.

Mi pregunta se refiere a si los cálculos lambda mecanografiados pueden expresar todos los algoritmos por debajo de un límite de complejidad determinado, o solo algunos Por ejemplo, ¿hay algún algoritmo de tiempo exponencial que no sea expresable por ningún formalismo en el Lambda Cube? ¿Cuál es la "forma" del espacio de complejidad que está completamente cubierto por diferentes vértices del Cubo?

Daré una respuesta parcial, espero que otros llenen los espacios en blanco.

En mecanografiada -calculi, se puede dar un tipo a las representaciones habituales de datos ( N un t para Church (unarios) números enteros, S t r para cadenas binarias, B o o l para Booleanos) y preguntarse qué es la complejidad de las funciones / problemas representables / decidibles por términos escritos. Conozco una respuesta precisa solo en algunos casos, y en el caso simplemente mecanografiado depende de la convención utilizada al definir "representable / decidible". De todos modos, no sé de ningún caso en el que haya un límite superior doblemente exponencial.$\lambda$$\mathsf{Nat}$$\mathsf{Str}$$\mathsf{Bool}$

Primero, un breve resumen del Cubo Lambda. Sus 8 cálculos se obtienen habilitando o deshabilitando los siguientes 3 tipos de dependencias además del cálculo simplemente tipado (STLC):$\lambda$

• polimorfismo : los términos pueden depender de los tipos;
• tipos dependientes : los tipos pueden depender de los términos;
• orden superior : los tipos pueden depender de los tipos.

(La dependencia de los términos en los términos siempre está ahí).

Adición de polimorfismo rendimientos Sistema F. Aquí, puede escribir los números enteros iglesia con , y de manera similar para cadenas binarias y booleanos. Girard demostró que los términos del Sistema F de tipo N a t → N a t representan exactamente las funciones numéricas cuya totalidad es demostrable en aritmética de Peano de segundo orden. Eso es casi matemática cotidiana (aunque sin ninguna forma de elección), por lo que la clase es enorme, la función de Ackermann es una especie de microbio diminuto, y mucho menos la función 2 $\mathsf{Nat}:=\forall X.(X\rightarrow X)\rightarrow X\rightarrow X$$\mathsf{Nat}\rightarrow\mathsf{Nat}$ . No conozco ninguna función numérica "natural" que no pueda representarse en el Sistema F. Los ejemplos generalmente se construyen por diagonalización, o codifican la consistencia de PA de segundo orden u otros trucos autorreferenciales (como decidir laigualdadβdentro del Sistema F en sí). Por supuesto, en el Sistema F puede convertir entre enteros unariosNaty su representación binariaStr, y luego probar, por ejemplo, si el primer bit es 1, por lo que la clase de problemas decidibles (por términos de tipoStr→Bool) es igualmente enorme.$2^{2^n}$$\beta$$\mathsf{Nat}$$\mathsf{Str}$$\mathsf{Str}\rightarrow\mathsf{Bool}$

Los otros 3 cálculos del Cubo Lambda que incluyen el polimorfismo son, por lo tanto, al menos tan expresivos como el Sistema F. Estos incluyen el Sistema F ω (polimorfismo + orden superior), que puede expresar exactamente las funciones probables totales en el orden superior PA, y el cálculo de Construcciones (CoC), que es el cálculo más expresivo del Cubo (todas las dependencias están habilitadas). No conozco una caracterización de la expresividad del CoC en términos de teorías aritméticas o teorías de conjuntos, pero debe ser bastante aterrador :-)$_\omega$

Soy mucho más ignorante con respecto a los cálculos obtenidos al habilitar tipos dependientes (esencialmente la teoría de tipos de Martin-Löf sin igualdad y números naturales), tipos de orden superior o ambos. En estos cálculos, los tipos son poderosos, pero los términos no pueden acceder a este poder, por lo que no sé lo que obtienes. Computacionalmente, no creo que obtengas mucha más expresividad que con los tipos simples, pero puedo estar equivocado.

Entonces nos quedamos con el STLC. Hasta donde yo sé, este es el único cálculo del Cubo con límites superiores de complejidad interesantes (es decir, no monstruosamente grandes). Hay una pregunta sin respuesta sobre esto en TCS.SE, y de hecho la situación es un poco sutil.

Primero, si fija un átomo y define N a t : = ( X → X ) → X → X , existe el resultado de Schwichtenberg A ] → N a t con A arbitrario, se puede representar mucho más. Por ejemplo, cualquier torre de exponenciales (por lo que puede ir mucho más allá de doblemente exponencial), así como la función predecesora, pero aún así no hay resta (si considera las funciones binarias y trata de escribirlas con N a t$X$$\mathsf{Nat}:=(X\rightarrow X)\rightarrow X\rightarrow X$ (sé que hay una traducción al inglés de ese documento en algún lugar de la web, pero no puedo encontrarlo ahora) que le dice que las funciones de tipo son exactamente los polinomios extendidos (con if-then-else). Si permite alguna "holgura", es decir, permite que el parámetro X se instancia a voluntad y considere los términos de tipo N a t$\mathsf{Nat}\rightarrow\mathsf{Nat}$$X$$\mathsf{Nat}[A]\rightarrow\mathsf{Nat}$$A$ ). Entonces, la clase de funciones numéricas representables en el STLC es un poco extraña, es un subconjunto estricto de las funciones elementales pero no corresponde a nada bien conocido.$\mathsf{Nat}[A]\rightarrow\mathsf{Nat}[A']\rightarrow\mathsf{Nat}$

En aparente contradicción con lo anterior, hay un artículo de Mairson que muestra cómo codificar la función de transición de una máquina Turing arbitraria , de la que se obtiene un término de tipo N a t [ A ] → B o o l (para algún tipo A dependiendo de M ) que, dado un entero de Iglesia n como entrada, simula la ejecución de M a partir de una configuración inicial fija para varios pasos de la forma 2 2 ⋮ 2 n$M$$\mathsf{Nat}[A]\rightarrow\mathsf{Bool}$$A$$M$$n$$M$

De hecho, el STLC es extremadamente débil en lo que puede decidir "uniformemente". Llamemos la clase de idiomas decidible por términos simplemente mecanografiadas de tipo S t r [ A ] → B O O l por alguna Un (como el anterior, se permite arbitraria "holgura" en la tipificación). Hasta donde yo sé, una caracterización precisa de C S $\mathcal C_{ST}$$\mathsf{Str}[A]\rightarrow\mathsf{Bool}$$A$$\mathcal C_{ST}$ faltaSin embargo, sabemos que $\mathcal C_{ST}\subsetneq\mathrm{LINTIME}$(tiempo lineal determinista). Tanto la contención como el hecho de que es estricto pueden demostrarse mediante argumentos semánticos muy claros (utilizando la semántica denotativa estándar del STLC en la categoría de conjuntos finitos). El primero fue mostrado recientemente por Terui . Este último es esencialmente una reformulación de los viejos resultados de Statman. Un ejemplo de problema en es MAYORIDAD (dada una cadena binaria, indique si contiene estrictamente más 1s que 0s).$\mathrm{LINTIME}\setminus\mathcal C_{ST}$

(Mucho) más tarde complemento: Me acabo de enterar de que la clase que llamo anteriormente en realidad no tienen una caracterización precisa, que además es extremadamente simple. En este hermoso artículo de 1996 , Hillebrand y Kanellakis demuestran, entre otras cosas, que$\mathcal C_{ST}$

Teorema. (los idiomas regulares en { 0 , 1 } ).$\mathcal C_{ST}=\mathsf{REG}$$\{0,1\}$

(Este es el Teorema 3.4 en su artículo).

Esto me resulta doblemente sorprendente: estoy sorprendido por el resultado en sí mismo (nunca se me ocurrió que podría corresponder a algo tan "ordenado") y por lo poco que se sabe. También es divertido que la prueba de Terui de la L I N T $\mathcal C_{ST}$límite superior M E utilice los mismos métodos empleados por Hillebrand y Kanellakis (interpretando el cálculo λ de tiposimple en la categoría de conjuntos finitos). En otras palabras, Terui (y yo) podría haber redescubierto fácilmente este resultado si no fuera por el hecho de que de alguna manera estábamos contentos con que C S T fuera una clase "extraña" :-)$\mathrm{LINTIME}$$\lambda$$\mathcal C_{ST}$

(Por cierto, compartí mi sorpresa en esta respuesta a una pregunta de MO sobre "teoremas desconocidos").

Una respuesta a una pregunta que Damiano planteó en su excelente respuesta:

Soy mucho más ignorante con respecto a los cálculos obtenidos al habilitar tipos dependientes (esencialmente la teoría de tipos de Martin-Löf sin igualdad y números naturales), tipos de orden superior o ambos. En estos cálculos, los tipos son poderosos, pero los términos no pueden acceder a este poder, por lo que no sé lo que obtienes.

Agregar tipos dependientes no cambia la fuerza de consistencia de la teoría. Los tipos dependientes simples tienen la misma fuerza de consistencia que la lambda de tipo simple, y el cálculo de las construcciones tiene la misma fuerza de consistencia que el Sistema F .$_\omega$

De hecho, la teoría pura del tipo Martin-Löf ( en el cubo lambda) no puede probar que 0 = 1 implica falso. Para hacer esto, necesita al menos un universo, y los universos aumentan enormemente la fuerza de la teoría. El cálculo de las construcciones inductivas (en términos generales,$\lambda{P}$ más tipos inductivos más innumerables universos) es igual en fuerza de consistencia a ZFC con innumerables cardinales inaccesibles.$\lambda{P}\omega$

No sé cuál es la fuerza del cálculo impredecible de las construcciones, si agrega tipos inductivos y grandes eliminaciones.

Intentaré complementar la excelente respuesta de Damiano.

$\lambda$$F$ $\mathrm{HA}_2$

$\cal{T}$$\cal{L}$$\cal{T}$$\cal{L}$ .

$\cal{L}$

• $F$$\mathrm{HA}_2$ (esto incluye la función de Ackermann y funciones de crecimiento mucho, mucho más rápido)

• $T$$\mathrm{PA}$$F$ )!

$\lambda$$\mathrm{PTIME}$Baillot y Terui .

En general, esta es una gran vía de investigación, por lo que solo me referiré a una de mis respuestas anteriores .