96

$\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) ...


39

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 ...


34

One is internal and the other is external. A category $\mathcal{C}$ consists of objects and morphisms. When we write $f : A \to B$ we mean that $f$ is a morphism from object $A$ to object $B$. We may collect all morphisms from $A$ to $B$ into a set of morphisms $\mathrm{Hom}_{\mathcal{C}}(A,B)$, called the "hom-set". This set is not an object of $\mathcal{C}...


28

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 ...


27

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 ...


21

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 ...


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 ...


21

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'...


20

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 ...


20

Update [2011-09-20]: I expanded the paragraph about $\eta$-expansion and extensionality. Thanks to Anton Salikhmetov for pointing out a good reference. $\eta$-conversion $(\lambda x . f x) = f$ is a special case of $\beta$- conversion only in the special case when $f$ is itself an abstraction, e.g., if $f = \lambda y . y y$ then $$(\lambda x . f x) = (\...


20

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 ...


20

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 $...


19

No, it's not possible. Consider the following two inhabitants of the type $(A \to B) \to (A \to B)$. $$ \begin{array}{l} M = \lambda f.\;f \\ N = \lambda f.\;\lambda a.\; f\;a \end{array} $$ These are distinct $\beta$-normal forms, but cannot be distinguished by a lambda-term, since $N$ is an $\eta$-expansion of $M$, and $\eta$-expansion preserves ...


19

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

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

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, ...


17

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 ...


16

First, note that the result states that the only beta redex where the right-hand side is equal (modulo alpha-conversion) to the left-hand side is $(\lambda x. x x) (\lambda x. x x)$. There are other terms that reduce to themselves, having this redex in a context. I can see how most of Lercher's proof work, though there are points where I can't get past ...


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

A nice example is given by Godelization: in lambda calculus, the only thing you can do with a function is to apply it. As a result, there is no way to write a closed function of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$, which takes a function argument and returns a Godel code for it. Adding this as an axiom to Heyting arithmetic is usually called "...


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 ...


14

A calculus is a system of computation based on the manipulation of symbolic expressions. An algebra is a system of symbolic expressions and relations between them[*]. That is, a calculus is a system for figuring out answers, and an algebra is a way of expressing the relations between terms. The $\lambda$-calculus is either a calculus or an algebra, ...


14

I presume that by extensionality you mean the law $$(\forall x . f x = g x) \implies f = g.$$ If this is what you mean then the graph model $\mathcal{P}\omega$ is not extensional, while Dana Scott's $D_\infty$ is (I presume $D^\infty$ is Dana Scott's model of the $\beta\xi\eta\lambda$-calculus). To see this, recall that $\mathcal{P}\omega$ is an algebraic ...


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 : ...


14

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 $...


14

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 ...


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

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 ...


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