Selective Strictness and Parametricity in Structural Operational Semantics, Inequationally

ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
Patricia Johann Ph.D, Professor (Creator)
Institution
Appalachian State University (ASU )
Web Site: https://library.appstate.edu/

Abstract: Parametric polymorphism constrains the behavior of pure functional pro-grams in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. The formal background of such ‘free theorems’ is well developed for extensions of the Girard-Reynolds polymorphic lambda calculus by algebraic datatypes and general recursion, provided the resulting calculus is endowed with either a purely strict or a purely nonstrict semantics. But modern functional languages like Clean and Haskell, while using nonstrict evaluation by default, also provide means to enforce strict evaluation of subcomputations at will. The resulting selective strictness gives the advanced programmer explicit control over evaluation order, but is not without semantic consequences: it breaks standard parametricity results. This paper develops an operational semantics for a core calculus supporting all the language features emphasized above. Its main achievement is the characterization of observational approximation with respect to this operational semantics via a carefully constructed logical relation. This establishes the formal basis for new parametricity results, as illustrated by several example applications, including the first complete correctness proof for short cut fusion in the presence of selective strictness. The focus on observational approximation, rather than equivalence, allows a finer-grained analysis of computational behavior in the presence of selective strictness than would be possible with observational equivalence alone.

Additional Information

Publication
Janis Voigtlaender and Patricia Johann. (2007) "Selective Strictness and Parametricity in Structural Operational Semantics, Inequationally". Theoretical Computer Science, vol. 388, no. 1 - 3 (2007), pp. 290 - 318. ISSN: 0304-3975 [doi:10.1016/j.tcs.2007.09.014] Version or Record Available From www.sciencedirect.com
Language: English
Date: 2007
Keywords
clean, haskell, extensionality principles, fixpoint recursion, functional programming languages, identity extension

Email this document to