← Back to Denotational semantics
Exercises |
---|
Prove that power2 is strict. While one can base the proof on the "obvious" fact that power2 n is , 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 ⊥
.