¿Usa el cálculo lambda para derivar la complejidad del tiempo?

¿Hay algún beneficio en el cálculo de la complejidad temporal de un algoritmo que utiliza cálculo lambda? ¿O hay otro sistema diseñado para este propósito?

Cualquier referencia sería apreciada.

Ohad tiene toda la razón sobre los problemas que enfrenta el cálculo lambda como base para hablar sobre las clases de complejidad. Se ha trabajado bastante para caracterizar la complejidad de la reducibilidad en el cálculo lambda, particularmente en torno al trabajo sobre reducciones etiquetadas y óptimas de la tesis doctoral de Lèvy. En términos generales, los modelos de buen costo para el cálculo lambda no deberían asignar un peso constante a todas las reducciones beta: intuitivamente, sustituir un gran subterráneo en muchos lugares con diferentes alcances debería costar más que contratar una pequeña K redex, y si uno quiere una cierta cantidad de la invariabilidad del costo bajo diferentes estrategias de reescritura, esto se vuelve esencial.

Dos enlaces:

1. Lawall y Mairson, 1996, Optimalidad e ineficiencia: ¿qué no es un modelo de costo del cálculo lambda? (.ps.gz) - Encuesta seminal de cuestiones relacionadas con la elección del modelo de costos, y por qué muchas ideas plausibles no funcionan.
2. Dal Lago & Martini, 2008, El cálculo lambda débil como una máquina razonable : ofrece un modelo de costo para el cálculo lambda basado en el valor, junto con una buena discusión de la literatura.

$\lambda$$\lambda$

Para algo más cercano a su pregunta, hay un proyecto actual que desarrolla y estudia un sistema de tipos (un lenguaje de programación funcional) que mediante análisis estático puede determinar los límites de tiempo de ejecución (polinómicos) de los programas (así como otros recursos utilizados por programas). Entonces, en cierto sentido, esto podría indicar que podría haber alguna ventaja en el uso de la programación funcional para analizar la complejidad del tiempo de ejecución. La página de inicio del proyecto está aquí .

Un posible documento representativo de este proyecto es: Jan Hoffmann, Martin Hofmann. Análisis de recursos amortizados con potencial polinómico: una inferencia estática de límites polinómicos para programas funcionales. En Actas del XIX Simposio europeo sobre programación (ESOP'10). enlazar

$\lambda$$\lambda$

$\lambda$

http://arxiv.org/abs/1405.3311

Existe una línea de trabajo muy interesante basada en la lógica lineal, llamada teoría de la complejidad implícita, que caracteriza varias clases de complejidad al imponer varias disciplinas tipo en el cálculo lambda. IIRC, este trabajo comenzó cuando Bellantoni y Cook, y Leivant descubrieron cómo usar el sistema de tipos para vincular la recursividad primitiva para capturar varias clases de complejidad.

En general, la atracción de trabajar con cálculos lambda es que a veces es posible encontrar caracterizaciones más extensionales (es decir, más manejables matemáticamente) de varias características intensionales que dan poder a modelos como las máquinas de Turing. Por ejemplo, una diferencia entre las máquinas de Turing y el cálculo lambda puro es que, dado que Turing recibe códigos de programas, un cliente puede implementar manualmente tiempos de espera, implementar cola de milano y, por lo tanto, puede calcular paralelo o. Sin embargo, los tiempos de espera también se pueden modelar métricamente, y Escardo ha conjeturado (no sé su estado) que los modelos de espacio métrico del cálculo lambda son completamente abstractos para los tiempos de espera de PCF +. Los espacios métricos son objetos matemáticos muy bien estudiados, y es muy agradable poder hacer uso de ese cuerpo de teoría.

Sin embargo, la dificultad de usar el cálculo lambda es que te obliga a enfrentar fenómenos de orden superior directamente desde la puerta de inicio. Esto puede ser muy sutil, ya que la tesis de Church-Turing falla en el tipo superior: los modelos naturales de cómputo difieren en el tipo superior, ya que difieren en lo que se le permite hacer con las representaciones de los cálculos. (Paralelo o es un ejemplo simple de este fenómeno, ya que exhibe una diferencia entre LC y TM). Además, ni siquiera hay una inclusión estricta entre los diferentes modelos, ya que la contravarianza del espacio funcional significa que el poder más expresivo en un orden implica menos poder expresivo un orden más alto.

Hasta donde sé, el cálculo lambda no es adecuado para este propósito, ya que la noción de complejidad de tiempo / espacio es difícil de formular en el cálculo lambda.

¿Qué es 1 unidad de complejidad de tiempo? ¿Una reducción beta? ¿Qué pasa con las unidades de complejidad espacial? La longitud de la cuerda?

El cálculo Lambda es más adecuado para la manipulación abstracta de algoritmos, ya que es mucho más fácil de componer que las máquinas de Turing.

También puede buscar cálculos de sustituciones explícitas que dividen la sustitución a nivel meta del cálculo lambda en una serie de pasos de reducción explícitos. Esto toca el punto de Charles de que todas las sustituciones no deben considerarse iguales cuando se considera la complejidad del tiempo.

Ver Nils Anders Danielsson, Análisis de complejidad de tiempo semiformal ligero para estructuras de datos puramente funcionales que se implementa como una biblioteca en Agda. Las citas dadas en el documento también parecen muy prometedoras.

Una conclusión clave para mí es que es apropiado / útil / razonable / semiautomatizable deducir la complejidad temporal de los algoritmos en el cálculo lambda simplemente tipado, especialmente si esos algoritmos son fácilmente expresables en él (es decir, puramente funcionales) y muy especialmente si esos Los algoritmos hacen un uso esencial de, por ejemplo, la semántica de llamada por nombre. Junto con esto está el punto probablemente obvio de que uno no calcula la complejidad solo "en el cálculo lambda" sino en el cálculo lambda bajo una estrategia de evaluación dada.