NOTE: What is lambda calculus
source link: https://dannypsnl.github.io/blog/2020/01/01/cs/note-what-is-lambda-calculus/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
NOTE: What is lambda calculus
What is lambda-calculus? Or, more specific, what is untyped/pure lambda-calculus? To answer this, I wrote the note for myself. Lambda-calculus was a formal system invented by Alonzo Church in the 1920s, and we can enrich it in a variety of ways, for example, adding special concrete syntax like numbers, tuples, records, etc. Such extensions eventually lead to languages like ML, Haskell, or Scheme.
For easy functionality, we usually would do it directly, like +1
is quite simple for most people, but for those complex operations(or had special meaning like math formula), repeat them would be an annoying job. So we created procedural/functional abstraction. For example: square(x) = x^2
.
The syntax of lambda-calculus comprises just three sorts of terms, the following syntax use BNF[1] form:
term ::= terms
x variable
λx.term abstraction
term term application
A variable x
by itself is a term; an abstraction of a variable x
from a term t1
, written λx.t1
, is a term; an application of a term t1
to another term t2
, written as t1 t2
, is a term.
β\betaβ-reduction
If an expression of the form (λx. M) N
is a term, then we can rewrite it to M[x := N]
, i.e. The expression M
in which every x
has been replaced with N
. We call this process β\betaβ-reduction[2] of (λx. M) N
to M[x := N]
. For example (λx. (x + 1)) 2
(assume that we add numbers into lambda-calculus), where M
is x + 1
and N
is 2
, (x+1)[x := 2]
would produce 2 + 1
as the result. BTW, we also use
this form.
Currying(in honor of Haskell Curry)
The behavior of a function of two or more arguments can be simulated by converting it into a composite of functions of a single argument was called Currying[3]. For example λ(x y). M
can write λx. (λy. M)
.
Church Booleans
Definition:
How to use it, first we define a and
function.
Then apply with arguments:
or
and not
function:
We even can create ifThenElse
:
Church Numerals
Represent Numbers by lambda-calculus is only slightly more intricate than Booleans. First, we define successor function(called suc
) and some numbers:
Once we got the idea that suc 0
is the construction of 1
and suc suc 0
is the construction of 2
. We know the construction of church numbers was s
and suc
was trying to take n
(previous number) to construct the next number suc n
, we keep λs.λz
as common prefix and add s
into body, n s z
consume the previous λs.λz
part.
Then we can define the add
and times
function for them:
add
takes two arguments: m
and n
, but we keep λs.λz
as usual to make it been a number, then we can demonstrate it:
mult
can define as:
Evaluation Rules (t→t′t \to t't→t′)
References
Types and Programming Languages
- Author: Benjamin C. Pierce
- ISBN: 0-262-16209-1
Types Theory and Formal Proof: An Introduction
- Author: Rob Nederpelt & Herman Geuvers
- ISBN: 9781316056349
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK