Abstract
We introduce a novel resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the innermost runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system \(\mathcal R\) can be well-typed, then there exists a polynomial interpretation that orients \(\mathcal R\). For this we adequately adapt the standard notion of polynomial interpretations to the typed setting.
This research is partly supported by FWF (Austrian Science Fund) project P25781.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. JAR 46 (2011)
Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117–133. Springer, Heidelberg (2010)
Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011)
Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. JAR 51, 27–56 (2013)
Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 781–786. Springer, Heidelberg (2012)
Avanzini, M., Moser, G.: Tyrolean complexity tool: Features and usage. In: Proc. 24th RTA. LIPIcs, vol. 21, pp. 71–80 (2013)
Okasaki, C.: Purely functional data structures. Cambridge University Press (1999)
Tarjan, R.: Amortized computational complexity. SIAM J. Alg. Disc. Math. 6, 306–318 (1985)
Turing, A.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67–69. Cambridge University (1949)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)
Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. JFP 11, 33–53 (2001)
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proc. 30th POPL, pp. 185–197. ACM (2003)
Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-interpretations a way to control resources. TCS 412, 2776–2796 (2011)
Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 287–306. Springer, Heidelberg (2010)
Hoffmann, J., Hofmann, M.: Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 172–187. Springer, Heidelberg (2010)
Hofmann, M., Moser, G.: Amortised resource analysis and typed polynomial interpretations (extended version). CoRR, cs.LO (2014), http://arxiv.org/abs/1402.1922
Jouannaud, J.P., Rubio, A.: The higher-order recursive path ordering. In: Proc. 14th LICS, pp. 402–411. IEEE Computer Society (1999)
TeReSe: Term Rewriting Systems. Cambridge Tracks in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Jost, S., Loidl, H.-W., Hammond, K., Scaife, N., Hofmann, M.: “Carbon Credits” for resource-bounded computations using amortised analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 354–369. Springer, Heidelberg (2009)
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. TOPLAS 34, 14 (2012)
Hoffmann, J.: Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. PhD thesis, Ludwig-Maximilians-Universiät München (2011)
Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. JAR 34, 325–363 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Hofmann, M., Moser, G. (2014). Amortised Resource Analysis and Typed Polynomial Interpretations. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-08918-8_19
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08917-1
Online ISBN: 978-3-319-08918-8
eBook Packages: Computer ScienceComputer Science (R0)