Un exemple où le plus petit terme lambda normal n'est pas le plus rapide

Soit la de -terms définie comme suit:$size$$\lambda$

• $size(x) = 1$ ,
• $size(λx.t) = size(t) + 1$ ,
• $size(t s) = size(t) + size(s) + 1$ .

Soit la complexité d'un $\lambda$ -term $t$ définie comme le nombre de réductions bêta parallèles de $t x$ à sa forme normale (en utilisant un évaluateur optimal au sens de Levy).

Je cherche un exemple de deux normales $\lambda$ -termes pour la même fonction où le terme plus est moins complexe.

...

Modifier pour plus de clarté

comme il semble que ce que je demande n'est pas évident, je vais essayer de donner un exemple solide. On pense souvent que la définition "naïve" / "la plus simple" d'une fonction est lente et non optimale. De meilleures performances augmentent la complexité du terme, car vous avez besoin de structures de données, de formules, etc. supplémentaires. Un excellent exemple est fibonacci, qui peut être défini "naïvement" comme:

-- The fixed fibonacci definition
fib_rec fib n =
    if (is_zero x) 
        then 1 
        else fib (n - 1) + f (n - 2)

-- Using church numbers instead of the λ-combinator to get a normal form
fib n = n fib_rec 0 n 

Ceci est souvent considéré comme la définition "la plus simple" de fib, et est très lent (exponentiel). Si nous développons les dépendances de fib(les définitions habituelles pour l'addition du nombre d'églises, pred, is_zero) et le normalisons, nous obtenons ce terme:

fib = (λa.(a(λbc.(c(λdef.f)(λde.d)(λde.(de))
      (λde.(b(λfg.(c(λhi.(i(hf)))(λh.g)(λh.h)))
      d(b(λfg.(c(λhi.(i(h(λjk.(k(jf))))))(λhi.g)
      (λh.h)(λh.h)))de)))))(λbc.c)a))

Des améliorations telles que des tables de mémorisation rendraient ce terme plus long. Pourtant, il existe un terme différent qui est beaucoup plus petit ...

fib = (λa.(a(λb.(b(λcde.(e(λfg.(cf(dfg)))c))))
      (λb.(b(λcd.(cd))(λcd.d)))(λbc.b)))

et, curieusement, elle est également asymptotiquement supérieure à la naïve qui court O(N). De toutes les définitions que je connais, c'est à la fois la plus rapide et la plus simple . Le même effet se produit avec le tri. Les définitions "naïves" telles que le tri à bulles et le tri par insertion sont souvent développées en termes énormes (20+ lignes de long), mais il existe une petite définition:

-- sorts a church list (represented as the fold) of church numbers
sort = λabc.a(λdefg.f(d(λhij.j(λkl.k(λmn.mhi)l)(h(λkl.l)i))
       (λhi.i(λjk.bd(jhk))(bd(h(λjk.j(λlm.m)k)c))))e)(λde.e)
       (λde.d(λfg.g)e)c

Ce qui se trouve également être plus rapide, asymptotiquement, que toutes les autres définitions que je connais. Cette observation me porte à croire que, contrairement à la croyance commune, le terme le plus simple, avec la plus petite complexité de Kolmogorov, est généralement le plus rapide. Ma question est essentiellement de savoir s'il existe des preuves du contraire, bien que j'aurais du mal à le formaliser.

Le théorème d'accélération de Blum est généralement énoncé dans le langage des fonctions partiellement récursives, mais jusqu'aux différences triviales de notation, il fonctionne de la même façon dans le langage de -calculus.$\lambda$

Il dit que compte tenu de toute mesure de complexité raisonnable (par exemple, le nombre optimal de réductions comme dans la question) et d'une fonction récursive (par exemple, ), nous pouvons trouver un prédicat récursif tel que:f ( x , y ) 2 y P ( x $M$$f(x,y)$$2^y$$P(x)$

Pour chaque algorithme (c'est-à-dire -term sous forme normale ici) calculant , il existe un autre algorithme pour qui a accélération sur : g P h P f g f ( x , M ( h , x ) ) ≤ M ( g , x )  pour toutes les entrées suffisamment grandes  x $\lambda$$g$$P$$h$$P$$f$$g$

$$f(x,M(h,x))\le M(g,x)\text{ for all large enough inputs }x,$$

où désigne la complexité du calcul de à l' entrée en fonction de la mesure .g x $M(g,x)$$g$$x$$M$

Par conséquent:

• $P$ n'a pas d'algorithme asymptotiquement optimal dans la mesure donnée

• en particulier, l'algorithme le plus court pour n'est pas asymptotiquement optimal$P$

• pour tout algorithme pour , il existe un algorithme asymptotiquement plus rapide dont la forme normale est plus longue (car jusqu'au renommage des variables, il n'y a qu'un nombre fini de termes normaux d'une longueur donnée)$P$