# Jun 21, 2011: Jeroen Ketema: Computing with Infinite Terms and Infinite Reductions

June 21, 2011 | Computing with Infinite Terms and Infinite Reductions |

Room: Zi 5126 | Jeroen Ketema |

12:30-13:30 | We define computable infinitary term rewriting, thus introducing computability to the study of convergent, potentially infinite reductions over potentially infinite terms. Computable reductions of any ordinal length strictly below the Church-Kleene ordinal are supported; hence, we treat a maximal set of computable ordinals. Using computable infinitary rewriting, we give the first constructive proofs of two central results from infinitary rewriting under the assumption that rules have finite right-hand sides: (i) compression of left-linear systems, and (ii) confluence of orthogonal, non-collapsing systems. Thus, for (i) we show that there is a program that, given a computable reduction |