Les termes de logique combinatoire sont-ils toujours plus gros?

Il existe donc un algorithme pour convertir les termes de calcul lambda en logique combinatoire à l'aide de combinateurs SK. Il produit des choses qui explosent en taille. J'aimerais en savoir plus sur cette explosion de taille. Je n'arrive pas à penser à un meilleur algorithme cependant. J'ai entendu dire que des langages fonctionnels étaient pratiquement compilés en combinateurs, il semble donc qu'un meilleur algorithme doit exister. J'ai recherché l'article de David Turner sur le sujet et il dit simplement d'appliquer quelques optimisations et qu'elles provoquent une "amélioration considérable".

Une "amélioration considérable" signifie-t-elle que la taille ne tombe qu'à une augmentation polynomiale? Existe-t-il un moyen connu de convertir les termes lambda en logique combinatoire avec seulement une augmentation polynomiale (ou moins?) De la taille? Si un tel algorithme existe, est-il pratique?

pas un expert en la matière, mais voici deux articles historiques qui semblent être étroitement liés à la question et il s'agit peut-être d'un domaine de recherche semi-actif. Turner a proposé un ensemble de combinateurs qui peuvent être réduits à des combinateurs SK. ce prochain article soutient que même les combinateurs Turner non réduits aux combinateurs SK conduisent à une explosion exponentielle (et que la réduction aux termes SK serait probablement encore plus importante). mais alors le deuxième article dit qu'il existe un algorithme efficace de l'espace O (n log n) basé sur les combinateurs Turner. (il semble peut-être que des allégations sur l'efficacité polynomiale soient considérées comme n'étant pas entièrement démontrées / non prouvées et sont donc considérées comme des conjectures ...

• Qu'est-ce qu'une mise en œuvre efficace du λ-calcul? / Frandsen, Sturtivant (1991) (voir p.18)

  De plus, nous montrons que les implémentations basées sur des combinateurs Turner ou des super-combinateurs Hughes ont des complexités , c'est-à-dire une borne inférieure exponentielle. Il est possible de savoir s'il existe une implémentation de complexité polynomiale, , bien que certaines implémentations aient été implicitement revendiquées comme ayant cette complexité.$2^{Ω(ν)}$$ν^{O(1)}$

• Traduction de Turner Combinators dans l'espace O (n log n) / Noshita (1985)

  Une méthode pratique pour représenter les combinateurs Turner est présentée, qui n'a besoin que de l'espace O (n log n) dans le pire des cas pour traduire des expressions lambda de longueur n.