0

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?

Patrick Browne
  • 521
  • 2
  • 10
  • 2
    Why do you handle the $n=1$ case with an if statement instead of pattern matching? – md2perpe Aug 11 '21 at 16:06
  • @md2perpe Yes, of course that would be the more uniform way. But I want to understand how to represent the definition using a mixed approach. – Patrick Browne Aug 11 '21 at 16:29
  • 1
    In programming different implementation might have very different behavior when it comes to running time and memory use. But in mathematics such things don't matter; it's only the final value that matters. – md2perpe Aug 11 '21 at 18:03

1 Answers1

2

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$

md2perpe
  • 26,770