Learning Outcomes
by the End of the Lecture, Students that Complete

the Recommended Exercises should be Able to:
Implement some Simple s Define Equational Reasoning / Referential Transparency Demonstrate How Haskell performs Evaluation Use Property-Testing to Support Claims of Correctness

Chapter 2: “Ready, set, go!” “Baby’s first functions”

Expression Notation
Expressions can be Represented using Tree Structures, with Operations and Operands as Internal and External Nodes (respectively)
Infix, Prefix, and Postfix are Different Notations that can be Used to Write Equivalent Expressions
(n.b., you are probably already familiar with the corresponding tree traversals)

Expression Notation
in Infix, Binary Operators appear Between Operands, Unary Operators typically appear Before, and Higher- Arity Operators use Multiple Symbols (e.g., 𝑎 ? 𝑏 ∶ 𝑐)

Expression Notation
in Prefix, All Operators appear Before the Operands, and if the Operators have Fixed Arity, the Need for Parentheses is essentially Eliminated

Executing s
Natural Languages
Algorithm Design
Pseudocode / Flowchart
Programming
Programming Languages
Compilation / Interpretation
Machine Languages

Executing s
Compilers are Programs that Translate Source Code into Machine Code for Execution
n.b., Glasgow (GHC) is a
Interpreters are Programs that Directly Execute Instructions without compilation
n.b., Glasgow Interactive (GHCi) is a

toBinary :: Int -> [Char] toBinary 0 = [‘0’] toBinary n
| (mod n 2 == 1) = toBinary (div n 2) ++ [‘1’]
| otherwise = toBinary (div n 2) ++ [‘0’]
countOnes :: [Char] -> Int countOnes [] = 0
countOnes n
| (head n == ‘1’) = countOnes (tail n) + 1 | otherwise = countOnes (tail n)
isEven :: Int -> Bool
isEven n = (mod n 2 == 0)
isEvil :: Int -> Bool
isEvil n = isEven (countOnes (toBinary n))

Basics a Definition Associates a Name with a Type
name :: Type name = Expression
a Function Definition also Describes the Parameters name :: Type1 -> Type2 -> Type3 -> Type
name = parameter1 parameter2 parameter3 = result
n.b., there is no symbol separating parameter and return types … more on this later

Evaluation
Consider the following Sample Program: double :: Integer -> Integer
double n = 2 * n
With that Definition, How would the Interpreter Evaluate the following Expression?
32 – (double (1 + 2))

Evaluation
double :: Integer -> Integer double n = 2 * n
32 – (double (1 + 2))
32 – (2 * (1 + 2))
32 – (2 * 3) 32 – 6

Evaluation
each Subexpression is a Reducible Expression and Evaluation is the Process of Reducing
a Redex to a Simpler Equivalent Form
in Haskell, Evaluation can be Traced by Replacing Redexes using the Body of the Function Definition and Substituting Arguments for Parameters
n.b., this should be reminiscent of the β-Reduction process in λ-Calculus

Evaluation
double :: Integer -> Integer
double n = 2 * n
32 – (double (1 + 2))
Replace double n With 2 * n For Whatever n

Evaluation
double :: Integer -> Integer
double n = 2 * n
32 – (double (1 + 2))
Replace double n With 2 * n For Whatever n
32 – (2 * (1 + 2)) 32 – (2 * 3)

Equational Reasoning
Haskell has Referential Transparency, meaning that Every Function Call with the Same Argument is Guaranteed to Produce the Same Result
this, allows Definitions to be Used as though they were Logical Equivalences, Set Identities, or any other Mathematical “Law”

𝑝→ 𝑝∨𝑞 ¬𝑝 ∨ 𝑝 ∨ 𝑞
¬𝑝 ∨ 𝑝 ∨ 𝑞 𝑡𝑟𝑢𝑒 ∨ 𝑞
by the Implication equivalence by the Associativity equivalence by the Negation equivalence
by the Commutativity equivalence by the Domination equivalence
Equational Reasoning

Equational Reasoning
that was an Example of Equational Reasoning – each Step was simply Replacing Something with Something Else that is Known to be Equal
since Haskell is Referentially Transparent, this Equational Reasoning is Possible with Source Code written in Haskell as well

strike you as Unusual?
32 – (double (1 + 2)) 32 – (2 * (1 + 2)) 32 – (2 * 3)

because it was Not Necessary for (1+2) to
be Evaluated Before performing the Substitution double n = 2 * n, Evaluation
with Lazy Evaluators (like Haskell) Expressions are Not Evaluated Until their Results are Needed, meaning Arguments are Not Evaluated Before they are Passed
Lazy Evaluation

square :: Integer -> Integer square n = n * n
double :: Integer -> Integer double n = 2 * n
With this Definition, How would the Evaluate the following Expression?
double (square 2)
Lazy Evaluation

Lazy Evaluation the Order for Replacing Redexes is
Language Dependent
double (square 2)
in Python, or Java, Evaluate: in Haskell, Evaluate:

Ensuring the Validity of a Program often requires Test Cases (i.e., Cases with Expected Responses designed to ensure a program is Operating Correctly)
a More Powerful approach is Property-Testing, where Assertions are made about Program Behaviour and Tested using lots of Randomly-Generated Inputs
Property Testing

Even More Powerful that Property Testing is the Development of Proofs (which is, in fact, Much Easier in Functional Programming)
Property Testing
Test Cases Property Testing Formal Proofs (n.b., the blue regions are cases where the program is known to function correctly)

Property Testing an Example of a Property is
“the Double of an Integer n is the Sum n + n” double :: Integer -> Integer
double n = 2 * n
testDouble :: Integer -> Bool testDouble n = (double n == n + n)