Skip to main content
19 votes

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 ...
Martin Berger's user avatar
12 votes

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 ...
Noam Zeilberger's user avatar
9 votes
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]{\...
Andrew Polonsky's user avatar
7 votes

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 ...
John Tromp's user avatar
5 votes
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....
Andrej Bauer's user avatar
  • 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 ...
NinjaDarth's user avatar
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(...
John Tromp's user avatar

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