Publication Date

5-2016

Advisor(s)

Norman Danner, Daniel Licata , Olivier Hermant

Department

Computer Science

Language

English

Abstract

We develop a formalism for extracting recurrences from programs written in a variant of Plotkin's PCF, a typed higher-order functional language that integrates functions and natural numbers through general recursion. The complexity of an expression is de_ned as a pair consisting of a cost and a potential. The former is the explicit cost of evaluating the expression to a value while the latter is the cost of future use of the value. The extraction function is a language-to-language translation that makes evaluation costs explicit by mapping source language expressions to complexity language expressions. We prove by a logical relations argument that recurrences extracted by the extraction function are upper bounds for evaluation cost. The proof makes use of bounded recursion, a key property of which is the principle of fixed point induction, which allows us to be able to reason about recursive computations.

Share

COinS
 

© Copyright is owned by author of this document