Outline
•Syntax of the lambda calculus
–abstraction over variables
•Operational semantics
–beta reduction
–substitution
•Programming in the lambda calculus
–representation tricks
Basic ideas
•introduce variables ranging over values
•define functions by (lambda-) abstracting over variables
•apply functions to values
Pure lambda calculus: start with nothing but variables.
Scope, free and bound occurences
Occurences of x in the body t are bound. Nonbound variable occurrences are called free.
Beta reduction
Computation in the lambda calculus takes the form of beta-reduction:
(lx. t1) t2 --> [x --> t2]t1
where [x --> t2]t1 denotes the result of substituting t2 for all free occurrences of x in t1.
A term of the form (lx. t1) t2 is called a beta-redex (or b-redex).
A (beta) normal form is a term containing no beta-redexes.
Beta reduction: Examples
Evaluation strategies
•Full beta-reduction
–any beta-redex can be reduced
•Normal order
–reduce the leftmost-outermost redex
•Call by name
–reduce the leftmost-outermost redex, but not inside abstractions
–abstractions are normal forms
•Call by value
–reduce leftmost-outermost redex where argument is a value
–no reduction inside abstractions (abstractions are values)
Programming in the lambda calculus
•multiple parameters through currying
•booleans
•pairs
•Church numerals and arithmetic
•lists
•recursion
–call by name and call by value versions
Computation in the lambda calculus takes the form of beta-reduction:
(lx. t1) t2 --> [x --> t2]t1
where [x --> t2]t1 denotes the result of substituting t2 for all free occurrences of x in t1.
A term of the form (lx. t1) t2 is called a beta-redex (or b-redex).
A (beta) normal form is a term containing no beta-redexes.
Symbols
•Syntax of the lambda calculus
–abstraction over variables
•Operational semantics
–beta reduction
–substitution
•Programming in the lambda calculus
–representation tricks
•introduce variables ranging over values
•define functions by (lambda-) abstracting over variables
•apply functions to values
- x + 1
- lx. x + 1
- (lx. x + 1) 2
Pure lambda calculus: start with nothing but variables.
Lambda terms
t ::=
x variable
lx . t abstraction
t t application
t ::=
x variable
lx . t abstraction
t t application
Occurences of x in the body t are bound. Nonbound variable occurrences are called free. (lx . ly. zx(yx))x
Beta reduction
Computation in the lambda calculus takes the form of beta-reduction:
(lx. t1) t2 --> [x --> t2]t1
where [x --> t2]t1 denotes the result of substituting t2 for all free occurrences of x in t1.
A term of the form (lx. t1) t2 is called a beta-redex (or b-redex).
A (beta) normal form is a term containing no beta-redexes.
Beta reduction: Examples
- (lx.ly.y x)(lz.u) --> ly.y(lz.u)
- (lx. x x)(lz.u) --> (lz.u) (lz.u)
- (ly.y a)((lx. x)(lz.(lu.u) z)) --> (ly.y a)(lz.(lu.u) z)
- (ly.y a)((lx. x)(lz.(lu.u) z)) --> (ly.y a)((lx. x)(lz. z))
- (ly.y a)((lx. x)(lz.(lu.u) z)) --> ((lx. x)(lz.(lu.u) z)) a
Evaluation strategies
•Full beta-reduction
–any beta-redex can be reduced
•Normal order
–reduce the leftmost-outermost redex
•Call by name
–reduce the leftmost-outermost redex, but not inside abstractions
–abstractions are normal forms
•Call by value
–reduce leftmost-outermost redex where argument is a value
–no reduction inside abstractions (abstractions are values)
Programming in the lambda calculus
•multiple parameters through currying
•booleans
•pairs
•Church numerals and arithmetic
•lists
•recursion
–call by name and call by value versions
Computation in the lambda calculus takes the form of beta-reduction:
(lx. t1) t2 --> [x --> t2]t1
where [x --> t2]t1 denotes the result of substituting t2 for all free occurrences of x in t1.
A term of the form (lx. t1) t2 is called a beta-redex (or b-redex).
A (beta) normal form is a term containing no beta-redexes.
Symbols
Symbols l ® b a ð Ô Ù ú
No comments:
Post a Comment