OPUS 4 Latest Documents RSS FeedLatest documents
http://publikationen.stub.uni-frankfurt.de/index/index/
Wed, 19 Apr 2006 18:07:13 +0200Wed, 19 Apr 2006 18:07:13 +0200Deciding subset relationship of co-inductively defined set constants
http://publikationen.stub.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ützworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/3046Wed, 19 Apr 2006 18:07:13 +0200Polynomial Equality Testing for Terms with Shared Substructures
http://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/3252
Sharing of substructures like subterms and subcontexts in terms is a common method for space-efficient representation of terms, which allows for example to represent exponentially large terms in polynomial space, or to represent terms with iterated substructures in a compact form. We present singleton tree grammars as a general formalism for the treatment of sharing in terms. Singleton tree grammars (STG) are recursion-free context-free tree grammars without alternatives for non-terminals and at most unary second-order nonterminals. STGs generalize Plandowski's singleton context free grammars to terms (trees). We show that the test, whether two different nonterminals in an STG generate the same term can be done in polynomial time, which implies that the equality test of terms with shared terms and contexts, where composition of contexts is permitted, can be done in polynomial time in the size of the representation. This will allow polynomial-time algorithms for terms exploiting sharing. We hope that this technique will lead to improved upper complexity bounds for variants of second order unification algorithms, in particular for variants of context unification and bounded second order unification.Manfred Schmidt-Schaußworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/3252Mon, 21 Nov 2005 09:13:09 +0100A complete proof of the safety of Nöcker's strictness analysis
http://publikationen.stub.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 Sabelworkingpaperhttp://publikationen.stub.uni-frankfurt.de/frontdoor/index/index/docId/4394Tue, 14 Jun 2005 12:27:46 +0200