Пример замен во время компиляции, ухудшающих программу

Question

Представьте себе наивный компилятор типизированного лямбда-исчисления (чтобы исключить довольно болезненную проблему нетерминации и неявной рекурсии), который использует нормализацию (включая подстановки под лямбда-выражения) в качестве "оптимизации".

Для простых программ, когда большинство или все переменные используются только один раз, нормализация приводит к программам, которые и короче, и быстрее.

Для меня это "очевидно", что в целом это не очень хорошая идея. То есть, поскольку нормализация уменьшает совместное использование, существуют условия, которые ухудшаются из-за оптимизации. Термин с 2 умножениями

\x -> let a = x * x in a * a

"оптимизируется" в

\x -> (x * x) * (x * x)

с 3 из них.

Как мне построить пример, который становится как угодно хуже? Есть ли термин, который может привести к переполнению оперативной памяти при нормализации?

Мы работаем в системе типов с сильной нормализацией, поэтому расхождение невозможно, например, в подходящем подмножестве системы F с константами и дельта-правилами.

Или с "свободным" подходом к добавлению констант, таких как mulнапример,

\mul x -> let a = mul x x in mul a a

Поэтому вместо добавления констант они являются просто "дополнительными параметрами, предоставляемыми во время выполнения".

Может показаться, что вопрос принадлежит SE Computer Science, но IMO - это действительно начальный уровень, так что я думаю, что он более уместен здесь.

Answer 1

Как насчет размещения вашей слегка измененной функции поверх себя, например, так:

позволять p:nat->nat->nat - непрозрачная константа (или параметр).

q:(nat->nat->nat)->nat->nat->nat = \f:(nat->nat->nat).(\a b:nat.f (f a b) (f a b))

q p => \a b.p (p a b) (p a b)

q (q p) => \c d.q p (q p c d) (q p c d) 
  => \c d.q p (p (p c d) (p c d)) (p (p c d) (p c d))
  => \c d.p (p [p (p (p c d) (p c d))] [p (p (p c d) (p c d))]) (p [p (p (p c d) (p c d))] [p (p (p c d) (p c d))])

q (q (q p)) расширяется до какого-то огромного срока

Это растет в геометрической прогрессии. Вы можете проверить это в Coq:

Section Expand.

Variable nat:Type.

Variable p:nat->nat->nat.

Definition q:(nat->nat->nat)->nat->nat->nat :=
  fun f:(nat->nat->nat) => fun a b:nat => f (f a b) (f a b).

Eval compute in (q p).
(*
  = fun a b : nat => p (p a b) (p a b)
     : nat -> nat -> nat
*)

Eval compute in (q (q p)).
(*
  = fun a b : nat =>
       p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
         (p (p (p a b) (p a b)) (p (p a b) (p a b)))
     : nat -> nat -> nat
*)

Eval compute in (q (q (q p))).
(*
     = fun a b : nat =>
       p
         (p
            (p
               (p
                  (p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
                     (p (p (p a b) (p a b)) (p (p a b) (p a b))))
                  (p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
                 =============SKIPPED LOTS OF LINES==========
                  (p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
                     (p (p (p a b) (p a b)) (p (p a b) (p a b)))))))
     : nat -> nat -> nat
*)

Но Haskell, благодаря своей лени и долевого участия, способен очень быстро вычислять даже большие условия (за доли секунды):

Prelude> q f a b = f (f a b) (f a b)
Prelude> (q $ q $ q (+)) 1 1
256
Prelude> (q $ q $ q $ q (+)) 1 1
65536
Prelude> (q $ q $ q $ q $ q (+)) 1 1
4294967296
Prelude> (q $ q $ q $ q $ q $ q (+)) 1 1
18446744073709551616
Prelude> (q $q $ q $ q $ q $ q $ q (+)) 1 1
340282366920938463463374607431768211456
Prelude> (q $ q $ q $ q $ q $ q $ q $ q (+)) 1 1
115792089237316195423570985008687907853269984665640564039457584007913129639936
Prelude> (q $ q $ q $ q $ q $ q $ q $ q $ q (+)) 1 1
13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096