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 ...
- 3,469
64
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 ...
52
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 ...
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 ...
- 5,860
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 ...
- 8,114
24
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 ...
- 2,486
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)...
- 14.4k
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 ...
- 355
16
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 ...
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 ...
- 14.4k
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 ...
- 29.7k
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....
- 370
12
votes
Accepted
Universal/existential quantification?
It helps to remember that $\forall$ (or $\Pi$ as you sometimes see) is a type. It's generalizing $\to$. So while it makes perfect sense to say $(\lambda x : A. M)\ N$, it doesn't make sense to say $(\...
- 1,480
12
votes
Is there an algorithm for converting Turing machines into equivalent Lambda expressions?
All proofs of the equivalence of these two models of computation are constructive, that is they describe an algorithm for converting a program from one model of computation to the other. However, I ...
- 275k
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. ...
- 29.7k
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.♦
- 156k
11
votes
Accepted
Can a functional language be homoiconic?
The definition implies not only that programs are represented by a "primitive" datatype, but presumably also that it is possible to inspect the elements of this type, i.e., one can actually get at the ...
- 30k
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 ...
- 81.4k
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 ...
- 30k
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 ...
- 14.4k
10
votes
Accepted
Is there an algorithm for converting Turing machines into equivalent Lambda expressions?
Sure there is. I'm going to assume you can figure out how to convert Haskell into the lambda calculus; for a reference, look at the GHC implementation.
Now just to be clear: a Turing Machine is a (...
- 394
10
votes
Is there an algorithm for converting Turing machines into equivalent Lambda expressions?
Since you did not like Yuval's answer, you deserve this one:
The equivalence of Church's $\lambda$-calculus and Turing machines is proved in the Appendix of Alan Turing's 1937 paper On computable ...
- 30k
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 ...
- 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 ...
- 30k
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 ...
- 14.4k
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 ...
- 908
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 ...
- 30k
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.
- 6,968
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 ...
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 ...
- 8,308
Only top scored, non community-wiki answers of a minimum length are eligible