Selective strictness and parametricity in structural operational semantics, inequationally Export

@article{voijoh07, abstract = {Parametric polymorphism constrains the behavior of pure functional programs 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 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.}, author = {Voigtl\"{a}nder, Janis and Johann, Patricia}, citeulike-article-id = {2090449}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.tcs.2007.09.014}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6V1G-4PPW77G-1/2/c5480418b8e83af13cb37d3576861b96}, citeulike-linkout-2 = {http://wwwtcs.inf.tu-dresden.de/~voigt/TCS.pdf}, doi = {10.1016/j.tcs.2007.09.014}, journal = {Theoretical Computer Science}, keywords = {call-by-name, free-theorems, functional-programming, haskell, lambda-calculus, laziness, lazy-evaluation, logical-relations, operational-semantics, parametricity, pcf, polymorphism, program-transformation, rank-2, selective-strictness, seq, shortcut-deforestation, strict-evaluation, types}, number = {1-3}, pages = {290--318}, posted-at = {2007-12-11 15:51:34}, priority = {0}, publisher = {Elsevier}, title = {Selective strictness and parametricity in structural operational semantics, inequationally}, url = {http://dx.doi.org/10.1016/j.tcs.2007.09.014}, volume = {388}, year = {2007} }

TY - JOUR ID - voijoh07 L3 - citeulike-article-id:2090449 N2 - Parametric polymorphism constrains the behavior of pure functional programs 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 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. IS - 1-3 JF - Theoretical Computer Science EP - 318 TI - Selective strictness and parametricity in structural operational semantics, inequationally PB - Elsevier VL - 388 SP - 290 KW - call-by-name KW - free-theorems KW - functional-programming KW - haskell KW - lambda-calculus KW - laziness KW - lazy-evaluation KW - logical-relations KW - operational-semantics KW - parametricity KW - pcf KW - polymorphism KW - program-transformation KW - rank-2 KW - selective-strictness KW - seq KW - shortcut-deforestation KW - strict-evaluation KW - types AU - Voigtländer, Janis AU - Johann, Patricia PY - 2007/// UR - http://dx.doi.org/10.1016/j.tcs.2007.09.014 ER -