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