编译时替换使程序恶化的示例

Question

想象一个使用规范化（包括 lambda 下的替换）作为 "optimization".

的类型化 lambda 演算的朴素编译器（以排除非终止和隐式递归的相当痛苦的问题）

对于大多数或所有变量仅使用一次的简单程序，规范化会导致程序更短更快。

对我来说 "obvious" 总的来说这不是一个好主意。也就是说，随着规范化减少共享，有些项会因为优化而变得更糟。有 2 次乘法的项

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

得到"optimized"进入

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

其中 3 个。

如何构造一个任意变差的示例？是否有一个术语在标准化时可能会溢出 RAM？

我们正在一个具有强规范化的类型系统中工作，所以发散是不可能的，例如在具有常量和增量规则的系统 F 的合适子集中。

或者使用 "free" 方法添加常量，例如 mul，例如

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

所以他们只是 "extra parameters provided at runtime".

而不是添加常量

这个问题似乎属于 SE Computer Science，但 IMO 它确实是一个入门级的问题，所以我认为它在这里更合适。

Answer 1

如何将稍微修改过的函数堆叠在自身之上，如下所示：

let 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

编译时替换使程序恶化的示例

Example of compile-time substitutions worsening the program

compiler-optimization

lambda-calculus