Can these Haskell operations be presented as piecewise mathematical functions

functionsnotationprogrammingrecursion

I am researching the idea from O'Donnell,Hall and Page that

Haskell serves both as a formal, mathematical notation, and as a
practical and powerful programming language

See also the The Haskell Road to Logic, Maths and Programming by
Jan van Eijck.

Given the Haskell code in Listing 1, is it possible to represent the two operations $\mathsf{eq}$ and $\mathsf{plus}$ as piecewise mathematical functions?

Listing 1

    -- Peano numbers
    data Nat = Zero | Suc Nat deriving Show 
    -- Equality
    eq :: Nat -> Nat -> Bool
    eq Zero Zero = True
    eq (Suc x) (Suc y) = eq x y
    eq _ _ = False
    
    plus :: Nat -> Nat -> Nat
    plus x Zero =  x
    plus x (Suc y) = Suc (plus x y)

My assumption is that patterns in Haskell function definitions are like mathematical piecewise functions. The arguments on left hand side of each Haskell equation, when compared to some value, represents the condition for each mathematical case. Here are my attempts:

\begin{align*}
\forall x,y \in \mathbb{N}~ \colon \mathsf{eq}(x,y) = \begin{cases}
True & \text{if $x=Zero \land y=Zero$}, \\
\mathsf{eq}(x',y') & \text{if $ x = \mathsf{Suc}(x') \land y = \mathsf{Suc}(y')$}, \\
False & \text{otherwise}. \\
\end{cases}
\end{align*}

\begin{align*}
\forall x,y \in \mathbb{N} ~\colon \mathsf{plus}(x,y) = \begin{cases}
x & \text{if $y=Zero$}, \\
\mathsf{Suc}(\mathsf{plus}(x,y')) & \text{if $y = \mathsf{Suc}(y')$}. \\
\end{cases}
\end{align*}

Are these attempts reasonable? Are there alternative mathematical notations for these recursive function definitions?

Best Answer

You can write it like that, though the version you will find in most texts in mathematical logic is simply

$$ \begin{align} x + 0 &= x \\ x + Sy &= S(x+y) \end{align} $$

which looks a lot more like the Haskell definition of plus. This is no coincidence: the origin of Haskell's pattern-matching function definitions is a wish to mimic existing mathematical notation.

The big-curly-bracket notation in mathematics corresponds more directly to Haskell's notion of guards.

The situation with eq is not as straightforward. Again your attempt is not wrong, but it doesn't really look like idiomatic mathematics.

This is mostly the fault of the mathematical tradition that insists on distinguishing syntactically between claims (which can either be true or not) and expressions (which produce values). Programming languages tend to consider such a distinction superfluous and just handle claims as expressions that happen to produce truth values as results.

In most mathematical contexts, one wouldn't even attempt to write the eq purely symbolically, but would instead use prose, something like

The relation $\equiv$ is defined recursively by

  1. $0\equiv0$.
  2. $Sx \equiv Sy$ iff $x\equiv y$.
  3. Nothing else is related by $\equiv$.

In theoretical computer science, sitting halfway between mathematics and programming, it is common to notate such definitions symbolically as an inference system which looks like

$$ \frac{}{0 \equiv 0} \qquad \frac{x\equiv y}{Sx\equiv Sy} $$

But this will not be generally recognized by most non-logician mathematicians.

Related Question