Coinductive Techniques in Infinitary Lambda-Calculus
Łukasz Czajka · arXiv (Cornell University) · 2015
The main aim of this paper is to promote a certain style of doing coinductive proofs, similar to inductive proofs as commonly done by mathematicians. For this purpose we provide a reasonably direct justification for coinductive proofs written in this style, i.e., converting a coinductive proof into a non-coinductive argument is purely a matter of routine. Our main interest is in applying this coinductive style of arguments in infinitary lambda-calculus. In the second part of the paper we present a new coinductive proof of confluence of B\ohm reduction in infinitary lambda-calculus. The proof is simpler than previous proofs of this result. The technique of the proof is new, i.e., it is not merely a coinductive reformulation of any earlier proofs.