Off-line narrowing-driven partial evaluator for inductively sequential programs

Jump to...

- Off-line partial evaluator...
- Benchamark list

Example: ackermann's function

[ Original program ]  [ Annotated program ]  [ Specialized program ] [ Runtimes ]

Original program

This is the classical Ackermann's function. Its transformation for optimization has been undertaken before in the tupling field.

In the next program, we want to produce a specialized version of acker function, for this, the first function that appears in the program contains the expression to be partially evaluated, i.e., for  numbers greater than or equal than 10 (expressed in Peano natural numbers).

 
         
import Benchmark (runBenchmark)

data Nat = Z | S Nat

main x = acker (S(S(S(S(S(S(S((S(S(S(S(S(S(S(S(S(S(S(S(S x)))))))))))))))))))))

acker     n    = ack (S(S Z))   n

ack Z     n    = S n
ack (S m) Z    = ack  m   (S Z)
ack (S m) (S n)= ack  m   (ack (S m) n) 


--for annotations
GEN x = x

bench  = runBenchmark 10 (\_ -> print (x =:= ( main  (n2s 500) )   ) ) 
               where x free


n2s n = if n==0 then Z else S (n2s (n-1))
s2n Z    =  0
s2n (S n)= (s2n n) +1      

        

Annotated program [ go top ]

Below, the annotated program at third rule of ack function, shows one mark for the nested function call: ack (S m) n .

 
import Benchmark (runBenchmark)

data Nat = Z | S Nat

main x = acker (S(S(S(S(S(S(S((S(S(S(S(S(S(S(S(S(S(S(S(S x)))))))))))))))))))))

acker     n    = ack (S(S Z))   n

ack Z     n    = S n
ack (S m) Z    = ack  m   (S Z)
ack (S m) (S n)= ack  m   (GEN (ack (S m) n) )


--for annotations
GEN x = x

bench  = runBenchmark 10 (\_ -> print (x =:= ( main  (n2s 500) )   ) ) 
               where x free


n2s n = if n==0 then Z else S (n2s (n-1))
s2n Z    =  0
s2n (S n)= (s2n n) +1      

Specialized program [ go top ]

First load OffPeval in PAKCS environment, then mix de program with: mix "examples/ackermann", after load and show the specialized version.

 prelude> :l ackermann_pe
Compiled Curry program 'ackermann_pe.pl' is up-to-date.

ackermann_pe(module: ackermann)> :show
No source program file available, generating source from FlatCurry...

-- Program file: ackermann_pe
module ackermann(Nat(Z,S),acker,ack,GEN,bench,n2s,s2n,main,ack_pe1,ack_pe4,ack_pe23) where

import Benchmark

data Nat = Z | S Nat

acker :: Nat -> Nat
acker v0 = ack (S (S Z)) v0

ack :: Nat -> Nat -> Nat
ack eval flex
ack Z v1 = S v1
ack (S v2) Z = ack v2 (S Z)
ack (S v2) (S v3) = ack v2 (GEN (ack (S v2) v3))

GEN :: a -> a
GEN v0 = v0

bench :: IO ()
bench = Benchmark.runBenchmark 10 (ackermann_lambda0_0 v0) where v0 free

n2s :: Int -> Nat
n2s v0 = 
   if v0 == 0
   then Z
   else S (n2s (v0 - 1))

s2n :: Nat -> Int
s2n eval flex
s2n Z = 0
s2n (S v1) = (s2n v1) + 1

ackermann_lambda0_0 :: Nat -> Int -> IO ()
ackermann_lambda0_0 v0 v1 = print (v0 =:= (main (n2s 500)))

main :: b -> a
main v0 = ack_pe1 (ack_pe4 v0)

ack_pe1 :: b -> a
ack_pe1 eval flex
ack_pe1 Z = S (S Z)
ack_pe1 (S v506) = S (ack_pe1 v506)

ack_pe4 :: b -> a
ack_pe4 v0 = ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 
   (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 (ack_pe1 
   (ack_pe1 (ack_pe1 (ack_pe23 v0)))))))))))))))))))

ack_pe23 :: b -> a
ack_pe23 eval flex
ack_pe23 Z = S (ack_pe1 Z)
ack_pe23 (S v6206) = ack_pe1 (ack_pe23 v6206)


-- end of module ackermann_pe
       
      

Partial evaluator has decomposed de original recursive function ack in 3 functions, it has modified the recursive characteristics of ack function giving a successful speed up.

Runtimes [ go top ]

[ go to top ]