Skip to main content r/math

Search in r/math Log In

r/math • 12y ago

[deleted]

What are applications of lambda calculus?

I've been taking some basic computer science classes and recently have been doing a little reading on lambda
calculus. I don't really understand what makes it different from any other formal system and thought I'd come here
for an explanation. Why is it a powerful tool? What sets it apart? I've read that lambda calculus was used to solve
the Entscheidungsproblem and was interested in finding out exactly what made it a viable method for doing so.

21 · 21

ClickUp_App • Promoted

The everything app, for work. Get everyone working in a single platform designed to
manage any type of work.

Learn More [Link]

tfb • 12y ago

I think there is a distinction between power and usefulness by humans.

It's known that lambda calculus has the same power as a universal Turing machine, so you might argue that
it has no real benefit: why not just that formalism?

Well, I think the answer is that if you want a system in which to actually express computations as opposed to
a system which will let you answer various questions about what is computable, then you want a system
which is easy to use by humans. That's why we write programs in high-level languages: patching the hex is
all very well for Real Programmers, but the rest of us need a language in which it's easy to express ideas.
Turing machines are patching the hex, so we want something more human-friendly than that.

And lambda calculus is an example of something which is more human-friendly, while remaining formally
well-defined.

I've carefully avoided saying why lambda calculus is more human-friendly, because I don't know. What I do
know is that lambda calculus has given rise to a significant family of programming languages which combine
great power with great expressivity, and which turn out to be very pleasant to program in for people willing to
spend the time on them. These languages include, famously, the Lisp family, but also many purer functional
programming languages. So today I can type to my scheme interpreter:

> (((λ (f) (λ (g) (f g))) (λ (f) f)) 1)

1
 (which is not meant to do anything useful, I just didn't want to to the normal ((λ (x) (+ x x)) 2) thing
Skip to main content
because that relies on + ). Log In

13

[deleted] OP • 12y ago

So what you're saying is that although lambda calculus is equivalent to a Turing machine in what it's
capable of expressing, lambda calculus is easier for humans to understand. If you don't mind going on, is
either formalism more theoretically powerful than the other in any situation, or are they just two ways of
representing the exact same thing? Also, could you explain the meaning of the expression you wrote?
3

sumoruman • 12y ago

To give you an idea of how easy LC is to understand, have a look at this video which shows a
programmer building up a FizzBuzz program using the Lambda Calculus (in Ruby).
4

frankster • 12y ago

Basically Church came up with the lambda calculus at around the same time (or slightly before?) that
Turing independently came up with universal machines. It was later demonstrated that they were
equivalent or sthg like that.
3

Nerdlinger • 12y ago

They are sort of ways of representing the same thing in that one system can simulate the other.
All the lambda calculus is is a system for modeling computating using nothing but function
composition and evaluation. There is no notion of memory, for example, like with the Turing machine
tape, but it can be simulated. There is no notion of integers, though they can be represented by
functions which can be manipulated by other functions to perform math, and so on.

A similar notion to this is the pi calculus, which models computation entirely through message passing
and is also equivalent in power to the lambda calculus.

edit: A good introductory read on both of these systems is Benjamin Pierce's Foundational Calculi for
programming languages.
2

yen223 • 12y ago

Not the OP, but I guess it depends on which model of calculation you're more comfortable with. As a
programmer, I actually prefer the Turing machine, because it's conceptually closer to how things work
at a CPU level.

But I understand mathematicians prefer partially recursive functions and all that jazz. And like u/tfb
mentioned, functional programming languages, which are loosely based on lambda calculus, have
certain advantages that make them easy to reason about.
The key point behind the Church-Turing thesis is it doesn't matter which you choose, because
algorithms that can be performed in one model, can also be expressed in the other.
1
 1 more reply
Skip to main content
Log In
tfb • 12y ago
They are formally equivalent.
In Scheme (or similar) an expression like (λ (x) t) is the same as λx.t in the traditional notation (as
described here), and (t s) is the same as ts in the same notation. If we allow numerals to stand for
themselves (just to make my expression make sense, and adding some parens to make things a bit
clearer, then the Scheme expression is
((λf.(λ[Link]))(λf.f))1

Well that's confusing because I've used f twice so we can rename it (this is alpha equivalence I think)
to get
((λf.(λ[Link]))(λh.h))1
OK, so looking at the inner thing, we're applying λf.(λ[Link]) to λh.h and we can do that (beta reduction)
to get λg.(λh.h)g. Now we are applying this function to the numeral 1, so we get (λh.h)1 and one final
reduction gives 1.
Note that in Lisp/Scheme parentheses are never optional, which is rather different than the standard
notation. Note also that you'd never actually write programs like this unless it was to torture students.
1

dagit • 12y ago

It's known that lambda calculus has the same power as a universal Turing machine

Interestingly, the equivalence breaks down at higher types:

[Link]
lambda-calculus-and-turing-mac
1

myfootinyourmouth • 12y ago

I don't know much about it, but it seems like L.S. is a basis for functional languages like LISPs.
7

5outh • 12y ago

Yep. Unityped LC is the basis for most LISPs, and more featureful typed lambda calculi are the basis for
other like Haskell (modified system F) and Idris (lambda pi, i.e dependently typed lambda calculus). Coq
and Agda are automated theorem provers that use dependently typed lambda calculus as a basis as well.
2

[deleted] • 12y ago

I worked on Featherweight Java, a model of Java with strong types. The model is built with an extension of
lambda calculus, and is used to prove for example type correctness and completude of a restriction of the
Java language (i'm not sure all I said makes sense, this was some years ago).
3
Skipu/bloomberg • Promoted
to main content
Log In
For investors seeking pre-IPO exposure, access comes with caveats and
constraints.

Learn More [Link]

[deleted] • 12y ago

The lambda calculus serves as a model of computation similar to the turing machine. But while the turing
machine models a computer in terms of some mechanical system, the lambda calculus does it in terms of a
recursively defined rewrite system. Because of its recursive nature, it tends to be more compositional. You
can combine smaller terms into larger ones. This makes it easy to study programming languages using
mathematical tools. (The turing machine, on the other hand, has a simpler cost model, making it better for
studying algorithms).

The lambda calculus is also a logic. It was originally created to solve one of the many early formulations of
the halting problem. It turned out, though, that the raw untyped lambda calculus allowed for unrestricted
recursion (the fixedpoint combinators), making it unsuitable for logic (turing completeness in a logic makes
your logic inconsistent. The liar's paradox is just an infinite loop).

To fix this problem, Church revised the lambda calculus, adding types to it. The "simply typed" lambda
calculus restrict the expressivity of the language severely, but kept it consistent.

Over the years, people worked on expanding the expressivity while maintaining consistency. One very
famous succcessful attempt was System F, a lambda calculus reminicent of 2nd order logic. It is not turing
complete, but it's powerful enough to write a sorting algorithm for lists, and theoretically, larger software
systems, as long as they don't ask for a self-evaluator.
Programming languages guys got ahold of lambda calculus when computers became available and they
loved it. It is the foundation of Lisp, ML, Haskell, Coq, and the many variations on those. In most languages
(save Coq and other "Dependently typed languages"), consistency is forfeited, but the typing discipline is
kept in some capacity because it was found to be useful as a sanity check for the programmer.
2

[deleted] • 12y ago

Emacs :)
2

[deleted] • 12y ago

MathBosss • 12y ago

It pretty much is what powers Haskell. This idea of composition of functions
1
 daymi • 12y ago
Skip to main content
Log In
I don't really understand what makes it different from any other formal system

it's simple (few parts, each does only one thing).

it's powerful, it's thought to be as powerful as any other formal system can be. If anything, it's too
powerful.
it's understandable. All it does it generalize functions.

All other formal systems I know are either an awful mess (many parts, each part does 30 unrelated things),
too weak (primitive recursive functions) or inhuman (combinatory logic).

Why is it a powerful tool? What sets it apart?

I've read that lambda calculus was used to solve the Entscheidungsproblem and was interested in
finding out exactly what made it a viable method for doing so.

All mathematical expressions and statements can be modeled using lambda calculus. Then you encode
these lambda expressions as a number. Then you can try to make a theory for finding things out about these
numbers. Then it was tried to make tools that tell you things about statements without actually having to
evaluate the statements (finding whether they are true or false) directly. Turns out for the very interesting
cases this is not actually possible. For a limited class of problems, it is possible (!!).

Lambda calculus is small and a powerful set you need for expressing yourself. So it was used as "source"
material instead of more complicated ones which would have made you want to hit yourself, what with the
34332 different productions you have to encode - and for no gain.
Depending on your level of familiarity, you might think that you need lambda calculus and numbers and
booleans. That is not true. I thought so in the beginning as well. But actually, as a foundation lambda calculus
suffices on its own. No built-in numbers, boolean, sets, lists, ... . Or maybe you need built-in conditionals or
loops or recursion? No. Implication, equivalence, comparison etc? No.
Just these:

means for referring to things, called "symbols". For example: x

means for parametrizing things (which you want to keep variable), for example (keeps x variable): λx.B
means for substituting a value for a parameter in B. For example (substitutes y for x in B): (λx.B) y
(eventual evaluation keeps substituting as needed and is how you reduce the source expression to a
value, so it's called reduction)

Nothing else. If that sounds familiar to functions in "normal" school mathematics, it should. Note that the
domain and codomain are also such functions.
Can do all of mathematics, all computation.

Practical applications: (almost) all modern programming languages. Even the ones who weren't based on it
on purpose will end up being based on it by natural improvements.

What was really new is that this has functions take functions and then do something with them. And I don't
mean f(g(x)) or something, I mean f(g). This was the most important step and makes possible very strange
things.
 For example, if you don't have builtin natural numbers, what can you do to get them? Well assume we had a
Skip to main content
Log In
way, given a number, to get a successor. But we don't. So parametrize the way. Later never substitute
anything for it. Call such an expression "natural number".

This trick is called "lambda lifting" and I associate it to the (half-in-jest) saying in Informatics: "All problems
can be solved by an extra level of indirection".
1

[deleted] • 12y ago

Depending on your level of familiarity, you might think that you need lambda calculus and
numbers and booleans. That is not true. I thought so in the beginning as well. But actually, as a
foundation lambda calculus suffices on its own. No built-in numbers, boolean, sets, lists, ... . Or
maybe you need built-in conditionals or loops or recursion? No. Implication, equivalence,
comparison etc? No.

In my opinion, that is a bigger problem than if it needed those as primitives, because it then raises the
question: why do we think of them as primitives if they are not?

This is similar to Wittgenstein's criticism against Set Theory, namely, if the axioms of Set Theory tell us
that 2 + 2 = 5, then we would conclude that Set Theory is wrong, because it is "obvious" that 2 + 2 != 5.
So why do we need Set Theory to "reassure" us that "mathematics is sound"?
2

daymi • 12y ago

Yeah, I know what you mean. But the axioms are an arbitrary choice so long as they are not
contradictory. So with fewer primitives the axioms here are as few as possible and still contain the
ones we need to do mathematics. In general axioms' truth has to be assumed (and defended from
other axioms). Each axiom that you need is a problem. More axioms are more problems.

Lambda calculus can do substitutions - because the goal was to abstract over these (and those are
intuitive operations as well) and tell things about them without doing them. If there were additionally
primitive numbers you'd have to have a case analysis for the case when a number comes in and a
function comes out at this place. What if a function comes in and a number comes out at the same
place etcetc.
That said, because of thoughts like what if the numbers are more important and a big meta-level
problem that has plagued us ever since (in order to be able to talk about the Gödel number of the
expression, you already have to have numbers. So you implement them using lambda expressions.
These have Gödel numbers which you'd like to check. So you need numbers ........), lambda calculus
is extended much in practise to add primitives and something in order to be able to distinguish
numbers and functions. All practical programming languages do extend lambda calculus in some
such way.
In a sense, I think it's like with linear algebra - without some concrete assumed basis, the basis
substitution in a vector is never going to end. However, the assumed basis is in a large way arbitrary.
So why not assume natural numbers, indeed.

But I think the most horrible result in all of mathematics throws a wrench into the works either way:
any formal system powerful enough to prove statements about the natural numbers is incomplete. So
not only is lambda calculus with natural numbers incomplete, lambda calculus as such is incomplete.
It's minimal and already broken.