λ-Calculus as a Programming Language
Copyright © 2018 by . All Rights Reserved.
Learning Outcomes
Copyright By PowCoder代写 加微信 powcoder
by the End of the Lecture, Students that Complete
the Recommended Exercises should be Able to:
Identify (informally) Programming Language Elements Explain How Boolean Values can be Represented Demonstrate How Logical Operations are Possible Show How the Y-Recombinator permits Recursion
Copyright © 2018 by . All Rights Reserved.
Reading and Suggested Exercises
Copyright © 2018 by . All Rights Reserved.
Read the following Chapter(s): None
Conway’s Game of Life
Intermediate (and Advanced) Students of Programming have seen Conway’s “Game of Life” (and possibly implemented it for themselves)
1. A living cell with fewer than two living
neighbours dies.
2. A living cell with two or three living neighbours continues to live.
Copyright © 2018 by . All Rights Reserved.
3. A living cell with more than three living neighbours dies.
4. A dead cell with exactly three living neighbours becomes alive.
Conway’s Game of Life
many are also aware that it is Turing Complete (i.e., it can be used to Solve Any Computational Problem and/or simulate any Turing machine)
3. A living cell with more than three living neighbours dies.
4. A dead cell with exactly three living neighbours becomes alive.
1. A living cell with fewer than two living
neighbours dies.
2. A living cell with two or three living neighbours continues to live.
How would you Convince someone of that? Copyright © 2018 by . All Rights Reserved.
Conway’s Game of Life a Convincing Argument requires Only:
“Gliders” can Act as Signals (or, if you prefer, Electrons)
a Collision between “Gliders” (properly aligned) Annihilates Both “Glider Guns” Generates a constant stream of “Gliders” “Eaters” can Annihilate Gliders with No Additional Effects
“Glider” “Glider Gun” “Eater”
Copyright © 2018 by . All Rights Reserved.
Conway’s Game of Life
with the Presence or Absence of a Glider used
to Represent 1 or 0 (or True or False) respectively, the following Configurations are used to Encode the Logic Gates NOT, AND, and OR (respectively)
Copyright © 2018 by . All Rights Reserved.
Conway’s Game of Life
No Signal 0 GUN
No Collision
for the NOT Gate, the Glider Gun is Aligned such that it Emits Gliders towards the Output, and the Input is Aligned such that, If it were to Emit a Glider it would Annihilate with the Glider on its way to the Output
No Signal 0
1 GUN Collision
Copyright © 2018 by . All Rights Reserved.
Conway’s Game of Life
No Signal GUN 0 No Signal Collision
0 No Signal
No Signal 0
No Signal 0 the AND Gate
No Signal 1 Signal
No Signal 0
Copyright © 2018 by . All Rights Reserved.
Introducing λ-Calculus as a Language
Logic Gates can be Used to Implement Circuits for Arithmetic (e.g., Adders) or Data Storage (e.g., Flip-Flops), so the capacity to Reproduce many of the Computer’s Abilities is Established
similarly, to Establish that λ-Calculus is to Software what the Turing Machine is to Hardware, we will Demonstrate how the Common Elements of a Computer Program can be Created with λ-Calculus
Copyright © 2018 by . All Rights Reserved.
Introducing λ-Calculus as a Language
it has Already been Demonstrated that λ-Calculus can be used to perform Arithmetic Operations
What Else does it Need before you can Easily Recognize λ-Calculus as a Programming Language?
Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching
Boolean Data is used for Encoding Truth Values primarily for use in Conditional Statements in order to Branch the Control Flow of a Program
since there is No Concept of Data in λ-Calculus, How must the Boolean Values True and False be Encoded?
Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching
𝒕𝒓𝒖𝒆 = 𝝀𝒙. 𝝀𝒚.𝒙 𝒇𝒂𝒍𝒔𝒆 = 𝝀𝒙. 𝝀𝒚. 𝒚
these Function Definitions are Not Arbitrary What Happens if you perform β-Reduction on Each of
these with Two Unspecified “Values” 𝒂 and 𝒃? Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching
𝒕𝒓𝒖𝒆𝒂𝒃 𝒇𝒂𝒍𝒔𝒆𝒂𝒃
Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching
𝒕𝒓𝒖𝒆𝒂𝒃 𝒇𝒂𝒍𝒔𝒆𝒂𝒃
𝝀𝒙. 𝝀𝒚.𝒙 𝒂𝒃 𝝀𝒙. 𝝀𝒚.𝒚 𝒂𝒃 𝝀𝒚.𝒂 𝒃 𝝀𝒚.𝒚 𝒃
Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching the Function 𝒕𝒓𝒖𝒆, taken Literally, means
“From Two options, Take the First” the Function 𝒇𝒂𝒍𝒔𝒆, taken Literally, means
“From Two options, Take the Second”
What is the Relationship between these Meanings and
the Typical Uses for Values of the Boolean Data Type?
Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching a Branching Control Structure divides the Flow
into Either the Left Branch or the Right Branch cnt % 2
evil = True
If cnt % 2 == 0 Evaluates to True Then… “From the Two options, Take the First”
Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching
If 𝒕𝒓𝒖𝒆 and 𝒇𝒂𝒍𝒔𝒆 themselves Already Encode the idea of Choosing between Paths, then How could a Branching Control Structure (and specifically an If-Else Statement) be Implemented in λ-Calculus?
Copyright © 2018 by . All Rights Reserved.
Boolean Values and Branching
𝒊𝒇𝒆𝒍𝒔𝒆 = 𝝀𝒑. 𝝀𝒕. 𝝀𝒇. 𝒑𝒕𝒇
where 𝒑 is the Predicate/Condition of the Branch, 𝒕 corresponds to the “True” Branch,
and 𝒇 corresponds to the “False” Branch
Copyright © 2018 by . All Rights Reserved.
Logical Operations
Having Established the functions for the values of True and False, What are the Fundamental Operations for working with Truth Values?
How would you Implement each of these Operations?
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕 = 𝝀𝒃. 𝝀𝒑. 𝝀𝒕. 𝝀𝒇. 𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕 = 𝝀𝒃. 𝝀𝒑. 𝝀𝒕. 𝝀𝒇. 𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 this appears to be More Complex than it actually Is
do you Recognize this Section?
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕 = 𝝀𝒃. 𝝀𝒑. 𝝀𝒕. 𝝀𝒇. 𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 this appears to be More Complex than it actually Is
do you Recognize this Section? 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝝀𝒑. 𝝀𝒕. 𝝀𝒇. 𝒑𝒕𝒇
𝒏𝒐𝒕 = 𝝀𝒃. 𝒊𝒇𝒆𝒍𝒔𝒆 𝒃 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕=𝝀𝒃. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆
How would you Perform β-Reduction on 𝒏𝒐𝒕 𝒕𝒓𝒖𝒆 ?
𝒏𝒐𝒕 𝒇𝒂𝒍𝒔𝒆 ?
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕=𝝀𝒃. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 𝒏𝒐𝒕 𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕=𝝀𝒃. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆
=𝝀𝒃. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆
= 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒕𝒓𝒖𝒆𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 = 𝝀𝒕. 𝝀𝒇 𝒕𝒓𝒖𝒆 𝒕 𝒇 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆
= 𝝀𝒇 𝒕𝒓𝒖𝒆 𝒇𝒂𝒍𝒔𝒆 𝒇 𝒕𝒓𝒖𝒆
= 𝒕𝒓𝒖𝒆 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆 = 𝒇𝒂𝒍𝒔𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕=𝝀𝒃. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 𝒏𝒐𝒕 𝒇𝒂𝒍𝒔𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒏𝒐𝒕=𝝀𝒃. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆
=𝝀𝒃. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 𝒇𝒂𝒍𝒔𝒆
= 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒇𝒂𝒍𝒔𝒆𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆
= 𝝀𝒕. 𝝀𝒇 𝒇𝒂𝒍𝒔𝒆 𝒕 𝒇 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆
= 𝝀𝒇 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒇 𝒕𝒓𝒖𝒆 = 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
before attempting to Construct a Function Definition for the Logical Or, How would you Phrase it as a Conditional Statement?
Copyright © 2018 by . All Rights Reserved.
Logical Operations
What Happens if you Type the Following Python 3 Statements into Python in Interactive Mode?
False or False False or True True or False
Copyright © 2018 by . All Rights Reserved.
Logical Operations
What Happens if you Type the Following Python 3 Statements into Python in Interactive Mode?
False or False False or True True or False False or ‘a’
Copyright © 2018 by . All Rights Reserved.
Logical Operations
the Logical Or Function, applied to Two Operands
𝒂 and 𝒃, can be Phrased as: “If 𝒂 is True then 𝒂,
Otherwise 𝒃” Does that mean that
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 ? Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒕𝒓𝒖𝒆𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐
𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒕𝒓𝒖𝒆𝒕𝒓𝒖𝒆 = 𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆 𝒃𝟐 𝒕𝒓𝒖𝒆
= 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆 = 𝝀𝒕.𝝀𝒇𝒕𝒓𝒖𝒆𝒕𝒇 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆
= 𝝀𝒇𝒕𝒓𝒖𝒆𝒕𝒓𝒖𝒆𝒇 𝒕𝒓𝒖𝒆
= 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒕𝒓𝒖𝒆𝒇𝒂𝒍𝒔𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐
𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒕𝒓𝒖𝒆𝒇𝒂𝒍𝒔𝒆 = 𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆 𝒃𝟐 𝒇𝒂𝒍𝒔𝒆
= 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆 𝒇𝒂𝒍𝒔𝒆 = 𝝀𝒕.𝝀𝒇𝒕𝒓𝒖𝒆𝒕𝒇 𝒕𝒓𝒖𝒆 𝒇𝒂𝒍𝒔𝒆
= 𝝀𝒇𝒕𝒓𝒖𝒆𝒕𝒓𝒖𝒆𝒇 𝒇𝒂𝒍𝒔𝒆
= 𝒕𝒓𝒖𝒆 𝒕𝒓𝒖𝒆 𝒇𝒂𝒍𝒔𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐
𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒇𝒂𝒍𝒔𝒆𝒕𝒓𝒖𝒆 = 𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒃𝟐 𝒕𝒓𝒖𝒆
= 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆 = 𝝀𝒕. 𝝀𝒇 𝒇𝒂𝒍𝒔𝒆 𝒕 𝒇 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆
= 𝝀𝒇𝒇𝒂𝒍𝒔𝒆𝒇𝒂𝒍𝒔𝒆𝒇 𝒕𝒓𝒖𝒆
= 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒕𝒓𝒖𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒇𝒂𝒍𝒔𝒆𝒇𝒂𝒍𝒔𝒆
Copyright © 2018 by . All Rights Reserved.
Logical Operations
𝒐𝒓=𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐
𝝀𝒃𝟏.𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒃𝟏 𝒃𝟏 𝒃𝟐 𝒇𝒂𝒍𝒔𝒆𝒇𝒂𝒍𝒔𝒆 = 𝝀𝒃𝟐. 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒃𝟐 𝒇𝒂𝒍𝒔𝒆
= 𝝀𝒑. 𝝀𝒕. 𝝀𝒇 𝒑 𝒕 𝒇 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 = 𝝀𝒕. 𝝀𝒇 𝒇𝒂𝒍𝒔𝒆 𝒕 𝒇 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆
= 𝝀𝒇𝒇𝒂𝒍𝒔𝒆𝒇𝒂𝒍𝒔𝒆𝒇 𝒇𝒂𝒍𝒔𝒆
= 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆
Copyright © 2018 by . All Rights Reserved.
Additional Exercise
How would you Implement Exclusive Disjunction (i.e., XOR) in λ-Calculus?
Copyright © 2018 by . All Rights Reserved.
Looping and Recursion
the following Components (required for our classification as a Programming Language) are Supported by λ-Calculus
Integer Values Arithmetic Operations Boolean Values Logical Operations Branching
What still Remains? Copyright © 2018 by . All Rights Reserved.
Looping and Recursion
cnt = 0 i=0
i< len(bin)
bin[i] == '1'
cnt = cnt + 1
Any Problem Implementing this Functionally? Copyright © 2018 by . All Rights Reserved.
i< len(bin)
bin[i] == '1'
i≠i+1 i=i+1
cnt = cnt + 1
Looping and Recursion
cnt = 0 i=0
Referential Transparency would be Lost Copyright © 2018 by . All Rights Reserved.
Repeating Functions
with Imperative and Procedural Programming, Looping Control Structures are Controlled by Events (such as a Counter reaching a Specific Value)
this is Difficult to Achieve without Values that can Change (e.g., a Flag needs to Change from False to True, a Counter needs to Increase or Decrease in Value, etc.)
Copyright © 2018 by . All Rights Reserved.
Repeating Functions
What are the β-Reductions of 𝝀𝒙.𝒙 𝒚?
𝝀𝒙.𝒙𝒙 𝒚? 𝝀𝒙.𝒙𝒙 𝝀𝒙.𝒙𝒙?
𝝀𝒙.𝒛𝒙𝒙 𝝀𝒙.𝒛𝒙𝒙 ?
Copyright © 2018 by . All Rights Reserved.
Repeating Functions
Copyright © 2018 by . All Rights Reserved.
Repeating Functions
𝝀𝒙.𝒙𝒙 𝒚 =𝒚𝒚
Copyright © 2018 by . All Rights Reserved.
𝝀𝒙.𝒙𝒙 𝝀𝒙.𝒙𝒙 = 𝝀𝒙.𝒙𝒙 𝝀𝒙.𝒙𝒙 = 𝝀𝒙.𝒙𝒙 𝝀𝒙.𝒙𝒙
= 𝝀𝒙.𝒙𝒙 𝝀𝒙.𝒙𝒙 ... this is an Infinite Loop
(albeit one that Does Nothing) Copyright © 2018 by . All Rights Reserved.
Repeating Functions
Repeating Functions
𝝀𝒙.𝒛 𝒙𝒙 𝝀𝒙.𝒛 𝒙𝒙 =𝒛 𝝀𝒙.𝒛𝒙𝒙 𝝀𝒙.𝒛𝒙𝒙
=𝒛𝒛 𝝀𝒙.𝒛𝒙𝒙 𝝀𝒙.𝒛𝒙𝒙 ... this is also an Infinite Loop
(but at least it Does Some "Work" 𝒛) Copyright © 2018 by . All Rights Reserved.
Recursion and the Y-Combinator
𝒀=𝝀𝒇.𝝀𝒙.𝒇𝒙𝒙 𝝀𝒙.𝒇𝒙𝒙
this is the Y-Combinator, and it is Similar to the Previous Infinite Loop, except that the "Work" 𝒛 is a Function that can be Passed as a Parameter
Copyright © 2018 by . All Rights Reserved.
Recursion and the Y-Combinator
=𝝀𝒇. 𝝀𝒙.𝒇𝒙𝒙 𝝀𝒙.𝒇𝒙𝒙 𝒂
= 𝝀𝒙.𝒂𝒙𝒙 𝝀𝒙.𝒂𝒙𝒙 =𝒂 𝝀𝒙.𝒂𝒙𝒙 𝝀𝒙.𝒂𝒙𝒙
=𝒂𝒂𝝀𝒙.𝒂𝒙𝒙𝝀𝒙.𝒂𝒙𝒙 ... Copyright © 2018 by . All Rights Reserved.
Recursion and the Y-Combinator Why is the Y-Combinator so Special?
𝒀=𝝀𝒇.𝝀𝒙.𝒇𝒙𝒙 𝝀𝒙.𝒇𝒙𝒙
Copyright © 2018 by . All Rights Reserved.
Recursion and the Y-Combinator Why is the Y-Combinator so Special?
𝒀=𝝀𝒇.𝝀𝒙.𝒇𝒙𝒙 𝝀𝒙.𝒇𝒙𝒙 𝒀𝒂=𝒂(𝒀𝒂)=𝒂 𝒂 𝒀𝒂 =𝒂 𝒂 𝒂 𝒀𝒂
If you could Find a Way to Terminate it (Using a Branch, for instance) then you could use it to Achieve Recursion!
Copyright © 2018 by . All Rights Reserved.
Recursion and the Y-Combinator
in the interest of simplifying the next β-Reduction Example, please recall that we have Already Demonstrated the Ability of λ-Calculus to Encode Integers, Booleans, Multiply, and Branch...
Copyright © 2018 by . All Rights Reserved.
Recursion and the Y-Combinator
𝒀=𝝀𝒇.𝝀𝒙.𝒇𝒙𝒙 𝝀𝒙.𝒇𝒙𝒙 𝒀𝒂=𝒂(𝒀𝒂)=𝒂 𝒂 𝒀𝒂 =𝒂 𝒂 𝒂 𝒀𝒂
𝒛𝒆𝒓𝒐=𝝀𝒇. 𝝀𝒙.𝒙 𝒐𝒏𝒆= 𝝀𝒇. 𝝀𝒙.𝒇𝒙 𝒕𝒘𝒐=𝝀𝒇. 𝝀𝒙.𝒇(𝒇𝒙) 𝒕𝒉𝒓𝒆𝒆=𝝀𝒇. 𝝀𝒙.𝒇(𝒇(𝒇𝒙))
𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚=𝝀𝒎.𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒏 𝒎𝒇 𝒙
𝒕𝒓𝒖𝒆= 𝝀𝒙. 𝝀𝒚.𝒙 𝒇𝒂𝒍𝒔𝒆 = 𝝀𝒙. 𝝀𝒚. 𝒚
𝒊𝒇𝒆𝒍𝒔𝒆= 𝝀𝒑.𝝀𝒕.𝝀𝒇𝒑𝒕𝒇
Copyright © 2018 by . All Rights Reserved.
Recursion and the Y-Combinator
in the interest of simplifying the next β-Reduction Example, please recall that we have Already Demonstrated the Ability of λ-Calculus to Encode Integers, Booleans, Multiply, and Branch...
... and although we Did Not Demonstrate Equality or Subtraction, hopefully you will accept my promise that they do Exist
Copyright © 2018 by . All Rights Reserved.
Recursion Example
What does the following Function Implement? 𝝀𝒇.𝝀𝒏.𝒊𝒇𝒆𝒍𝒔𝒆=𝒏𝒐𝒏𝒆 𝒐𝒏𝒆 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚𝒏𝒇 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕𝒏𝒐𝒏𝒆
n.b., as a hint consider that recursion lectures typically start with the same operation...
Copyright © 2018 by . All Rights Reserved.
Recursion Example
𝒂 = 𝝀𝒇. 𝝀𝒏. 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒏 𝒐𝒏𝒆 𝒐𝒏𝒆 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒏 𝒇 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒏 𝒐𝒏𝒆
= 𝝀𝒇.𝝀𝒏. 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒏 𝒐𝒏𝒆
= 𝝀𝒏. 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒏 𝒐𝒏𝒆
= 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒐𝒏𝒆 𝒐𝒏𝒆
𝒀𝒂 𝒐𝒏𝒆 =𝒂 𝒀𝒂 𝒐𝒏𝒆
𝒐𝒏𝒆 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒏 𝒇 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒏 𝒐𝒏𝒆 𝒀 𝒂 𝒐𝒏𝒆
𝒐𝒏𝒆 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒏 𝒀 𝒂 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒏 𝒐𝒏𝒆 𝒐𝒏𝒆
𝒐𝒏𝒆 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒐𝒏𝒆 𝒀 𝒂 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒐𝒏𝒆 𝒐𝒏𝒆
= 𝒊𝒇𝒆𝒍𝒔𝒆 𝒕𝒓𝒖𝒆 𝒐𝒏𝒆 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒐𝒏𝒆 𝒀 𝒂 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒐𝒏𝒆 𝒐𝒏𝒆 = 𝒐𝒏𝒆
Copyright © 2018 by . All Rights Reserved.
Recursion Example
𝒂 = 𝝀𝒇. 𝝀𝒏. 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒏 𝒐𝒏𝒆 𝒐𝒏𝒆 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒏 𝒇 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒏 𝒐𝒏𝒆
𝒀𝒂 𝒕𝒘𝒐 =𝒂 𝒀𝒂 𝒕𝒘𝒐
= 𝝀𝒇.𝝀𝒏. 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒏𝒐𝒏𝒆 𝒕𝒘𝒐 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚𝒏𝒇 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕𝒏𝒐𝒏𝒆 𝒀𝒂 𝒕𝒘𝒐
= 𝝀𝒏. 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒏 𝒐𝒏𝒆 𝒕𝒘𝒐 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒏 𝒀 𝒂 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒏 𝒐𝒏𝒆 𝒕𝒘𝒐
= 𝒊𝒇𝒆𝒍𝒔𝒆 = 𝒕𝒘𝒐 𝒐𝒏𝒆 𝒕𝒘𝒐 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒕𝒘𝒐 𝒀 𝒂 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒕𝒘𝒐 𝒐𝒏𝒆
= 𝒊𝒇𝒆𝒍𝒔𝒆 𝒇𝒂𝒍𝒔𝒆 𝒕𝒘𝒐 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒕𝒘𝒐 𝒀 𝒂 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒕𝒘𝒐 𝒐𝒏𝒆 = 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒕𝒘𝒐 𝒀 𝒂 𝒔𝒖𝒃𝒕𝒓𝒂𝒄𝒕 𝒕𝒘𝒐 𝒐𝒏𝒆
=𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚𝒕𝒘𝒐 𝒀𝒂 𝒐𝒏𝒆 = 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒚 𝒕𝒘𝒐 𝒐𝒏𝒆
refer to the Previous Slide for this
Copyright © 2018 by . All Rights Reserved.
Introducing λ-Calculus as a Language
we could continue by showing that Structures (like Lists, Trees, etc.,) are also Possible, but by now you have (hopefully) been convinced that
Any Computable Function can be Expressed and Evaluated with λ-Calculus (even if it is not easy to do so)
from a Practical perspective
(i.e., as COMP3007 Students) Why should you Care?
Copyright © 2018 by . All Rights Reserved.
Introducing λ-Calculus as a Language
Haskell is actually Compiled into something Similar to λ-Calculus, so Knowing How λ-Calculus
is Evaluated will Help you Understand Evaluation in Haskell (and the Neat "Tricks" you can Achieve)
n.b., you may also find λ-Calculus useful one day if you want to add something to a programming language (but that would be an additional benefit and isn't expected here)
Copyright © 2018 by . All Rights Reserved.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com