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.
Selective Strictness and Parametricity in Structural Operational Semantics, Inequationally
PDF (Portable Document Format)
303 KB
Created on 5/2/2016
Views: 1292
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