Formulation équivalente de la théorie de la complexité dans Lambda Calculus?

Dans la théorie de la complexité, la définition de la complexité du temps et de l'espace fait référence à une machine de Turing universelle: resp. le nombre d'étapes avant de s'arrêter et le nombre de cellules sur la bande touchées.

Compte tenu de la thèse de Church-Turing, il devrait également être possible de définir la complexité en termes de calcul lambda.

Ma notion intuitive est que la complexité temporelle peut être exprimée comme le nombre de β-réductions (nous pouvons définir l'écart α-conversion en utilisant les indices De Brujin, et η est à peine une réduction de toute façon), tandis que la complexité de l'espace peut être définie comme le nombre de symboles (λ, index DB, symboles «appliquer») dans la plus grande réduction.

Est-ce correct? Si oui, où puis-je obtenir une référence? Sinon, comment me trompe-je?

Comme vous le faites remarquer, le λ-calcul a une notion apparemment simple de complexité temporelle: il suffit de compter le nombre d'étapes de réduction β. Malheureusement, les choses ne sont pas simples. Nous devons demander:

 Is counting β-reduction steps a good complexity measure?

Pour répondre à cette question, nous devons clarifier ce que nous entendons par mesure de complexité en premier lieu. Une bonne réponse est donnée par la thèse de Slot et van Emde Boas : toute bonne mesure de complexité devrait avoir une relation polynomiale avec la notion canonique de complexité temporelle définie à l'aide des machines de Turing. En d'autres termes, il devrait y avoir un codage tr (.) Raisonnable des termes λ-calcul vers les machines de Turing, tel que pour chaque terme $M$ de taille $|M|$: $M$ réduit à une valeur dans $poly(|M|)$ exactement lorsque $tr(M)$se réduit à une valeur en $poly(|tr(M)|)$ .

Pendant longtemps, on ne savait pas si cela pouvait être réalisé dans le λ-calcul. Les principaux problèmes sont les suivants.

• Il existe des termes qui produisent des formes normales en un nombre polynomial d'étapes de taille exponentielle. Voir (1). Même l'écriture des formes normales prend un temps exponentiel.

• La stratégie de réduction choisie joue également un rôle important. Par exemple, il existe une famille de termes qui se réduit en un nombre polynomial de pas β parallèles (dans le sens de la réduction λ optimale (2), mais dont la complexité est non élémentaire (3, 4).

L'article (1) clarifie le problème en montrant un codage raisonnable qui préserve la classe de complexité PTIME en supposant des réductions d'appel par nom les plus à gauche. L'idée clé semble être que l'explosion exponentielle ne peut se produire que pour des raisons inintéressantes qui peuvent être vaincues par un partage approprié des sous-termes.

Notez que des articles comme (1) montrent que les classes de complexité grossière comme PTIME coïncident, que vous comptiez les étapes β ou les étapes de Turing-machine. Cela ne signifie pas que des classes de complexité inférieure comme O (log n) coïncident également. Bien entendu, ces classes de complexité ne sont pas non plus stables sous la variation du modèle de machine de Turing (par exemple, 1 bande contre plusieurs bandes).

Les travaux de D. Mazza (5) prouvent le théorème de Cook-Levin (𝖭𝖯-complétude de SAT) en utilisant un langage fonctionnel (une variante du λ-calcul) au lieu des machines de Turing. L'aperçu clé est le suivant:

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

Je ne sais pas si la situation concernant la complexité de l'espace est comprise.

---

1. B. Accattoli, U. Dal Lago, la réduction bêta est invariante, en effet .

2. J.-J. Levy, Reductions correctes et optimales dans le lambda-calcul.

3. JL Lawall, HG Mairson, Optimalité et inefficacité: qu'est-ce qui n'est pas un modèle de coût du calcul lambda ?

4. A. Asperti, H. Mairson, La réduction bêta parallèle n'est pas élémentaire récursive .

5. D. Mazza, l' Église rencontre Cook et Levin .

$\beta$$\lambda$

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

$\beta$