14
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 associated tooling
ecosystem.
Some reasons why maths is involved:
PLs are highly non-trivial, and it's not clear that they
do the right thing without proof. ...
9
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 random λ-terms. Our main results show that asymptotically, almost all terms are strongly normalizing and that any fixed closed term almost never appears in a ...
9
[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 number of distinct bound variable names in }t
$$
so that for example the term $t = (\lambda x.x(\lambda y.y))(\lambda x.\lambda y.yx)$ counts as having two bound ...
9
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 undecidable to prove that a certain application of the combinator even halts).
There are several simple open questions of a similar flavor, e.g. problems #4, #...
8
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]{\lceil #1 \rceil}$
1.
The answer to the boxed question is no. The term $\Omega_3 = (\lambda x.xxx)(\lambda x.xxx)$ suggested by your friend is indeed a ...
7
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 given what you want. They call it Zot.
http://arxiv.org/pdf/cs/0508056v1.pdf
I am not sure if you can say or prove that there is a minimal combinator. The paper ...
6
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, and the SEP entry on combinatory logic gives a sketch of a proof that does work.
6
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 discusses the problems to which beta-reduction gives rise.
As to the question, "could we use strong reduction to evaluation lambda terms?", the correspondence is not ...
6
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, if you wish) definitely links the three objects you mention: it actually tells that two of them, IL and $\lambda$c, are the same thing. The term is used ...
5
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.3.1 of Jaap van Oosten's book. I don't have any other books with me right now, but am sure almost any book on this topic will have the result, Barendregt's ...
4
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 otherwise) without binders.
Typed $\lambda$-calculi can easily be translated into combinatory logic. Some combinatory logics can easily be translated to typed
$\...
3
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 closed lambda expressions you can generate all the others.
Closed lambda expressions give you the equivalent of implications where any conclusion/output you ...
1
This is the same as picking a subset and replacing the elements in the subset with X
Only top voted, non community-wiki answers of a minimum length are eligible