the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all
so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it
if you can't, you may have gained enough insight into the problem to show that the system actually does guarantee termination, and maybe even show useful time bounds on it
if you can, you have usually shown the system is turing-complete, which means you can appeal to rice's theorem whenever you are tempted to analyze the behavior of the system in any way, so you can satisfy yourself with partial decision procedures that work often enough to be useful and are conservative in the appropriate way, rather than wasting time trying to find a complete solution
(also if you're designing the system you might consider either supporting iteration more directly or removing the back door)
every once in a while it's also useful in practice to be able to program a weird machine, too
> the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all
This is only the case for untyped systems. If we try to type the Y combinator, we will eventually need some notion of recursion. For example, in Haskell/OCaml we can type it with iso/equi-recursive types. How many truly untyped systems we use in practice?
The Y combinator as a counterexample of termination is a great insight though!
Dynamically typed programming languages are statically untyped.
You might argue they are unityped, but that’s really a type theoretician’s job security: if a language has the untyped lambda calculus as a subset (like the python example in this discussion) it’s reasonable to call it untyped.
so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it
if you can't, you may have gained enough insight into the problem to show that the system actually does guarantee termination, and maybe even show useful time bounds on it
if you can, you have usually shown the system is turing-complete, which means you can appeal to rice's theorem whenever you are tempted to analyze the behavior of the system in any way, so you can satisfy yourself with partial decision procedures that work often enough to be useful and are conservative in the appropriate way, rather than wasting time trying to find a complete solution
(also if you're designing the system you might consider either supporting iteration more directly or removing the back door)
every once in a while it's also useful in practice to be able to program a weird machine, too