Calcul des constructions: compresser l'expression dans sa plus petite forme

11

Je suis conscient que le calcul des constructions est en train de normaliser fortement, ce qui signifie que chaque expression a une normale pour laquelle elle ne peut pas être bêta, eta-réduite davantage. Il s'agit donc en fait de l'expression la plus efficace qui calcule la même valeur que l'expression d'origine.

Mais dans certains cas, la normalisation peut réduire une petite expression à une énorme expression (en termes de taille).

Existe-t-il une forme d'expression la plus petite? Un formulaire qui calcule la même valeur avec la plus petite taille.

En d'autres termes, au lieu d'une forme normale économe en temps, économe en espace.

lambda-calculus reductions typed-lambda-calculus normalization calculus-of-constructions user47376
la source

8

Il y a un peu de liberté dans ce que nous considérons comme "la même valeur". Permettez-moi de montrer qu’il n’existe pas un tel algorithme si «la même valeur» signifie «équivalent sur le plan de l’observation». J'utiliserai un fragment du calcul des constructions, à savoir le système T de Gödel (simplement tapé -calculus, les nombres naturels et la récursion primitive sur eux), donc l'argument s'applique déjà à un calcul beaucoup plus faible. $\lambda$

Étant donné un nombre , soit soit le chiffre correspondant le représentant, c'est-à-dire, applications de à . Étant donné un mahcine Turing , soit le chiffre codant d'une manière raisonnable. $n$ $\overline{n}$ $n$ $\mathtt{succ}$ $0$ $M$ $\lceil M \rceil$ $M$

Disons que deux termes fermés sont équivalents , écrits , quand pour tout , et se normalisent tous les deux au même chiffre (ils se normalisent à un chiffre parce que nous sommes dans un claculus fortement normalisant). $t, u : \mathtt{nat} \to \mathtt{nat}$ $t \simeq u$ $n \in \mathbb{N}$ $t \, \overline{n}$ $s \, \overline{n}$

Supposons que nous ayons un algorithme qui, étant donné tout terme fermé de type calcule un terme équivalent minimal. Ensuite, nous pouvons résoudre l'oracle Halting comme suit. $\mathtt{nat} \to \mathtt{nat}$

Il existe un terme tel que, pour tous les et toutes les machines de Turing , normalise en si s'arrête en étapes, et il se normalise en sinon. Ceci est bien connu, car la simulation d'une machine de Turing pour un nombre fixe d'étapes est récursive primitive. $S : \mathtt{nat} \times \mathtt{nat} \to \mathtt{nat}$ $n \in \mathbb{N}$ $M$ $S (\lceil M \rceil, \overline{n})$ $\overline{1}$ $T$ $n$ $\overline{0}$ $n$

Il existe de nombreux termes fermés qui sont des termes minimaux équivalents à . Notre algorithme de minimisation renvoie l'un d'eux lorsque nous lui donnons , et il peut même arriver que soit en fait le seulement ce terme minimal. Tout cela n'a pas d'importance, la seule chose qui compte, c'est qu'il existe un nombre fini de termes minimaux équivalents à . $Z_1, \ldots, Z_k$ $\lambda x : \mathtt{nat} .\, 0$ $\lambda x : \mathtt{nat} .\, 0$ $\lambda x : \mathtt{nat} .\, 0$ $\lambda x : \mathtt{nat} .\, 0$

Maintenant, étant donné n'importe quelle machine , considérons le terme Si s'exécute pour toujours, alors normalise en pour chaque et est équivalent à . Pour décider si s'exécute pour toujours, nous introduisons dans notre algorithme de minimisation et vérifions si l'algorithme a renvoyé l'un des . Si c'est le cas, alors s'exécute pour toujours. Si ce n'est pas le cas, cela s'arrête. (Remarque: l'algorithme n'a pas besoin de calculer les $M$

u : = λ x : n a t . S (⌈ M ⌉, x)

$u \mathbin{{:}{=}} \lambda x : \mathtt{nat} .\, S (\lceil M \rceil, x)$

M

$M$

u \bar{n}

$u \overline{n}$

\bar{0}

$\overline{0}$

n

$n$

λ x : n a t . 0

$\lambda x : \mathtt{nat} .\, 0$

M

$M$

u

$u$

Z_{1}, \dots, Z_{k}

$Z_1, \ldots, Z_k$

M

$M$

Z_{1}, \dots, Z_{k}

$Z_1, \ldots, Z_k$ en soi, ceux-ci peuvent être codés en dur dans l'algorithme.)

Ce serait bien de connaître un argument qui fonctionne avec une notion plus faible d'équivalence, par exemple juste réductibilité. $\beta$

Andrej Bauer
la source

Comment calcule-t-on Z1, .. Zk?

user47376

Tu n'es pas obligé. Autrement dit, l'algorithme que je décris est là-bas, et nous ne savons pas exactement ce que c'est, mais ce n'est pas pertinent. Je n'essaie pas d'exécuter l'algorithme, j'ai juste besoin de son existence pour montrer que votre algorithme n'existe pas.

Andrej Bauer

Oui, mais votre argument dit que si mon algorithme existe, nous pouvons résoudre le problème d'arrêt. Pour déterminer si une machine de Turing M arrête votre algorithme normalise u et vérifie s'il s'agit de Z1, .. Zk. Il doit donc pouvoir les énumérer, sinon il risque de ne pas s'arrêter.

user47376

Les sont câblés dans l'algorithme, l'algorithme n'a pas besoin de les énumérer dans un sens de calcul. Si vous préférez, le code source de l'algorithme commencerait par une déclaration d'un entier (par exemple une directive #define en C) et un tableau de longueur , puis le code peut utiliser librement , quels qu'ils soient sont. Nous n'avons pas besoin de les connaître explicitement, nous avons juste besoin de savoir qu'ils existent.

Z_{1}, \dots, Z_{k}

$Z_1,\ldots,Z_k$

k

$k$

Z

$Z$

k

$k$

Z [i]

$Z[i]$

Damiano Mazza

7

Comme l'a dit Andrej, le problème est indécidable si vous permettez de remplacer un terme par un autre, extensionnellement égal. Cependant, vous pourriez être intéressé par un partage optimal des expressions, dans le sens suivant: étant donné la réduction il est clair que les occurrences de la le terme peut être partagé en mémoire , et chaque réduction appliquée à l'un peut être appliquée à l'autre.

(λ x : T . C x x) u \to_{β} C u u

$(\lambda x:T.C\ x\ x)\ u\rightarrow_\beta C\ u\ u$

u

$u$

En ce sens, on sait réduire de manière optimale les termes non typés, en réduisant au maximum le partage. Ceci est expliqué ici: /programming//a/41737550/2059388 et la citation pertinente est un algorithme de J. Lamping pour une réduction optimale du calcul lambda . Il ne fait aucun doute que le théorème du calcul non typé peut être étendu au CIC.

Une autre question pertinente est la quantité d'informations de type qui peuvent être effacées lors de la conversion de type, ou bien comment effectuer une conversion efficace, qui est un domaine de recherche actif, voir par exemple la thèse de Mishra-Linger .

cody
la source

6

Permettez-moi d'insister sur le point de vue abordé par la réponse de Cody.

Pour autant que l'on puisse le voir, la question de trouver un plus petit -term équivalent à un autre -term n'est pas vraiment intéressante, même s'il existait un algorithme le calculant. En fait, la plupart des programmes que vous écrivez dans le -calculus (ou quel que soit le calcul du -cube) sont déjà sous forme normale, ou au moins sous forme normale, donc ils sont déjà à leur "plus petite" dans le sens où vous décris. De plus, être "petit" ne signifie pas être plus efficace comme discuté dans cette question . $\lambda$ $\lambda$ $\lambda$ $\lambda$

Ainsi, le problème que vous signalez (que la normalisation fait exploser la taille) est un vrai problème uniquement lorsque vous souhaitez appliquer une fonction à un argument et réduire à la forme normale pour obtenir le résultat. Par exemple, supposons que vous ayez un terme calculant une fonction sur des chaînes binaires. Vous avez alors où est le nombre d'étapes de réduction utilisant la réduction la plus à gauche, ce qui est garanti de trouver une forme normale si elle existe (dans CoC, elle existe toujours, mais ce que je dis s'applique également au cas non typé). Supposons maintenant, en outre, que pour une constante . Pouvez-vous conclure que est calculable en temps polynomial? $M$ $f$

M \bar{x} \to^{l (| x |)} \bar{f (x)}

$M\,\overline{x}\to^{l(|x|)}\overline{f(x)}$

l (| x |)

$l(|x|)$

l (n) = O (n^{k})

$l(n)=O(n^k)$

k

$k$

f

$f$

Il est très facile de construire des exemples de -terms dont la taille augmente de façon exponentielle avec la réduction (la plus à gauche), c'est-à-dire qu'en étapes vous obtenez un terme de taille . Cela peut nous rendre sérieusement douteux en ce qui concerne une réponse positive à la question ci-dessus: il semble que le -calculus soit capable d'effectuer une quantité exponentielle de travail en temps linéaire. En d'autres termes, il semble que le -calculus ne soit pas un modèle raisonnable de calcul en termes de complexité. $\lambda$ $\Theta(n)$ $\Theta(2^n)$ $\lambda$ $\lambda$

Bien que légitime, le doute ci-dessus provient d'une hypothèse erronée, à savoir que termes sont des représentations efficaces d'eux-mêmes. Ils ne sont pas! En plaisantant moins, termes sont des représentations très inefficaces des états qu'une machine qui les exécute doit réellement passer. $\lambda$ $\lambda$

Il s'avère qu'il existe une syntaxe, appelée -calculus avec des substitutions explicites linéaires et introduite par Beniamino Accattoli, qui est très bonne pour représenter le phénomène de partage évoqué dans la réponse de cody. En particulier, cette syntaxe peut être utilisée pour fournir des représentations de termes extrêmement fidèles de machines abstraites de toutes sortes (voir l'article de Beniamino ICFP 2014 "Distilling Abstract Machines", dont je suis co-auteur. Je m'excuse pour l'autopromotion, mais cela semble pertinent ici). $\lambda$

Cette même syntaxe peut être utilisée pour prouver que, contrairement à l'intuition naïve, la réponse à la question ci-dessus est oui, en effet: le nombre d'étapes les plus à gauche vers la forme normale est une mesure de coût raisonnable, même si la taille explose, car il existe en fait une autre manière de représenter le même calcul (en utilisant des substitutions explicites linéaires) dans laquelle:

la taille n'explose pas ;
étant donné deux termes dans la syntaxe de substitution explicite linéaire, il existe un algorithme à temps polynomial qui teste s'ils représentent le même -term, c'est-à-dire qu'il existe un moyen intelligent de comparer des termes qui n'ont pas besoin de "déplier" le partage ( simplement «déplier» puis comparer ne fonctionnerait pas car le terme «non partagé» peut être exponentiellement grand). $\lambda$

Tout cela est expliqué dans le document d'Accattoli et Dal Lago "La réduction bêta est invariante, en effet" (LICS 2014, puis je pense qu'il existe une version de journal plus récente).

Je pense que le point 2 va beaucoup dans le sens de votre question sur les représentations "efficaces de l'espace" des termes : le calcul de substitution linéaire fournit de telles représentations, bien qu'elles ne soient en aucun cas "normales", c'est-à-dire qu'elles ne sont pas les forme normale d'une procédure de réécriture. $\lambda$

Damiano Mazza
la source

Je pensais par exemple à un terme qui déploie un million d'étapes pour générer une liste d'un million d'éléments. Cela se normalise à la liste réelle, qui est la représentation la plus efficace de cette valeur (c'est le résultat final réel, aucune autre étape nécessaire). Mais le terme déployé lui-même peut être très petit.

user47376

Eh bien, mais vous rencontrez tous les manigances de la complexité de Kolmogorov. Si je comprends bien, vous demandez une description, pour chaque classe d'équivalence d'un type donné (par exemple, le type de chaînes binaires), d'un terme représentatif de taille minimale. Cela équivaut à définir la fonction de complexité de Kolmogorov et il est bien connu que cela n'est pas calculable, indescriptible, etc. etc.

β

$\beta$

Damiano Mazza

Oui, c'est impossible comme l'a dit Andrej. Cela a répondu à ma question.

user47376

Calcul des constructions: compresser l'expression dans sa plus petite forme

Réponses: