The 2024 Developer Survey results are live! See the results

# Tag Info

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
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 ...
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,270
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,252
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
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.6k
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
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 ...
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.6k

### 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.9k

### 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
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.9k

### 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.) ...
• 163k
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 ...
• 30.9k
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.6k
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 ...
• 30.9k
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.6k
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 ...
• 30.9k

### 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,128
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
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
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 ...
• 30.9k
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-...

### $\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 ...
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 ...
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 ...
• 29.9k
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
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.
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