inria-00100523, version 1
On lexicographic termination ordering with space bound certifications
International Andrei Ershov Memorial Conference - PSI'01 2244 (2001) 482-493
Abstract: We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space.
- a – UNIVERSITE HENRI POINCARE
- b – UNIVERSITE NANCY 2
- 1:
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Other
- Keywords : lexicographic path ordering – polynomial space certification || lexicographic path ordering – espace polynomial – certification
- Internal note : A01-R-187 || bonfante01a
- Comment : Colloque avec actes et comité de lecture. internationale.
- inria-00100523, version 1
- http://hal.inria.fr/inria-00100523
- oai:hal.inria.fr:inria-00100523
- From:
- Submitted on: Tuesday, 26 September 2006 14:46:28
- Updated on: Thursday, 28 September 2006 15:22:47
Export