CS代写 CS 314: Principles of Programming Languages

CS 314: Principles of Programming Languages
Lambda Calculus
CS 314 Spring 2022 1

Turing Machine
CS 314 Spring 2022 7

Turing Completeness
A language L is Turing complete if it can compute any function computable by a Turing Machine
Show a language L is Turing complete if
• We can map every Turing machine to a program in L
Ø I.e., a program can be written to emulate a Turing machine • Or, we can map any program in a known Turing-
complete language to a program in L
Turing complete languages the “most powerful”
• Church-Turing thesis (1936): Computability by a Turing Machine defines “effectively computable”
CS 314 Spring 2022 8

Programming Language Expressiveness
So what language features are needed to express all computable functions?
• What’s a minimal language that is Turing Complete?
Observe: some features exist just for convenience
• Multi-argument functions
Ø Use currying or tuples • Loops
Ø Use recursion • Side effects
foo ( a, b, c )
while (a < b) ... Ø Use functional programming pass “heap” as an argument to each function, return it when with function’s result CS 314 Spring 2022 9 Lambda Calculus (λ-calculus) Proposed in 1930s by Formal system • Designed to investigate functions & recursion • For exploration of foundations of mathematics Now used as • Tool for investigating computability • Basis of functional programming languages Ø Lisp, Scheme, ML, OCaml, Haskell... CS 314 Spring 2022 10 Lambda Calculus Syntax A lambda calculus expression is defined as abstraction (func def) application (func call) Ø This grammar describes ASTs; not for parsing Ø Lambda expressions also known as lambda terms • λx.eislike(funx->e)inOCaml
That’s it! Nothing but (higher-order) functions
CS 314 Spring 2022 11

Why Study Lambda Calculus?
It is a “core” language
• Very small but still Turing complete
But with it can explore general ideas
• Language features, semantics, proof systems, algorithms, …
Plus, higher-order, anonymous functions (aka lambdas) are now very popular!
• C++ (C++11), PHP (PHP 5.3.0), C# (C# v2.0), Delphi (since 2009), Objective C, Java 8, Swift, Python, Ruby (Procs), … (and functional languages like OCaml, Haskell, F#, …)
CS 314 Spring 2022 12

Two Conventions
Scope of λ extends as far right as possible • Subject to scope delimited by parentheses
• λx. λy.x y is same as λx.(λy.(x y))
Function application is left-associative
• xyzis(xy)z
• Same rule as OCaml
CS 314 Spring 2022 13

OCaml Lambda Calc Interpreter
type id = string
type exp = | Var of id | Lam of id * exp
| App of exp * exp
λx.λy.x y (λx.λy.x y) λx.x x
CS 314 Spring 2022
Lam (“x”, Var “x”)
Lam (“x”,(Lam(“y”,App (Var “x”, Var “y”))))
App (Lam(“x”,Lam(“y”,App(Var“x”,Var“y”))),
Lam (“x”, App (Var “x”, Var “x”)))

λx.(y z) and λx.y z are equivalent
CS 314 Spring 2022
A. True B. False

λx.(y z) and λx.y z are equivalent
CS 314 Spring 2022

What is this term’s AST?
A. App (Lam (“x”, Var “x”), Var “x”) B. Lam (Var “x”, Var “x”, Var “x”) C. Lam (“x”, App (Var “x”,Var “x”)) D. App (Lam (“x”, App (“x”, “x”)))
CS 314 Spring 2022 17
type id = string
type exp =
| Lam of id * exp | App of exp * exp

What is this term’s AST?
A. App (Lam (“x”, Var “x”), Var “x”) B. Lam (Var “x”, Var “x”, Var “x”) C. Lam (“x”, App (Var “x”,Var “x”)) D. App (Lam (“x”, App (“x”, “x”)))
CS 314 Spring 2022 18
type id = string
type exp =
| Lam of id * exp | App of exp * exp

This term is equivalent to which of the following?
CS 314 Spring 2022
A. (λx.x) (a b) B. (((λx.x) a) b) C. λx.(x (a b)) D. (λx.((x a) b))

Lambda Calculus Semantics
Evaluation: All that’s involved are function calls
(λx.e1) e2
• Evaluate e1 with x replaced by e2
This application is called beta reduction
• (λx.e1) e2 → e1{e2/x}
Ø e1{e2/x} is e1 with occurrences of x replaced by e2 Ø This operation is called substitution
• Replace formal parameters with actual arguments
• Instead of using environment to map formals to actuals
• We allow reductions to occur anywhere in a term Ø Order reductions are applied does not affect final value!
When a term cannot be reduced further it is in
beta normal form, e.g., x, λx.e, x x, x (λx.e).
CS 314 Spring 2022 21

Beta Reduction Example
(λx.λz.x z) y
→ (λx.(λz.(x z))) y
→ (λx.(λz.(x z))) y → λz.(y z)
// since λ extends to right
// apply (λx.e1) e2 → e1{e2/x}
// where e1 = λz.(x z), e2 = y // final result
Parameters
Equivalent OCaml code
• (funx->(funz->(xz)))y → funz->(yz)
CS 314 Spring 2022 22

Beta Reduction Examples
(λx.x) z → z
y (λx.xy)z→ zy
(λx.y) z →
• A function that applies its argument to y
CS 314 Spring 2022 23

Beta Reduction Examples (cont.)
(λx.x y) (λz.z) → (λz.z) y → y
(λx.λy.x y) z →
• A curried function of two arguments
• Applies its first argument to its second
(λx.λy.x y) (λz.zz) x →(λy.(λz.zz)y)x → (λz.zz)x → xx CS 314 Spring 2022 24

Beta Reduction Examples (cont.) (λx.x (λy.y)) (u r) → (u r) (λy.y)
(λx.(λw. x w)) (λz.z) → (λw. (λz.z) w) → (λw.w)
CS 314 Spring 2022 25

Confluence
We allow reductions to occur anywhere in a term
Ø Order reductions are applied does not affect final value!
CS 314 Spring 2022 26

(λx.y) z can be beta-reduced to
A.y B. y z C.z
D. cannot be reduced
CS 314 Spring 2022

Which of the following reduces to λz. z?
a) (λy. λz. x) z
b) (λz. λx. z) y
c) (λy. y) (λx. λz. z) w
d) (λy. λx. z) z (λz. z)
CS 314 Spring 2022 29

Which of the following reduces to λz. z?
a) (λy. λz. x) z
b) (λz. λx. z) y
c) (λy. y) (λx. λz. z) w
d) (λy. λx. z) z (λz. z)
CS 314 Spring 2022 30

Beta reducing the following term produces what result?
λx.(λy. y y) w z
a) λx. w w z
b) λx. w z
d) Does not reduce
CS 314 Spring 2022 31

Beta reducing the following term produces what result?
λx.(λy. y y) w z
a) λx. w w z
b) λx. w z
d) Does not reduce
CS 314 Spring 2022 32

Static Scoping & Alpha Conversion
Lambda calculus uses static scoping Consider the following
• (λx.x (λx.x)) z → ?
Ø The rightmost “x” refers to the second binding
• This is a function that
Ø Takes its argument and applies it to the identity function This function is “the same” as (λx.x (λy.y))
• Renaming bound variables consistently preserves meaning Ø This is called alpha-renaming or alpha conversion
• Ex. λx.x = λy.y = λz.z λy.λx.y = λz.λx.z CS 314 Spring 2022

Terminology: Free and Bound Variables
A free variable is one that doesn’t have a surrounding lambda that binds it
• In (λy.y z x), the variables z and x are free • In (λy.λz.y z x), the variable x is free
• In (λy.λz.y z), there are no free variables
A bound variable is one that does have a corresponding binder
• In (λy.y z x), the variable y is bound (but not z and x)
• In (λy.λz.y z x), the variables y and z are bound (not x) • In (λy.λz.y), the variable y is bound (z does not appear)
CS 314 Spring 2022 34

Which of the following expressions is alpha
equivalent to (alpha-converts from) (λx. λy. x y) y
a) λy. y y
b) λz. y z
c) (λx. λz. x z) y d) (λx. λy. x y) z
CS 314 Spring 2022

Definitional Interpreter as Semantics
let rec reduce e = match e with
(λx. e1) e2 -> e1{e2/x} | e1 e2 ->
let e1′ = reduce e1 in if e1’ <> e1 then e1′ e2 else e1 (reduce e2)
Straight β rule Reduce lhs of app
Reduce rhs of app Reduce function body
| λx. e -> λx. (reduce e)
| _ -> eAlready in a normal form nothing to do
CS 314 Spring 2022 37

Defining Substitution
Use recursion on structure of terms
• x{e/x}=e //Replacexbye
• y{e/x} = y // y is different than x, so no effect • (e1 e2){e/x} = (e1{e/x}) (e2{e/x})
// Substitute both parts of application
• (λx.e’){e/x} = λx.e’
Ø In λx.e’, the x is a parameter, and thus a local variable that is
different from other x’s. Implements static scoping.
Ø So the substitution has no effect in this case, since the x being
CS 314 Spring 2022
substituted for is different from the parameter x that is in e’ Example:(λx.x(λx.yx))y =x(λx.yx){y/x}
= x {y/x} (λx. y x) {y/x} = y (λx. y x) {y/x}
= y (λx. y x)

Defining Substitution
Use recursion on structure of terms
• x{e/x}=e //Replacexbye
• y{e/x} = y // y is different than x, so no effect • (e1 e2){e/x} = (e1{e/x}) (e2{e/x})
// Substitute both parts of application
• (λx.e’){e/x} = λx.e’
Ø In λx.e’, the x is a parameter, and thus a local variable that is
different from other x’s. Implements static scoping.
Ø So the substitution has no effect in this case, since the x being
substituted for is different from the parameter x that is in e’ • (λy.e’){e/x} = ?
Ø The parameter y does not share the same name as x, the variable being substituted for
Ø Is λy.(e’{e/x}) correct? No…
CS 314 Spring 2022 39

Variable capture
How about the following?
(λy.e’){e/x} = λy.(e’{e/x}) ?
• (λx.λy.xy)y→λy.xy{y/x}→λy.yy??
• When we replace y inside, we don’t want it to be captured by the inner binding of y, as this violates static scoping
• I.e., (λx.λy.x y) y ≠ λy.y y Solution
• (λx.λy.x y) is “the same” as (λx.λz.x z) Ø Due to alpha conversion
• So alpha-convert (λx.λy.x y) y to (λx.λz.x z) y first Ø Now (λx.λy.x y) y =𝛼 (λx.λz.x z) y → λz.y z
CS 314 Spring 2022 40

(λy.e’){e/x} = λy.(e’{e/x}) ? Completing the Definition of Substitution
Recall: we need to define (λy.e’){e/x}
• We want to avoid capturing free occurrences of y in e
• Solution: alpha-conversion!
Ø Change y to a variable w that does not appear in e’ or e (Such a w is called fresh)
Ø Replace all occurrences of y in e’ by w.
Ø Then replace all occurrences of x in e’ by e!
(λy.e’){e/x} =𝛼 λz.(e’{z/y}){e/x} (z is fresh WRT e and e’)
E.g. (λx.λy.x y) y → (λy.x y){y/x} =𝛼 (λz.x z){y/x} → λz.y z CS 314 Spring 2022 41

Beta-Reduction, Again
Whenever we do a step of beta reduction
• (λx.e1) e2 → e1{e2/x}
• We alpha-convert x if necessary
CS 314 Spring 2022 42

Beta-reducing the following term produces what result?
(λx.x λy.y x) y
A. y (λz.z y) B. z (λy.y z) C. y (λy.y y) D. yy
CS 314 Spring 2022 43

Beta-reducing the following term produces what result?
(λx.x λy.y x) y
A. y (λz.z y)
B. z (λy.y z) C. y (λy.y y) D. yy
(λx.x λy.y x) y → (x λy.y x){y/x} → (x {y/x}) (λy.y x {y/x})
→y (λy.y x {y/x}) =𝛼 y (λz.z x {y/x})→y λz.z y CS 314 Spring 2022 44

O ementation: Substitution
(* substitute e for y in m — m {e/y} *)
let rec subst e y m = match m with
Var x -> (* x {e/y} *)
if y = x then e (* substitute *) else m (* don’t subst *)
| App (e1,e2) -> (* e1 e2 {e/y} *) App (subst e y e1, subst e y e2)
| Lam (x,e0) -> … (* (λx.e0){e/y} *) CS 314 Spring 2022

O : Substitution (cont’d)
(* substitute e for y in Lam (x,e0) *)
let rec subst e y m = match m with …
| Lam (x,e0) -> (*(λx.e0){e/y}*) Shadowing blocks
if y = x then m substitution else if not (List.mem x (fvs e)) then
CS 314 Spring 2022
Lam (x, subst e y e0)
Safe: no capture possible Might capture; need to α-convert
let z = newvar() in (* fresh *) let e0′ = subst (Var z) x e0 in Lam (z,subst e y e0′)

O ementation: Free variables
(* compute free variables in e *)
let rec fvs e = match e with
Var x -> [x]“Naked” variable is free
| App (e1,e2) -> (fvs e1) @ (fvs e2)
| Lam (x,e0) ->
Append free vars of sub-expressions
CS 314 Spring 2022
List.filter (fun y -> x <> y) (fvs e0)
Filter x from the free variables in e0

O : Reduction
let rec reduce e = match e with
Straight β rule
CS 314 Spring 2022
App (Lam (x,e), e2) -> subst e2 x e | App (e1,e2) ->
let e1′ = reduce e1 in
if e1’ <> e1 then App(e1′,e2)
else App (e1,reduce e2)
| Lam (x,e) -> Lam (x, reduce e)
Reduce function body Already in a normal form nothing to do
Reduce lhs of app
Reduce rhs of app

Termination
May or may not terminate based on the applications chosen to reduce.
CS 314 Spring 2022 49

Call-by-name vs. Call-by-value
Sometimes we have a choice about where to apply beta reduction. Before call (i.e., argument):
• (λz.z) ((λy.y) x) → (λz.z) x → x Or after the call:
• (λz.z) ((λy.y) x) → (λy.y) x → x
The former strategy is called call-by-value (CBV)
• Evaluate any arguments before calling the function
The latter is called call-by-name (CBN)
• Delay evaluating arguments as long as possible
CS 314 Spring 2022 50

Call-by-name vs. Call-by-value
Call-by-name
Call by value
CS 314 Spring 2022 51

Partial Evaluation
It is also possible to evaluate within a function (without calling it):
• (λy.(λz.z) y x) → (λy.y x)
Called partial evaluation
• Can combine with CBN or CBV (as in the interpreter)
• In practical languages, this evaluation strategy is employed in a limited way, as compiler optimization
CS 314 Spring 2022
int foo(int x) {
return 0+x;
int foo(int x) {

Lambda calculus is a core model of computation
• We can encode familiar language constructs using only functions
Ø E.g., Booleans, control-flows, recursive functions. Useful for understanding how languages work
• Ideas of types, evaluation order, termination, proof systems, etc. can be developed in lambda calculus,
Ø then scaled to full languages
CS 314 Spring 2022 53

The Power of Lambdas
Despite its simplicity, the lambda calculus is quite expressive: it is Turing complete!
Means we can encode any computation we want*
• Let bindings
• Booleans
• Natural numbers & arithmetic • Looping
CS 314 Spring 2022
*To show Turing completeness we have to map every Turing machine to lambda calculus term. We are not doing that here. Rather, we are showing how typical PL constructs can be represented in lambda calculus, to show what it can do 54

Let bindings
Local variable declarations are like defining a function and applying it immediately (once):
• letx=e1ine2=(λx.e2)e1 Example
• letx=(λy.y)inxx=(λx.xx)(λy.y) where
(λx.x x) (λy.y) → (λy.y) (λy.y) → (λy.y)
CS 314 Spring 2022 55

Church’s encoding of mathematical logic
• true = λx.λy.x
• false = λx.λy.y
• ifathenbelsec
Ø Defined to be the expression: a b c
• iftruethenbelsec=(λx.λy.x)bc→(λy.b)c→b • iffalsethenbelsec=(λx.λy.y)bc→(λy.y)c→c
CS 314 Spring 2022 56

Booleans (cont.)
Other Boolean operations
• not = λx.x false true
Ø not x = x false true = if x then false else true
Ø not true → (λx.x false true) true → (true false true) →
if true then false else true → false Ø and x y = x y false = if x then y else false
• and = λx.λy.x y false • or = λx.λy.x true y
Ø or x y = x true y = if x then true else y Given these operations
• Can build up a logical inference system
CS 314 Spring 2022 57

Natural Numbers (Church* Numerals)
Encoding of non-negative integers
• 0 = λf.λy.y
• 1=λf.λy.fy
• 2=λf.λy.f(fy)
• 3=λf.λy.f(f(fy))
i.e., n = λf.λy.f (f (f …. f y))
• Formally: n+1 = λf.λy.f (n f y)
CS 314 Spring 2022
*( , of course)

Operations On Church Numerals
• succ = λz.λf.λy.f (z f y)
(λz.λf.λy.f (z f y)) (λf.λy.y) → λf.λy.f ((λf.λy.y) f y) → λf.λy.f ((λy.y) y) →
CS 314 Spring 2022
• 0 = λf.λy.y • 1 = λf.λy.f y

Operations On Church Numerals (cont.)
• iszero = λz.z (λy.false) true
• iszero 0 =
(λz.z (λy.false) true) (λf.λy.y) → (λf.λy.y) (λy.false) true → (λy.y) true →
CS 314 Spring 2022
• 0 = λf.λy.y

Arithmetic Using Church Numerals
If M and N are numbers (as λ expressions)
• Can also encode various arithmetic operations
• M+N=λf.λy.Mf(Nfy)
Equivalently: + = λM.λN.λf.λy.M f (N f y)
Ø In prefix notation (+ M N)
Multiplication
• M*N=λf.λy.M(Nf)y
Equivalently: * = λM.λN.λf.λy.M (N f) y
Ø In prefix notation (* M N)
CS 314 Spring 2022 61

Discussion
Lambda calculus is Turing-complete
• Most powerful language possible
• Can represent pretty much anything in “real” language
Ø Using clever encodings
But programs would be
• Pretty slow (10000 + 1 → thousands of function calls) • Pretty large (10000 + 1 → hundreds of lines of code) • Pretty hard to understand (recognize 10000 vs. 9999)
In practice
• We use richer, more expressive languages
• That include built-in primitives
CS 314 Spring 2022 62

程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts