# Tag Info

### What is the "question" that programming language theory is trying to answer?

The overall purpose of PLT is to make industrial software engineering (in a general sense) cheaper (also in a general sense), through optimising the most important tool (programming languages) and ...
• 11.5k

### Incomplete basis of combinators

[Expanding the comment into an answer.] First, just a clarification about counting bound variables in a combinator (= closed term) $t$. I interpret the question as asking about  \text{the total ...
• 4,561
Accepted

### How can non-terminating $\lambda$-terms be turned into fixed-point combinators?

There are several aspects to this very nice question, so I will structure this answer accordingly. $\newcommand{\setof}[1]{\{#1\}}$ $\newcommand{\thra}{\twoheadrightarrow}$ \$\newcommand{\codeof}[1]{\...

### Smallest possible universal combinator

The smallest basis is the single point combinator A = λx λy λz. x z (y (λ_.z)) of size 4 abstractions + 3 applications, and of minimal size 26 bits in the binary lambda calculus. Minimal ...
• 271
Accepted

### Algorithm for extensional equality in combinator calculus

Equality of terms in the combinator calculus is undecidable. We can encode the natural numbers as Church numerals and then show that every recursive function is represented, see for instance section 1....
• 29.2k
1 vote

### Algorithm for extensional equality in combinator calculus

If either of two combinator terms has a strong normal form, and are η-equivalent when treated as λ-terms, then they will both have a strong normal form, it will be the same one, and it may be found by ...
• 121
1 vote
Accepted

### Concatenative binary lambda calculus/combinatory logic

Yes, there exists a version of BLC working similarly to Zot. Consider the zot implementation at [1], which mimics the original definition at [2]. It defines 3 lambda expressions: zot = \c.c I 0 = \c.c(...
• 271

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