← Back to Denotational semantics

Exercises
Prove that `power2` is strict. While one can base the proof on the "obvious" fact that `power2 n` is ${\displaystyle 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 `⊥`.