Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
85 votes
Accepted

What does the "Lambda" in "Lambda calculus" stand for?

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 ...
Anton Trunov's user avatar
  • 3,479
65 votes
Accepted

Is Lambda Calculus purely syntactic?

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 ...
Derek Elkins left SE's user avatar
53 votes
Accepted

How does the Y combinator exemplify "Lambda calculus inconsistency"?

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 ...
Gilles 'SO- stop being evil''s user avatar
31 votes
Accepted

What are some interesting/important Programming Language Concepts I could teach myself in the coming semester?

Very good explanations of programming paradigms and the programming concepts from which those paradigms are built are found in Peter van Roy's works. Especially in the book Concepts, Techniques, and ...
Jörg W Mittag's user avatar
29 votes
Accepted

if (λ x . x x) has a type, then is the type system inconsistent?

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 ...
cody's user avatar
  • 8,233
25 votes
Accepted

Lambda calculus didn't seem abstract. And I can't see the point of it

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 ...
Hans Hüttel's user avatar
  • 2,516
24 votes
Accepted

Lambda Calculus Generator

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)...
chi's user avatar
  • 14.6k
18 votes
Accepted

Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?

Consider the terms of the $S,K_2,I$ calculus as trees (with binary nodes representing applications, and $S, K_2$ leaves representing the combinators. For example, the term $S(SS)K_2$ would be ...
Z. A. K.'s user avatar
  • 355
17 votes
Accepted

Strictness in both arguments but not in each individually

That's a very good question! It turns out the answer is both yes and no. A classic example of a function we'd like to write is Plotkin's parallel or. We know from basic boolean logic that both ...
Gilles 'SO- stop being evil''s user avatar
14 votes
Accepted

What is the difference between strong normalization and weak normalization in the context of rewrite systems?

Weak normalization means that any term has a terminating rewriting sequence, i.e. admits a finite amount of rewritings which lead to a normal form (no more rewritings from that). Strong normalization ...
chi's user avatar
  • 14.6k
13 votes

Solving functional equations for unknown functions in lambda calculus

This is a known problem, known as Higher Order Unification. Unfortunately, this problem is undecidable in general. There is a decidable fragment, known as Miller's Pattern Fragment. It's used ...
Joey Eremondi's user avatar
13 votes

Lambda Calculus Generator

As has been mentioned, this is just enumerating terms from a context free language, so definitely doable. But there's more interesting math behind it, going into the field of analytical combinatorics....
phipsgabler's user avatar
12 votes
Accepted

λ -calculus : What is the most efficient in memory representation of functions?

The thing is, there's really not much leeway in terms of function encoding. Here are the main options: Term rewriting: you store functions as their abstract syntax trees (or some encoding thereof. ...
Joey Eremondi's user avatar
12 votes

Lambda Calculus Generator

Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) ...
D.W.'s user avatar
  • 160k
11 votes

What is the purpose of the SKI combinator calculus(or even lambda calculus)? What are some real life examples of its use?

The obvious application of the lambda calculus is any functional programming language (e.g., Lisp, ML, Haskell), and any language that supports anonymous functions. As for combinator calculus, does ...
David Richerby's user avatar
11 votes
Accepted

What is a super universe?

One intention behind having a universe operator and a super-universe closed under it, is to give a type-theoretic version of large cardinal axioms known from set theory. An inaccessible cardinal is ...
Andrej Bauer's user avatar
  • 30.5k
11 votes
Accepted

$\lambda$-calculus, is there encoding of for or while?

Sure! Let me show how to encode FOR using an example. Suppose we want to translate a simple factorial FOR program x := 1 for i := 1 to N do x := x * i We ...
chi's user avatar
  • 14.6k
10 votes

What does the "Lambda" in "Lambda calculus" stand for?

here is some other near-firsthand info/ angle on this by Church student Dana Scott as just reported by Ghica and documented in a youtube video.[1] He says that when Church was asked what the ...
vzn's user avatar
  • 11k
10 votes
Accepted

What's the difference between a calculus and a programming language?

The meaning of the words is not fixed, but I can give you my interpretation. A calculus is something that we calculate with in the sense of juggling equations (think manipulation of Taylor series or ...
Andrej Bauer's user avatar
  • 30.5k
10 votes
Accepted

Are there lambda-calculus functions which always output booleans, but are not constant functions?

That is not possible. By the "genericity lemma" (Barendregt book, lemma 14.3.24), if $C[M] = N$ with $M$ unsolvable, and $N$ normal form, then $C[L] = N$ for any term $L$. So, if $x$ is an unsolvable ...
chi's user avatar
  • 14.6k
10 votes
Accepted

How do we know $\neg \neg LEM$ isn't provable in MLTT?

The task here is indeed to find a model of MLTT in which $\neg LEM$ holds (and so $\neg\neg\neg LEM$ holds as well). Realizability models have this feature, for instance; see also this. Here, MLTT ...
András Kovács's user avatar
10 votes
Accepted

Lambda Calculus as a branch of set theory

It's false. The $\lambda$-calculus arose through efforts to understand foundations of mathematics. Nowadays some people mistakenly equate foundations with set theory. The Stanford Encyclopaedia of ...
Andrej Bauer's user avatar
  • 30.5k
10 votes

What are some interesting/important Programming Language Concepts I could teach myself in the coming semester?

Check out the book Types and Programming Languages (TAPL) by Benjamin Pierce. This is an excellent introduction to the fundamental concepts of the field of programming languages.
Caleb Stanford's user avatar
9 votes
Accepted

Is there a correspondence between the syntaxes and the type systems of programming languages?

You seem to have a misunderstanding of the purpose of abstract binding trees (ABTs). They are a tool for describing syntax, much like abstract syntax trees (ASTs). They simply allow you to describe ...
Derek Elkins left SE's user avatar
9 votes
Accepted

Lambda Calculus in Rewriting systems

See also this question: "How is Lambda Calculus a specific type of Term Writing system?". Term rewriting, as introduced in (1), and described in e.g. (2), is a first-order system that cannot handle ...
Martin Berger's user avatar
9 votes
Accepted

Algorithm for deciding alpha-equivalence of terms in languages with bindings

There are several ways to do what you want. One of them is to use a different syntax representation under which $\alpha$-equivalent terms are actually equal. Such representations go under the name ...
Andrej Bauer's user avatar
  • 30.5k
9 votes
Accepted

Abstractions in call-by-push-value

thanks for your interest in call-by-push-value. The fact that functions (all functions, not just lambda-abstractions) are computations is the main difference between call-by-push-value and call-by-...
Paul Blain Levy's user avatar
9 votes

$\lambda$-calculus, is there encoding of for or while?

There are encodings of loops, but they don't work exactly like the loops that you're used to, because the lambda calculus is not an imperative language. The lambda calculus has no side effects (it's a ...
Gilles 'SO- stop being evil''s user avatar
8 votes
Accepted

Is Applicative-order and Normal-order evaluation model's definition contradictory as per sicp text book?

Those definitions are saying the same thing (at the level of precision of the English description). An example from the book Normal-order evaluation goes “fully expand and then reduce”, meaning that ...
Gilles 'SO- stop being evil''s user avatar
8 votes
Accepted

Why is Church-Rosser so important for basing programming languages on lamdba-calculus?

Think of it as a sanity check. CR cones from the days when we were just figuring out what programming languages were. The Lambda calculus was new, and its basic properties were unknown. CR says that ...
Joey Eremondi's user avatar

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