CS计算机代考程序代写 scheme DrRacket Lambda Calculus Lambda Calculus (λ Calculus)

Lambda Calculus (λ Calculus)
March 10, 2021

Outline
􏰉 what is lambda calculas
􏰉 beta reducton and alpha renaming 􏰉 lazy evaluation
􏰉 Church encoding

Overview
􏰉 The smallest programming language
􏰉 Syntax and examples
􏰉 α−renaming and β−reduction
􏰉 order of evaluation
􏰉 λ encoding
􏰉 Books: The Lambda Calculus. Its Syntax and Semantics, An Introduction to Functional Programming Through Lambda Calculus

Smallest Universal Programming Language
􏰉 e ::= x|λx.e|e0 e1
􏰉 As a programming language, sometimes a concrete implementation of lambda calculus also supports predefined constants such as ’0’ ’1’ and predefined functions such as ’+’ ’*’

Examples
􏰉 λx.x (lambda abstraction: building new function) 􏰉 (λx.x) y (function application)
The parenthesis is to separate function and function application.

What is λ Calculus and Why is it important?
1. A mathematical language; A formal computation model for functional programming; a theoretical foundation for the family of functional programming languages.
2. Study interactions between functional abstraction and function applications
3. By Alonzo Church in the 1930s
4. In 1920s – 1930s, the mathematicians came up different systems for capturing the general idea of computation:
􏰉 Turing machines – Turing
􏰉 m-recursive functions – G ̈odel
􏰉 rewrite systems – Post
􏰉 the lambda calculus – Church
􏰉 combinatory logic – Scho ̈nfinkel, Curry
These systems are all computationally equivalent in the sense that each could encode and simulate the others.

The Mathematical Precursor to Scheme
Mathematical formalism to express computation using functions:
􏰉 Everything is a function. There are no other primitive types—no integers, strings, objects, booleans … If you want these things, you must encode (simulate) them using functions.
􏰉 No state or side effects. It is purely functional. Thus we can think exclusively in terms of the substitution model.
􏰉 Only unary (one-argument) functions.

Implementation in Scheme/DrRacket
􏰉 Syntax implemented in Scheme:

Lambda Calculus: Review
􏰉 Smallest language
􏰉 Syntax
S → Name
|
Function | λx.x
| Application λx.xy (λx.x) y (λx.x y) (λ(x) y) (Lambda(x) y) (xλ(x)y)x
(
(x
) helps with clarity )x helps with clarity
x
􏰉 Turing machine is the model for imperative programming language, and, λ calculus is the model for functional programming language. They have equal computing power and can simulate each other.

Lambda Calculus Semantics
􏰉 β-reduction
Function definition Actual parameter
The bound variable x will be replaced by the argument expression in the body expression x.
(λx.x) x

β-reduction The AST view:

β-reduction
((λ(x) e1 ) e2) evaluates the expression e1 by replacing every (“free”) occurrences of x in e1 using e2, denoted as e1[x→e2]
􏰉 ((λ(x)(λ(y)(+xy)))1)
􏰉 ((((λ(x)(λ(y)(λ(x)(+xy))))1)2)3)

β-reduction (Contd.)
((λ(x) e1 ) e2) evaluates the expression e1 by replacing every (“free”) occurrences of x in e1 using e2, denoted as e1[x→e2]
􏰉 ((λ(x)(λ(y)(+xy)))1) output: (λ(y) (+ 1 y) )

β-reduction
((λ(x) e1 ) e2) evaluates the expression e1 by replacing every (“free”) occurrences of x in e1 using e2, denoted as e1[x→e2]
􏰉 ((λ(x)(λ(y)(+xy)))1)
􏰉 ((((λ(x)(λ(y)(λ(x)(+xy))))1)2)3) = ( ( (λ(y) (λ (x) (+ x y) ) ) 2) 3)
= ( (λ (x) (+ x 2) ) 3)
=5

α-renaming
Rename a variable:
􏰉 ((((λ(x)(λ(y)(λ(x)(+xy))))1)2)3) 􏰉 ((((λ(x)(λ(y)(λ(z)(+zy))))1)2)3)

The Order of Evaluation
The order of evaluation does not impact β-reduction results if the evaluation terminates:
( (λ(x) (+ x 1)) ((λ(y) (+ y 1)) 2 ) )

Lazy Evaluation
􏰉 The evaluation is deferred until their results are needed.
􏰉 Arguments are not evaluated before they are passed to a function,
but only when their values are actually used.
( (λ(x) (+ x 1)) ((λ(y) (+ y 1)) 2 ) ) ( (λ(x) 1) ((λ(y) (+ y 1)) 2 ) )

Simulating the Computation
What is the result of ((λ(x)x) (λ(y)y))
Soln: (λ(y)y)

Identity Function
(λ(x)x): this function applies to any entity return the entity itself f(x) = x+0 or f(x) = x*1 or f(x) = x-0

Self-Application Function
(λ(x)(x x)): this function applies to any entity will return the entity aplies to itself
((λ(x)(x x)) 3) Soln: (3 3)
((λ(x)(x x)) (λ(y) y)) Soln: ((λ(y) y) (λ(y) y))
(λ(y) y)

More Examples
(λ(f) (λ(x) (f x) ))
􏰉 (f x) means application of function f on x.
􏰉 It is a function without formal parameter, cannot be reduced any further through β-reduction.
( ((λ(f) (λ(x) (f x) )) (λ(y) y )) (λ(z) (z z) )) F A1 A2
Let (λ(y) y ) = g and (λ(z) (z z) ) = v
((λ(x) (g x) ) v) = (g v)
= ((λ(y) y ) v) =v
= (λ(z) (z z) )

Church encoding
􏰉 In mathematics, Church encoding is a means of representing data and operators in the lambda calculus
􏰉 The Church numerals are a representation of the natural numbers using lambda notation.
􏰉 The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.

Church encoding
Representing data and operations using functions:
􏰉 non-negative integers: 0, 1, 2 …, and their computation of addition, subtraction, multiplication …
􏰉 boolean, true, false, and, or, not, ite (if then else control flow)
􏰉 pairs and lists
􏰉 rational numbers: may be encoded as a pair of signed numbers
􏰉 computable real numbers may be encoded by a limiting process that guaranetees that the difference from the real value differs by a number which maybe as small as we need (considering pi)
􏰉 complex numbers are naturally encoded as a pair of real numbers.

Encoding Natural Numbers (Church Numbers)
􏰉 Encoding of numbers: 0, 1, 2, . . . , as functions such that their semantics follow the natural number semantics (e.g., counting, sequencing)
􏰉 Intuition: The number n means how many times one can do certain operation.
􏰉 A natural number encoding function takes two arguments (function and entity on which the function is to be applied)

More examples of understanding the functions of natural numbers
(two g) =
( (f λ(f)(x λ(x)(f (f x))x)f g) = (x λ(x)(g (g x))x)
This is a function that takes a parameter x and returns the result of applying the function g twice on x.
((z λ(z)((threef)z))z two)
Soln:
(f(f(f two)))

Operations on natural numbers

the Successor functinon

Exercise
(succ (succ zero))

Encoding Add using the Successor functinon
Semantics of Addition: Addition takes two natural numbers as arguments and produces a new natural number whose semantics/representation is the sum of two inputs.
􏰉 Add requires two arguments and returns a natural number representation:
(m λ(m)(n λ(n)(f λ(f )(x λ(x ) … )x )f )n )m
The definition is follows:
􏰉 ( (m succ) n) generates:
(succ (succ (succ …(succ n)) …))
This produces a natural number equivalent to m+n
􏰉 It should be applied to some function f to represent the natural number
((( (m succ) n) f) x)
􏰉 Therefore, the add function is:
(m λ(m)(n λ(n)(f λ(f )(x λ(x) ((((m succ) n) f ) x) )x )f )n)m

Exericse
((add (succ zero)) (succ zero))

Natural Numbers Encoding in λ-calculus (Revisit)
Representation of:
Each number is represented by the number of times some function is applied to some entity.

Natural Numbers Encoding in λ-calculus (Revisit)
􏰉 Develop a successor function succ that takes a natural number as an argument and returns the next natural number.
􏰉 Example:
(succ zero) should return (f λ(f )(x λ(x ) (f x )x )f = one (succ one) should return (f λ(f )(x λ(x ) (f (f x ))x )f = two

Natural Numbers Encoding in λ-calculus (Revisit)

Boolean and if-then-else (ITE)

or a b:
( (ite a) true
((ite b) true false) )

Boolean Operations
􏰉 Basic operators: and, or, not
􏰉 which then can be extended to xor, implication and equievelnce

More about Lambda Caculus
􏰉 there is no recursion in lambda calculus
􏰉 do we program in lambda calculus? mostly no
􏰉 it helps understand functional computation
􏰉 it helps design new functional programming languages

Problem Solving
􏰉 beta reduction:
􏰉 parsing the function
􏰉 understand what is the function, what is the actual parameters
􏰉 remember steps of function applications, even when functions and
actual parameters can be complex
􏰉 beta reduction and encoding recognition (e.g., what does this function compute?):
􏰉 remember existing encoding and functions
􏰉 understand the semantics of certain functions and patterns, e.g.,
identity function, natural numbers …

Further Learning Materials
􏰉 Lambda calculus examples: https://www.ics.uci.edu/~lopes/teaching/inf212W12/ readings/lambda-calculus-handout.pdf
􏰉 Programming Languages: Lambda Calculus – 1 https://www.youtube.com/watch?v=v1IlyzxP6Sg
􏰉 Programming Languages: Lambda Calculus – 2 https://www.youtube.com/watch?v=Mg1pxUKeWCk