Ugo Dal Lago (University of Bologna), Higher-order Interpretations and Program Complexity (joint work with Patrick Baillot).
Schedule
- Jan. 30, 2012, 15:00 - 15:30
Abstract
Polynomial interpretations and their generalizations like quasi-interpretations have
been used in the setting of rst-order functional languages to design criteria en-
suring statically some complexity bounds on programs. This ts in the area of
implicit computational complexity, which aims at giving machine-free character-
izations 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 de ne higher-order polynomial interpretations (HOPI) for them and give a cri-
terion based on HOPIs to ensure that a program can be executed in polynomial
time. In order to obtain a criterion which is
exible enough to validate some inter-
esting programs using higher-order primitives, we introduce a notion of polynomial
quasi-interpretations, coupled with a simple termination criterion.
Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of rst-order functional languages to design criteria en- suring statically some complexity bounds on programs. This ts in the area of implicit computational complexity, which aims at giving machine-free character- izations 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 de ne higher-order polynomial interpretations (HOPI) for them and give a cri- terion based on HOPIs to ensure that a program can be executed in polynomial time. In order to obtain a criterion which is exible enough to validate some inter- esting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion.