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

TL;DR

This paper provides a formal grammar model for call-by-name stack behavior and proves that Turchin's relation can effectively terminate all computations within this model, enhancing supercompilation techniques.

Contribution

It introduces a formal grammar model for call-by-name semantics and proves Turchin's relation's termination capability within this framework.

Findings

Formal grammar model of call-by-name stack behavior

Classification of the model in the Chomsky hierarchy

Proof that Turchin's relation terminates all computations in the model

Abstract

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.