Formulação equivalente da teoria da complexidade no Lambda Calculus?

Na teoria da complexidade, a definição de complexidade do tempo e do espaço faz referência a uma máquina universal de Turing: resp. o número de etapas antes de parar e o número de células na fita tocadas.

Dada a tese de Church-Turing, também deve ser possível definir a complexidade em termos de cálculo lambda.

Minha noção intuitiva é que a complexidade do tempo pode ser expressa como o número de reduções β (podemos definir a conversão α ausente usando os índices De Brujin e η é apenas uma redução de qualquer maneira), enquanto a complexidade do espaço pode ser definida como o número de símbolos (λ, índices DB, símbolos "aplicar") na maior redução.

Isso está correto? Se sim, onde posso obter uma referência? Se não, como estou enganado?

Como você aponta, o cálculo λ tem uma noção aparentemente simples de complexidade de tempo: basta contar o número de etapas de redução β. Infelizmente, as coisas não são simples. Devemos perguntar:

 Is counting β-reduction steps a good complexity measure?

$M$$|M|$$M$$poly(|M|)$$tr(M)$$poly(|tr(M)|)$

Durante muito tempo, não ficou claro se isso pode ser alcançado no cálculo λ. Os principais problemas são os seguintes.

• Existem termos que produzem formas normais em um número polinomial de etapas com tamanho exponencial. Veja (1). Mesmo anotando os formulários normais leva tempo exponencial.

• A estratégia de redução escolhida também desempenha um papel importante. Por exemplo, existe uma família de termos que reduz em um número polinomial de etapas β paralelas (no sentido de redução λ ideal (2), mas cuja complexidade é não elementar (3, 4).

O artigo (1) esclarece a questão, mostrando uma codificação razoável que preserva a classe de complexidade PTIME, assumindo reduções de chamada por nome mais à esquerda e mais à esquerda. O insight principal parece ser que a explosão exponencial só pode acontecer por razões desinteressantes que podem ser derrotadas pelo compartilhamento adequado de sub-termos.

Observe que artigos como (1) mostram que classes de complexidade grossa como PTIME coincidem, independentemente de você contar as etapas β ou as etapas da máquina de Turing. Isso não significa que classes de menor complexidade, como O (log n), também coincidam. É claro que essas classes de complexidade também não são estáveis ​​sob a variação do modelo da máquina de Turing (por exemplo, 1 fita versus fita múltipla).

D. O trabalho de Mazza (5) prova o teorema de Cook-Levin (𝖭𝖯-completude do SAT) usando uma linguagem funcional (uma variante do cálculo-λ) em vez de máquinas de Turing. O principal insight é o seguinte:

$$\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine $\lambda$-terms}}{\text{$\lambda$-terms}}$$

Não sei se a situação relativa à complexidade do espaço é compreendida.

---

1. B. Accattoli, U. Dal Lago, redução beta é invariante, de fato .

2. J.-J. Impostos, Reduções corretas e ótimas no cálculo lambda.

3. JL Lawall, HG Mairson, Optimalidade e ineficiência: o que não é um modelo de custo do cálculo lambda ?

4. A. Asperti, H. Mairson, a redução beta paralela não é recursiva elementar .

5. D. Mazza, Igreja Encontra Cook e Levin .

$\beta$$\lambda$

$\mathsf L$$\mathsf P$$M\to^\ast N$$M$

$\beta$