New answers tagged

2

It is. There's a fairly simple construction compiling from CT to CT2. First, consider that it's possible to double every command in a CT program without producing any behaviour (that is, A becomes AA, B becomes BB, C becomes CC). The queue of bits now has every bit doubled, but the cycle of commands only does anything with every second bit, so the modified ...


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