Computing with Infinite Terms and Infinite Reductions
Jeroen Ketema, Jakob Grue Simonsen · Fundamenta Informaticae · 2019
We define computable infinitary rewriting by introducing computability to the study of strongly convergent infinite reductions over infinite first-order terms. Given computable infinitary reductions, we show that descendants and origins—essential to proving fundamental properties such as compression and confluence—are computable across such reductions.