Norman Danner, Daniel Licata , Olivier Hermant
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.
Kim, Theodore Seok, "Cost Semantics for Plotkin's PCF" (2016). Masters Theses. 130.
© Copyright is owned by author of this document