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

Question

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

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

Для меня это «очевидно», что в целом это не очень хорошая идея. То есть, поскольку нормализация уменьшает совместное использование, есть условия, которые ухудшаются из-за оптимизации. Термин 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