Electronic Proceedings in Theoretical Computer Science (Jul 2016)

Turchin's Relation for Call-by-Name Computations: A Formal Approach

  • Antonina Nepeivoda

DOI
https://doi.org/10.4204/EPTCS.216.8
Journal volume & issue
Vol. 216, no. Proc. VPT 2016
pp. 137 – 159

Abstract

Read online

Supercompilation is a program transformation technique that was first described by V. F. Turchin in the 1970s. In supercompilation, Turchin's relation as a similarity relation on call-stack configurations is used both for call-by-value and call-by-name semantics to terminate unfolding of the program being transformed. In this paper, we give a formal grammar model of call-by-name stack behaviour. We classify the model in terms of the Chomsky hierarchy and then formally prove that Turchin's relation can terminate all computations generated by the model.