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

9

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?

Jake
la source
l'article date de 1979. il y a une pensée / technologie beaucoup plus moderne / récente sur la façon de traduire le code en logique, par exemple avec des FPGA et des GPU et ne serait généralement pas basée sur des langages fonctionnels ....
vzn
Pouvez-vous me les indiquer?
Jake
la recherche que vous citez est une "preuve de principe" plus théorique ... il serait préférable de citer le concept / la section sur "l'augmentation polynomiale de la taille" qui semble être au centre de votre question ... êtes-vous intéressé par la théorie générale de la conversion de code en logique / circuits, du côté théorique ou appliqué, ou théorie de le faire efficacement, ou les deux? la question est très transversale dans ses différents aspects ... peut-être peut-être en savoir plus dans Computer Science Chat
vzn
1) existe-t-il un moyen d'importer cela dans un chat? Je n'arrive pas à comprendre cela. 2) Il n'y a pas de section sur l'augmentation polynomiale de la taille et c'est mon problème. Il ne dit en fait rien de substantiel (ni de telles références) sur l'ampleur de l'augmentation de taille.
Jake
les commentaires peuvent être importés dans le chat après un seuil de commentaires publiés séparés. ce n'est pas nécessaire pour démarrer un chat. concernant l'augmentation polynomiale, il pourrait s'agir d'un concept de «rumeur» ou de «folklore» concernant cette ligne de recherche, je n'en suis pas sûr. mais où avez-vous entendu des trucs comme "ça produit des choses qui explosent en taille"; il serait utile d'être plus précis etc ...
vzn

Réponses:

4

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.

vzn
la source
1
parfait! J'ai également trouvé ce document après avoir recherché ces deux documents. sciencedirect.com/science/article/pii/002001908790161X Merci!
Jake