Jump to...
Example: ackermann's function
[ Original program ] [ Annotated program ]
This is the classical function Ackermann, here, for natural numbers.
data Nat = Z | S Nat
ack Z n = S n
ack (S m) Z = ack m (S Z)
ack (S m) (S n)= ack m (ack (S m) n)
Below, the annotated program. The third rule of the
function ack, contains one mark for the second argument of
each function call (from size-change graph analysis). But in the second rule where the second argument of
function is a value, i.e., it is a ground argument.
module ackS where
data Nat
= Z
| S Nat
GEN :: a -> a
GEN x
| success
= x
ack :: Nat -> Nat -> Nat
ack Z n = S n
ack (S m) Z = ack m (S Z)
ack (S m) (S n) = ack m (GEN (ack (S m) (GEN n)))
[ go top ]