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 ...
- 10.7k
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 ...
- 4,411
8
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]{\...
- 601
6
votes
Is combinatory strong reduction equivalent to lambda beta-eta reduction?
The answer to the second question is yes, beta-reduction is harder to imitate than beta-eta-reduction. There is an article by J P Seldin in "Theoretical Computer Science" (2011) I think that ...
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....
- 28.1k
Only top scored, non community-wiki answers of a minimum length are eligible