“Termination and Productivity Checking with Continuous Types” Second Thoughts

Andreas Abel

19 May 2010

The last display before Section 5 characterizes the legal return types of corecursive functions. The second example, Nat × Y does not fit the grammar, contrary to the claim in the paper. Consequently, the definition of fib′ from the introduction is not legal according to the rules given in the paper. Indeed, if Nat × Y was legal, then the term

fix^{ν}g. (fst g, fst g :: snd g) : ∀Y ≈ Stream. Nat × Y

would be accepted, but it is not productive.

The grammar for legal result types is correct, the fib′ example is wrong. The old errata below no longer apply.

Old, erroneous errata (8 January 2005)

The reduction rule for fix^{ν} is strongly normalizing, but it does not have enough reductions in case the result type of corecursion is not directly a coinductive type. This problem arises in case of the unfolded stream of Fibonacci numbers fib′ : ∀Y ≈ Stream. Nat×Y (the type is a product of some type and a coinductive type): The term

fst fib′ = fst (fix^{ν}f. (0, 1 :: sum (fold f) (snd f)))

does not reduce, since the evaluation context fst • is not of the form unfold E[•]. Trying to get the other Fibonacci numbers out of the stream, we obtain

fst (unfold (snd fib′))  ⟶^{+} 1,  and
fst (unfold (snd (unfold (snd fib′))) ⟶^{+} fst fib′ + 1.

This means that we cannot compute the values of the Fibonacci numbers.

The problem cannot be mended by relaxing the reduction rule for corecursion to E[fix^{ν}g.M] ⟶_{β} E[[fix^{ν}g.M/g]M], since then snd fib′ loops immediately. It would be sound, though, to let both

fst fib′  and

unfold (snd fib′) reduce. This, of course, complicates the term calculus, since fix^{ν} would need to carry the annotation under which evaluation contexts it should unfold. The list of evaluation contexts would depend on the derivation of Y legal^{ν} τ(Y) in the typing rule of fix^{ν}.