Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Accattoli, B., Lago, U.D.: On the invariance of the unitary cost model for head reduction. In: Tiwari, A. (ed.) RTA. LIPIcs, vol. 15, pp. 22–37. Leibniz-Zentrum fuer Informatik, Schloss Dagstuhl (2012)
Beckmann, A.: Exact bounds for lengths of reductions in typed lambda-calculus. J. Symb. Log. 66(3), 1277–1285 (2001)
Bernadet, A., Lengrand, S.: Complexity of strongly normalising λ-terms via non-idempotent intersection types. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 88–107. Springer, Heidelberg (2011)
Clairambault, P.: Estimation of the length of interactions in arena game semantics. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 335–349. Springer, Heidelberg (2011)
Coquand, T.: A semantics of evidence for classical arithmetic. J. Symb. Log. 60(1), 325–337 (1995)
Danos, V., Herbelin, H., Regnier, L.: Game semantics and abstract machines. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, LICS 1996, pp. 394–405. IEEE (1996)
Danos, V., Regnier, L.: How abstract machines implement head linear reduction (2003) (unpublished)
Danos, V., Joinet, J.-B.: Linear logic and elementary time. Inf. Comput. 183(1), 123–137 (2003)
de Carvalho, D., Pagani, M., de Falco, L.T.: A semantic measure of the execution time in linear logic. TCS 412(20), 1884–1902 (2011)
Girard, J.-Y.: Light linear logic. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 145–176. Springer, Heidelberg (1995)
Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)
Johnsson, T.: Lambda lifting: Transforming programs to recursive equations. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 190–203. Springer, Heidelberg (1985)
Dal Lago, U., Laurent, O.: Quantitative game semantics for linear logic. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 230–245. Springer, Heidelberg (2008)
Schwichtenberg, H.: An upper bound for reduction sequences in the typed λ-calculus. Archive for Mathematical Logic 30(5), 405–408 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clairambault, P. (2013). Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction. In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications. TLCA 2013. Lecture Notes in Computer Science, vol 7941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38946-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-38946-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38945-0
Online ISBN: 978-3-642-38946-7
eBook Packages: Computer ScienceComputer Science (R0)