The under-performing unfold: a new approach to optimising corecursive programs

Hackett, Jennifer; Hutton, Graham; Jaskelioff, Mauro

Abstract

This paper presents a new approach to optimising corecursive programs by factorisation. In particular, we focus on programs written using the corecursion operator unfold. We use and expand upon the proof techniques of guarded coinduction and unfold fusion, capturing a pattern of generalising coinductive hypotheses by means of abstraction and representation functions. The pattern we observe is simple, has not been observed before, and is widely applicable. We develop a general program factorisation theorem from this pattern, demonstrating its utility with a range of practical examples.

Citation

Hackett, J., Hutton, G., & Jaskelioff, M. (2013). The under-performing unfold: a new approach to optimising corecursive programs.

• Conference Name: International Symposium on Implementation and Application of Functional Languages (25th)
• End Date: Aug 30, 2013
• Publication Date: Jan 1, 2013
• Deposit Date: Feb 26, 2015
• Publicly Available Date: Feb 26, 2015
• Peer Reviewed: Peer Reviewed
• Keywords: fusion, factorisation, coinduction, unfolds
• Public URL: https://nottingham-repository.worktribe.com/output/1004333
• Publisher URL: http://dl.acm.org/citation.cfm?doid=2620678.2620679
• Additional Information: Published in: IFL '13: proceedings of the 25th Symposium on Implementation and Application of Functional Languages. New York : ACM, 2014, ISBN: 978-1-4503-2988-0. pp. 4321-4332, doi: 10.1145/2620678.2620679