Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: functional programming languages

Sortuj według:

Ogranicz wyniki do:

The Impact of seq on Free Theorems-Based Program Transformations

Johann P., Voigtländer J.

Fundamenta Informaticae

2006

Vol. 69, nr 1,2

63-102

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. Unfortunately, standard parametricity results - including so-called free theorems - fail for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq. A folk theorem maintains that such results hold for a subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints and algebraic datatypes even when seq is present provided the relations which appear in their derivations are required to be bottom-reflecting and admissible. In this paper we show that this folklore is incorrect, but that parametricity results can be recovered in the presence of seq by restricting attention to left-closed, total, and admissible relations instead. The key novelty of our approach is the asymmetry introduced by left-closedness, which leads to ``inequational'' versions of standard parametricity results together with preconditions guaranteeing their validity even when seq is present. We use these results to derive criteria ensuring that both equational and inequational versions of short cut fusion and related program transformations based on free theorems hold in the presence of seq.

Infinite Unfolding and Transformations of Nondeterministic Programs

Lisper B.

Fundamenta Informaticae

2005

Vol. 66, nr 4

415--439

We prove some new results about the correctness of transformations of nondeterministic programs. The reported work formalises the intuitive idea that two recursive programs ought to be equivalent, also in a nondeterministic setting, if they can be symbolically unfolded, through deterministic reductions, to the same, possibly infinite, term. In order to do this we develop two related semantics, based on computations modeled by reduction sequences, and argue that they are operationally meaningful. We then specialise to the case of Combinatory Reduction Systems, which provides a suitable rewrite setting for higher order functional programs with nondeterministic constructs, e.g., stream or process primitives. In this setting we prove a theorem about equivalence of programs based on possibly infinite, deterministic unfoldings of programs converging to the same term. We then use the theorem to show a correctness criterion for unfold/fold-transformations of nondeterministic recursive programs. This criterion is similar to the well-known Tamaki-Sato correctness criterion for unfold/fold-transformations of logic programs.