REVISED: Thursday, February 8, 2024
Haskell Proofs.
1. HASKELL TYPE THEORY
Propositions are types. A type corresponds to a theorem if that type is inhabited. Every type is inhabited by the value undefined in Haskell.
Prelude> :type undefined
undefined :: a
Prelude>
If we work with a limited subset of Haskell's type system, and disallow polymorphic types, we have a consistent logic system. Hereafter it is assumed we are working in such a type system.
2. LAWS
Law of detachment called modus ponens or MP says if X is true then Y is true. X is true. Therefore Y is true. (A tautology is any sentence that must always be true.)
Law of the excluded middle says that every statement must be either true or false, never both or none.
3. DEFINITIONS
3.1. ALGORITHM
An algorithm is a step-by-step procedure or formula for calculations, problem-solving operations, or accomplishing a task in a certain number of steps.
3.2. ARGUMENT
An argument is an attempt to persuade someone of something, by giving reasons or evidence for accepting a particular conclusion.
3.3. AXIOMS
Assumptions are called axioms or postulates. They are basic truths we accept on faith to get a theory started.
3.4. CONJUNCTION "&&" AND
The Boolean "and".
Prelude> :type (&&)
(&&) :: Bool -> Bool -> Bool
Prelude>
If the first argument of a conjunction evaluates to False, then the conjunction evaluates to False; if the first argument evaluates to True, then the conjunction gets the same value as its second argument.
Another way of expressing a conjunction is to find a value that contains two sub-values: the first whose type corresponds to A, and the second whose type corresponds to B; for example, a Haskell tupple (a, b).
3.5. CONTRAPOSITIVE PROOF
If not q then not p.
3.6. CORROLARIES
When a theorem is proved, a few additional steps can produce one or more other theorems. Such a secondary theorem is called a corollary.
3.7. DEFINITION
A definition, an expression, is a well-defined and unambiguous unique interpretation or description of the essence of what is being defined.
Create a list of definitions, axioms, and postulates to use in your proof.
3.8. DIRECT PROOF
If p then q.
p is the antecedent or hypothesis.
An antecedent is a preceding event, condition, or cause.
A hypothesis is a proposition made as a basis for reasoning, without any assumption of its truth.
q is the consequence. For example, the cause p results in the effect q. Therefore, q is the resulting consequence.
3.9. DISJUNCTION "||" OR
The Boolean "or".
Prelude> :type (||)
(||) :: Bool -> Bool -> Bool
Prelude>
If the first argument of a disjunction evaluates to False, then the disjunction gets the same value as its second argument. If the first argument of a disjunction evaluates to True, then the disjunction evaluates to True.
Another way of expressing a disjunction is to find a value which contains either a value of type A or a value of type B; for example, Haskell Either A B.
Prelude> :type either
either :: (a -> c) -> (b -> c) -> Either a b -> c
Prelude>
3.10. EQUIVALENCE ==
Logical equivalence is similar to Haskell equality ==.
Prelude> :type (==)
(==) :: Eq a => a -> a -> Bool
Prelude>
3.11. GIVEN
You start your proof with what is given.
A given or a supposition, is something that is accepted or assumed to be true without proof.
A postulate is a statement that is assumed true without proof.
3.12. HYPOTHESIS
The hypothesis is what you can assume is true at the beginning of the proof. Therefore, we begin a proof by listing the hypothesis.
3.13. IMPLICATION "IF THEN"
An expression of the form P => Q (if P, then Q; Q if P) is called the implication of P and Q. P is the antecedent of the implication and Q the consequent.
If we want to implement implication in Haskell, we can do so in terms of if, then, not, and ||.
The Boolean otherwise is defined as the value True.
The only time an implication is False is when the antecedent is True and the consequent is False.
The only time an implication is False is when the antecedent is True and the consequent is False.
3.14. INDUCTION
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 value of n.
Step 2. Assume that the statement is true for n = k.
Step 3. Prove that the statement is true for n = k + 1.
Then it follows the statement must be true for all values of n.
3.15. LEMMAS
When the proof of a theorem involves many steps, it can help if we prove some preliminary theorems first, using them as stepping stones on the way to the final proof of the intended theorem. A minor theorem of this sort is called a lemma.
3.16. LOGICAL EQUIVALENCE
Logical equivalence is a type of relationship between two statements which translates verbally into "if and only if" and is symbolized by a double-lined, double arrow pointing to the left and right <=>.
3.17. MODUS PONENS
Modus ponens is a rule of inference which can be summarized as P implies Q and P is asserted to be true, so therefore Q must be true.
3.18. MODUS TOLLENS
Modus Tollens is the rule of logic stating that if a conditional statement ( if p then q ) is accepted, and the consequent does not hold ( not q ), then the negation of the antecedent ( not p ) can be inferred.
3.19. NEGATION "NOT"
A negation has the opposite truth value than that which is negated.
The Haskell equations f x y = ... used in the definition of a function f are genuine mathematical equations. They state that the left hand side and the right hand side of the equation have the same value.
Every statement that makes mathematical sense is either True or False.
Haskell uses True and False for the truth values. Together, these form the type Bool.
data means that we are defining a new data type. The part before the = denotes the type, which is Bool. The parts after the = are value constructors. They specify the different values that this type can have. The | is read as or. So we can read this as: the Bool type can have a value of True or False. Both the type name and the value constructors have to be capital cased.
data Bool = False | True
The Boolean "not".
Prelude> :type not
not :: Bool -> Bool
Prelude>
Prelude> not True
False
it :: Bool
Prelude>
Prelude> not False
True
it :: Bool
Prelude>
3.20. PROOF
A proof is a logical argument that establishes the truth of a statement.
When building a proof, be sure that your argument is clearly developed and that each step is supported by a property, theorem, postulate or definition.
3.21. PROOF BY CONTRADICTION
Assume not p and find contradiction.
3.22. PROPOSITIONS
The process of theory-building involves taking the definitions and axioms and putting them together according to the rules of logic. Statements we intend to prove are called propositions until their truth has been firmly established. A proposition is a statement that is either True for False.
A sentence, also called a proposition, is the smallest possible entity in propositional logic.
A hypotheses, also called a proposition, is a supposition or proposed explanation made on the basis of limited evidence as a starting point for further investigation.
A conjecture, also called a proposition, is an idea believed to be true, but not yet proven. Conjecture is a statement or hypothesis, an educated and reasonable guess based on observed patterns.
The outcome, or logic value, of an operation in propositional logic is always either True or False.
A truth table is a method of denoting all possible combinations of truth values for the variables in a proposition. The values for the individual variables, with all possible permutations, are shown in vertical columns at the left. The truth values for compound sentences, as they are built up from the single-variable (or atomic) propositions, are shown in horizontal rows.
3.23. PROVE
To prove is to demonstrate or establish that something, a proposition, is True.
Order of operations:
1. Parentheses
2. Not
3. And, &&, left to right.
4. Or, ||, left to right.
Equational Reasoning:
x + 0 = x -- Identity for addition.
x * 1 = x -- Identity for multiplication.
x + y = y + x -- Commutative
x * y = y * x -- Commutative
(x + y) + z = x + (y + z) -- Associative
(x * y) * z = x * (y * z) -- Associative
x * (y + z) = x * y + x * z -- Multiplication distributes over addition.
x + 0 = x -- Identity for addition.
x * 1 = x -- Identity for multiplication.
x + y = y + x -- Commutative
x * y = y * x -- Commutative
(x + y) + z = x + (y + z) -- Associative
(x * y) * z = x * (y * z) -- Associative
x * (y + z) = x * y + x * z -- Multiplication distributes over addition.
Haskell QuickCheck:
QuickCheck is a tool for testing Haskell programs automatically. The programmer provides a specification of the program, in the form of properties which functions should satisfy, and QuickCheck then tests that the properties hold in a large number of randomly generated cases.
3.24. Q.E.D.
When mathematicians finish proofs, they write “Q.E.D.” at the end. This is an abbreviation of the Latin phrase, "Quod erat demonstradum". It translates as, “Which was to be demonstrated".
A □ tombstone symbol is also often used to signify the end of a proof.
3.25. REDUCTIO AD ABSURDUM
Reductio ad absurdum is a method of proving the falsity of a premise by showing that its logical consequence is absurd or contradictory.
3.26. SETS
There are a very large number of sets; common sets are as follows:
ℂ is the set of complex numbers; ℂ = {a number of the form a+bi where a and b are real numbers and i is the square root of -1.}.
ℝ is the set of real numbers; ℝ = {any positive or negative number; e.g., π, e, √2}.
ℚ is the set of rational numbers; ℚ = {ratio of two integers; e.g., 1/2}.
ℤ is the set of integers; ℤ = {... -2, -1, 0, 1, 2, ...}.
ℕ is the set of natural numbers; ℕ = {1, 2, 3, 4, 5 ...}.
3.27. TAUTOLOGY
If you construct a truth table for a statement and all of the column values for the statement are true, then the statement is a tautology because it is always true.
3.28. THEOREMS
Once a proposition has been proved within the framework of a mathematical system, that proposition becomes a theorem.
3.29. TRIVIALITY
A trivial solution is an easy obvious solution. For example:
0n + 0n + 0n = 0n
Despite the simplicity of the trivial case, it should not be ignored.
4. HASKELL 'PALINDROME' PROOF
4.1. GIVEN
Hypothesis:
1. The character string "level".
2. Definition:
A palindrome is a word, phrase, or sequence that reads the same backward as forward.
4.2. TO BE PROVED
Proposition:
The character string "level" is a palindrome.
4.3. PROOF
Algorithm:
Let s equal the character string "level". Reverse the string s. Compare the original string s to the reversed string. Return True if and only if s reads the same backward as forward.
Prelude> let s = "level"
s :: [Char]
Prelude>
Prelude> let ispal s = s == reverse s
ispal :: Eq a => [a] -> Bool
Prelude>
Prelude> :type ispal
ispal :: Eq a => [a] -> Bool
Prelude>
Prelude> ispal s
True
it :: BoolPrelude>
Q.E.D.
5. HASKELL 'FUNCTIONS ARE EQUAL' PROOF
5.1. EXAMPLE 1
5.1.1 GIVEN
Hypothesis:
f x = ( 1 + x ) ^ 2
g x = x ^ 2 + 2 * x + 1
5.1.2. TO BE PROVED
Proposition:
f x == g x
5.1.3. PROOF
Algorithm:
Prelude> let f x = ( 1 + x ) ^ 2
f :: Num a => a -> aPrelude>
Prelude> :type f
f :: Num a => a -> a
Prelude> let g x = x ^ 2 + 2 * x + 1
g :: Num a => a -> a
Prelude>
Prelude> :type g
g :: Num a => a -> a
Prelude>
Prelude> let x = 9 -- Substituting any integer value for x; f x == g x
x :: Num a => a
Prelude>
Prelude> f x == g x
True
it :: Bool
Prelude>
Prelude>
Prelude> f x == g x
True
it :: Bool
Prelude>
Prelude> import Test.QuickCheck
Prelude>Prelude> let prop_fg x = f x == g x
prop_fg :: (Num a, Eq a) => a -> Bool
Prelude>
Prelude> quickCheck prop_fg
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package Win32-2.3.0.2 ... linking ... done.
Loading package old-locale-1.0.0.6 ... linking ... done.
Loading package time-1.4.2 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package pretty-1.1.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.6 ... linking ... done.
+++ OK, passed 100 tests.
it :: ()
Prelude>
Q.E.D.
5.2. EXAMPLE 2
5.2.1. GIVEN
Hypothesis:
f x = ( x ^ 2 ) / x
g x = x
5.2.2 TO BE PROVED
Proposition:
f x == g x
5.2.3. PROOF
Algorithm:
Prelude> let f x = ( x ^ 2 ) / x
f :: Fractional a => a -> aPrelude>
Prelude> :type f
f :: Fractional a => a -> a
Prelude>Prelude> let g x = x
g :: t -> t
Prelude>
Prelude> :type g
g :: t -> t
Prelude>
Prelude> let x = 3 -- Substituting any integer value for x; f x == g x; EXCEPT FOR 0
x :: Num a => a
Prelude>
Prelude> f x == g x
True
it :: Bool
Prelude>
Prelude>
Prelude> f x == g x
True
it :: Bool
Prelude>
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude>
Prelude> import Test.QuickCheck
Prelude>
Prelude> let f x = (x^2) / x
f :: Fractional a => a -> a
Prelude>
Prelude> let g x = x
g :: t -> t
Prelude>
Prelude> let prop_fg x = f x == g x
prop_fg :: (Fractional a, Eq a) => a -> Bool
Prelude>
Prelude> quickCheck prop_fg
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package Win32-2.3.0.2 ... linking ... done.
Loading package old-locale-1.0.0.6 ... linking ... done.
Loading package time-1.4.2 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package pretty-1.1.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.6 ... linking ... done.
*** Failed! Falsifiable (after 1 test):
0.0
it :: ()
Prelude>
The proof failed because of division by zero!
Substituting zero for x in g x = x is no problem.
Substituting zero for x in f x = (x^2) / x results in a division by zero error!
Prelude> f x == g x
True
it :: Bool
Prelude>
The above was misleading because it referred only to x = 3.
This is proof QuickCheck is a tool you should take the time to learn how to use.
6. CONCLUSION
In this tutorial, you have received an introduction to Haskell proofs.
7. 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.
Doets K. & Van Eijck J. (2004). The Haskell Road to Logic, Maths and Programming. Second Edition. Norcross, Georgia: College Publications, Inc.
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.
