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

June 21, 2011Computing with Infinite Terms and Infinite Reductions
Room: Zi 5126Jeroen Ketema

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 S having computable ordinal length, will output a program computing a reduction of length at most ω with the same start and end term as S. For (ii) we show that if the peak of a confluence diagram consists of computable reductions, then so does the valley, and there exists a program computing the valley when given the peak as input. As a corollary, we obtain a simple constructive proof of an infinitary Church-Rosser property.

We provide Haskell implementations of all constructions.