REVISED: Thursday, February 8, 2024
1. INTRODUCTION
This tutorial introduces using Haskell for proof by Mathematical Induction that the left hand side (LHS) of an infinite equation equals the right hand side (RHS).
Recursive proofs are called induction. Mathematical Induction is a method of formal proof in which a statement is proved for one step in a process, and it is shown that if the statement holds for that step, it holds for the next. The beauty of induction is that it allows a theorem to be proven true where an infinite number of cases exist without exploring each case individually.
Step 1. Show that the statement is true for the initial lowest value of n, which is often n = 1.
Step 2. Assume that the statement is true for n = k.
Step 3. Use the assumption in "Step 2." to prove that the statement is true for n = k + 1.
Then it follows the statement must be true for all values of n.
2. GHCi RUN
GHCi, version 9.8.1: http://www.haskell.org/ghc/ :? for help
Prelude> :l mathematicalInduction
[1 of 1] Compiling Main ( mathematicalInduction.hs, interpreted )
Ok, modules loaded: Main.
*Main> main
==========================================================
Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction.
Step 1: Show it is True for n = 1.
LHS = 2*n and RHS = n*(n+1).
LHS = 2 and RHS = 2.
LHS = RHS; therefore, it is True for n = 1.
==========================================================
Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction.
Step 2: Assume it is True for n = k.
That is: 2 + 4 + 6 +...+ (2*k) = k*(k+1).
==========================================================
Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction.
Step 3: Show it is True for n = k + 1.
That is: 2 + 4 + 6 +...+ (2 * k) + 2 * (k + 1) = (k + 1) * (k + 2).
LHS = 2 + 4 + 6 + ... + (2 * k) + 2 * (k + 1)
= k * (k + 1) + 2 * (k + 1)
= (k + 1) * ( (k * 1) + (2 * 1))
= (k + 1) * (k + 2) = RHS
Therefore, it is True for n = k + 1.
Therefore, the statement is True for n >= 1.
Q.E.D.
==========================================================
*Main>
3. HASKELL PROGRAM
The Haskell program is as follows:
-- C:\Users\Tinnel\Haskell2024\mathematicalInduction.hs
{-
LHS is left hand side of the = sign.
RHS is right hand side of the = sign.
Prove 2+4+6+...+(2*n) = n * (n+1) by mathematical induction.
Step 1. Show that the statement is true for the initial value of n = 1.
LHS = 2 * 1 = 2
RHS = 1 * (1 + 1) = 2
LHS == RHS
-}
import System.IO
import Data.List
l :: Num t => t
l = 1
r :: Num t => t
r = 1
lHs :: Num a => a -> a
lHs l = 2 * l
rHs :: Num a => a -> a
rHs r = r * (r + 1)
main :: IO ()
main = do { putStrLn "" -- putStrLn Has type I/O action.
; putStrLn "=========================================================="
; putStrLn ""
; putStrLn "Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction."
; putStrLn ""
; putStrLn "Step 1: Show it is True for n = 1."
; putStrLn ""
; putStrLn ("LHS = 2*n and " ++ "RHS = n*(n+1).")
; putStrLn ""
; let lS = show (lHs l) -- Type converted from Integer z to String z.
; let rS = show (rHs r) -- Type converted from Integer z to String z.
; putStrLn ("LHS = " ++ lS ++ " and RHS = " ++ rS ++ ".")
; putStrLn ""
; let i = if (lHs l == rHs r) then "True" else "False"
; putStrLn ("LHS = RHS; therefore, it is " ++ i ++ " for n = 1.")
; putStrLn ""
; putStrLn "=========================================================="
; putStrLn ""
; putStrLn "Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction."
; putStrLn ""
; putStrLn "Step 2: Assume it is True for n = k."
; putStrLn ""
; putStrLn "That is: 2 + 4 + 6 +...+ (2*k) = k*(k+1)."
; putStrLn ""
; putStrLn "=========================================================="
; putStrLn ""
; putStrLn "Prove: 2 + 4 + 6 +...+ (2*n) = n*(n+1) by mathematical induction."
; putStrLn ""
; putStrLn "Step 3: Show it is True for n = k + 1."
; putStrLn ""
; putStrLn "That is: 2 + 4 + 6 +...+ (2 * k) + 2 * (k + 1) = (k + 1) * (k + 2)."
; putStrLn ""
; putStrLn "LHS = 2 + 4 + 6 + ... + (2 * k) + 2 * (k + 1)"
; putStrLn ""
; putStrLn "= k * (k + 1) + 2 * (k + 1)"
; putStrLn ""
; putStrLn "= (k + 1) * ( (k * 1) + (2 * 1))"
; putStrLn ""
; putStrLn "= (k + 1) * (k + 2) = RHS"
; putStrLn ""
; putStrLn "Therefore, it is True for n = k + 1."
; putStrLn ""
; putStrLn "Therefore, the statement is True for n >= 1."
; putStrLn ""
; putStrLn "Q.E.D."
; putStrLn ""
; putStrLn "=========================================================="
; putStrLn ""
}
--
4. CONCLUSION
Using Haskell and Mathematical Induction we have proven 2+4+6+...+(2*n) = n * (n+1).
5. REFERENCES
Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.
Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.
Goerzen, J. & O'Sullivan, B. & Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.
Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.
Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.
Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.
