Abstract
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.
