Latest documents http://publikationen.stub.uni-frankfurt.de/index/index/ Mon, 22 Oct 2007 12:53:00 +0200 Mon, 22 Oct 2007 12:53:00 +0200 http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/510 The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in a an extended lambda-calculus with case, constructors, seq, let, and choice, with a simple set of reduction rules. Unfortunately, a direct proof appears to be impossible. The correctness proof is by defining another calculus comprising the complex variants of copy, case-reduction and seq-reductions that use variablebinding chains. This complex calculus has well-behaved diagrams and allows a proof that of correctness of transformations, and also that the simple calculus defines an equivalent contextual order. Manfred Schmidt-Schauß; Matthias Mann workingpaper http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/510 Mon, 22 Oct 2007 12:53:00 +0200 http://publikationen.stub.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.stub.uni-frankfurt.de/frontdoor/index/index/docId/1569 Wed, 28 Feb 2007 16:45:20 +0100 http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/1568 This paper extends the internal frank report 28 as follows: It is shown that for a call-by-need lambda calculus LRCCP-Lambda extending the calculus LRCC-Lambda by por, i.e in a lambda-calculus with letrec, case, constructors, seq and por, copying can be done without restrictions, and also that call-by-need and call-by-name strategies are equivalent w.r.t. contextual equivalence. Manfred Schmidt-Schauß workingpaper http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/1568 Wed, 28 Feb 2007 16:43:27 +0100 http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/1567 Call-by-need lambda calculi with letrec provide a rewritingbased operational semantics for (lazy) call-by-name functional languages. These calculi model the sharing behavior during evaluation more closely than let-based calculi that use a fixpoint combinator. In a previous paper we showed that the copy-transformation is correct for the small calculus LR-Lambda. In this paper we demonstrate that the proof method based on a calculus on infinite trees for showing correctness of instantiation operations can be extended to the calculus LRCC-Lambda with case and constructors, and show that copying at compile-time can be done without restrictions. We also show that the call-by-need and call-by-name strategies are equivalent w.r.t. contextual equivalence. A consequence is correctness of all the transformations like instantiation, inlining, specialization and common subexpression elimination in LRCC-Lambda. We are confident that the method scales up for proving correctness of copy-related transformations in non-deterministic lambda calculi if restricted to "deterministic" subterms. Manfred Schmidt-Schauß workingpaper http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/1567 Wed, 28 Feb 2007 16:41:03 +0100 http://publikationen.stub.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.stub.uni-frankfurt.de/frontdoor/index/index/docId/1573 Wed, 28 Feb 2007 16:37:52 +0100