gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-03 19:42:23 27 4
gpt4 key购买 nike

想象一个简单的类型化 lambda 演算编译器(排除一个相当痛苦的非终止和隐式递归问题),它使用规范化(包括 lambdas 下的替换)作为“优化”。

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

对我来说,“显而易见”一般来说这不是一个好主意。也就是说,随着归一化减少共享,有些项会因为优化而变得更糟。有 2 个乘法的项

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

被“优化”成
\x -> (x * x) * (x * x)

其中 3 个。

我如何构建一个变得任意糟糕的例子?是否有一个术语在规范化时可能会溢出 RAM?

我们正在一个具有强规范化的类型系统中工作,因此不可能发生分歧,例如在具有常量和增量规则的系统 F 的合适子集中。

或者使用“免费”方法添加常量,例如 mul ,例如
\mul x -> let a = mul x x in mul a a

因此,它们不是添加常量,而是“在运行时提供的额外参数”。

这个问题似乎属于 SE 计算机科学,但 IMO 这确实是一个入门级问题,所以我认为它在这里更合适。

最佳答案

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

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

关于compiler-optimization - 编译时替换使程序恶化的示例,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/41175765/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com