OPUS 4 Latest Documents RSS FeedLatest documents
http://publikationen.ub.uni-frankfurt.de/index/index/
Thu, 15 Sep 2011 13:56:24 +0200Thu, 15 Sep 2011 13:56:24 +0200A termination proof of reduction in a simply typed calculus with constructors
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 Sabelworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/22711Thu, 15 Sep 2011 13:56:24 +0200Towards correctness of program transformations through unification and critical pair computation
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7940
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 is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, which results in so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting systems. We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study of an application we describe a finitary and decidable unification algorithm for the combination of the equational theory of left-commutativity modelling multi-sets, context variables and many-sorted unification. Sets of equations are restricted to be almost linear, i.e. every variable and context variable occurs at most once, where we allow one exception: variables of a sort without ground terms may occur several times. Every context variable must have an argument-sort in the free part of the signature. We also extend the unification algorithm by the treatment of binding-chains in let- and letrec-environments and by context-classes. This results in a unification algorithm that can be applied to all overlaps of normal-order reductions and transformations in an extended lambda calculus with letrec that we use as a case study.Conrad Rau; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7940Sat, 04 Sep 2010 13:04:42 +0200Simulation in the call-by-need lambda-calculus with letrec
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 Machkasovaworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7828Tue, 22 Jun 2010 17:47:16 +0200Reconstruction a logic for inductive proofs of properties of functional programs
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ßworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7826Tue, 22 Jun 2010 17:44:13 +0200