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 ...
- 12.1k
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 ...
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 ...
- 6,298
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,317
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 ...
- 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)...
- 14.7k
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
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 ...
16
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.7k
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 ...
- 30.1k
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
λ -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. ...
- 30.1k
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.♦
- 166k
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 ...
- 31.2k
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.7k
10
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 ...
- 31.2k
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 ...
- 31.2k
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.7k
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 ...
- 31.2k
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.
- 7,248
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 ...
- 12.1k
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,358
9
votes
How does the Y combinator exemplify "Lambda calculus inconsistency"?
I'd like to add one to what @Giles said.
The Curry-Howard correspondence makes a parallel between $\lambda$-terms (more specifically, the types of $\lambda$-terms) and proof systems.
For example, $\...
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-...
- 106
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 ...
9
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 ...
- 948
8
votes
Accepted
why nominal unification is a first-order unification?
Most experience people have with unification (if any) is usually unification modulo syntactic equality: two terms unify if there is a substitution for unification variables that makes the terms ...
- 12.1k
8
votes
Accepted
Recursive type encoding on System F (and other pure type systems)
There is a convention in category theory that the same symbol is used for a type constructor and the map function over that type constructor. Hence, if f : X -> Y then F f : F X -> F Y.
8
votes
Accepted
Why are combinators important in lambda calculus?
The word "combinator" has some connotations that you don't seem to be intending here and sometimes a stricter definition. Another term for the definition you gave is a closed term. The opposite is ...
- 12.1k
8
votes
Accepted
Intuitive explanation of neutral / normal form in lambda calculus
I can reassure you that this property is not immediately self-evident. In trying to describe/enumerate the set of normal forms, the main observation required is the following:
Abstraction preserves ...
- 8,317
Only top scored, non community-wiki answers of a minimum length are eligible