# Tag Info

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

41

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 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 ... 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-Lö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 ... 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 ... 21 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 ... 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 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

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

18

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

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

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

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 $... 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 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 : C ... 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 I'm assuming you mean Krivine's notation from Lambda Calculus: Types and Models. This notation, used as a data representation, makes many algorithms on lambda-terms simpler to implement and prove correct. That is, given a lambda term$f\; e_1\; e_2\; \ldots\; e_n$, you want to view it as a head$f$, together with a list of arguments$[e_1, e_2, \ldots, ...

13

Here's a slightly different perspective on Fredrik's answer. It's generally the case that impredicative Church encodings of types will satisfy the relevant $\beta$ laws, but will not satisfy the $\eta$ laws. So this means we can define a dependent pair as follows:  \exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \...

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

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