Haskell/Solutions/Denotational semantics

← Back to Denotational semantics

Exercises
Prove that power2 is strict. While one can base the proof on the "obvious" fact that power2 n is $2^{n}$, the latter is preferably proven using fixed point iteration.

Remember that:

power2 0 = 1
power2 n = 2 * power2 (n-1)

First, we need to consider whether ⊥ - 1 is ⊥ or not. Using similar reasoning to the ⊥ + 1 case, we can determine that ⊥ - 1 is indeed ⊥. From there, we know that power2 ⊥ is 2 * power2 ⊥. Since this recurses indefinitely, it is equivalent to ⊥.