プログラムを悪化させるコンパイル時の置換の例

Question

正規化（lambdaの下での置換を含む）を「最適化」として使用する型付きlambda-calculus（非終端と暗黙の再帰の厄介な問題を除外する）の素朴なコンパイラを想像してみてください。

ほとんどまたはすべての変数が1回だけ使用される単純なプログラムでは、正規化によってプログラムが短くて高速になります。

私にとっては、それは一般的には良いアイデアではないことは「明らかです」。つまり、正規化によって共有が減少するため、最適化のために悪化する用語があります。 2回の乗算

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

との用語は、それらの3と

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

に "最適化" されます。

任意に悪化する例を作成するにはどうすればよいですか？正規化するとRAMがオーバーフローする可能性のある用語はありますか？

私たちは強い正規化を持つ型システムで作業しているので、発散することはできません。システムFの適切なサブセットにおいて、定数およびデルタルールを用いて計算される。

またはmulのような定数を追加するための「フリー」アプローチでは、

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

定数を追加する代わりに、これらは単に「実行時に提供される追加のパラメータ」です。

質問はSEコンピュータサイエンスに属しているようですが、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 
*) 

しかし、（第2の割合で）非常に迅速にも、大規模な条件を計算することができ、その怠惰と共有するハスケル、：

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