The lazy natural numbers, also called conats, are defined as the least solution to the equation X \simeq \mathbf {1} + X.

1. Sketch the first four approximations to the least fixed point. Call the two sum injections \mathsf {zero} and \mathsf {succ}.

   Solution.

   • Liam O'Connor

   \begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {zero}\ \bot )), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {succ}\ \bot )), \bot \} \\ \end {array}
2. Repeat this exercise assuming:
   1. \mathsf {zero} is strict (i.e. \mathsf {zero}\ \bot = \bot )

      Solution.

      • Liam O'Connor

      \begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {succ}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {succ}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {succ}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {succ}\ \bot )), \bot \} \\ \end {array}
   2. \mathsf {succ} is strict (i.e. \mathsf {succ}\ \bot = \bot )

      Solution.

      • Liam O'Connor

      \begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {zero}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {zero}\ \bot )), \bot \} \\ \end {array}