Lambda Calculus Pt. 1

19 Feb 2017

Lambda calculus is a language to express function application, which enables us to

• Define functions (anonymous)
• Apply functions

It is also a source of functional programming, and consists of Syntax (grammar) and Symantics (meaing) as other languages.

Syntax

There are only 4 syntactic expressions in lambda calculus (E for expression)

• Rule 1: E -> ID e.g. x
• Rule 2: E -> λID.E e.g. λx.x
• Rule 3: E -> E E e.g. foo λ bar . (foo (bar baz))
• Rule 4: E -> (E)

But, there is ambiguous syntax in such as λx.xy since it can be parsed in either direction e.g. Rule 2, 3 and Rule 3, 2 This can resolved with disambiguation rules

• E -> E E is left associative e.g. xyz is (xy)z and wxyz is ((wx)y)z
• λID.E extends as far to the right e.g. λx.xy is λx.(xy) and λx.λx.x is λx.(λx.(x))

Examples

• (λx.y)x != λx.yx (== λx.(yx))
• λx.(x)y == λx.((x)y)
• λa.λb.λc.abc == λa.(λb.(λc.((ab)c)))

Semantics

Every ID in lambda calculus is called as “variable”

• E -> λID.E is “abstraction”
  • ID is the variable of the abstraction
  • E is the body of abstration

• E -> E E is “application” (Calling a function)

• Semantic 1: E -> λID.E defines a new anonymous function
  • That’s why anonymous function is called “lambda expressions” in programming language
  • ID is the parameter of the function
  • E is the body of the function
• Semantic 2: E -> E1 E2, is similar to calling function E1 and setting its parameter to be E2

Examples

• Semantic 1: λx.+ x 1 (Taking x as parameter and summing up x and 1)
• Semantic 2: (λx.+ x 1)2 (Calling function E1 setting its parameter as 2 i.e. + 2 1 = 3)

How can + function be defined if abractions only accept 1 parameter? Currying…

• A function that takes multiple arguments into a seuqence of functions that each take a single arguments

• λx.λy.((+ x) y)
• (λx.λy.((+ x) y))1 = λy.((+ 1) y)
• (λx.λy.((+ x) y)) 10 20 = (λy.((+ 10) y))20 = ((+ 10) 20) = 30

Free variable

It doesn’t appear within the body of the abstraction with a metavariable of the same name (e.g. x in λx)

• x free in λx.xyz ? no
• y free in λx.xyz ? yes
• x free in (λx.(+ x 1)) x ? yes
• z free in λx.λy.λz.zyx ? no
• x free in (λx.z foo)(λy.y x) ? yes

See CSE 340 11-23-15 Lecture: “Lambda Calculus Pt. 1”