100

$\lambda$-calculus has two key roles. It is a simple mathematical foundation of sequential, functional, higher-order computational behaviour. It is a representation of proofs in constructive logic. This is also known as the Curry-Howard correspondence. Jointly, the dual view of $\lambda$-calculus as proof and as (sequential, functional, higher-order) ...


45

Turing-machines and $\lambda$-calculus are equivalent only w.r.t. the functions $\mathbb{N} \rightarrow \mathbb{N}$ they can define. From the point of view of computational complexity they seem to behave differently. The main reason people use Turing machines and not $\lambda$-calculus to reason about complexity is that using $\lambda$-calculus naively ...


33

First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as starting at Martin-Löf type theory with universes, and then adding a sort Prop at the bottom of the type hierarchy. This is a very different beast than the ...


29

I think $\lambda$-calculus has contributed in many ways to this field, and still contributes to it. Three examples follow, and this is not exhaustive. Since I am not a specialist in $\lambda$-calculus, I certainly miss some important points. First, I think having different models of computation that turn out to represent the exact same set of functions was ...


26

He wanted to create a formal system for the foundations of logic and mathematics that was simpler than Russell's type theory and Zermelo's set theory. The basic idea was to add a constant $\Xi$ to the untyped lambda calculus (or combinatory logic) and interpret $XZ$ as expressing "$Z$ satisfies the predicate $X$" and $\Xi XY$ as expressing "$X\subseteq Y$". ...


22

I can think of a few possible answers coming from linear logic. The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once. This condition is preserved by reduction and it is immediate to see that the size of affine terms strictly decreases with each reduction step. Therefore, the untyped affine ...


22

Apart from the foundational role of the $\lambda$-calculus, which was mentioned in all other answers, I would like to add something on What exactly did the lambda calculus do to advance the theory of CS? I believe that concurrency theory is one field of CS which has been tremendously influenced by the compositional view mentioned by Martin Berger. Of ...


22

You're in good company. Kurt Gödel criticized $\lambda$-calculus (as well as his own theory of general recursive functions) as not being a satisfactory notion of computability on the grounds that it is not intuitive, or that it does not sufficiently explain what is going on. In contrast, he found Turing's analysis of computability and the ensuing notion of ...


22

The question you are asking is interesting and known. You are using the so-called impredicative encoding of the natural numbers. Let me explain a bit of the background. Given a type constructor $T : \mathsf{Type} \to \mathsf{Type}$, we might be interested in the "minimal" type $A$ satisfying $A \cong T(A)$. In terms of category theory $T$ is a functor and $...


22

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. The Coq interactive theorem prover is based on an underlying type theory, sometimes lovingly called the calculus of inductive constructions with universes. You'...


21

A recent developpement on this topic: U. dal Lago and B. Accatoli proved that the length of the leftmost-outermost reduction (LOr) of a $\lambda$-term is an invariant (time) cost model for $\lambda$-calculus. They show that Turing machines (with cost=time) and $\lambda$-terms (with cost=length of the LOr) can simulate each other with a polynomial overhead ...


21

Alright I'll give a crack at it: In general for a given type system $T$, the following is true: If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a logic. The proof generally proceeds by assuming you have a term $\mathrm{absurd}$ of type $\mathrm{False}$, using subject reduction to get a normal form, and ...


20

I will give a partial answer, I hope others will fill in the blanks. In typed $\lambda$-calculi, one may give a type to usual representations of data ($\mathsf{Nat}$ for Church (unary) integers, $\mathsf{Str}$ for binary strings, $\mathsf{Bool}$ for Booleans) and wonder what is the complexity of the functions/problems representable/decidable by typed terms. ...


19

A calculus is just a system of reasoning. One particular calculus (well, actually two closely related calculi: the differential calculus and the integral calculus) has become so widespread that it is just known as "calculus", as if it were the only one. But, as you have observed, there are other calculi, such as the lambda calculus, mu calculus, pi calculus, ...


19

First, your friend is wrong about the history of the $\lambda$-calculus. Church created the untyped calculus first, which he intended as a foundation for mathematics. Fairly quickly, it was discovered that the logic derived from this calculus was inconsistent (because non-terminating programs existed). Eventually Church developed the simple theory of types ...


19

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive mathematician. To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc: We provide a function $f$ which ...


17

The answer is it depends what you mean by Term Rewrite System. When it was introduced, the concept of Term Rewrite Systems, or TRSes, described what is now called first order TRSes, which is simply a set of computation rules of the form $$ l\rightarrow r $$ where $l$ and $r$ are first order terms of the form $$ t :=\ x\ \mid\ f(t_1,\ldots,t_n) $$ where $...


16

You may wish to look at cost semantics for functional languages. These are various computational complexity measures for functional languages that do not pass through any kind of Turing machine, RAM machine, etc. A good place to start looking is this Lambda the Ultimate post, which has some good further references. Section 7.4 of Bob Harper's Practical ...


15

One apparent strength of his approach is that it allows higher-order functions (i.e. lambda terms) to be observable outcomes, which measure theory generally makes quite tricky. (The basic problem is that spaces of measurable functions generally have no Borel $\sigma$-algebra for which the application function - sometimes called "eval" - is measurable; see ...


15

To me, your question seems analogous to saying "I've heard that non-Euclidean geometry requires me to give up Euclid's fifth axiom, which is very useful in many mathematical contexts." You don't have to give up the axiom in the sense of "personally agree, at a basic philosophical level, that it doesn't hold", you just have to think of it in terms like: "As a ...


15

As you point out, the λ-calculus has a seemingly simple notion of time-complexity: just count the number of β-reduction steps. Unfortunately, things are not simple. We should ask: Is counting β-reduction steps a good complexity measure? To answer this question, we should clarify what we mean by complexity measure in the first place. One good answer is ...


14

The author is not misinformed, I'm afraid; it's part of the development process of any computer scientist to go through several phases: Phase 1: $\alpha$-equivalence is easy! Why is everyone making a big deal about this? Phase 2: $\alpha$-equivalence is impossible! Why should I do computer science if such a basic notion is so impossibly complex? Phase 3: I'...


14

Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it. Alpha-renaming the example makes it easier to follow: ((\x.x) (\y.y)) 10 For maximum clarity, let's start by assigning type variables to each sub expression: x : A (\x.x) : B y : C ...


14

You seem to be confusing several things here. First of all, like Alexis said in her answer, I don't see why you would need to accept/reject the principles of a given logical theory in order to study it and learn about it. The fact that your theory is intuitionistic doesn't mean that your meta-theory has to be! You may freely use proof by contradiction or ...


14

At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising. I recently wrote a paper in which I look at how to prove the Cook-Levin theorem ($\mathsf{NP}$-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. A summary: the key notion is that of affine ...


14

The overall purpose of PLT is to make industrial software engineering (in a general sense) cheaper (also in a general sense), through optimising the most important tool (programming languages) and associated tooling ecosystem. Some reasons why maths is involved: PLs are highly non-trivial, and it's not clear that they do the right thing without proof. ...


13

Your questions can be approached from many sides. I'd like to leave the historical and philosophical aspects on the side and address your main question, which I take to be this: What's the point of lambda calculus? Why go through all these functions/reductions? What is the point of Boolean Algebra, or Relational Algebra, or First-Order Logic, or Type ...


13

I paste part of an answer I wrote for another question: Implicit Computational Complexity aims at characterizing complexity classes by means of dedicated languages. The first results such as Bellantoni-Cook's Theorem were stated in terms of $\mu$-recursive functions, but more recent results use the vocabulary and techniques of $\lambda$-calculus. See this ...


13

First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent. The second means that the type $\bot$ is not inhabited. CR implies the first kind of consistency, not the second. This, as has been pointed out in the ...


12

The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for. If you use the strict lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser'...


Only top voted, non community-wiki answers of a minimum length are eligible