프로그램을 악용하는 컴파일 타임 대체 예제

Question

정규화 (람다 아래에서의 대체 포함)를 "최적화"로 사용하는 형식화 된 람다 - 미적분의 단순한 컴파일러 (비단 말 및 암시 적 재귀 문제를 제외)를 상상해보십시오.

대부분 또는 모든 변수를 한 번만 사용하는 간단한 프로그램의 경우 정규화로 인해 프로그램이 더 짧아지고 빠릅니다.

제게는 "명백합니다"일반적으로 좋은 생각이 아닙니다. 즉, 정규화로 공유가 줄어들 기 때문에 최적화로 인해 악화되는 용어가 있습니다. 2 곱셈

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

와 용어는 그 중 3

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

에 "최적화"됩니다.

임의로 악화되는 예제를 구성하려면 어떻게해야합니까? 정상화 될 때 RAM 오버플로 가능성이있는 용어가 있습니까?

Google은 정규화가 강한 유형 시스템에서 작업하므로 발산 할 수 없습니다. 예 : 상수 및 델타 규칙을 사용하여 시스템 F의 적절한 하위 집합에서

또는 mul과 같은 상수를 추가하는 "자유로운"방법으로.

따라서 상수를 추가하는 대신 "런타임시 제공되는 추가 매개 변수"입니다.

질문은 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 
*) 

그러나 하스켈 때문에 (순식간에) 매우 빠르게도 큰 조건을 계산할 수의 게으름과 공유에 :

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