82

An excerpt from History of Lambda-calculus and Combinatory Logic by F. Cardone and J.R. Hindley(2006): By the way, why did Church choose the notation “$\lambda$”? In [Church, 1964, §2] he stated clearly that it came from the notation “$\hat{x}$” used for class-abstraction by Whitehead and Russell, by first modifying “$\hat{x}$” to “$\wedge x$” to ...


63

Ironically, the title is on point but not in the way you seem to mean it which is "is the lambda calculus just a notational convention" which is not accurate. Lambda terms are not functions1. They are pieces of syntax, i.e. collections of symbols on a page. We have rules for manipulating these collections of symbols, most significantly beta reduction. You ...


51

It's inspired from real events, but the way it's stated is barely recognizable and “should be regarded with suspicion” is nonsense. Consistency has a precise meaning in logic: a consistent theory is one where not all statements can be proved. In classical logic, this is equivalent to the absence of a contradiction, i.e. a theory is inconsistent if and only ...


36

Yes, sure. Many typed lambda calculi accept only strongly normalizing terms, by design, so they cannot express arbitrary computations. But a type system can be anything you like; make it broad enough, and you can express all deterministic computations. A trivial type system that encompasses a Turing-complete fragment of the lambda calculus is the one that ...


29

I haven't read this anywhere, but this is how I believe $Y$ could have been derived: Let's have a recursive function $f$, perhaps a factorial or anything else like that. Informally, we define $f$ as pseudo-lambda term where $f$ occurs in its own definition: $$f = \ldots f \ldots f \ldots $$ First, we realize that the recursive call can be factored out as ...


29

Certainly, assigning a type to $\lambda x. x\ x$ is not enough for inconsistency: in system $F$, we can derive $$ \lambda x.x\ x:(\forall X.X)\rightarrow (\forall X.X)$$ in a pretty straightforward way (this is a good exercise!). However, $(\lambda x.x\ x)(\lambda x.x\ x)$ cannot be well typed in this system, assuming $\omega$-consistency of 2nd order ...


24

There are many reasons why the lambda calculus is so important. A very important reason is the lambda calculus allows us to have a model of computation in which computable functions are first-class citizens. One cannot express higher-order functions in the language of middle school algebra. Take as example the lambda expression $$\lambda f. \lambda g. \...


23

The main theorem regarding this issue is due to a British mathematician from the end of the 16th century, called William Shakespeare. His best known paper on the subject is entitled "Romeo and Juliet" was published in 1597, though the research work was conducted a few years earlier, inspired but such precursors as Arthur Brooke and William Painter. His main ...


21

Turing-complete is just a name. You can call it Abdul-complete if you want. Names are decided upon historically and are often named after the "wrong" people. It's a sociological process that has no clear criteria. The name has no meaning beyond its official semantics. Imperative languages are not based on Turing machines. They are based on RAM machines. ...


20

$\to_\beta$ is the one-step relation between terms in the $\lambda$-calculus. This relation is neither reflexive, symmetric, or transitive. The equivalence relation $\equiv_\beta$ is the reflexive, symmetric, transitive closure of $\to_\beta$. This means If $M\to_\beta M'$ then $M\equiv_\beta M'$. For all terms $M$, $M\equiv_\beta M$ holds. If $M\...


19

In a nutshell: What characterizes imperative programming languages as close to Turing machines and to usual computers such as PCs, (themselves closer to random access machines (RAM) rather than to Turing machine) is the concept of an explicit memory that can be modified to store (intermediate results). It is an automata view of computation, with a concept ...


19

Sure, this is a standard encoding exercise. First of all, let $p : \mathbb N^2 \to \mathbb N$ any bijective computable function, called a pairing function. A standard choice is $$ p(n,m) = \dfrac{(n+m)(n+m+1)}{2}+n $$ One can prove that this is a bijection, so given any natural $k$, we can compute $n,m$ such that $p(n,m)=k$. To enumerate lambda terms, ...


18

First encode natural numbers and pairs, as described by jmad. Represent an integer $k$ as a pair of natural numbers $(a,b)$ such that $k = a - b$. Then you can define the usual operations on integers as (using Haskell notation for $\lambda$-calculus): neg = \k -> (snd k, fst k) add = \k m -> (fst k + fst m, snd k + snd m) sub = \k m -> add k (neg ...


18

The expressive completeness of the typed combinators compared to the simply typed lambda calculus has been demonstrated. For each untyped combinator, one needs a whole family of typed combinators. For example, one has $\mathbf{I}_{\alpha\to\alpha}$ $\mathbf{K}_{\alpha\to(\beta\to\alpha)}$ $\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\...


17

The first is an abbreviation for the second. It's a common syntactic convention to shorten expressions. On the other hand, if you have tuples in the language, then there is a difference between $\lambda x.\lambda y.xy$ and $\lambda (x,y).xy$. In the former case I can provide a single argument to the function, and pass the resulting function around to ...


17

here is a half-baked answer: I know that Ugo Dal Lago at University of Bologna has been studying quantum lambda calculus. You may want to check his publications and perhaps this one in particular: Quantum implicit computational complexity by U. Dal Lago, A. Masini, M. Zorzi. I am saying it's a half-baked answer, because I haven't had chance to read any of ...


17

You are asking for an application outside of computer science and logic. That is easily found, for example in algebraic topology it is convenient to have a cartesian closed category of spaces, see convenient category of topological spaces on nLab. The formal language corresponding to cartesian closed categories is precisely the $\lambda$-calculus. Let me ...


16

I just want to explain why intersection types are well-suited to characterize classes of normalization (strong, head or weak), whereas other type systems can not. (simply-typed or system F). The key difference is that you have to say: "if I can type $M_2$ and $M_1→M_2$ then I can type $M_1$". This is often not true in non-intersection types because a term ...


16

In the lambda calculus with no constants with the Hindley-Milner type system, you cannot get any such types where the result of a function is an unresolved type variable. All type variables have to have an “origin” somewhere. For example, the there is no term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$, but there is a term of type $\...


15

These are just differences of notations. $λxyz.t$ is short for $λx.λy.λz.t$. No magic here. Indeed, $\mbox{pair}=λxyp.pxy$ but you tend to emphasize that $\mbox{pair}\,t\,u$ is a function $λp.ptu$ by changing the way you write the definition. But it is really the same.


15

Lambda terms are simplified by the β-reduction rule: $$(\lambda x.M)N\,\rightarrow_\beta\,M[x:=N]$$ It means, if you have a subterm that looks like $(\lambda x.M)N$ (called redex) you can replace it by $M[x:=N]$, which is $M$ with $N$ substituted for $x$. The replacement $M[x:=N]$ is often called contractum. (Capital letters likes $M$ and $N$ are used to ...


15

Jean Louis Krivine introduced an abstract calculus which extends the "Krivine Machine" in a very non-trivial way (note that the Krivine machine already supports the call/cc instruction from lisp): He introduces a "quote" operator in this article defined in the following manner: if $\phi$ is a $\lambda$-term, note $n_\phi$ the image of $\phi$ by some ...


15

The term you are reducing is $(K_y \Omega)$ where $K_y$ is the constant function $\lambda x. y$ (it always returns $y$, ignoring its argument) and $\Omega = (\lambda x. (x \, x) \: \lambda x. (x \, x))$ is a non-terminating term. In some sense $\Omega$ is the ultimate non-terminating term: it beta-reduces to itself, i.e. $\Omega \to \Omega$. (Make sure to ...


15

There are four main approaches, though these only scratch the surface of what is available: via lambdas and records: the idea is to encode objects, classes and methods in terms of more traditional constructs. Benjamin Pierce's work from the mid 90s is representative of this approach. Abadi and Cardelli's object calculi (see Abadi and Cardelli's book A ...


15

In traditional Martin-Löf type theory there is no distinction between types and propositions. This goes under the slogan "propositions as types". But there are sometimes reasons for distinguishing them. CoC does precisely that. There are many variants of CoC, but most would have $$\mathsf{Prop} : \mathsf{Type}$$ but not $\mathsf{Type} : \mathsf{Prop}$. ...


14

The lambda calculus is fundamental in logic, category theory, type theory, formal verification, ... Basically, anything to do with programming language semantics and formal logic. It is such a fundamental formalism that people working in these fields do not even question the benefit of it. I think that it is extremely useful for understanding functional ...


14

Context are used for many purposes, but typically to define congruences on programs. Evaluation contexts are a subset of contexts. They are typically used to define reduction relations. Let me give an example of each. One formal way of defining program equality is to say two programs $M$ and $N$ are contextually equal they can replace each other in each ...


14

A context is a syntactic notion. A context is a term with one hole in it. (Occasionally there are multi-hole contexts, the definition will be given clearly in that case.) The syntax of contexts is defined by taking the syntax of terms and allowing one subterm to be a hole $[]$ instead of a term. In BNF (I use the lambda-calculus as an example, without ...


13

Lambda-calculus can encode most data structures and basic types. For example, you can encode a pair of existing terms in the lambda calculus, using the same Church encoding that you usually see to encode nonnegative integers and boolean: $$\mbox{pair}= λxyz.zxy$$ $$\mbox{fst} = λp.p(λxy.x)$$ $$\mbox{snd} = λp.p(λxy.y)$$ Then the pair $(a,b)$ is $p=(\mbox{...


13

In this answer, I'll stick to a core ML fragment of the language, with just lambda-calculus and polymorphic let following Hindley-Milner. The full OCaml language has additional features such as row polymorphism (which if I recall correctly doesn't change the theoretical complexity, but with which real programs tend to have larger types) and a module system (...


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