New answers tagged

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


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 + \...


Top 50 recent answers are included