Cost Semantics for Plotkin's PCF

Document
Document

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.

    Item Description
    Name(s)
    Thesis advisor: Danner, Norman
    Thesis advisor: Licata, Daniel R.
    Thesis advisor: Hermant, Olivier
    Date
    May 01, 2016
    Extent
    62 pages
    Language
    eng
    Genre
    Physical Form
    electronic
    Discipline
    Rights and Use
    In Copyright - Non-Commercial Use Permitted
    Digital Collection
    PID
    ir:2461