hal-00667816, version 1
Higher-order Interpretations and Program Complexity (Long Version)
Patrick Baillot
1Ugo Dal Lago 2
Résumé : Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs. This fi ts in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. Here we extend this approach to the higher-order setting. For that we consider the notion of simply typed term rewriting systems, we defi ne higher-order polynomial interpretations (HOPI) for them and give a criterion based on HOPIs to ensure that a program can be executed in polynomial time. In order to obtain a criterion which is flexible enough to validate some interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.
- 1 : Laboratoire de l'Informatique du Parallélisme (LIP)
- Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I
- 2 : Dipartimento di Scienze dell'Informazione
- Università di Bologna
- Domaine : Informatique/Logique en informatique
- Mots-clés : implicit computational complexity – rewrite systems – polynomial interpretations – quasi-interpretations – polynomial time complexity
- Commentaire : 21 pages
- hal-00667816, version 1
- http://hal.archives-ouvertes.fr/hal-00667816
- oai:hal.archives-ouvertes.fr:hal-00667816
- Contributeur : Patrick Baillot
- Soumis le : Mercredi 8 Février 2012, 14:15:19
- Dernière modification le : Mercredi 8 Février 2012, 14:17:41






Documents associés
Exporter