Bounding skeletons were recently introduced as a tool to study the length of interactions in Hyland/Ong game semantics. In this paper, we investigate the precise connection between them and execution of typed λ-terms. Our analysis sheds light on a new condition on λ-terms, called local scope. We show that the reduction of locally scoped terms matches closely that of bounding skeletons. Exploiting this connection, we give upper bound to the length of linear head reduction for simply-typed locally scoped terms. General terms lose this connection to bounding skeletons. To compensate for that, we show that λ-lifting allows us to transform any λ-term into a locally scoped one. We deduce from that an upper bound to the length of linear head reduction for arbitrary simply-typed λ-terms. In both cases, we prove the asymptotical optimality of the upper bounds by providing matching lower bounds. © 2013 Springer-Verlag.
CITATION STYLE
Clairambault, P. (2013). Bounding skeletons, locally scoped terms and exact bounds for linear head reduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7941 LNCS, pp. 109–124). https://doi.org/10.1007/978-3-642-38946-7_10
Mendeley helps you to discover research relevant for your work.