REVISED: Monday, October 28, 2024
1. INTRODUCTION
Haskell Functions as Mathematical Functions
In Haskell, functions are conceptualized as mathematical functions, mapping inputs to outputs. This means they take one or more values as arguments and produce a single result.
Pure Functions
Haskell functions are inherently pure, meaning they have the following properties:
No side effects: They don't modify external state or produce observable effects beyond their return value.
Referential transparency: Replacing a function call with its result doesn't change the program's behavior.
First-Class Citizens
Functions in Haskell are first-class citizens, treated like any other data type:
Passed as arguments: You can pass functions as arguments to other functions.
Returned as values: Functions can return other functions as results.
Assigned to variables: You can store functions in variables.
Syntax and Types
Definition: Functions are defined using the = operator.
Type annotation: The type of a function is specified after its name, using ::. For example, f :: Int -> Int indicates that f takes an integer as input and returns an integer.
Arguments: Multiple arguments are separated by spaces.
Return value: The return value is the expression on the right side of the = operator.
Examples
Simple function:
add :: Num a => a -> a -> a
add x y = x + y
Function taking multiple arguments:
multiply :: Num a => a -> a -> a -> a
multiply x y z = x * y * z
Function returning a function:
makeAdder :: Num a => a -> a -> a
makeAdder x = (\y -> x + y)
Higher-Order Functions
Haskell supports higher-order functions, taking functions as arguments or returning functions as results. This enables powerful programming techniques like:
Map: Applies a function to each element of a list.
map :: (a -> b) -> [a] -> [b]
Filter: Selects elements from a list based on a predicate function.
filter :: (a -> Bool) -> [a] -> [a]
Reduce: Combines elements of a list using a binary function.
reduce :: Integral a => a -> a -> Ratio a
Recursion
Recursion is a common programming technique in Haskell, where a function calls itself to solve smaller instances of a problem. Haskell's type system and pattern matching make it well-suited for recursive functions.
Benefits of Haskell Functions
Readability: Haskell's functional style and concise syntax make code more readable and easier to understand.
Correctness: Pure functions are easier to reason about and test for correctness.
Concurrency: Haskell's functional nature makes it well-suited for concurrent programming.
Modularity: Functions can be composed to build complex programs from smaller, reusable components.
By understanding these concepts, you can effectively use Haskell functions to write elegant, efficient, and maintainable code.
2. PROOFS
Computer program function proofs are mathematical proofs partially or fully generated by a computer program.
You can evaluate (prove) Integer arithmetic; however, computers still have problems with Floating-Point arithmetic.
Before assuming a Lemma check it with QuickCheck.
A function algorithm proof is a step-by-step procedure or formula for calculations, problem-solving operations, or accomplishing a task in a certain number of steps.
There are four basic proof techniques used in mathematics: Direct Proof, Proof by Contradiction, Proof by Induction, and Proof by Contrapositive.
PROOF BY INDUCTION EXAMPLE
Proving a recursion reverse function:
sum (reverse []) = sum [] -- def reverse base case
sum (reverse (x:xs)) = sum (reverse xs ++ [x]) -- def reverse recursion
Base Case:
sum (reverse []) = sum []
This follows directly from the definition of reverse and sum.
Recursive Case:
Inductive Hypothesis: Assume that sum (reverse ys) = sum ys for all lists ys.
Inductive Steps:
sum (reverse (x:xs)) = sum (reverse xs ++ [x]) -- definition of `reverse`
sum (reverse (x:xs)) = sum (reverse xs) + sum [x] -- lemma (proven below separately)
sum (reverse (x:xs)) = sum xs + sum [x] -- inductive hypothesis
sum (reverse (x:xs)) = sum xs + x -- definition of `sum`
sum (reverse (x:xs)) = sum (x:xs) -- definition of `sum`
Key Points:
The proof relies on a strong inductive hypothesis and a correctly proven lemma.
The commutativity of sum is implicitly used, a direct consequence of the definition.
A formal proof of the lemma enhances the rigor of the overall proof.
LEMMA PROOF
The lemma can be proven using the definition of sum and induction on the length of xs.
Proving the Lemma: sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]
Proof by Induction on the Length of xs:
Base Case:
When xs = []:
sum (reverse [] ++ [x]) = sum ([x]) = x
sum (reverse []) + sum [x] = sum [] + sum [x] = 0 + x = x
Thus, the equation holds for the base case.
Recursive Case:
Inductive Hypothesis: Assume the equation holds for a list xs of length n. That is:
sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]
Inductive Steps:
Consider a list (y:xs) of length n+1:
sum (reverse (y:xs) ++ [x])
= sum (reverse xs ++ [y] ++ [x]) -- Definition of `reverse`
= sum (reverse xs ++ [y + x]) -- Definition of `++` and `sum`
= sum (reverse xs) + sum [y + x] -- Inductive Hypothesis
= sum (reverse xs) + (y + x) -- Definition of `sum`
= (sum (reverse xs) + y) + x -- Associativity of `+`
= (sum (reverse xs) + sum [y]) + x -- Definition of `sum`
= sum (reverse xs) + (sum [y] + x) -- Associativity of `+`
= sum (reverse xs) + sum [y, x] -- Definition of `sum` and `++`
= sum (reverse xs) + sum [x, y] -- Commutativity of `+`
= sum (reverse xs) + sum [x] + sum [y] -- Definition of `sum`
= sum (reverse xs) + sum [x] -- Definition of `sum` for a singleton list
Therefore, by the principle of mathematical induction, the lemma holds for all lists xs.
3. CONCLUSION
4. 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.
