1Types and Type Based Analysis:
Lambda Calculus, Intro to Haskell
1
Announcements
n Quiz 4 on Abstract Interpretation
n HW5 is out
n Moving on to Types and Type-based
Analysis
n Have a great Spring break!
Program Analysis CSCI 4450/6450, A Milanova 2
2
2Overview
3
Program Execution: Signs Analysis:
xà1,yà-1,zà2
Lattice 2Z
|[x=y+z]|({(1,-1,2),(0,1,2),…})
=
{(1,-1,2),(…),…}
xà+,yà-,zà+
Signs Lattice
γ
α
|[x=y+z]|( (+, -, +) )
=
(T, -, 0)
3
Outline
n Pure lambda calculus, a review
n Syntax and semantics
n Free and bound variables
n Rules (alpha rule, beta rule)
n Normal forms
n Reduction strategies
n Interpreters for the Lambda calculus
n Coding them in Haskell
Program Analysis CSCI 4450/6450, A Milanova 4
4
3Lambda Calculus
n A theory of functions
n Theory behind functional programming
n Turing-complete: any computable function can
be expressed and evaluated using the calculus
n Lambda (l) calculus expresses function
definition and function application
n f(x)=x*x becomes lx. x*x
n g(x)=x+1 becomes lx. x+1
n f(5) becomes (lx. x*x) 5 à 5*5à 25
Program Analysis CSCI 4450/6450, A Milanova 5
5
Program Analysis CSCI 4450/6450, A Milanova/BG Ryder 6
Syntax of Pure Lambda Calculus
n l-calculus formulae (e.g., lx. x y) are called
expressions or terms
n E ::= x | ( lx. E1 ) | ( E1 E2 )
n A l-expression is one of
n Variable: x
n Abstraction (i.e., function definition): lx. E1
n Application: E1 E2
6
4Program Analysis CSCI 4450/6450, A Milanova/BG Ryder 7
Syntactic Conventions
n Parentheses may be dropped from “stand-
alone” terms ( E1 E2 ) and ( lx. E )
n E.g., ( f x ) may be written as f x
n Function application groups from left-to-right
(i.e., it is left-associative)
n E.g., x y z abbreviates ( ( x y ) z )
n E.g., E1 E2 E3 E4 abbreviates ( ( ( E1 E2 ) E3 ) E4 )
n Parentheses in x (y z) are necessary! Why?
7
8
Syntactic Conventions
n Application has higher precedence than
abstraction
n Another way to say this is that the scope of the
dot extends as far to the right as possible
n E.g., lx. x z = lx. ( x z ) = ( lx. ( x z ) ) =
( lx. (x z) ) ≠ ( ( lx. x ) z )
n WARNING: This is the most common
syntactic convention (e.g., Pierce 2002).
However, some books give abstraction
higher precedence; you might have seen that
different convention
8
5Semantics of Lambda Calculus
n An expression has as its meaning the value
that results after evaluation is carried out
n Somewhat informally, evaluation is the
process of reducing expressions
E.g., (lx.ly. x + y) 3 2 à (ly. 3 + y) 2 à 3 + 2 = 5
(Note: this example is just an informal illustration.
There is no + in the pure lambda calculus!)
9
9
Program Analysis CSCI 4450/6450, A Milanova 10
Free and Bound Variables
n Abstraction ( lx. E ) is also referred as binding
n Variable x is said to be bound in lx. E
n The set of free variables of E is the set of
variables that appear unbound in E
n Defined by cases on E
n Var x:
n App E1 E2:
n Abs lx. E:
free(x) = {x}
free(E1 E2) = free(E1) U free(E2)
free(lx.E) = free(E) - {x}
10
611
Free and Bound Variables
n A variable x is bound if it is in the scope of a
lambda abstraction: as in lx. E
n Variable is free otherwise
1. (lx. x) y
2. (lz. z z) (lx. x)
Program Analysis CSCI 4450/6450, A Milanova
11
12
Free and Bound Variables
3. lx.ly.lz. x z (y (lu. u))
Program Analysis CSCI 4450/6450, A Milanova
12
713
Free and Bound Variables
n We must take free and bound variables into
account when reducing expressions
E.g., (lx.ly. x y) (y w)
n First, rename bound y in ly. x y to z: lz. x z
(lx.ly. x y) (y w)à (lx.lz. x z) (y w)
n Second, apply the reduction rule that substitutes
(y w) for x in the body ( lz. x z )
( lz. x z ) [(y w)/x] à ( lz. (y w) z ) = lz. y w z
13
14
Substitution, formally
n (lx.E) M à E[M/x] replaces all free occurrences
of x in E by M
n E[M/x] is defined by cases on E:
n Var: y[M/x] =
y[M/x] =
n App: (E1 E2)[M/x] =
n Abs: (ly.E1)[M/x] =
(ly.E1)[M/x] =
Program Analysis CSCI 4450/6450, A Milanova
M if x = y
y otherwise
(E1[M/x] E2[M/x])
(ly.E1) if x = y
lz.((E1[z/y])[M/x]) otherwise,
where z NOT in free(E1) U free(M) U {x}
14
8Substitution, formally
(lx.ly. x y) (y w)
à (ly. x y)[(y w)/x]
à l1_. ( ((x y)[1_/y])[(y w)/x] )
à l1_. ( (x 1_)[(y w)/x] )
à l1_. ( (y w) 1_ )
à l1_. y w 1_
You will have to implement precisely this
substitution algorithm in Haskell
Program Analysis CSCI 4450/6450, A Milanova 15
15
Program Analysis CSCI 4450/6450, A Milanova 16
Rules (Axioms) of Lambda
Calculus
n a rule (a-conversion): renaming of parameter
(choice of parameter name does not matter)
n lx. E àa lz. (E[z/x]) provided z is not free in E
n e.g., lx. x x is the same as lz. z z
n b rule (b-reduction): function application
(substitutes argument for parameter)
n (lx.E) M àb E[M/x]
Note: E[M/x] as defined on previous slide!
n e.g., (lx. x) z àb z
16
9Program Analysis CSCI 4450/6450, A Milanova 17
Rules of Lambda Calculus:
Exercises
n Reduce
(lx. x) y à ?
(lx. x) (ly. y) à ?
(lx.ly.lz. x z (y z)) (lu. u) (lv. v) à ?
17
Program Analysis CSCI 4450/6450, A Milanova 18
Rules of Lambda Calculus:
Exercises
(lx.ly.lz. x z (y z)) (lu. u) (lv. v) àab
18
10
Program Analysis CSCI 4450/6450, A Milanova 19
Reductions
n An expression ( lx.E ) M is called a redex
(for reducible expression)
n An expression is in normal form if it cannot
be β-reduced
n The normal form is the meaning of the term,
the “answer”
19
Definitions of Normal Form
n Normal form (NF): a term without redexes
n Head normal form (HNF)
n x is in HNF
n (lx. E) is in HNF if E is in HNF
n (x E1 E2 … En) is in HNF
n Weak head normal form (WHNF)
n x is in WHNF
n (lx. E) is in WHNF
n (x E1 E2 … En) is in WHNF
Program Analysis CSCI 4450/6450, A Milanova (from MIT’s 2015 Program Analysis OCW) 20
20
11
Questions
n lz. z z is in NF, HNF, or WHNF?
n (lz. z z) (lx. x) is in?
n lx.ly.lz. x z (y (lu. u)) is in?
n (lx.ly. x) z ((lx. z x) (lx. z x)) is in?
n z ((lx. z x) (lx. z x)) is in?
n (lz.(lx.ly. x) z ((lx. z x) (lx. z x))) is in?
Program Analysis CSCI 4450/6450, A Milanova 21
21
Simple Reduction Exercise
n C = lx.ly.lf. f x y
n H = lf. f (lx.ly. x) T = lf. f (lx.ly. y)
n What is H (C a b)?
à (lf. f (lx.ly. x)) (C a b)
à (C a b) (lx.ly. x)
à ((lx.ly.lf. f x y) a b) (lx.ly. x)
à (lf. f a b) (lx.ly. x)
à (lx.ly. x) a b
à a CSCI 4450/6450, A Milanova (from MIT 2015 Program Analysis OCW) 22
22
12
Program Analysis CSCI 4450/6450, A Milanova 23
Exercise
n S = lx.ly.lz. x z (y z)
n I = lx. x
n What is S I I I?
( lx.ly.lz. x z (y z) ) I I I
à (ly.lz. I z (y z) ) I I
à (lz. I z (I z) ) I
à I I (I I) = (lx. x) I (I I)
à I (I I) = (lx. x) (I I)
à I I = (lx. x) Ià I
An expression with no free
variables is called combinator.
S, I, C, H, T are combinators.
Reducible expression is underlined
at each step.
23
Outline
n Pure lambda calculus, a review
n Syntax and semantics
n Free and bound variables
n Rules (alpha rule, beta rule)
n Normal form
n Reduction strategies
n Lambda calculus interpreters
n Coding them in Haskell
Program Analysis CSCI 4450/6450, A Milanova 24
24
13
25
Reduction Strategy
n Let us look at (lx.ly.lz. x z (y z)) (lu. u) (lv. v)
n Actually, there are (at least) two “reduction paths”:
Path 1: (lx.ly.lz. x z (y z)) (lu. u) (lv. v) àβ
(ly.lz. (lu. u) z (y z)) (lv. v)àβ
(lz. (lu. u) z ((lv. v) z)) àβ (lz. z ((lv. v) z)) àβ
lz. z z
Path 2: (lx.ly.lz. x z (y z)) (lu. u) (lv. v) àβ
(ly.lz. (lu. u) z (y z)) (lv. v) àβ
(ly.lz. z (y z)) (lv. v)àβ (lz. z ((lv. v) z)) àβ
lz. z z
25
Program Analysis CSCI 4450/6450, A Milanova 26
Reduction Strategy
n A reduction strategy (also called evaluation
order) is a strategy for choosing redexes
n How do we arrive at the normal form (answer)?
n Applicative order reduction chooses the
leftmost-innermost redex in an expression
n Also referred to as call-by-value reduction
n Normal order reduction chooses the leftmost-
outermost redex in an expression
n Also referred to as call-by-name reduction
26
14
27
Reduction Strategy: Examples
n Evaluate (lx. x x) ( (ly. y) (lz. z) )
n Using applicative order reduction:
(lx. x x) ( (ly. y) (lz. z) )
à (lx. x x) (lz. z)
à (lz. z) (lz. z)à (lz. z)
n Using normal order reduction
(lx. x x) ( (ly. y) (lz. z) )
à (ly. y) (lz. z) ( (ly. y) (lz. z) )
à (lz. z) ( (ly. y) (lz. z) )
à (ly. y) (lz. z)à (lz. z)
27
Program Analysis CSCI 4450/6450, A Milanova 28
Reduction Strategy
n In our examples, both strategies produced
the same result. This is not always the case
n First, look at expression (lx. x x) (lx. x x). What
happens when we apply β-reduction to this
expression?
n Then look at (lz.y) ((lx. x x) (lx. x x))
n Applicative order reduction – what happens?
n Normal order reduction – what happens?
28
15
Program Analysis CSCI 4450/6450, A Milanova 29
Church-Rosser Theorem
n Normal form implies that there are no more
reductions possible
n Church-Rosser Theorem, informally
n If normal form exists, then it is unique (i.e., result
of computation does not depend on the order
that reductions are applied; i.e., no expression
can have two distinct normal forms)
n If normal form exists, then normal order will find it
29
Program Analysis CSCI 4450/6450, A Milanova 30
Reduction Strategy
n Intuitively:
n Applicative order (call-by-value) is an eager
evaluation strategy. Also known as strict
n Normal order (call-by-name) is a lazy
evaluation strategy
n What order of evaluation do most PLs use?
30
16
Exercises
n Evaluate (lx.ly. x y) ((lz. z) w)
n Using applicative order reduction
n Using normal order reduction
31Program Analysis CSCI 4450/6450, A Milanova
31
Interpreters
n An interpreter for the lambda calculus is a
program that reduces lambda expressions to
“answers”
n We must specify
n The definition of “answer”. Which normal form?
n The reduction strategy. How do we choose
redexes in an expression?
Program Analysis CSCI 4450/6450, A Milanova 32
32
17
An Interpreter
n Definition by cases on E ::= x | lx. E1 | E1 E2
interpret(x) = x
interpret(lx.E1) = lx.E1
interpret(E1 E2) = let f = interpret(E1)
in case f of
lx.E3 -> interpret(E3[E2/x])
- -> f E2
n What normal form: Weak head normal form
n What strategy: Normal order
33
Haskell syntax:
let …. in
case f of
->
Program Analysis CSCI 4450/6450, A Milanova (modified from MIT 2015 Program Analysis OCW)
33
Another Interpreter
n Definition by cases on E ::= x | lx. E1 | E1 E2
interpret(x) = x
interpret(lx.E1) = lx.E1
interpret(E1 E2) = let f = interpret(E1)
a = interpret(E2)
in case f of
lx.E3 à interpret(E3[a/x])
- à f a
n What normal form: Weak head normal form
n What strategy: Applicative order 34
34
18
Outline
n Pure lambda calculus, a review
n Syntax and semantics
n Free and bound variables
n Rules (alpha rule, beta rule)
n Reduction strategies
n Normal form
n Lambda calculus interpreters
n Coding them in Haskell
Program Analysis CSCI 4450/6450, A Milanova 35
35
Coding them in Haskell
n In HW5 you will code an interpreter in Haskell
n Haskell
n A functional programming language
n Key ideas
n Lazy evaluation
n Static typing and polymorphic type inference
n Algebraic data types and pattern matching
n Monads … and more
Program Analysis CSCI 4450/6450, A Milanova 36
36
19
Lazy Evaluation
n Haskell implements lazy evaluation, i.e., normal
order reduction
n It won’t evaluate an argument expr. until it is needed
> f x = [] // f takes x and returns the empty list
> f (repeat 1) // returns?
> []
> head (tail [1..]) // returns?
> 2 // [1..] is infinite list of integers
n Lazy evaluation allows us to work with infinite
structures!
37
37
Static Typing and Type Inference
n Unlike Python, which is dynamically typed,
Haskell is statically typed!
n Unlike Java/C++ we don’t always have to
write type annotations. Haskell infers types!
n A lot more on type inference later!
> f x = head x // f returns the head of list x
> f True // returns?
• Couldn't match expected type ‘[a]’ with actual type ‘Bool’
• In the first argument of ‘f’, namely ‘True’
In the expression: f True … 38
38
20
Algebraic Data Types
n Algebraic data types are tagged unions (aka
sums) of products (aka records)
data Shape = Line Point Point
| Triangle Point Point Point
| Quad Point Point Point Point
Program Analysis CSCI 4450/6450, A Milanova (from MIT 2015 Program Analysis OCW) 39
union
Haskell keyword
the new type
new constructors (a.k.a. tags, disjuncts, summands)
Line is a binary constructor, Triangle is a ternary …
39
Algebraic Data Types in HW5
n Constructors create new values
n Defining a lambda expression
type Name = String
data Expr = Var Name
| Lambda Name Expr
| App Expr Expr
> e1 = Var “x” // Lambda term x
> e2 = Lambda “x” e1 // Lambda term lx.x 40
40
21
Examples of Algebraic Data
Types
data Bool = True | False
data Day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
data List a = Nil | Cons a (List a)
data Tree a = Leaf a | Node (Tree a) (Tree a)
data Maybe a = Nothing | Just a
Maybe type denotes that result of computation can
be a or Nothing. Maybe is a monad.
Program Analysis CSCI 4450/6450, A Milanova (from MIT 2015 Program Analysis OCW) 41
Polymorphic types.
a is a type parameter!
41
Data Constructors vs Type
Constructors
n Data constructor constructs a “program
object”
n E.g., Var, Lambda, and App are data constructs
n Type constructor constructs a “type object”
n E.g., Maybe is a unary type constructor
Program Analysis CSCI 4450/6450, A Milanova 42
42
22
Pattern Matching
n Examine values of an algebraic data type
anchorPnt :: Shape à Pnt
anchorPnt s = case s of
Line p1 p2 à p1
Triangle p3 p4 p5 à p3
Quad p6 p7 p8 p9 à p6
n Two points
n Test: does the given value match this pattern?
n Binding: if value matches, bind corresponding
values of s and pattern
Program Analysis CSCI 4450/6450, A Milanova (from MIT 2015 Program Analysis OCW) 43
Type signature of anchorPnt: takes
a Shape and returns a Pnt.
43
Pattern Matching in HW5
isFree::Name à Exprà Bool
isFree v e =
case e of
Var n à if (n == v) then True else False
Lambda …
Program Analysis CSCI 4450/6450, A Milanova 44
Type signature of isFree. In Haskell, all functions
are curried, i.e., they take just one argument.
isFree takes a variable name, and returns a function
that takes an expression and returns a boolean.
Of course, we can interpret isFree as a function
that takes a variable name name and an expression
E, and returns true if variable name is free in E.
44

学霸联盟