The two constructors encode a natural number by its number of successors. Structural recursion replaces the zero constructor by zero and every successor by one addition:
convert :: Natural -> Integer
convert Zero = 0
convert (Succ n) = 1 + convert nStructural induction gives . The output uses unbounded integers, so there is no machine-word overflow.
Recurse on the first argument for addition and multiplication, and on the exponent for exponentiation:
add :: Natural -> Natural -> Natural
add Zero n = n
add (Succ m) n = Succ (add m n)
mul :: Natural -> Natural -> Natural
mul Zero n = Zero
mul (Succ m) n = add n (mul m n)
power :: Natural -> Natural -> Natural
power m Zero = Succ Zero
power m (Succ n) = mul m (power m n)The defining arithmetic identities areEach recursive call consumes one constructor. The base of exponentiation makes
power Zero Zero equal to one, the empty-product convention. Applying convert and using structural induction verifies all three operations.The base value can have any type
a. The recursive result has that same type, so the step must accept and return a. Thus the most general polymorphic type signature of the natural-number fold isfoldNat :: (a -> a) -> a -> Natural -> aIn mathematical type notation, . No equality, ordering or numeric constraint is needed: the natural-number fold manipulates constructors, rather than performing arithmetic on the result.
A natural-number fold iterates its first argument once per successor. For addition, iterate
Succ starting at the other operand; for multiplication, iterate addition starting at zero; for exponentiation, iterate multiplication starting at one:addF :: Natural -> Natural -> Natural
addF m n = foldNat Succ n m
mulF :: Natural -> Natural -> Natural
mulF m n = foldNat (addF n) Zero m
powerF :: Natural -> Natural -> Natural
powerF m n = foldNat (mulF m) (Succ Zero) nThe common identity is , with interpreted through
convert. Substituting each step and seed reproduces the recursive arithmetic equations of part (b).Keep the two adjacent Fibonacci numbers in one shared pair. From the Fibonacci recurrence, if the current pair is , the next is . This gives the paired Fibonacci recurrence:
twoFibs :: Integer -> (Integer, Integer)
twoFibs 0 = (0, 1)
twoFibs n
| n > 0 = let (a, b) = twoFibs (n - 1)
in (b, a + b)
| otherwise = error "negative Fibonacci index"
fib :: Integer -> Integer
fib = fst . twoFibsThe pair pattern shares the result of the single recursive call. Mathematical induction establishesThere are pair updates and additions, rather than the repeated subcomputations of the original branching recursion. This is linear arithmetic-operation count; exact Fibonacci numbers have growing bit length. The pattern
fib (n+2) in the source expresses the recurrence; the guarded definition above uses ordinary Haskell syntax without requiring an n+k pattern extension.Let . The equations derived in part (e) become and , where . Replacing zero and successor by that seed and step is exactly a natural-number fold:
twoFibsNat :: Natural -> (Integer, Integer)
twoFibsNat = foldNat step (0, 1)
where
step :: (Integer, Integer) -> (Integer, Integer)
step (a, b) = (b, a + b)
fibNat :: Natural -> Integer
fibNat = fst . twoFibsNatConsequentlyStructural induction follows the constructors of
Natural: the seed gives the first two Fibonacci numbers, and the successor step uses the Fibonacci recurrence. The extra component carries exactly the information needed for the next update. Articles by others on the same topic
There are currently no matching articles.