71 search hits
-
Correctness of an STM Haskell implementation
(2012)
-
Manfred Schmidt-Schauß
David Sabel
- A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of con
icting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence.
This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.
-
Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq
(2012)
-
Manfred Schmidt-Schauß
David Sabel
Elena Machkasova
- This paper shows equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seqoperator. LR models an untyped version of the core language of Haskell. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations.
The proof is by a fully abstract and surjective transfer of the contextual
approximation into a call-by-name calculus, which is an extension
of Abramsky's lazy lambda calculus. In the latter calculus equivalence
of similarity and contextual approximation can be shown by Howe's
method. Using an equivalent but inductive definition of behavioral preorder
we then transfer similarity back to the calculus LR.
The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite tress, which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, and also with a call-by-need letrec calculus with a less complex definition of reduction than LR.
-
On conservativity of concurrent Haskell
(2011)
-
David Sabel
Manfred Schmidt-Schauß
- The calculus CHF models Concurrent Haskell extended by
concurrent, implicit futures. It is a process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional
lambda-calculus which comprises data constructors, case-expressions,
letrec-expressions, and Haskell’s seq. Futures can be implemented in Concurrent
Haskell using the primitive unsafeInterleaveIO, which is available in most implementations of Haskell. Our main result is conservativity
of CHF, that is, all equivalences of pure functional expressions are
also valid in CHF. This implies that compiler optimizations and transformations
from pure Haskell remain valid in Concurrent Haskell even if
it is extended by futures. We also show that this is no longer valid if Concurrent
Haskell is extended by the arbitrary use of unsafeInterleaveIO.
-
An abstract machine for concurrent Haskell with futures
(2012)
-
David Sabel
- We show how Sestoft’s abstract machine for lazy evaluation
of purely functional programs can be extended to evaluate expressions of
the calculus CHF – a process calculus that models Concurrent Haskell
extended by imperative and implicit futures. The abstract machine is
modularly constructed by first adding monadic IO-actions to the machine
and then in a second step we add concurrency. Our main result is that
the abstract machine coincides with the original operational semantics
of CHF, w.r.t. may- and should-convergence.
-
Pattern matching of compressed terms and contexts and polynomial rewriting
(2011)
-
Manfred Schmidt-Schauß
- A generalization of the compressed string pattern match that applies to terms with variables is investigated: Given terms s and t compressed by singleton tree grammars, the task is to find an instance of s that occurs as a subterm in t. We show that this problem is in NP and that the task can be performed in time O(ncjVar(s)j), including the construction of the compressed substitution, and a representation of all occurrences. We show that the special case where s is uncompressed can be performed in polynomial time. As a nice application we show that for an equational deduction of t to t0 by an equality axiom l = r (a rewrite) a single step can be performed in polynomial time in the size of compression of t and l; r if the number of variables is fixed in l. We also show that n rewriting steps can be performed in polynomial time, if the equational axioms are compressed and assumed to be constant for the rewriting sequence. Another potential application are querying mechanisms on compressed XML-data bases.
-
Computing overlappings by unification in the deterministic lambda calculus LR with letrec, case, constructors, seq and variable chains
(2011)
-
Conrad Rau
Manfred Schmidt-Schauß
- Correctness of program transformations in extended lambda calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach to proving correctness is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules.The method is similar to the computation of critical pairs for the completion of term rewriting systems. We describe an effective unification algorithm to determine all overlaps of transformations with reduction rules for the lambda calculus LR which comprises a recursive let-expressions, constructor applications, case expressions and a seq construct for strict evaluation. The unification algorithm employs many-sorted terms, the equational theory of left-commutativity modeling multi-sets, context variables of different kinds and a mechanism for compactly representing binding chains in recursive let-expressions. As a result the algorithm computes a finite set of overlappings for the reduction rules of the calculus LR that serve as a starting point to the automatization of the analysis of program transformations.
-
Fast equality test for straight-line compressed strings
(2011)
-
Manfred Schmidt-Schauß
Georg Schnitger
- The paper describes a simple and fast randomized test for equality of grammar-compressed strings. The thorough running time analysis is done by applying a logarithmic cost measure. Keywords: randomized algorithms, straight line programs, grammar-based compression
-
A contextual semantics for concurrent Haskell with futures
(2011)
-
David Sabel
Manfred Schmidt-Schauß
- In this paper we analyze the semantics of a higher-order functional language with concurrent threads, monadic IO and synchronizing variables as in Concurrent Haskell. To assure declarativeness of concurrent programming we extend the language by implicit, monadic, and concurrent futures. As semantic model we introduce and analyze the process calculus CHF, which represents a typed core language of Concurrent Haskell extended by concurrent futures. Evaluation in CHF is defined by a small-step reduction relation. Using contextual equivalence based on may- and should-convergence as program equivalence, we show that various transformations preserve program equivalence. We establish a context lemma easing those correctness proofs. An important result is that call-by-need and call-by-name evaluation are equivalent in CHF, since they induce the same program equivalence. Finally we show that the monad laws hold in CHF under mild restrictions on Haskell’s seq-operator, which for instance justifies the use of the do-notation.
-
A termination proof of reduction in a simply typed calculus with constructors
(2010)
-
Manfred Schmidt-Schauß
David Sabel
- The well-known proof of termination of reduction in simply typed calculi is adapted to a monomorphically typed lambda-calculus with case and constructors and recursive data types. The proof differs at several places from the standard proof. Perhaps it is useful and can be extended also to more complex calculi.
-
Neuronal networks for sepsis prediction - the MEDAN project
(2004)
-
Rüdiger W. Brause
Ernst Hanisch
Jürgen Paetz
Björn Arlt
- Since the description of sepsis by Schottmüller in 1914, the amount on knowledge available on sepsis and its underlying pathophysiology has substantially increased. Epidemiologic examinations of abdominal septic shock patients show the potential for high risk posed by and the extensive therapy situation in the intensive care unit (ICU) (5). Unfortunately, until now it has not been possible to significantly reduce the mortality rate of septic shock, which is as high as 50-60% worldwide, although PROWESS' results (1) are encouraging. This paper summarizes the main results of the MEDAN project and their medical impacts. Several aspects are already published, see the references. The heterogeneity of patient groups and the variations in therapy strategies is seen as one of the main problems for sepsis trials. In the MEDAN multi-center study of 71 intensive care units in Germany, a group of 382 patients made up exclusively of abdominal septic shock patients who met the consensus criteria for septic shock (3) was analysed. For use within scores or stand-alone experiments variables are often studied as isolated variables, not as a multidimensional whole, e.g. a recent study takes a look at the role thrombocytes play (15). To avoid this limitation, our study compares several established scores (SOFA, APACHE II, SAPS II, MODS) by a multi-dimensional neuronal network analysis. For outcome prediction the data of 382 patients was analysed by using most of the commonly documented vital parameters and doses of medicine (metric variables). Data was collected in German hospitals from 1998 to 2001. The 382 handwritten patient records were transferred to an electronic database giving the amount of 2.5 million data entries. The metric data contained in the database is composed of daily measurements and doses of medicine. We used range and plausibility checks to allow no faulty data in the electronic database. 187 of the 382 patients are deceased (49 %).
