Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
Quasi-interpretations are a tool to bound the size of the values computed by a first-order functional program (or a term rewriting system) and thus a mean to extract bounds on its computational complexity. We study the synthesis of quasi-interpretations selected in the space of polynomials over the max-plus algebra. We prove that the synthesis problem is NP-hard under various conditions and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. We provide a polynomial time algorithm to synthesize homogeneous quasi-interpretations of bounded degree and show how to extend the algorithm to synthesize (general) quasi-interpretations. The resulting algorithm generalizes certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity.
Wydawca
Czasopismo
Rocznik
Tom
Strony
29--60
Opis fizyczny
Bibliogr. 24 poz.
Twórcy
autor
- Université de Provence Centre de Mathèmatiques et d'Informatique (CMI), France, amadio@cmi.univ-mrs.fr
Bibliografia
- [1] R. Amadio, S. Coupet-Grimal, S. Dal Zilio and L. Jakubiec. A functional scenario for bytecode verification of resource bounds. In Proc. Computer Science Logic, Springer LNCS 3210, 2004.
- [2] R. Amadio and S. Dal Zilio. Resource control for synchronous cooperative threads. In Proc. CONCUR, Springer LNCS 3170, 2004.
- [3] L. Aceto, Z. Ėsik, and A. Ingólfsdóttir. The max-plus algebra of the natural numbers has no finite equational basis. Theoretical Computer Science 293(1):169–188, 3 February 2003.
- [4] R. Amadio. Max-plus quasi-interpretations. In Proc. Typed Lambda Calculi and Applications, Springer LNCS 2701, 2003.
- [5] S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the poly-time functions. Computational Complexity, 2:97–110, 1992.
- [6] A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137–160, 1987.
- [7] F. Baccelli, G. Cohen, G. Olsder, and J.-P. Quadrat. Synchronization and linearity. Wiley, 1992.
- [8] G. Bonfante, J.-Y. Marion, and J.-Y. Moyen. On lexicographic termination methods with space bound certifications. In Proc. Perspectives of System Informatics, Springer LNCS 2244, 2001.
- [9] F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998.
- [10] V. Caseiro. Equations for defining polytime functions. PhD thesis, University of Oslo, 1997.
- [11] A. Cobham. The intrinsic computational difficulty of functions. In Proc. Logic ,Methodology, and Philosophy of Science II, North Holland, 1965.
- [12] S. Cook. Characterizations of pushdown machines in terms of time-bounded computers. Journal of the ACM, 18(1):4–18, 1971.
- [13] B. Gramlich. On proving termination by innermost termination. In Proc. RTA 96, Springer Lecture Notes in Computer Science 1103, 1996.
- [14] J. Giesl. POLO - a system for termination proofs using polynomial orderings. Technical Report IBN 95/24, Technische Hochschule Darmstadt, 1995.
- [15] M. Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7(4):258–289, 2000.
- [16] M. Hofmann. The strength of non size-increasing computation. In Proc. ACM POPL, 2002.
- [17] M. Hofmann and S. Jost. Static prediction of heap space usage for first-order functional programs. In Proc. ACM POPL, 2003.
- [18] R. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Proc. ACM POPL, 1996.
- [19] N. Jones. Computability and complexity, from a programming perspective. MIT-Press, 1997.
- [20] D. Leivant. Predicative recurrence and computational complexity i: word recurrence and poly-time. Feasible mathematics II, Clote and Remmel (eds.), Birkhäuser:320–343, 1994.
- [21] J.-Y. Marion. Complexité implicite des calculs, de la théorie à la pratique. Université de Nancy, 2000. Habilitation à diriger des recherches.
- [22] J.-Y. Marion and J.-Y. Moyen. Efficient first order functional program interpreter with time bound certifications. In Proc. LPAR, Springer Lecture Notes in Computer Science 1955, 2000.
- [23] Y. Matiyasevich. Hilbert’s tenth problem. MIT Press, 1993.
- [24] J.-Y. Moyen. System presentation: An analyser of rewriting systems complexity. In Electronic Notes In Theoretical Computer Science, 59(4), 2001.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS2-0007-0002