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 ...
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 ...
10
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 ...
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 ...
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]{\...
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 ...
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, ...
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 ...
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,...
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....
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 ...
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 ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
combinatory-logic × 21lambda-calculus × 14
lo.logic × 3
pl.programming-languages × 3
big-picture × 3
soft-question × 2
functional-programming × 2
universal-computation × 2
cc.complexity-theory × 1
ds.algorithms × 1
reference-request × 1
graph-theory × 1
computability × 1
type-theory × 1
machine-learning × 1
pr.probability × 1
boolean-functions × 1
permutations × 1
typed-lambda-calculus × 1
calculus-of-constructions × 1
boolean-formulas × 1
constructive-mathematics × 1
intuition × 1
ppad × 1
extensionality × 1