16 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 ...
user avatar
11 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 ...
user avatar
9 votes
Accepted

Upper bound on Chaitin's constant for lambda calculus and SKI combinatory logic

You probably want to look at David et al's paper, Asymptotically Almost All λ-terms are Strongly Normalizing: We present a quantitative analysis of various (syntactic and behavioral) properties of ...
user avatar
9 votes

Smallest possible universal combinator

It should be noted that finding combinators with certain reduction properties is always difficult, and finding the smallest such combinator may easily be undecidable (for trivial reasons, as it may be ...
user avatar
  • 13.1k
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]{\...
user avatar
7 votes

Smallest possible universal combinator

For your first question I believe this paper may help a bunch. It has a 6 bit combinator calculus that is also an UTM. Also it has a universal combinator that seems to have size 7 with one element ...
user avatar
6 votes

Church-Rosser equivalent for concatenative languages?

SK combinators are Church-Rosser. However, the usual $\lambda$-calculus method of proving local confluence and then appealing to Newman's lemma doesn't work. You need a slightly fancier argument, ...
user avatar
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 ...
user avatar
6 votes
Accepted

What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?

I don't understand exactly what you are looking for, I'll try to explain the Curry-Howard correspondence in a nutshell, you'll let me know if it helps. The Curry-Howard correspondence (or isomorphism,...
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....
user avatar
  • 26.4k
4 votes

What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?

Simple summary: Typed $\lambda$-calculi are a way of presenting intuitionistic logics. Combinatory logic is a presentation of logic (propositional, first-order, higher-order, intuitionistic or ...
user avatar
3 votes

What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?

Let me offer the simple, intuitive way that I think about this. If you restrict yourself to closed lambda expressions, you have an equivalent of the combinatory logic. In fact with just a few simple ...
user avatar
  • 2,864

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