Double Natural Recursion

Posted on 2018-01-01 by nbloomf
Tags: arithmetic-made-difficult, literate-haskell

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.


{-# LANGUAGE NoImplicitPrelude #-}
module DoubleNaturalRecursion (
  dnaturalRec, _test_dnaturalRec, main_dnaturalRec
) where

import Testing
import Booleans
import DisjointUnions
import NaturalNumbers

Today we’ll implement a slight generalization of natural recursion that allows recursion on two arguments.

[]{@#thm-dnatrec-zero-nat} Let \(A\) be a set. Let \(\delta : \nats \rightarrow A\), \(\psi : A \rightarrow A\), and \(\chi : \nats \times A \times A \rightarrow A\). Then there is a unique map \(Θ : \nats \times \nats \rightarrow A\) such that \[Θ(\zero,k) = \delta(k),\] \[Θ(\next(n),\zero) = \psi(Θ(n,\zero)),\] and \[Θ(\next(n),\next(k)) = \chi(k,Θ(n,k),Θ(n,\next(k))).\] We denote this map by \(\dnatrec(\delta)(\psi)(\chi).\)$

Define \(φ : A^\nats \rightarrow A^\nats\) casewise by \[\begin{eqnarray*} φ(g)(\zero) & = & \psi(g(\zero)) \\ φ(g)(\next(k)) & = & \chi(k,g(k),g(\next(k))). \end{eqnarray*}\] We then define \(Θ : \nats \times \nats \rightarrow A\) by \[Θ(n,k) = \natrec(\delta)(φ)(n)(k).\]

First we show that \(Θ\) satisfies the claimed equations. To this end, note that \[\begin{eqnarray*} & & Θ(\zero,k) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \natrec(\delta)(φ)(\zero)(k) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-zero} = & \delta(k) \end{eqnarray*}\] that \[\begin{eqnarray*} & & Θ(\next(n),\zero) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \natrec(\delta)(φ)(\next(n))(\zero) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & φ(\natrec(\delta)(φ)(n))(\zero) \\ & \hyp{φ(g)(\zero) = \psi(g(\zero))} = & \psi(\natrec(\delta)(φ)(n)(\zero)) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \psi(Θ(n,\zero)) \end{eqnarray*}\] and that \[\begin{eqnarray*} & & Θ(\next(n),\next(k)) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \natrec(\delta)(φ)(\next(n))(\next(k)) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & φ(\natrec(\delta)(φ)(n))(\next(k)) \\ & \hyp{φ(g)(\next(k)) = \chi(k,g(k),g(\next(k)))} = & \chi(k,\natrec(\delta)(φ)(n)(k),\natrec(\delta)(φ)(n)(\next(k))) \\ & \hyp{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \chi(k,Θ(n,k),\natrec(\delta)(φ)(n)(\next(k))) \\ & \hyp{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \chi(k,Θ(n,k),Θ(n,\next(k))) \end{eqnarray*}\] as claimed.

Next suppose \(\Psi : \nats \times \nats \rightarrow A\) also satisfies these equations. We show that \(\Psi = Θ\) by induction on \(n\). For the base case \(n = \zero\) for all \(k\) we have \[\begin{eqnarray*} & & \Psi(\zero,k) \\ & \hyp{\Psi(\zero,k) = \delta(k)} = & \delta(k) \\ & \hyp{Θ(\zero,k) = \delta(k)} = & Θ(\zero,k) \end{eqnarray*}\] as needed. For the inductive step, suppose \(\Psi(n,k) = Θ(n,k)\) for all \(k\) for some \(n\). Now let \(k \in \nats\). We have two possibilities; if \(k = \zero\), then \[\begin{eqnarray*} & & \Psi(\next(n),\zero) \\ & \hyp{\Psi(\next(n),\zero) = \psi(\Psi(n,\zero))} = & \psi(\Psi(n,\zero)) \\ & \hyp{Θ(n,\zero) = \Psi(n,\zero)} = & \psi(Θ(n,\zero)) \\ & \hyp{Θ(\next(n),\zero) = \psi(Θ(n,\zero))} = & Θ(\next(n),\zero) \end{eqnarray*}\] and if \(k = \next(m)\), we have \[\begin{eqnarray*} & & \Psi(\next(n),\next(m)) \\ & \hyp{\Psi(\next(n),\next(m)) = \chi(\next(m),\Psi(n,m),\Psi(n,\next(m)))} = & \chi(\next(m),\Psi(n,m),\Psi(n,\next(m))) \\ & \let{Θ(n,m) = \Psi(n,m)} = & \chi(\next(m),Θ(n,m),Θ(n,\next(m))) \\ & \hyp{Θ(\next(n),\next(m)) = \chi(\next(m),Θ(n,m),Θ(n,\next(m)))} = & Θ(\next(n),\next(m)) \end{eqnarray*}\] as needed.

Implementation

There’s a couple of ways to implement \(\dnatrec\).

dnaturalRec, dnaturalRec' :: (Natural n)
  => (n -> a)
  -> (a -> a)
  -> (n -> a -> a -> a)
  -> n -> n -> a

We can use the definition in the theorem:

dnaturalRec' delta psi chi = naturalRec delta phi
  where
    phi g k = case unnext k of
      Left () -> psi (g zero)
      Right m -> chi m (g m) (g (next m))

And there’s the definition from the universal property:

dnaturalRec delta psi chi n k = case unnext n of
  Left () -> delta k
  Right m -> case unnext k of
    Left () -> psi (dnaturalRec delta psi chi m zero)
    Right t -> chi t
      (dnaturalRec delta psi chi m t)
      (dnaturalRec delta psi chi m (next t))

While we’re here, we should test that these two implementations aren’t not equivalent.

_test_dnaturalRec_equiv
  :: (Natural n, Equal a)
  => n -> a
  -> Test ((n -> a) -> (a -> a) -> (n -> a -> a -> a) -> n -> n -> Bool)
_test_dnaturalRec_equiv _ _ =
  testName "dnaturalRec == dnaturalRec'" $
  \delta psi chi n k -> eq
    (dnaturalRec delta psi chi n k)
    (dnaturalRec' delta psi chi n k)

The “uniqueness” part of double natural recursion is also handy. To be a little more explicit, it says the following.

Let \(A\) be a set, with \(\delta : \nats \rightarrow A\), and \(\psi : A \rightarrow A\), and \(\chi : \nats \times A \times A \rightarrow A\). Then \(\dnatrec(\delta)(\psi)(\chi)\) is the unique solution \(f : \nats \times \nats \rightarrow A\) to the following system of functional equations for all \(n,k \in \nats\): \[\left\{\begin{array}{l} f(\zero,k) = \delta(k) \\ f(\next(n),\zero) = \psi(f(n,\zero)) \\ f(\next(n),\next(k)) = \chi(k,f(n,k),f(n,\next(k))) \end{array}\right.\]

Testing

Suite:

_test_dnaturalRec ::
  ( TypeName n, Show n, Equal n, Arbitrary n, CoArbitrary n, Natural n
  , CoArbitrary a, Arbitrary a, Show a, Equal a, TypeName a
  ) => Int -> Int -> n -> a -> IO ()
_test_dnaturalRec size cases n a = do
  testLabel2 "dnaturalRec" n a

  let args = testArgs size cases

  runTest args (_test_dnaturalRec_equiv n a)

Main:

main_dnaturalRec :: IO ()
main_dnaturalRec = do
  _test_dnaturalRec 10 50 (zero :: Unary) (zero :: Unary)
  _test_dnaturalRec 10 50 (zero :: Unary) (zero :: Unary)
  _test_dnaturalRec 10 50 (zero :: Unary) (true :: Bool)
  _test_dnaturalRec 10 50 (zero :: Unary) (true :: Bool)