Affiliations: [a] Department of Computing, Imperial College London, London, United Kingdom | [b] Department of Computer Science, University of Copenhagen (DIKU), Copenhagen, Denmark. simonsen@diku.dk
Correspondence:
[*]
Address for correspondence: Deptment of Computer Science, University of Copenhagen (DIKU), Copenhagen, Denmark.
Note: [†] Jeroen Ketema contributed to this work while at Imperial College London. He is currently at ESI (TNO), the Netherlands.
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.
Keywords: Infinitary term rewriting, computability, descendants, origins, needed reductions
