4
$\begingroup$

Let $L$ be a programming language, and $\cong$ a notion of equality of $L$-programs (in general $\cong$ will be undecidable). Let $syntax(n)$ be the number of $L$-programs of size $n$ (for some reasonable notion of program size), and $semantics(n)$ denotes the number of $\cong$-equivalence classes of $L$-programs of size $n$. Now define

$$ density(n) = semantics(n)\ /\ syntax(n)$$

So $density(n)$ tells us how many really distinct programs we can write of size $n$. What is known about the limit:

$$ \lim_{n \rightarrow \infty} density(n)?$$

I conjecture that $\lim_{n \rightarrow \infty} density(n) = 0$ for reasonable choices of $L$ and $\cong$, since the larger programs are allowed to be, the more room for redundancies like $M+N \cong N+M$.

Question. What is related work this direction?

$\endgroup$
12
  • 1
    $\begingroup$ just a side remark: your equivalence is not completely well-defined, since as soon as $L$ is Turing-complete the equivalence of two programs is undecidable, and there will be particular instances of pairs of programs for which equivalence is mathematically undecidable. You could define such programs to be non-equivalent, but this already shows the kind of difficulty we'll be facing to prove stuff about density. $\endgroup$ – Denis Feb 25 at 20:38
  • 3
    $\begingroup$ @Denis Yes $\cong$ is generally undecidable, but that doesn't affect the question's well-definedness. Only how easy/hard it is to answer (I expect it to be hard to say anything strong about this limit.) For approximations of $density(n)$, you can replace $\cong$ by computable over/under-approximations, like considering two programs the same iff they return the same result on 5 random inputs. $\endgroup$ – Martin Berger Feb 25 at 20:41
  • 1
    $\begingroup$ @Denis: your concern is irrelevant. By your reasoning we should worry about addition of numbers, because we can define a number whose value is predicated on some undecidable mathematical problem. There is no question about well-definedness, but we can ask about the logical complexity of the definition. $\endgroup$ – Andrej Bauer Feb 26 at 9:06
  • 1
    $\begingroup$ about this formulation of density, I am not sure I buy that it tells us "how many really distinct programs we can write of size n." For languages and equational theories of interest (like $\lambda$-calculus modulo $\beta$), both the number of programs and the number of inequivalent programs grows exponentially with size. Moreover, if we pick two random programs of size n, the probability they are equivalent is exponentially small. $\endgroup$ – Noam Zeilberger Feb 26 at 20:12
  • 1
    $\begingroup$ So if $\lim_{n\to\infty} density(n) = 0$, I wouldn't interpret it as saying that we can write very few distinct programs, but rather only (as you suggest at the end) that there is a lot of redundancy in the encoding. $\endgroup$ – Noam Zeilberger Feb 26 at 20:13
6
$\begingroup$

In terms of related work, Marek Zaionc and collaborators have been studying similar kinds of questions for some time. The following paper includes many results:

  • René David, Katarzyna Grygiel, Jakub Kozic, Christophe Raffalli, Guillaume Theyssier, Marek Zaionc. Asymptotically almost all λ-terms are strongly normalizing. Logical Methods in Computer Science, Volume 9, Issue 1 (February 15, 2013). arXiv

The result stated in the title is not exactly the same as the one you are asking about, but related: they prove that the asymptotic density of strongly normalizing terms among all terms of $\lambda$-calculus is 1. Surprisingly, they also prove that the asymptotic density of strongly normalizing SKI combinator terms among all SKI combinator terms is 0.

As suggested by Gabriel Scherer's response, the specific formulation of density you are asking about is related to the density of normal terms among all terms, or in other words the probability that a uniformly random term of a given size is already normalized. For subsystems of $\lambda$-calculus the probability that a term is normal typically decreases exponentially with size, and I believe it should be a small step from there to proving that the asymptotic density you are interested in is 0. Certainly this is true for linear $\lambda$-terms: since normalization cannot increase the size of a term, the number of equivalence classes of terms of size $n$ is at most $n$ times the number of normal terms of size $n$, hence the ratio of equivalence classes to terms is asymptotically 0.

$\endgroup$
2
  • $\begingroup$ Good points! I wonder if one can prove that the limit is 0 simply from assuming that a language is Turing-complete and some lightweight reasonableness conditions of $\cong$. $\endgroup$ – Martin Berger Feb 26 at 16:19
  • $\begingroup$ Note also that syntactically different NFs can be in the same $\cong$-equivalence class, e.g. $\lambda x.1+3 = \lambda x.4$, so counting NFs overestimates density. $\endgroup$ – Martin Berger Feb 26 at 16:21
5
$\begingroup$

Let's look at a simple example of a toy programming language with unary natural numbers and a "predecessor" operation.

$$t ::= 0 \mid S~t \mid p~t$$

whose semantics is given by the following rewrite rules

$$p~(S~t) \to t \qquad p~0 \to 0$$

with

$$\mathsf{size}(0) = 1 \qquad \mathsf{size}(S~t) = 1 + \mathsf{size}(t) \qquad \mathsf{size}(p~t) = 1 + \mathsf{size}(t)$$

(For equivalence we take the smallest congruence that includes the relation $(\to)$.)

Then the terms of size $n+1$ are of the form $c~(... (c~0)...)$, where each $c$ is either $S$ or $p$. There are $2^n$ such terms, and exactly $n+1$ normal forms (equivalence classes); for example a family of size-$n+1$ representatives are the $S~(S~(... S~(p~(p~...(p~0))))$: a term in this family with $k$ uses of $S$ and $n-k$ uses of $p$ is equivalent to $S^k~0$.

So we have $\mathsf{density}(n+1) = (n+1) / 2^n$, which quickly converges to $0$.

Now if you take the different language of normal forms of the grammar above, then those are exactly the terms without $p$. At size $n$ there is exactly one such term, and also one equivalence classe. So we have $\mathsf{density}(n) = 1$ for any $n$.

$\endgroup$
2
  • $\begingroup$ If I understand you correctly, trivial modifications of syntax get us any densitiy we want (or at least 0 and 1)? $\endgroup$ – Andrej Bauer Feb 26 at 9:08
  • $\begingroup$ @AndrejBauer As Gasche's last example removes all non-trivial reductions, I'd say that's a major semantic change. $\endgroup$ – Martin Berger Feb 26 at 16:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.