Productively recursing infinitely
Modelling evaluation of lambda calculus with coinduction in Agda
S.J.A. van de Noort (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jesper Cockx – Mentor (TU Delft - Programming Languages)
B. Liesnikov – Mentor (TU Delft - Programming Languages)
Diomidis Spinellis – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Coinduction is used to model infinite data or cycles in Agda. However, it is not as well explored in Agda as induction. Therefore, support for it might be lacking compared to induction. I explore how this applies for the evaluation of lambda calculus, what the different encodings of lambda calculus using coinduction are, and how they compare to each other and to an inductive evaluator. The two models I looked at are modelling cycles in variable references and modelling cycles in recursive variables. Cycles in variable references can be modelled coinductively, however, they do not help with evaluation. Since the evaluator is not coinductive, it is not accepted by the termination checker, therefore, it is not safer than an inductive evaluator. Encoding recursion using coinduction does make the evaluator terminate, aiding in creating a correct evaluator. This comes with the downside of sacrificing clarity and ease of reasoning about the code.