Lambda calculus is certainly tricky for counting steps, since a single step of beta-reduction can actually do a lot of "work", unlike e.g. a Turing machine wher

Lambda calculus is certainly tricky for counting steps, since a single step of beta-reduction can actually do a lot of "work", unlike e.g. a Turing machine where each step takes constant resources. For AIT, the binary encodings used in this paper have the nice property that they're complete and prefix-free, meaning that every binary string either decodes to a term (perhaps using only an initial portion of the string), or can be extended (arbitrarily) until it gives rise to a term. At first glance, it feels like it would be hard for lambda terms to "give a substring of their string as outputs", since that would require re-encoding a subterm. However, I don't think that's as bad as it sounds. For example, consider that a Turing machine can only move its head along the tape one cell at a time (we could use any finite step size, but we usually stick to one), which makes it difficult/impossible to "preserve" a section of tape. Hence Turing machines which "give a substring of their string as outputs" might sound simple, but would probably be somewhat complicated to ensure that any "corruption" caused when traversing the tape gets "undone" afterwards. (Unless they're multitape machines, like monotone turing machines!)