Synthesis of max-plus quasi-interpretations

• Autorzy: Amadio R. M.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

functional languages and term rewriting; function algebras and implicit computational complexity; static analysis; polynomial interpretations and max-plus algebras

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 65, nr 1,2
• Strony: 29--60
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Amadio R. M.

• Université de Provence Centre de Mathèmatiques et d'Informatique (CMI), France,

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.