编程代考 Arithmetic using λ-Calculus

Arithmetic using λ-Calculus
Copyright © 2018 by . All Rights Reserved.

Learning Outcomes

by the End of the Lecture, Students that Complete
the Recommended Exercises should be Able to:
Explain How Numbers can be Represented Evaluate an Expression using Successor Demonstrate How Arithmetic Operations are Possible Evaluate Expressions using Addition, Multiplication
Copyright © 2018 by . All Rights Reserved.

Reading and Suggested Exercises
Copyright © 2018 by . All Rights Reserved.
Read the following Chapter(s): None

to Demonstrate that λ-Calculus is capable of Arithmetic, we need an Approach for Representing Numbers using Functions
Church Encoding (named for ) is a Technique for Representing Non-Negative Integers using Repeated Function Compositions
Copyright © 2018 by . All Rights Reserved.
Church Encoding

the Most Common (but by no means the only) way to Represent Zero with a Function
𝒛𝒆𝒓𝒐=𝝀𝒇. 𝝀𝒙.𝒙
(n.b., once we define addition we can test if this is really the identity element of addition) How will we Represent the Other Numbers?
Church Encoding
Copyright © 2018 by . All Rights Reserved.

the Church Numeral 𝑛 is a Function that takes the Function 𝑓 as an Argument and Returns the 𝑛th Composition of 𝑓
in other words, the Number of Times a Function is “Wrapped” is Used to Represent the Numerical Value
Copyright © 2018 by . All Rights Reserved.
Church Encoding

𝒛𝒆𝒓𝒐=𝝀𝒇. 𝝀𝒙.𝒙
𝒐𝒏𝒆=𝝀𝒇. 𝝀𝒙.𝒇𝒙 𝒕𝒘𝒐=𝝀𝒇. 𝝀𝒙.𝒇 𝒇𝒙
𝒕𝒉𝒓𝒆𝒆=𝝀𝒇. 𝝀𝒙.𝒇 𝒇 𝒇𝒙
𝒏=𝝀𝒇. 𝝀𝒙.𝒇𝒏𝒙
Church Encoding
Copyright © 2018 by . All Rights Reserved.

Successor Function
What is the value of One? …Relative to the Value of Zero?
What is the value of Two Relative to the Value of One? What is the value of Two Relative to the Value of Zero?
Copyright © 2018 by . All Rights Reserved.

Successor Function
What is this Function? Copyright © 2018 by . All Rights Reserved.

Successor Function
the Function 𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 takes a Nonnegative Integer as an Argument and Returns the Integer that
is Greater than the Argument by One
the Application of the 𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 Function to the Nonnegative Value 𝒏 is Represented in λ-Calculus as
𝝀𝒏.𝝀𝒇.𝝀𝒙.𝒇 𝒏𝒇𝒙
Copyright © 2018 by . All Rights Reserved.

Successor Function
performing β-Reduction on the Application of the 𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 Function to the Church Encoding of 0 should Result in the Church Encoding for 1
performing β-Reduction on the Application of the 𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 Function to the Church Encoding of 1 should Result in the Church Encoding for 2
Copyright © 2018 by . All Rights Reserved.

Successor Function Does (𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 𝒛𝒆𝒓𝒐) Reduce to 𝒐𝒏𝒆?
𝝀𝒏. 𝝀𝒇. 𝝀𝒙. 𝒇 𝒏𝒇 𝒙 𝒛𝒆𝒓𝒐
Copyright © 2018 by . All Rights Reserved.

Successor Function Does (𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 𝒛𝒆𝒓𝒐) Reduce to 𝒐𝒏𝒆?
𝝀𝒏. 𝝀𝒇. 𝝀𝒙. 𝒇 𝒏𝒇 𝒙 𝒛𝒆𝒓𝒐 𝝀𝒇. 𝝀𝒙. 𝒇 𝒛𝒆𝒓𝒐𝒇 𝒙
Copyright © 2018 by . All Rights Reserved.

Successor Function Does (𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 𝒛𝒆𝒓𝒐) Reduce to 𝒐𝒏𝒆?
𝝀𝒏. 𝝀𝒇. 𝝀𝒙. 𝒇 𝒏𝒇 𝒙 𝒛𝒆𝒓𝒐
𝝀𝒇. 𝝀𝒙. 𝒇 𝒛𝒆𝒓𝒐𝒇 𝒙 𝝀𝒇.𝝀𝒙.𝒇 𝝀𝒈.𝝀𝒚.𝒚𝒇𝒙
Copyright © 2018 by . All Rights Reserved.

Successor Function
𝝀𝒇.𝝀𝒙.𝒇 𝝀𝒈.𝝀𝒚.𝒚𝒇𝒙
β-Reduce by Replacing Instances of the Variable in Expression with Expression
Copyright © 2018 by . All Rights Reserved.

Successor Function
𝝀𝒇.𝝀𝒙.𝒇 𝝀𝒈.𝝀𝒚.𝒚𝒇𝒙
β-Reduce by Replacing Instances of the Variable in Expression with Expression
𝝀𝒇. 𝝀𝒙. 𝒇 𝝀𝒚.𝒚 𝒙
Copyright © 2018 by . All Rights Reserved.

Successor Function
𝝀𝒇.𝝀𝒙.𝒇 𝝀𝒈.𝝀𝒚.𝒚𝒇𝒙
β-Reduce by Replacing Instances of the Variable in Expression with Expression
𝝀𝒇. 𝝀𝒙. 𝒇 𝝀𝒚.𝒚 𝒙
β-Reduce by Replacing Instances of the Variable in Expression with Expression
Copyright © 2018 by . All Rights Reserved.

Successor Function
Does (𝒔𝒖𝒄𝒄𝒆𝒔𝒔𝒐𝒓 𝒐𝒏𝒆) Reduce to 𝒕𝒘𝒐?
Copyright © 2018 by . All Rights Reserved.

Arithmetic in λ-Calculus 𝒂𝒅𝒅𝒊𝒕𝒊𝒐𝒏 takes Two Nonnegative Integers
as Arguments and Returns the Sum
the Application of the 𝒂𝒅𝒅𝒊𝒕𝒊𝒐𝒏 Function to the
Nonnegative Values 𝒎 and 𝒏 is Represented as 𝝀𝒎.𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒎𝒇 𝒏𝒇𝒙
Copyright © 2018 by . All Rights Reserved.

Arithmetic in λ-Calculus
How would you Evaluate the Result of 𝝀𝒎.𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒎𝒇 𝒏𝒇𝒙 𝒛𝒆𝒓𝒐𝒕𝒘𝒐
Copyright © 2018 by . All Rights Reserved.

Arithmetic in λ-Calculus
Is this Expression Valid?
Can you Identify the Components?
𝝀𝒎.𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒎𝒇 𝒏𝒇𝒙 𝒛𝒆𝒓𝒐𝒕𝒘𝒐
Copyright © 2018 by . All Rights Reserved.

𝝀𝒎.𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒎𝒇 𝒏𝒇𝒙
the “Result” of this -Reduction will be a Function and 𝒕𝒘𝒐 will be the Argument
so, what is this then?
Arithmetic in λ-Calculus
Is this Expression Valid?
Can you Identify the Components?
Copyright © 2018 by . All Rights Reserved.

𝝀𝒎.𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒎𝒇 𝒏𝒇𝒙
𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒛𝒆𝒓𝒐𝒇 𝒏𝒇𝒙 𝝀𝒇. 𝝀𝒙. 𝒛𝒆𝒓𝒐𝒇 𝒕𝒘𝒐𝒇 𝒙
𝒛𝒆𝒓𝒐𝒕𝒘𝒐 𝒕𝒘𝒐
Arithmetic in λ-Calculus
𝝀𝒇. 𝝀𝒙. 𝝀𝒈. 𝝀𝒚.𝒚 𝒇 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛
𝝀𝒇. 𝝀𝒙. 𝝀𝒚.𝒚 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛 𝒇 𝒙
𝝀𝒇. 𝝀𝒙. 𝝀𝒚.𝒚 𝝀𝒛. 𝒇 𝒇𝒛 𝒙 𝝀𝒇. 𝝀𝒙. 𝝀𝒚.𝒚 𝒇 𝒇𝒙
𝝀𝒇. 𝝀𝒙. 𝒇 𝒇𝒙
Copyright © 2018 by . All Rights Reserved.

Arithmetic in λ-Calculus 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒊𝒄𝒂𝒕𝒊𝒐𝒏 takes Two Nonnegative Integers
as Arguments and Returns the Product
the Application of the 𝒎𝒖𝒍𝒕𝒊𝒑𝒍𝒊𝒄𝒂𝒕𝒊𝒐𝒏 Function to the
Nonnegative Values 𝒎 and 𝒏 is Represented as 𝝀𝒎.𝝀𝒏.𝝀𝒇.𝝀𝒙. 𝒏𝒎𝒇𝒙
Copyright © 2018 by . All Rights Reserved.

Arithmetic in λ-Calculus
𝝀𝒎. 𝝀𝒏. 𝝀𝒇. 𝝀𝒙. 𝒏 𝒎𝒇 𝒙 𝒕𝒘𝒐𝒕𝒉𝒓𝒆𝒆 𝝀𝒏. 𝝀𝒇. 𝝀𝒙. 𝒏 𝒕𝒘𝒐𝒇 𝒙 𝒕𝒉𝒓𝒆𝒆
𝝀𝒇. 𝝀𝒙. 𝒕𝒉𝒓𝒆𝒆 𝒕𝒘𝒐 𝒇 𝝀𝒇.𝝀𝒙. 𝝀𝒈.𝝀𝒚.𝒈𝒈𝒈𝒚
𝝀𝒇.𝝀𝒙. 𝝀𝒈.𝝀𝒚.𝒈𝒈𝒈𝒚
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝒕𝒘𝒐𝒇 𝒕𝒘𝒐𝒇 𝒕𝒘𝒐𝒇 𝒚 𝒙
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝒕𝒘𝒐𝒇 𝒕𝒘𝒐𝒇 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛 𝒇 𝒚 𝒙
Copyright © 2018 by . All Rights Reserved.

Arithmetic in λ-Calculus
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝒕𝒘𝒐𝒇 𝒕𝒘𝒐𝒇 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛 𝒇 𝒚
𝝀𝒇.𝝀𝒙.𝝀𝒚. 𝒕𝒘𝒐𝒇 𝒕𝒘𝒐𝒇 𝝀𝒛.𝒇𝒇𝒛 𝒚 𝒙 𝝀𝒇.𝝀𝒙.𝝀𝒚.𝒕𝒘𝒐𝒇𝒕𝒘𝒐𝒇𝒇𝒇𝒚 𝒙
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝒕𝒘𝒐𝒇 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛 𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝒕𝒘𝒐𝒇 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝒕𝒘𝒐𝒇 𝝀𝒛. 𝒇 𝒇𝒛
𝒇 𝒇 𝒇𝒚 𝒇 𝒇 𝒇𝒚
Copyright © 2018 by . All Rights Reserved.

Arithmetic in λ-Calculus
𝝀𝒇.𝝀𝒙.𝝀𝒚. 𝒕𝒘𝒐𝒇 𝒇𝒇𝒇𝒇𝒚 𝒙
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛 𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝝀𝒉. 𝝀𝒛. 𝒉 𝒉𝒛
𝒇 𝒇 𝒇 𝒇 𝒇𝒚 𝒙
𝒇 𝒇 𝒇 𝒇 𝒇𝒚 𝒙 𝒇 𝒇 𝒇 𝒇𝒚 𝒙
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝝀𝒛. 𝒇 𝒇𝒛
𝝀𝒇. 𝝀𝒙. 𝝀𝒚. 𝒇 𝒇 𝒇 𝒇 𝒇 𝒇𝒚 𝒙
Copyright © 2018 by . All Rights Reserved.
𝝀𝒇. 𝝀𝒙.𝒇 𝒇 𝒇 𝒇 𝒇 𝒇𝒙

Arithmetic in λ-Calculus
Subtraction and Division are also Possible but the Predecessor Function is Substantially Harder than the Successor Function was
n.b., for our purposes, if you can accept that it is possible then that is sufficient
Having Established that it is Possible to Build a Calculator, What would it take to Convince you that you can Also Build a Computer?
Copyright © 2018 by . All Rights Reserved.

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

Related Posts