Latest documents http://publikationen.ub.uni-frankfurt.de/index/index/ Mon, 29 Oct 2012 15:45:08 +0100 Mon, 29 Oct 2012 15:45:08 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/27007 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. Manfred Schmidt-Schauß; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/27007 Mon, 29 Oct 2012 15:45:08 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/27005 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. Manfred Schmidt-Schauß; David Sabel; Elena Machkasova workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/27005 Mon, 29 Oct 2012 15:35:55 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24252 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. David Sabel; Manfred Schmidt-Schauß workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24252 Tue, 07 Feb 2012 16:16:23 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24253 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. David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24253 Tue, 07 Feb 2012 16:14:01 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22712 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. David Sabel; Manfred Schmidt-Schauß workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22712 Thu, 15 Sep 2011 14:04:58 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22711 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. Manfred Schmidt-Schauß; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22711 Thu, 15 Sep 2011 13:56:24 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7828 This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models.We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen. Manfred Schmidt-Schauß; David Sabel; Elena Machkasova workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7828 Tue, 22 Jun 2010 17:47:16 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7827 This note shows that in non-deterministic extended lambda calculi with letrec, the tool of applicative (bi)simulation is in general not usable for contextual equivalence, by giving a counterexample adapted from data flow analysis. It also shown that there is a flaw in a lemma and a theorem concerning finite simulation in a conference paper by the first two authors. Manfred Schmidt-Schauß; Elena Machkasova; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7827 Tue, 22 Jun 2010 17:45:50 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7826 A logical framework consisting of a polymorphic call-by-value functional language and a first-order logic on the values is presented, which is a reconstruction of the logic of the verification system VeriFun. The reconstruction uses contextual semantics to define the logical value of equations. It equates undefinedness and non-termination, which is a standard semantical approach. The main results of this paper are: Meta-theorems about the globality of several classes of theorems in the logic, and proofs of global correctness of transformations and deduction rules. The deduction rules of VeriFun are globally correct if rules depending on termination are appropriately formulated. The reconstruction also gives hints on generalizations of the VeriFun framework: reasoning on nonterminating expressions and functions, mutual recursive functions and abstractions in the data values, and formulas with arbitrary quantifier prefix could be allowed. David Sabel; Manfred Schmidt-Schauß workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7826 Tue, 22 Jun 2010 17:44:13 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6667 This paper describes a method to treat contextual equivalence in polymorphically typed lambda-calculi, and also how to transfer equivalences from the untyped versions of lambda-calculi to their typed variant, where our specific calculus has letrec, recursive types and is nondeterministic. An addition of a type label to every subexpression is all that is needed, together with some natural constraints for the consistency of the type labels and well-scopedness of expressions. One result is that an elementary but typed notion of program transformation is obtained and that untyped contextual equivalences also hold in the typed calculus as long as the expressions are well-typed. In order to have a nice interaction between reduction and typing, some reduction rules have to be accompanied with a type modification by generalizing or instantiating types. Manfred Schmidt-Schauß; David Sabel; Frederik Harwath workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6667 Tue, 07 Jul 2009 13:30:55 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6666 Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs. Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schauß workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6666 Tue, 07 Jul 2009 13:22:26 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6176 We show on an abstract level that contextual equivalence in non-deterministic program calculi defined by may- and must-convergence is maximal in the following sense. Using also all the test predicates generated by the Boolean, forall- and existential closure of may- and must-convergence does not change the contextual equivalence. The situation is different if may- and total must-convergence is used, where an expression totally must-converges if all reductions are finite and terminate with a value: There is an infinite sequence of test-predicates generated by the Boolean, forall- and existential closure of may- and total must-convergence, which also leads to an infinite sequence of different contextual equalities. Manfred Schmidt-Schauß; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6176 Thu, 29 Jan 2009 09:16:03 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6036 Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence. Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schauß workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6036 Thu, 20 Nov 2008 16:20:55 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/192 We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and must-convergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extension. Manfred Schmidt-Schauß; Joachim Niehren; Jan Schwinghammer; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/192 Fri, 07 Mar 2008 16:07:51 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/1569 We model sequential synchronous circuits on the logical level by signal-processing programs in an extended lambda calculus Lpor with letrec, constructors, case and parallel or (por) employing contextual equivalence. The model describes gates as (parallel) boolean operators, memory using a delay, which in turn is modeled as a shift of the list of signals, and permits also constructive cycles due to the parallel or. It opens the possibility of a large set of program transformations that correctly transform the expressions and thus the represented circuits and provides basic tools for equivalence testing and optimizing circuits. A further application is the correct manipulation by transformations of software components combined with circuits. The main part of our work are proof methods for correct transformations of expressions in the lambda calculus Lpor, and to propose the appropriate program transformations. Manfred Schmidt-Schauß; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/1569 Wed, 28 Feb 2007 16:45:20 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/1573 This paper proves several generic variants of context lemmas and thus contributes to improving the tools to develop observational semantics that is based on a reduction semantics for a language. The context lemmas are provided for may- as well as two variants of mustconvergence and a wide class of extended lambda calculi, which satisfy certain abstract conditions. The calculi must have a form of node sharing, e.g. plain beta reduction is not permitted. There are two variants, weakly sharing calculi, where the beta-reduction is only permitted for arguments that are variables, and strongly sharing calculi, which roughly correspond to call-by-need calculi, where beta-reduction is completely replaced by a sharing variant. The calculi must obey three abstract assumptions, which are in general easily recognizable given the syntax and the reduction rules. The generic context lemmas have as instances several context lemmas already proved in the literature for specific lambda calculi with sharing. The scope of the generic context lemmas comprises not only call-by-need calculi, but also call-by-value calculi with a form of built-in sharing. Investigations in other, new variants of extended lambda-calculi with sharing, where the language or the reduction rules and/or strategy varies, will be simplified by our result, since specific context lemmas are immediately derivable from the generic context lemma, provided our abstract conditions are met. Manfred Schmidt-Schauß; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/1573 Wed, 28 Feb 2007 16:37:52 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2181 Reasoning about the correctness of program transformations requires a notion of program equivalence. We present an observational semantics for the concurrent lambda calculus with futures Lambda(fut), which formalizes the operational semantics of the programming language Alice ML. We show that natural program optimizations, as well as partial evaluation with respect to deterministic rules, are correct for Lambda(fut). This relies on a number of fundamental properties that we establish for our observational semantics. Joachim Niehren; David Sabel; Manfred Schmidt-Schauß; Jan Schwinghammer workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2181 Mon, 30 Oct 2006 08:54:30 +0100 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2829 We present a higher-order call-by-need lambda calculus enriched with constructors, case-expressions, recursive letrec-expressions, a seq-operator for sequential evaluation and a non-deterministic operator amb, which is locally bottom-avoiding. We use a small-step operational semantics in form of a normal order reduction. As equational theory we use contextual equivalence, i.e. terms are equal if plugged into an arbitrary program context their termination behaviour is the same. We use a combination of may- as well as must-convergence, which is appropriate for non-deterministic computations. We evolve different proof tools for proving correctness of program transformations. We provide a context lemma for may- as well as must- convergence which restricts the number of contexts that need to be examined for proving contextual equivalence. In combination with so-called complete sets of commuting and forking diagrams we show that all the deterministic reduction rules and also some additional transformations keep contextual equivalence. In contrast to other approaches our syntax as well as semantics does not make use of a heap for sharing expressions. Instead we represent these expressions explicitely via letrec-bindings. David Sabel; Manfred Schmidt-Schauß workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2829 Wed, 19 Apr 2006 18:32:28 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/3046 Static analysis of different non-strict functional programming languages makes use of set constants like Top, Inf, and Bot denoting all expressions, all lists without a last Nil as tail, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics. This paper proves decidability, in particular EXPTIMEcompleteness, of subset relationship of co-inductively defined sets by using algorithms and results from tree automata. This shows decidability of the test for set inclusion, which is required by certain strictness analysis algorithms in lazy functional programming languages. Manfred Schmidt-Schauß; David Sabel; Marko Schütz workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/3046 Wed, 19 Apr 2006 18:07:13 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4394 This paper proves correctness of Nöcker's method of strictness analysis, implemented in the Clean compiler, which is an effective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work of Clark, Hankin and Hunt did on the correctness of the abstract reduction rules. Our method fully considers the cycle detection rules, which are the main strength of Nöcker's strictness analysis. Our algorithm SAL is a reformulation of Nöcker's strictness analysis algorithm in a higher-order call-by-need lambda-calculus with case, constructors, letrec, and seq, extended by set constants like Top or Inf, denoting sets of expressions. It is also possible to define new set constants by recursive equations with a greatest fixpoint semantics. The operational semantics is a small-step semantics. Equality of expressions is defined by a contextual semantics that observes termination of expressions. Basically, SAL is a non-termination checker. The proof of its correctness and hence of Nöcker's strictness analysis is based mainly on an exact analysis of the lengths of normal order reduction sequences. The main measure being the number of 'essential' reductions in a normal order reduction sequence. Our tools and results provide new insights into call-by-need lambda-calculi, the role of sharing in functional programming languages, and into strictness analysis in general. The correctness result provides a foundation for Nöcker's strictness analysis in Clean, and also for its use in Haskell. Manfred Schmidt-Schauß; Marko Schütz; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4394 Tue, 14 Jun 2005 12:27:46 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4594 This paper proves correctness of Nocker s method of strictness analysis, implemented for Clean, which is an e ective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work of Clark, Hankin and Hunt, which addresses correctness of the abstract reduction rules. Our method also addresses the cycle detection rules, which are the main strength of Nocker s strictness analysis. We reformulate Nocker s strictness analysis algorithm in a higherorder lambda-calculus with case, constructors, letrec, and a nondeterministic choice operator used as a union operator. Furthermore, the calculus is expressive enough to represent abstract constants like Top or Inf. The operational semantics is a small-step semantics and equality of expressions is defined by a contextual semantics that observes termination of expressions. The correctness of several reductions is proved using a context lemma and complete sets of forking and commuting diagrams. The proof is based mainly on an exact analysis of the lengths of normal order reductions. However, there remains a small gap: Currently, the proof for correctness of strictness analysis requires the conjecture that our behavioral preorder is contained in the contextual preorder. The proof is valid without referring to the conjecture, if no abstract constants are used in the analysis. Manfred Schmidt-Schauß; Marko Schütz; David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4594 Thu, 12 May 2005 16:51:58 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4591 In this paper we demonstrate how to relate the semantics given by the nondeterministic call-by-need calculus FUNDIO [SS03] to Haskell. After introducing new correct program transformations for FUNDIO, we translate the core language used in the Glasgow Haskell Compiler into the FUNDIO language, where the IO construct of FUNDIO corresponds to direct-call IO-actions in Haskell. We sketch the investigations of [Sab03b] where a lot of program transformations performed by the compiler have been shown to be correct w.r.t. the FUNDIO semantics. This enabled us to achieve a FUNDIO-compatible Haskell-compiler, by turning o not yet investigated transformations and the small set of incompatible transformations. With this compiler, Haskell programs which use the extension unsafePerformIO in arbitrary contexts, can be compiled in a "safe" manner. David Sabel workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4591 Thu, 12 May 2005 16:49:48 +0200