Monotonicity, Continuity and Least fix point of function

Question

I am learning semantics of language Haskell and there i come around this question.

For answering this, I am thinking in this way:

a) For a function to be monotonic, let's say I have 2 arguments: $f$ and $g$. If $f ≼ g$, I have to show that $ee(f) ≼ ee(g)$. Let's say I have $f = \bot$ and $g = 0$. Then on applying $f$, I get $\bot$, and on applying $0$, I get $True$. What is wrong here?

b) For function to be continuous, LUB of $f$ is equal as applying function on all inputs then take LUB. I am confused how to apply this here.

c) And I don't know what is least fixpoint. Is it the least possible input or the result?

Can anyone please help me solving this. Thank you.

Answer 1

About a): As you correctly state, $ee$ is said to be monotonic if, for all $f$ and $g$, whenever $f \preceq g$, then also $ee(f) \preceq ee(g)$.

The first thing you are missing is which values $f$ and $g$ can take: Note that $f$ and $g$ are functions from $\mathbb{Z}_\bot$ to $\mathbb{B}_\bot$, so you cannot take $g=0$ (as $0$ is not a function to the Booleans).

That being said, let's consider what we have to prove. First of all, when is $f \preceq g$? In this case, this means that for all $x \in \mathbb{Z}_\bot$, we have $f(x) \preceq g(x)$.

Let us now consider a special case of the proof. We know that $f \preceq g$, and we want to show that $ee(f)(x) \preceq ee(g)(x)$. Suppose that $f(x) = \bot$ for all $x$. Since $f(x) \preceq g(x)$, this means that $g(x)$ can be arbitrary (why?).

Now, we consider $ee(f)(x)$ and $ee(g)(x)$. We have to show that $ee(f)(x) \preceq ee(g)(x)$. Then there are four cases:

1. $x = \bot$. Then $ee(f)(x) = \bot$, and also $ee(g)(x) = \bot$, just from the definition of $ee$. But then, $ee(f)(x) \preceq ee(g)(x)$.
2. $x > 0$. Then $ee(f)(x) = \neg(f(x-1)) = \neg \bot$, where we use the assumption that $f(x) = \bot$ for all $x$. Since $\neg \bot = \bot$, we have $ee(f)(x) = \neg\bot = \bot \preceq ee(g)(x)$.
3. $x < 0$. This is completely analogous to (2).
4. $x = 0$. Then $ee(f)(x) = True = ee(g)(x)$, by definition of $ee$. Thus, $ee(f)(x) \preceq ee(g)(x)$.

The general proof proceeds is similar to this.

Abouyt b): What you need to show is the following: Suppose $f_1, f_2, \ldots$ is a sequence of functions $\mathbb{Z}_\bot \to \mathbb{B}_\bot$, such that $f_1 \preceq f_2 \preceq \ldots$. The least upper bound $f^* := \bigvee_{i=1}^\infty f_i$ is a function such that on one hand, $f_i \preceq f^*$ for all $i$, and on the other hand, if $f_i \preceq f'$ for all $i$, then also $f^* \preceq f'$.

To show that $ee$ is continous, let $f_1, f_2, \ldots$ be a sequence of functions as above. You have to show that $\bigvee_i ee(f_i) = ee(\bigvee_i f_i)$. Approach:

1. $\bigvee_i ee(f_i) \preceq ee(\bigvee_i f_i)$, or equivalently, $ee(f_j) \preceq ee(\bigvee_i f_i)$ for all $j$. This follows from (a); can you see how?.
2. $ee(\bigvee_i f_i) \preceq \bigvee_i ee(f_i)$. In this case, it is useful to note that $(\bigvee_i f_i)(x) = \bigvee_i (f_i(x))$, so you can work pointwise: Show that for all $x$, $ee(\bigvee_i f_i)(x) \preceq \bigvee_i ee(f_i)(x)$.

About c): The least fixed point of $ee$ is defined to be the $f$ such that $ee(f) = f$ and that for all $g$ such that $ee(g) = g$, we have $f \preceq g$. To find the least fixed point, note that $ee(f)(0) = True$ for any function $f$, so any fixpoint of $f$ will have $f(0) = True$. This also implies that $f(1) = f(-1) = \neg f(0) = False$, $f(2) = f(-2) = True$, \dots The pattern should now be easy to recognize.

Edit: Fixed some typos pointed out in the comments.