# Tag Info

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 ...
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 ...
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 ...
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 ...
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 ...
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)...
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 ...
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 ...

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

### 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....
Accepted

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