How to represent/specify this Haskell function in mathematical and logical notation

logicnotationprogramming

Below is a Haskell function definition that computes the $nth$ Fibonancci number.

fib :: Int  -> Int  
fib 0  = 0  -- equation 1   
fib n  = if n == 1 then 1 else      
   (fib (n - 1) + fib (n - 2))  -- equation 2

The definition is a mixture of pattern matching (equation 1) and an if_then_else function (equation 2). This is a rather unnatural way to write this function. But I am wondering is there a notational way to combine pattern matching and if_then_else ? See related question.

Here is my attempt to represent/specify the Haskell code as a mathematical function:
\begin{align*}
\forall n \colon \mathbb{Z}~~~fib(n) \triangleq \left\{ \begin{array}{rl}
0, & n = 0\\
fib (n)\triangleq\left\{ \begin{array}{rl}
1, & n = 1\\
fib(n – 1)+fib(n – 2), & otherwise\\
\end{array}\right.
\end{array}\right.
\end{align*}

Here is my attempt to represent/specify the Haskell code in first order logic, with equality:
\begin{align*}
(\forall n \colon \mathbb{Z} \colon ((n=0) \implies (fib(n) = 0))) \land \\
(\forall n \colon \mathbb{Z} \colon ((n=1) \implies (fib(n) = 1))) \land \\
(\forall n \colon \mathbb{Z} \colon (\neg((n=1) \lor (n=0)) \implies (fib(n) = fib(n – 1)+fib(n – 2))))
\end{align*}

Questions: Are these attempts reasonable? Can they be improved?

Best Answer

One could write it as $$ \mathsf{fib}(n) = \begin{cases} 0 & \text{if $n=0$}, \\ 1 & \text{if $n=1$}, \\ \mathsf{fib}(n-2)+\mathsf{fib}(n-1) & \text{otherwise}. \\ \end{cases} $$

A mathematician would normally write something like $F_0=0,\ F_1=1,\ F_n=F_{n-2}+F_{n-1}$ for $n=2,3,4,\ldots$

Related Question