<p>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:</p>
<ul>
<li>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). <a href="https://arxiv.org/abs/0903.5505" rel="noreferrer">arXiv</a></li>
</ul>
<p>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 <span class="math-container">$\lambda$</span>-calculus is 1.  Surprisingly, they also prove that the asymptotic density of strongly normalizing SKI combinator terms among all SKI combinator terms is 0.</p>
<p>As suggested by Gabriel Scherer's response, the specific formulation of density you are asking about is related to the density of <em>normal</em> 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 <span class="math-container">$\lambda$</span>-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 <span class="math-container">$\lambda$</span>-terms: since normalization cannot increase the size of a term, the number of equivalence classes of terms of size <span class="math-container">$n$</span> is at most <span class="math-container">$n$</span> times the number of normal terms of size <span class="math-container">$n$</span>, hence the ratio of equivalence classes to terms is asymptotically 0.</p>

CC BY-SA 4.0
2021-02-26T16:19:31.007Z
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$.
Martin Berger
CC BY-SA 4.0
2021-02-26T16:21:52.633Z
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.
Martin Berger
CC BY-SA 4.0
2021-02-26T15:58:47.990Z
2021-02-26T15:58:47.990Z
Noam Zeilberger
<p>Let's look at a simple example of a toy programming language with unary natural numbers and a &quot;predecessor&quot; operation.</p>
<p><span class="math-container">$$t ::= 0 \mid S~t \mid p~t$$</span></p>
<p>whose semantics is given by the following rewrite rules</p>
<p><span class="math-container">$$p~(S~t) \to t
\qquad p~0 \to 0$$</span></p>
<p>with</p>
<p><span class="math-container">$$\mathsf{size}(0) = 1
\qquad \mathsf{size}(S~t) = 1 + \mathsf{size}(t)
\qquad \mathsf{size}(p~t) = 1 + \mathsf{size}(t)$$</span></p>
<p>(For equivalence we take the smallest congruence that includes the relation  <span class="math-container">$(\to)$</span>.)</p>
<p>Then the terms of size <span class="math-container">$n+1$</span> are of the form <span class="math-container">$c~(... (c~0)...)$</span>, where each <span class="math-container">$c$</span> is either <span class="math-container">$S$</span> or <span class="math-container">$p$</span>. There are <span class="math-container">$2^n$</span> such terms, and exactly <span class="math-container">$n+1$</span> normal forms (equivalence classes); for example a family of size-<span class="math-container">$n+1$</span> representatives are the <span class="math-container">$S~(S~(... S~(p~(p~...(p~0))))$</span>: a term in this family with <span class="math-container">$k$</span> uses of <span class="math-container">$S$</span> and <span class="math-container">$n-k$</span> uses of <span class="math-container">$p$</span> is equivalent to <span class="math-container">$S^k~0$</span>.</p>
<p>So we have <span class="math-container">$\mathsf{density}(n+1) = (n+1) / 2^n$</span>, which quickly converges to <span class="math-container">$0$</span>.</p>
<p>Now if you take the different language of <em>normal forms</em> of the grammar above, then those are exactly the terms without <span class="math-container">$p$</span>. At size <span class="math-container">$n$</span> there is exactly one such term, and also one equivalence classe. So we have <span class="math-container">$\mathsf{density}(n) = 1$</span> for any <span class="math-container">$n$</span>.</p>

CC BY-SA 4.0
2021-02-26T09:08:43.787Z
If I understand you correctly, trivial modifications of syntax get us any densitiy we want (or at least 0 and 1)?
Andrej Bauer
CC BY-SA 4.0
2021-02-26T16:16:14.763Z
@AndrejBauer As Gasche's last example removes all non-trivial reductions, I'd
say that's a major semantic change.
Martin Berger
CC BY-SA 4.0
2021-02-26T06:48:27.313Z
2021-02-26T06:48:27.313Z
gasche
<p>Let <span class="math-container">$L$</span> be a programming language, and <span class="math-container">$\cong$</span> a notion of equality of <span class="math-container">$L$</span>-programs (in general <span class="math-container">$\cong$</span> will be undecidable).  Let <span class="math-container">$syntax(n)$</span> be the number  of <span class="math-container">$L$</span>-programs of size <span class="math-container">$n$</span> (for some reasonable notion of program  size), and <span class="math-container">$semantics(n)$</span> denotes the number of <span class="math-container">$\cong$</span>-equivalence  classes of <span class="math-container">$L$</span>-programs of size <span class="math-container">$n$</span>. Now define</p>
<p><span class="math-container">$$  density(n) = semantics(n)\ /\ syntax(n)$$</span></p>
<p>So <span class="math-container">$density(n)$</span> tells us how many really distinct programs we can
write of size <span class="math-container">$n$</span>. What is known about the limit:</p>
<p><span class="math-container">$$   \lim_{n \rightarrow \infty} density(n)?$$</span></p>
<p>I conjecture that <span class="math-container">$\lim_{n \rightarrow \infty} density(n) = 0$</span> for
reasonable choices of <span class="math-container">$L$</span> and <span class="math-container">$\cong$</span>, since the larger programs are
allowed to be, the more room for redundancies like <span class="math-container">$M+N \cong N+M$</span>.</p>
<p><b>Question.</b> What is related work this direction?</p>

CC BY-SA 4.0
2021-03-06T20:20:53.787Z
@NoamZeilberger That's true.  Some maybe the question could be refined to analysing
how fast $density(\cdot)$ goes to 0, which could be done by finding
nice functions $f$ such that $\lim_{n \rightarrow \infty}
density(n)/f(n) > 0$?
Martin Berger
CC BY-SA 4.0
2021-02-25T20:38:49.713Z
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.
Denis
CC BY-SA 4.0
2021-02-25T20:41:30.303Z
@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.
Martin Berger
CC BY-SA 4.0
2021-02-26T09:06:49.877Z
@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.
Andrej Bauer
CC BY-SA 4.0
2021-02-26T09:18:16.950Z
@AndrejBauer I'm not sure I follow. If numbers are defined with a natural syntax (say in binary), their addition is completely well-defined and decidable. On the other hand, there is no syntax for Turing-complete programs allowing this. No matter what you choose for $L$, you will have programs $P_1$ and $P_2$ whose equivalence is independent of ZFC.
Denis
CC BY-SA 4.0
2021-02-26T17:21:49.423Z
@Denis: you are still confusing well-definedness and decidability. I can apply your worries to numbers thus: given any Turing machine $T$, define $n$ to be $1$ if $T$ halts and $0$ if it does not. The number $n$ is well defined, but the question whether it is even might be difficult to answer.
Andrej Bauer
CC BY-SA 4.0
2021-02-26T17:22:09.543Z
@Denis: What are "Turing-complete programs"?
Andrej Bauer
CC BY-SA 4.0
2021-02-26T18:44:34.960Z
@AndrejBauer by " syntax for Turing-complete programs" I meant a syntax allowing to simulate Turing machines (badly worded indeed). But ok I see your point, although it is independent from ZFC, the equivalence of programs is well-defined :just compare their behaviour on any input. My point was that proving stuff about density is likely to be difficult, since it involves undecidable properties. This is inherent to the objects manipulated, contrarily to your example with numbers which is artificial: the undecidability is due to the special way you define them, not the numbers themselves.
Denis
CC BY-SA 4.0
2021-02-26T20:12:37.807Z
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.
Noam Zeilberger
CC BY-SA 4.0
2021-02-26T20:13:09.270Z
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.
Noam Zeilberger
CC BY-SA 4.0
2021-02-26T22:31:54.077Z
@NoamZeilberger I agree, $density(.)$ might be a tad simplistic. In order to side-step subtleties whose consequences I currently don't have an intuition about, I wanted to start simple! That's why I parameterised the definition by ≅. Are there reasonable languages where $\lim_{ \rightarrow \infty} ()>0$? One place to start looking are languages where $\cong$-classes are not closed under reduction (e.g. timed languages like Verilog, Lustre, Esterel): clearly those have, in some sense, more behaviour than untimed languages where $\rightarrow \subseteq \cong$.
Martin Berger
CC BY-SA 4.0
2021-02-27T08:00:52.013Z
The problem is that even if there is a little bit of redundancy, it is unlikely to be bounded as n grows to infinity and so the asymptotic density will be 0.  For example, suppose your "syntax" is arbitrary strings in $\Sigma^*$ and your "semantics" is just quotienting by cyclic equivalence $uv \cong vu$. This is a very mild notion of equivalence, but still every string of length n has n equivalent cyclic shifts and so, taking the limit as $n \to \infty$, the asymptotic density is 0.
Noam Zeilberger
<reference-request><pl.programming-languages><semantics><equivalence>
Density of semantics in syntax
Martin Berger
# Density of semantics in syntax

(Asked by: username_0 on 2021-02-25)

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?

**Tags:** reference-request, pl.programming-languages, semantics, equivalence

> **Comments:**
> **username_1**: 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.  
> **username_0**: @username_1 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.  
> **username_2**: @username_1: 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.  
> **username_1**: @AndrejBauer I'm not sure I follow. If numbers are defined with a natural syntax (say in binary), their addition is completely well-defined and decidable. On the other hand, there is no syntax for Turing-complete programs allowing this. No matter what you choose for $L$, you will have programs $P_1$ and $P_2$ whose equivalence is independent of ZFC.  
> **username_2**: @username_1: you are still confusing well-definedness and decidability. I can apply your worries to numbers thus: given any Turing machine $T$, define $n$ to be $1$ if $T$ halts and $0$ if it does not. The number $n$ is well defined, but the question whether it is even might be difficult to answer.  
> **username_2**: @username_1: What are "Turing-complete programs"?  
> **username_1**: @AndrejBauer by " syntax for Turing-complete programs" I meant a syntax allowing to simulate Turing machines (badly worded indeed). But ok I see your point, although it is independent from ZFC, the equivalence of programs is well-defined :just compare their behaviour on any input. My point was that proving stuff about density is likely to be difficult, since it involves undecidable properties. This is inherent to the objects manipulated, contrarily to your example with numbers which is artificial: the undecidability is due to the special way you define them, not the numbers themselves.  
> **username_3**: 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.  
> **username_3**: 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.  
> **username_0**: @NoamZeilberger I agree, $density(.)$ might be a tad simplistic. In order to side-step subtleties whose consequences I currently don't have an intuition about, I wanted to start simple! That's why I parameterised the definition by ≅. Are there reasonable languages where $\lim_{ \rightarrow \infty} ()>0$? One place to start looking are languages where $\cong$-classes are not closed under reduction (e.g. timed languages like Verilog, Lustre, Esterel): clearly those have, in some sense, more behaviour than untimed languages where $\rightarrow \subseteq \cong$.  
> **username_3**: The problem is that even if there is a little bit of redundancy, it is unlikely to be bounded as n grows to infinity and so the asymptotic density will be 0.  For example, suppose your "syntax" is arbitrary strings in $\Sigma^*$ and your "semantics" is just quotienting by cyclic equivalence $uv \cong vu$. This is a very mild notion of equivalence, but still every string of length n has n equivalent cyclic shifts and so, taking the limit as $n \to \infty$, the asymptotic density is 0.  
> **username_0**: @NoamZeilberger That's true.  Some maybe the question could be refined to analysing how fast $density(\cdot)$ goes to 0, which could be done by finding nice functions $f$ such that $\lim_{n \rightarrow \infty} density(n)/f(n) > 0$?  

---

## 2 answers

### Answer by username_3 on 2021-02-26. Score: 6

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](https://arxiv.org/abs/0903.5505)

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.

> **Comments:**
> **username_0**: 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$.  
> **username_0**: 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.  

---

### Answer by username_4 on 2021-02-26. Score: 5

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$.

> **Comments:**
> **username_2**: If I understand you correctly, trivial modifications of syntax get us any densitiy we want (or at least 0 and 1)?  
> **username_0**: @AndrejBauer As Gasche's last example removes all non-trivial reductions, I'd say that's a major semantic change.  

---

