Armed with the \textbf {fix} operator, we can return to our semantics of \mathsf {while} loops from § [dt-0006] and § [dt-000R], and at last define their semantics without relying on dubious recursive definitions: \begin {array}{l} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C} = \textbf {fix}(f)\\[0.5em] \qquad \text {where}\; f(X)\ \sigma \; \triangleq \; \begin {cases} X\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} \end {array}

Proof that f is continuous is technically required but is omitted here.

Consider the function \Phi \in (\mathbb {N}_\bot \rightarrow \mathbb {N}_\bot ) \rightarrow (\mathbb {N}_\bot \rightarrow \mathbb {N}_\bot ), given by: \Phi (f) = \lambda n.\ \text {if}\ n = 0\ \text {then}\ 1\ \text {else}\ n\cdot f(n-1) Looking at the first few elements of our Kleene chain, we get: \begin {array}{lcl} \Phi ^0(\bot ) & = & \lambda n.\ \bot \quad \text {(i.e. $\bot _{\mathbb {N}_\bot \rightarrow \mathbb {N}_\bot }$)}\\ \Phi ^1(\bot ) & = & \lambda n.\ \text {if}\ n = 0\ \text {then}\ 1\ \text {else}\ \bot \\ \Phi ^2(\bot ) & = & \lambda n.\ \text {if}\ n = 0\ \text {then}\ 1\ \text {else}\ n\cdot (\text {if}\ n - 1 = 0\ \text {then}\ 1\ \text {else}\ \bot )\\ \cdots \end {array} Continuing on, we see that the mth approximation \Phi ^m(\bot ) to \textbf {fix}(\Phi ) is the function that gives x! for all x up to m, and diverges (\bot ) for all other arguments. Hence the limit \textbf {fix}(\Phi ) is the factorial function on \mathbb {N}_\bot !

1. Write down the first few approximations \Phi ^m(\bot ) to \textbf {fix}(\Phi ), where the higher order function \Phi : (\mathbb {Z}_\bot \rightarrow [\mathbb {Z}_\bot ]) \rightarrow (\mathbb {Z}_\bot \rightarrow [\mathbb {Z}_\bot ]) is given by: \Phi (f) = \lambda n.\ n :: f (n+1) What is \Phi ^m(\bot )? What is \textbf {fix}(\Phi )?

Solution.

• Liam O'Connor

The approximations are \{ \lambda n.\ \bot , \lambda n.\ n :: \bot , \lambda n.\ n :: (n + 1) :: \bot , \dots \}. The limit is a function that, given a natural number n, produces the infinite list of natural numbers starting from n.

2. Repeat the same process, but this time for a new higher order function \Phi : (\mathbb {Z}_\bot \rightarrow \mathbb {Z}_\bot ) \rightarrow (\mathbb {Z}_\bot \rightarrow \mathbb {Z}_\bot ) given by: \Phi (f) = \lambda n.\ \text {if}\ n = 0\ \text {then}\ 0\ \text {else}\ f(n-2)

Solution.

• Liam O'Connor

The nth approximation returns 0 if the input number is non-negative, even and less than 2n, otherwise it diverges (returns \bot ). The limit returns 0 for any non-negative even number, and diverges otherwise.