λ Calculus (2013) [pdf]
cs.rpi.edu
cs.rpi.edu
He does a wonderful job of taking very dense mathematical notation and explaining it in ways that anyone can understand. He derives the basic concepts of the lambda calculus from the ground up using Python. Super fun to follow along with.
successor function: given a number, get the next number
try this in Python:
zero = lambda f: lambda x: x
one = lambda f: lambda x: f(x)
two = lambda f: lambda x: f(f(x))
to_int = lambda n: n(lambda i: i+1)(0)
succ = lambda n: lambda f: lambda x: f(n(f)(x))
three = succ(two)
four = succ(three)
to_int(four)
So that's just counting, the Church Numerals, where it begins.
|0| = λx. x
|n+1| = λ_. |n|
Can we write a function that tests if a numeral represents 0? I.e. a function f such that
f |0| = True
f |n+1| = False
This reminds me of someone proposing to represent the number n in combinatory logic with basis {S,K} as simply S^n K, i.e. using K as Zero and S as Successor. That one does turn out to be convertible to Church numerals [1].
The expansion into |n|(args...) must happen before we know what n is, because in the lambda calculus we can't know anything about a function without calling it. Since it happens before we know what n is, then the number of args will necessarily be the same for all n. When n > numargs, |n|(args...) ignores all its arguments and halts, and therefore f cannot be a useful test for zero.
Actually, this is not true. f |n| could expand into \x. \y. (|n| args...) instead, where the args contain x and y. But the rest of your argument still applies to the application of |n|.
Another slight correction/expansion is that (|n| args...) = n - numargs when n >= numargs. This happens to coincide with False when n = numargs + 1, so it would have been better if I had said "when n > numargs + 1".
> When n > numargs, |n|(args...) ignores all its arguments and halts
I would say it reduces to a term of the form \_. \_. M that is definitely different from both False and True.
[1] http://wcl.cs.rpi.edu/pdcs/slides/Chapter2-LambdaCalculus.pp...
> This combinator guarantees that x is evaluated before y, which is important in programs with side-effects
This part didn't make sense to me. I can apply Seq to x = Ω = (λx.x x)(λx.x x) and y = (λa.λb.b) and z = λx.x, resulting in Seq x y z = y x = λb.b, which leaves x unevaluated.
A sequencing operator cannot be defined within the lambda calculus, which has no notion of side-effect; it must be a function defined in a runtime, i.e. in an implementation of lambda calculus. An example is the function seq in Haskell.
For kids: http://worrydream.com/AlligatorEggs/ and: https://metatoys.org/alligator/
A lambda calculus calculator: https://lambster.dev/
A tetris style game for learning combinators: https://dirk.rave.org/combinatris/
Also, York University in Canada confused things.
# a factorial function written entirely with just single-argumented lambdas
# and calls
fac = ((lambda p: p(p)(lambda q: lambda n: ((n(lambda e: lambda e:
lambda a: a)(lambda i: lambda l: i))(lambda d: lambda c: c)
(lambda m: (lambda m: lambda z: m(n(z)))(q(m)))((lambda c: lambda x:
n(lambda g: lambda h: h(g(c)))(lambda u: x)(lambda u: u))))))
(lambda s: lambda q: lambda w: q(s(s)(q))(w)))
# for converting between church numerals and python numbers (you need
# a few python functions and operators to manipulate them)
natural = lambda c: c(lambda x: x+1)(0)
church = lambda n: reduce(lambda x,y:
(lambda n: lambda f: lambda x: f(n(f)(x)))(x), range(n), lambda f: lambda x: x)
# test!
# fac(10) is about the highest number computing in a few seconds on a core 2 CPU
print natural(fac(church(10)))You might find this interesting:
There was a concerted effort in the late 19th, early 20th century (perhaps earlier too) to mechanise computation i.e., reducing it to a pure symbolic manipulation. There were obvious benefits, a famous one being Enigma Machine that was used to (successfully I think) break the German code during WW-2.
On the philosophical side a parallel and overlapping effort was going on to figure out if mathematics could represent all possible truths, again as symbolic manipulation system. Bertrand Russel's magnum opus Principia Mathematica [1] was one such famous work towards it. Kurt Gödel then made a breakthrough when he proved that such a system is impossible; i.e., a system can either capture all the truths or it can be consistent but not both[2]. Put differently, any mathematical system capable of representing all the truths will necessarily contain contradictions within it.
Now coming to your question.
Lambda calculus emerged in this milieu. Alonzo Church[3] invented one such system to mechanise computation, named ƛ-calculus. Using this system one can mechanically compute any function purely by symbolic manipulation. Later on Turing, Church's student I think, invented a totally different system named Turing Machine with the same purpose. Later on it was proved (by Church and Turing I think, but I'm not 100% sure) that ƛ-Calculus and Turing Machine are equivalent, Church-Turing thesis[4].
All these work, and more, laid the theoretical foundation for the modern computers. If we can today safely assume that computers are provably correct it's because of them.
Phil Wadler has an absolutely delightful talk where he takes us through a whirlwind tour of the history of the mathematical foundation of computers [5], highly recommended.
[1] https://en.wikipedia.org/wiki/Principia_Mathematica
[2]https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...
[3] https://en.wikipedia.org/wiki/Alonzo_Church
There's no inherent connection. You're perfectly free to interpret lambda terms as functions on a domain, or function definitions as abstract rewrite rules.
Shouldn't that be:
f(x) = x^2, f : Z → Z+
?Z+ is not the range of this f either; it is Z^{>=0}.
Carlos A. Varela
2013
https://mitpress.mit.edu/9780262018982/programming-distribut...
He's also a certified pilot.
Drumming is some of that but other than motorcycles I've not found anything else that comes close to flying. I've never tried sailing but maybe that too?
Even more beautiful than the y combinator
That's a bit of a strange statement. The Y combinator is an expression in λ calculus. It's like saying French is even more beautiful than the phrase "nouveau départ".
Y = λf.(λx.f (x x)) (λx.f (x x))The Y combinator is a specific fixed-point combinator in lambda calculus. It is used to express recursion in lambda calculus where direct recursion is not initially available due to the lack of named functions. The Y combinator demonstrates the power of lambda calculus.
I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.
so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it
if you can't, you may have gained enough insight into the problem to show that the system actually does guarantee termination, and maybe even show useful time bounds on it
if you can, you have usually shown the system is turing-complete, which means you can appeal to rice's theorem whenever you are tempted to analyze the behavior of the system in any way, so you can satisfy yourself with partial decision procedures that work often enough to be useful and are conservative in the appropriate way, rather than wasting time trying to find a complete solution
(also if you're designing the system you might consider either supporting iteration more directly or removing the back door)
every once in a while it's also useful in practice to be able to program a weird machine, too
This is only the case for untyped systems. If we try to type the Y combinator, we will eventually need some notion of recursion. For example, in Haskell/OCaml we can type it with iso/equi-recursive types. How many truly untyped systems we use in practice?
The Y combinator as a counterexample of termination is a great insight though!
You might argue they are unityped, but that’s really a type theoretician’s job security: if a language has the untyped lambda calculus as a subset (like the python example in this discussion) it’s reasonable to call it untyped.