Open Access. Powered by Scholars. Published by Universities.®
Programming Languages and Compilers Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Keyword
Articles 1 - 3 of 3
Full-Text Articles in Programming Languages and Compilers
A Static Cost Analysis For A Higher-Order Language, Norman Danner, Jennifer Paykin, James Royer
A Static Cost Analysis For A Higher-Order Language, Norman Danner, Jennifer Paykin, James Royer
Norman Danner
We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a potential. The former is defined to be the size of the expression's evaluation derivation in a standard big-step operational semantics. The latter is a measure of the "future" cost of using the value of that expression. A translation function ||.|| maps target expressions to complexities. Our main result is the following Soundness Theorem: If t is a term in the target language, then the cost component of ||t|| is an upper …
Two Algorithms In Search Of A Type System, Norman Danner, James Royer
Two Algorithms In Search Of A Type System, Norman Danner, James Royer
Norman Danner
The authors’ ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR -definable ( ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR can fairly naturally express the classic insertion- and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based …
Ramified Structural Recursion And Corecursion, Norman Danner, James Royer
Ramified Structural Recursion And Corecursion, Norman Danner, James Royer
Norman Danner
We investigate feasible computation over a fairly general notion of data and codata. Specifically, we present a direct Bellantoni-Cook-style normal/safe typed programming formalism, RS1, that expresses feasible structural recursions and corecursions over data and codata specified by polynomial functors. (Lists, streams, finite trees, infinite trees, etc. are all directly definable.) A novel aspect of RS1 is that it embraces structure-sharing as in standard functional-programming implementations. As our data representations use sharing, our implementation of structural recursions are memoized to avoid the possibly exponentially-many repeated subcomputations a naive implementation might perform. We introduce notions of size for representations of data (accounting …