編譯時替換惡化程序的示例

想象一下，使用標準化（包括lambda下的替換）作爲「優化」的類型化lambda演算（排除一個非常痛苦的非終止和隱式遞歸問題）的樸素編譯器。編譯時替換惡化程序的示例

對於大多數或全部變量僅使用一次的簡單程序，規範化導致程序既短又快。

對我來說這是「明顯的」，總的來說這不是一個好主意。也就是說，由於規範化會減少共享，因此優化會導致條款惡化。 2個乘法

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

術語被「優化」到

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

與他們的3。

我該如何構建一個變得更加糟糕的例子？規範化時是否有可能溢出RAM的術語？

我們正在使用強歸一化的類型系統，因此不可能發生分歧。在系統F的一個合適的子集中有常量和delta規則。或者使用「免費」方法來添加常量，如mul，例如，

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

因此，不是添加常量，而是「運行時提供的額外參數」。

這個問題似乎屬於SE計算機科學，但IMO確實是一個入門級的問題，所以我認爲這裏更合適。

來源

2016-12-16 nponeccop

[CS。 se]是一個網站，可用於各種與cs有關的問題，包括入門級的問題。 [cstheory.se]是研究級別問題的地方。 –

如何堆疊在其本身上你稍微修改功能，像這樣：

讓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 
*)

但哈斯克爾，由於它的懶惰和共享，能夠非常快速地計算（在幾分之一秒）甚至是大方面：

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

來源

2016-12-16 06:11:41 deniss

編譯時替換惡化程序的示例

回答

相關問題