17 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

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
5 votes

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
  • 28.3k

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