@string{brics = "{BRICS}"} @string{daimi = "Department of Computer Science, University of Aarhus"} @string{iesd = "Department of Computer Science, Institute of Electronic Systems, Aalborg University"} @string{rs = "Research Series"} @string{ns = "Notes Series"} @string{ls = "Lecture Series"} @string{ds = "Dissertation Series"} @techreport{BRICS-RS-02-53, author = "Danvy, Olivier", title = "A Lambda-Revelation of the {SECD} Machine", institution = brics, year = 2003, type = rs, number = "RS-02-53", address = daimi, month = dec, note = "15~pp. Superseeded by the BRICS report \htmladdnormallink{RS-03-33}{http://www.brics.dk/RS/03/33/}", abstract = "We present a simple inter-derivation between lambda-interpreters, i.e., evaluation functions for lambda-terms, and abstract reduction machines for the lambda-calculus, i.e., transition functions. The two key derivation steps are the CPS transformation and Reynolds's defunctionalization. By transforming the interpreter into continuation-passing style (CPS), its flow of control is made manifest as a continuation. By defunctionalizing this continuation, the flow of control is materialized as a first-order data structure.\bibpar The derivation applies not merely to connect independently known lambda-interpreters and abstract machines, it also applies to construct the abstract machine corresponding to a lambda-interpreter and to construct the lambda-interpreter corresponding to an abstract machine. In this article, we treat in detail the canonical example of Landin's SECD machine and we reveal its denotational content: the meaning of an expression is a partial endo-function from a stack of intermediate results and an environment to a new stack of intermediate results and an environment. The corresponding lambda-interpreter is unconventional because (1) it uses a control delimiter to evaluate the body of each lambda-abstraction and (2) it assumes the environment to be managed in a callee-save fashion instead of in the usual caller-save fashion", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-52, author = "Danvy, Olivier", title = "A New One-Pass Transformation into Monadic Normal Form", institution = brics, year = 2002, type = rs, number = "RS-02-52", address = daimi, month = dec, note = "16~pp. Appears in " # lncs2622 # ", pages 77--89", abstract = "We present a translation from the call-by-value lambda-calculus to monadic normal forms that includes short-cut boolean evaluation. The translation is higher-order, operates in one pass, duplicates no code, generates no chains of thunks, and is properly tail recursive. It makes a crucial use of symbolic computation at translation time", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-51, author = "Brodal, Gerth St{\o}lting and Fagerberg, Rolf and {\"O}stlin, Anna and Pedersen, Christian N. S. and Rao, S. Srinivasa", title = "Computing Refined Buneman Trees in Cubic Time", institution = brics, year = 2002, type = rs, number = "RS-02-51", address = daimi, month = dec, note = "14~pp. Appears in " # lncs2812 # ", pages 259--270", abstract = "Reconstructing the evolutionary tree for a set of $n$~species based on pairwise distances between the species is a fundamental problem in bioinformatics. Neighbor joining is a popular distance based tree reconstruction method. It always proposes fully resolved binary trees despite missing evidence in the underlying distance data. Distance based methods based on the theory of Buneman trees and refined Buneman trees avoid this problem by only proposing evolutionary trees whose edges satisfy a number of constraints. These trees might not be fully resolved but there is strong combinatorial evidence for each proposed edge. The currently best algorithm for computing the refined Buneman tree from a given distance measure has a running time of $O(n^5)$ and a space consumption of $O(n^4)$. In this paper, we present an algorithm with running time~$O(n^3)$ and space consumption~$O(n^2)$", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-50, author = "Hansen, Kristoffer Arnsfelt and Miltersen, Peter Bro and Vinay, V.", title = "Circuits on Cylinders", institution = brics, year = 2002, type = rs, number = "RS-02-50", address = daimi, month = dec, note = "16~pp", abstract = "We consider the computational power of constant width polynomial size cylindrical circuits and nondeterministic branching programs. We show that every function computed by a ${{\bf\Pi}_2 \circ{\rm\bf MOD} \circ{\rm \bf AC}^0}$ circuit can also be computed by a constant width polynomial size cylindrical nondeterministic branching program (or cylindrical circuit) and that every function computed by a constant width polynomial size cylindrical circuit belongs to ${\mbox{\rm\bf ACC}}^0$", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-49, author = "Nygaard, Mikkel and Winskel, Glynn", title = "{HOPLA}---{A} Higher-Order Process Language", institution = brics, year = 2002, type = rs, number = "RS-02-49", address = daimi, month = dec, note = "18~pp. Appears in " # lncs2421 # ", pages 434--448", abstract = "A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a ``prefixed sum'', in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-48, author = "Nygaard, Mikkel and Winskel, Glynn", title = "Linearity in Process Languages", institution = brics, year = 2002, type = rs, number = "RS-02-48", address = daimi, month = dec, note = "27~pp. Appears in " # lics17 # ", pages 433--446", abstract = "The meaning and mathematical consequences of linearity (managing without a presumed ability to copy) are studied for a path-based model of processes which is also a model of affine-linear logic. This connection yields an af\-fine-linear language for processes, automatically respecting open-map bisimulation, in which a range of process operations can be expressed. An operational semantics is provided for the tensor fragment of the language. Different ways to make assemblies of processes lead to different choices of exponential, some of which respect bisimulation", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-47, author = "{\'E}sik, Zolt{\'a}n", title = "Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators", institution = brics, year = 2002, type = rs, number = "RS-02-47", address = iesd, month = dec, note = "16~pp. Appears in " # lncs2450 # ", pages 43--48", abstract = "We associate a modal operator with each language belonging to a given class of regular languages and use the (reverse) wreath product of monoids with distinguished generators to characterize the expressive power of the resulting logic", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-46, author = "{\'E}sik, Zolt{\'a}n and Lei{\ss}, Hans", title = "{G}reibach Normal Form in Algebraically Complete Semirings", institution = brics, year = 2002, type = rs, number = "RS-02-46", address = iesd, month = dec, note = "43~pp. An extended abstract appears in " # lncs2471 # ", pages 135--150", keywords = "Greibach normal form, context-free languages, pre-fixed-point induction, equational theory, Conway semiring, Kleene algebra, algebraically complete semiring", abstract = "We give inequational and equational axioms for semirings with a fixed-point operator and formally develop a fragment of the theory of context-free languages. In particular, we show that Greibach's normal form theorem depends only on a few equational properties of least pre-fixed-points in semirings, and elimination of chain- and deletion rules depend on their inequational properties (and the idempotency of addition). It follows that these normal form theorems also hold in non-continuous semirings having enough fixed-points", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-45, author = "Byskov, Jesper Makholm", title = "Chromatic Number in Time $O(2.4023^n)$ Using Maximal Independent Sets", institution = brics, year = 2002, type = rs, number = "RS-02-45", address = daimi, month = dec, note = "6~pp", abstract = "In this paper we improve an algorithm by Eppstein (2001) for finding the chromatic number of a graph. We modify the algorithm slightly, and by using a bound on the number of maximal independent sets of size~$k$ from our recent paper (2003), we prove that the running time is $O(2.4023^n)$. Eppstein's algorithm runs in time $O(2.4150^n)$. The space usage for both algorithms is $O(2^n)$", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-44, author = "{\'E}sik, Zolt{\'a}n and N{\'e}meth, Zolt{\'a}n L.", title = "Higher Dimensional Automata", institution = brics, year = 2002, type = rs, number = "RS-02-24", address = iesd, month = nov, note = "32~pp. A preliminary version appears under the title {\em Automata on Series-Parallel Biposets\/} in " # lncs2295 # ", pages 217--227. This report supersedes the earlier BRICS report RS-01-24", abstract = "We provide the basics of a 2-dimensional theory of automata on series-parallel biposets. We define recognizable, regular and rational sets of series-parallel biposets and study their relationship. Moreover, we relate these classes to languages of series-parallel biposets definable in monadic second-order logic", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-43, author = "Christiansen, Mikkel and Fleury, Emmanuel", title = "Using {IDD}s for Packet Filtering", institution = brics, year = 2002, type = rs, number = "RS-02-43", address = iesd, month = oct, note = "25~pp", abstract = "Firewalls are one of the key technologies used to control the traffic going in and out of a network. A central feature of the firewall is the {\em packet filter}. In this paper, we propose a complete framework for packet classification. Through two applications we demonstrate that both performance and security can be improved.\bibpar We show that a traditional ordered rule set can always be expressed as a first-order logic formula on integer variables. Moreover, we emphasize that, with such specification, the packet filtering problem is known to be constant time ($O(1)$). We propose to represent the first-order logic formula as {\em Interval Decision Diagrams}. This structure has several advantages. First, the algorithm for removing redundancy and unnecessary tests is very simple. Secondly, it allows us to handle integer variables which makes it efficient on a generic CPUs. And, finally, we introduce an extension of IDDs called {\em Multi-Terminal Interval Decision Diagrams} in order to deal with any number of policies.\bibpar In matter of efficiency, we evaluate the performance our framework through a prototype toolkit composed by a {\em compiler} and a {\em packet filter}. The results of the experiments shows that this method is efficient in terms of CPU usage and has a low storage requirements.\bibpar Finally, we outline a tool, called {\em Network Access Verifier}. This tool demonstrates how the IDD representation can be used for verifying access properties of a network. In total, potentially improving the security of a network", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-42, author = "Aceto, Luca and Hansen, Jens Alsted and Ing{\'o}lfsd{\'o}ttir, Anna and Johnsen, Jacob and Knudsen, John", title = "Checking Consistency of Pedigree Information is {NP}-complete (Preliminary Report)", institution = brics, year = 2002, type = rs, number = "RS-02-42", address = iesd, month = oct, note = "16~pp. Superseeded by RS-03-17", abstract = "{Consistency checking} is a fundamental computational problem in genetics. Given a pedigree and information on the genotypes of some of the individuals in it, the aim of consistency checking is to determine whether these data are consistent with the classic Mendelian laws of inheritance. This problem arose originally from the geneticists' need to filter their input data from erroneous information, and is well motivated from both a biological and a sociological viewpoint. This paper shows that consistency checking is NP-complete, even in the presence of three alleles. Several other results on the computational complexity of problems from genetics that are related to consistency checking are also offered. In particular, it is shown that checking the consistency of pedigrees over two alleles can be done in polynomial time", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-41, author = "Bloom, Stephen L. and {\'E}sik, Zolt{\'a}n", title = "Axiomatizing Omega and Omega-op Powers of Words", institution = brics, year = 2002, type = rs, number = "RS-02-41", address = daimi, month = oct, note = "16~pp", abstract = "In 1978, Courcelle asked for a complete set of axioms and rules for the equational theory of (discrete regular) words equipped with the operations of product, omega power and omega-op power. In this paper we find a simple set of equations and prove they are complete. Moreover, we show that the equational theory is decidable in polynomial time", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-40, author = "Aceto, Luca and Fokkink, Willem Jan and Ing{\'o}lfsd{\'o}ttir, Anna", title = "A Note on an Expressiveness Hierarchy for Multi-exit Iteration", institution = brics, year = 2002, type = rs, number = "RS-02-40", address = iesd, month = sep, note = "8~pp. Appears in {\em Information Processing Letters}, Elsevier, 87(1):17--23, 2003.", abstract = "Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of recursion equations of the form \begin{eqnarray*} X_1 & \stackrel{\mbox{\tiny def}}{=} & P_1 X_2 + Q_1 \\ & \vdots& \\ X_n & \stackrel{\mbox{\tiny def}}{=} & P_n X_1 + Q_n \end{eqnarray*} where $n$ is a positive integer, and the $P_i$ and the $Q_i$ are process terms. The addition of multi-exit iteration to Basic Process Algebra (BPA) yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star. This note offers an expressiveness hierarchy, modulo bisimulation equivalence, for the family of multi-exit iteration operators proposed by Bergstra, Bethke and Ponse", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-39, author = "Bloom, Stephen L. and {\'E}sik, Zolt{\'a}n", title = "Some Remarks on Regular Words", institution = brics, year = 2002, type = rs, number = "RS-02-39", address = iesd, month = sep, note = "27~pp", abstract = "In the late 1970's, Courcelle introduced the class of ``arrangements'', or labeled linear ordered sets, here called just ``words''. He singled out those words which are solutions of finite systems of fixed point equations involving finite words, which we call the ``regular words''. The current paper contains some new descriptions of this class of words related to properties of regular sets of binary strings, and uses finite automata to decide various natural questions concerning these words. In particular we show that a countable word is regular iff it can be defined on an ordinary regular language (which can be chosen to be a prefix code) ordered by the lexicographical order such that the labeling function satisfies a regularity condition. Those regular words whose underlying order is ``discrete'' or ``scattered'' are characterized in several ways", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-38, author = "Varacca, Daniele", title = "The Powerdomain of Indexed Valuations", institution = brics, year = 2002, type = rs, number = "RS-02-38", address = daimi, month = sep, note = "54~pp. Short version appears in " # lics17 # ", pages~299--308", abstract = "This paper is about combining nondeterminism and probabilities. We study this phenomenon from a domain theoretic point of view. In domain theory, nondeterminism is modeled using the notion of powerdomain, while probability is modeled using the powerdomain of valuations. Those two functors do not combine well, as they are. We define the notion of powerdomain of indexed valuations, which can be combined nicely with the usual nondeterministic powerdomain. We show an equational characterization of our construction. Finally we discuss the computational meaning of indexed valuations, and we show how they can be used, by giving a denotational semantics of a simple imperative language", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-37, author = "Ager, Mads Sig and Danvy, Olivier and Goldberg, Mayer", title = "A Symmetric Approach to Compilation and Decompilation", institution = brics, year = 2002, type = rs, number = "RS-02-37", address = daimi, month = aug, note = "45~pp. Appears in " # lncs2566 # ", pages 296--331", abstract = "Just as specializing a source interpreter can achieve compilation from a source language to a target language, we observe that specializing a target interpreter can achieve compilation from the target language to the source language. In both cases, the key issue is the choice of whether to perform an evaluation or to emit code that represents this evaluation.\bibpar We substantiate this observation by specializing two source interpreters and two target interpreters. We first consider a source language of arithmetic expressions and a target language for a stack machine, and then the lambda-calculus and the SECD-machine language. In each case, we prove that the target-to-source compiler is a left inverse of the source-to-target compiler, i.e., it is a decompiler.\bibpar In the context of partial evaluation, compilation by source-interpreter specialization is classically referred to as a Futamura projection. By symmetry, it seems logical to refer to decompilation by target-interpreter specialization as a Futamura embedding", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-36, author = "Damian, Daniel and Danvy, Olivier", title = "{CPS} Transformation of Flow Information, Part {II}: Administrative Reductions", institution = brics, year = 2002, type = rs, number = "RS-02-36", address = daimi, month = aug, note = "9~pp. To appear in the {\em Journal of Functional Programming}. This report supersedes the earlier BRICS report RS-01-40", abstract = "We characterize the impact of a linear $\beta $-reduction on the result of a control-flow analysis. (By ``a linear $\beta$-reduction'' we mean the $\beta$-reduction of a linear $\lambda $-abstraction, i.e., of a $\lambda$-abstraction whose parameter occurs exactly once in its body.)\bibpar As a corollary, we consider the administrative reductions of a Plotkin-style transformation into continuation-passing style (CPS), and how they affect the result of a constraint-based control-flow analysis and, in particular, the least element in the space of solutions. We show that administrative reductions preserve the least solution. Preservation of least solutions solves a problem that was left open in Palsberg and Wand's article ``CPS Transformation of Flow Information.''\bibpar Together, Palsberg and Wand's article and the present article show how to map in linear time the least solution of the flow constraints of a program into the least solution of the flow constraints of the CPS counterpart of this program, after administrative reductions. Furthermore, we show how to CPS transform control-flow information in one pass", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-35, author = "Bouyer, Patricia", title = "Timed Automata May Cause Some Troubles", institution = brics, year = 2002, type = rs, number = "RS-02-35", address = iesd, month = aug, note = "44~pp", abstract = "Timed automata are a widely studied model. Its decidability has been proved using the so-called region automaton construction. This construction provides a correct abstraction for the behaviours of timed automata, but it does not support a natural implementation and, in practice, algorithms based on the notion of zones are implemented using adapted data structures like DBMs. When we focus on forward analysis algorithms, the exact computation of all the successors of the initial configurations does not always terminate. Thus, some abstractions are often used to ensure termination, among which, a widening operator on zones.\bibpar In this paper, we study in details this widening operator and the forward analysis algorithm that uses it. This algorithm is most used and implemented in tools like Kronos and Uppaal. One of our main results is that it is hopeless to find a forward analysis algorithm, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in details this algorithm in the more general framework of updatable timed automata, a model which has been introduced as a natural syntactic extension of classical timed automata. We describe subclasses of this model for which a correct widening operator can be found", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-34, author = "Rhiger, Morten", title = "A Foundation for Embedded Languages", institution = brics, year = 2002, type = rs, number = "RS-02-34", address = daimi, month = aug, note = "29~pp. To appear in {\em TOPLAS, ACM Transactions on Programming Languages and Systems}", abstract = "Recent work on embedding object languages into Haskell use ``phantom types'' (i.e., parameterized types whose parameter does not occur on the right-hand side of the type definition) to ensure that the embedded object-language terms are simply typed. But is it a safe assumption that {\em only} simply-typed terms can be represented in Haskell using phantom types? And conversely, can {\em all} simply-typed terms be represented in Haskell under the restrictions imposed by phantom types? In this article we investigate the conditions under which these assumptions are true: We show that these questions can be answered affirmatively for an idealized Haskell-like language and discuss to which extent Haskell can be used as a meta-language", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-33, author = "Balat, Vincent and Danvy, Olivier", title = "Memoization in Type-Directed Partial Evaluation", institution = brics, year = 2002, type = rs, number = "RS-02-33", address = daimi, month = jul, note = "18~pp. Appears in " # lncs2487 # ", pages 78--92", abstract = "We use a code generator---type-directed partial evaluation---to verify conversions between isomorphic types, or more precisely to verify that a composite function is the identity function at some complicated type. A typed functional language such as ML provides a natural support to express the functions and type-directed partial evaluation provides a convenient setting to obtain the normal form of their composition. However, off-the-shelf type-directed partial evaluation turns out to yield gigantic normal forms.\bibpar We identify that this gigantism is due to redundancies, and that these redundancies originate in the handling of sums, which uses delimited continuations. We successfully eliminate these redundancies by extending type-directed partial evaluation with memoization capabilities. The result only works for pure functional programs, but it provides an unexpected use of code generation and it yields orders-of-magnitude improvements both in time and in space for type isomorphisms.", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-32, author = "Ager, Mads Sig and Danvy, Olivier and Rohde, Henning Korsholm", title = "On Obtaining {K}nuth, {M}orris, and {P}ratt's String Matcher by Partial Evaluation", institution = brics, year = 2002, type = rs, number = "RS-02-32", address = daimi, month = jul, note = "43~pp. Appears in " # acmasiapepm02 # ", pages 32--46", abstract = "We present the first formal proof that partial evaluation of a quadratic string matcher can yield the precise behaviour of Knuth, Morris, and Pratt's linear string matcher.\bibpar Obtaining a KMP-like string matcher is a canonical example of partial evaluation: starting from the naive, quadratic program checking whether a pattern occurs in a text, one ensures that backtracking can be performed at partial-evaluation time (a binding-time shift that yields a staged string matcher); specializing the resulting staged program yields residual programs that do not back up on the text, a la KMP. We are not aware, however, of any formal proof that partial evaluation of a staged string matcher precisely yields the KMP string matcher, or in fact any other specific string matcher.\bibpar In this article, we present a staged string matcher and we formally prove that it performs the same sequence of comparisons between pattern and text as the KMP string matcher. To this end, we operationally specify each of the programming languages in which the matchers are written, and we formalize each sequence of comparisons with a trace semantics. We also state the (mild) conditions under which specializing the staged string matcher with respect to a pattern string provably yields a specialized string matcher whose size is proportional to the length of this pattern string and whose time complexity is proportional to the length of the text string. Finally, we show how tabulating one of the functions in this staged string matcher gives rise to the `next' table of the original KMP algorithm.\bibpar The method scales for obtaining other linear string matchers, be they known or new", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-31, author = "Kohlenbach, Ulrich and Oliva, Paulo B.", title = "Proof Mining: A Systematic Way of Analysing Proofs in Mathematics", institution = brics, year = 2002, type = rs, number = "RS-02-31", address = daimi, month = jun, note = "47~pp. Appears in {\em Proceedings of the Steklov Institute of Mathematics}, 242:136--164, 2003", abstract = "We call {\it proof mining} the process of logically analyzing proofs in mathematics with the aim of obtaining new information. In this survey paper we discuss, by means of examples from mathematics, some of the main techniques used in proof mining. We show that those techniques not only apply to proofs based on classical logic, but also to proofs which involve non-effective principles such as the attainment of the infimum of $f\in C[0,1]$ and the convergence for bounded monotone sequences of reals. We also report on recent case studies in approximation theory and fixed point theory where new results were obtained", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-30, author = "Danvy, Olivier and Schultz, Ulrik P.", title = "Lambda-Lifting in Quadratic Time", institution = brics, year = 2002, type = rs, number = "RS-02-30", address = daimi, month = jun, note = "17~pp. Appears in " # lncs2441 # ", pages 134--151. Superseeded by the BRICS report \htmladdnormallink{RS-03-26}{http://www.brics.dk/RS/03/26/}", abstract = "Lambda-lifting is a program transformation used in compilers and in partial evaluators and that operates in cubic time. In this article, we show how to reduce this complexity to quadratic time.\bibpar Lambda-lifting transforms a block-structured program into a set of recursive equations, one for each local function in the source program. Each equation carries extra parameters to account for the free variables of the corresponding local function and of all its callees. It is the search for these extra parameters that yields the cubic factor in the traditional formulation of lambda-lifting, which is due to Johnsson. This search is carried out by a transitive closure.\bibpar Instead, we partition the call graph of the source program into strongly connected components, based on the simple observation that all functions in each component need the same extra parameters and thus a transitive closure is not needed. We therefore simplify the search for extra parameters by treating each strongly connected component instead of each function as a unit, thereby reducing the time complexity of lambda-lifting from O(n3logn) to O(n2logn), where n is the size of the program" } @techreport{BRICS-RS-02-29, author = "Pedersen, Christian N. S. and Scharling, Tejs", title = "Comparative Methods for Gene Structure Prediction in Homologous Sequences", institution = brics, year = 2002, type = rs, number = "RS-02-29", address = daimi, month = jun, note = "20~pp. Appears in " # lncs2452 # ", pages 220--234", abstract = "The increasing number of sequenced genomes motivates the use of evolutionary patterns to detect genes. We present a series of comparative methods for gene finding in homologous prokaryotic or eukaryotic sequences. Based on a model of legal genes and a similarity measure between genes, we find the pair of legal genes of maximum similarity. We develop methods based on genes models and alignment based similarity measures of increasing complexity, which take into account many details of real gene structures, e.g. the similarity of the proteins encoded by the exons. When using a similarity measure based on an exiting alignment, the methods run in linear time. When integrating the alignment and prediction process which allows for more fine grained similarity measures, the methods run in quadratic time. We evaluate the methods in a series of experiments on synthetic and real sequence data, which show that all methods are competitive but that taking the similarity of the encoded proteins into account really boost the performance", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-28, author = "Kohlenbach, Ulrich and Leu{\c{s}}tean, Lauren{\c{t}}iu", title = "Mann Iterates of Directionally Nonexpansive Mappings in Hyperbolic Spaces", institution = brics, year = 2002, type = rs, number = "RS-02-28", address = daimi, month = jun, note = "33~pp. To appear in {\em Abstract and Applied Analysis}.", abstract = "In a previous paper, the first author derived an explicit quantitative version of a theorem due to Borwein, Reich and Shafrir on the asymptotic behaviour of Mann iterations of nonexpansive mappings of convex sets $C$ in normed linear spaces. This quantitative version, which was obtained by a logical analysis of the ineffective proof given by Borwein, Reich and Shafrir, could be used to obtain strong uniform bounds on the asymptotic regularity of such iterations in the case of bounded $C$ and even weaker conditions. In this paper we extend these results to hyperbolic spaces and directionally nonexpansive mappings. In particular, we obtain significantly stronger and more general forms of the main results of a recent paper by W.A. Kirk with explicit bounds. As a special feature of our approach, which is based on logical analysis instead of functional analysis, no functional analytic embeddings are needed to obtain our uniformity results which contain all previously known results of this kind as special cases", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-27, author = "{\"O}stlin, Anna and Pagh, Rasmus", title = "Simulating Uniform Hashing in Constant Time and Optimal Space", institution = brics, year = 2002, type = rs, number = "RS-02-27", address = daimi, month = "", note = "11~pp", abstract = "Many algorithms and data structures employing hashing have been analyzed under the {\em uniform hashing} assumption, i.e., the assumption that hash functions behave like truly random functions. In this paper it is shown how to implement hash functions that can be evaluated on a RAM in constant time, and behave like truly random functions on any set of $n$ inputs, with high probability. The space needed to represent a function is $O(n)$ words, which is the best possible (and a polynomial improvement compared to previous fast hash functions). As a consequence, a broad class of hashing schemes can be implemented to meet, with high probability, the performance guarantees of their uniform hashing analysis", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-26, author = "Korovina, Margarita", title = "Fixed Points on Abstract Structures without the Equality Test", institution = brics, year = 2002, type = rs, number = "RS-02-26", address = daimi, month = jun, note = "14~pp. Appears in " # lncs2850 # ", pages 290--301. Appeared earlier in " # ns022 # ", pages 58--61", abstract = "In this paper we present a study of definability properties of fixed points of effective operators on abstract structures without the~equality test. In particular we prove that Gandy theorem holds for abstract structures. This provides a useful tool for dealing with recursive definitions using $\Sigma$-formulas.\bibpar One of the applications of Gandy theorem in the case of the reals without the equality test is that it allows us to define universal $\Sigma $--predicates. It leads to a topological characterisation of $\Sigma$--relations on ${\rm I\!R}$", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-25, author = "H{\"u}ttel, Hans", title = "Deciding Framed Bisimilarity", institution = brics, year = 2002, type = rs, number = "RS-02-25", address = iesd, month = may, note = "20~pp. Appears in " # entcsinfinity02 # ", 18~pp", abstract = "The spi-calculus, proposed by Abadi and Gordon, is a process calculus based on the $\pi $-calculus and is intended for reasoning about the behaviour of cryptographic protocols. We consider the finite-control fragment of the spi-calculus, showing it to be Turing-powerful (a result which is joint work with Josva Kleist, Uwe Nestmann, and Bj{\"o}rn Victor.) Next, we restrict our attention to finite (non-recursive) spi-calculus. Here, we show that framed bisimilarity, an equivalence relation proposed by Abadi and Gordon, showing that it is decidable for this fragment", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-24, author = "Christensen, Aske Simon and M{\o}ller, Anders and Schwartzbach, Michael I.", title = "Static Analysis for Dynamic {XML}", institution = brics, year = 2002, type = rs, number = "RS-02-24", address = daimi, month = may , note = "13~pp", abstract = "We describe the {\it summary graph} lattice for dataflow analysis of programs that dynamically construct XML documents. Summary graphs have successfully been used to provide static guarantees in the JWIG language for programming interactive Web services. In particular, the JWIG compiler is able to check validity of dynamically generated XHTML documents and to type check dynamic form data. In this paper we present summary graphs and indicate their applicability for various scenarios. We also show that summary graphs have exactly the same expressive power as the regular expression types from XDuce, but that the extra structure in summary graphs makes them more suitable for certain program analyses", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-23, author = "Nola, Antonio Di and Leu{\c{s}}tean, Lauren{\c {t}}iu", title = "Compact Representations of {BL}-Algebras", institution = brics, year = 2002, type = rs, number = "RS-02-23", address = daimi, month = may, note = "25~pp", abstract = "In this paper we define sheaf spaces of BL-algebras (or BL-sheaf spaces), we study completely regular and compact BL-sheaf spaces and compact representations of BL-algebras and, finally, we prove that the category of non-trivial BL-algebras is equivalent with the category of compact local BL-sheaf spaces", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-22, author = "Nielsen, Mogens and Palamidessi, Catuscia and Valencia, Frank D.", title = "On the Expressive Power of Concurrent Constraint Programming Languages", institution = brics, year = 2002, type = rs, number = "RS-02-22", address = daimi, month = may, note = "34~pp. Appears in " # acmppdp02 # ", pages 156--157", abstract = "The tcc paradigm is a formalism for timed concurrent constraint programming. Several tcc languages differing in their way of expressing infinite behaviour have been proposed in the literature. In this paper we study the expressive power of some of these languages. In particular, we show that: \begin{itemize} \item[(1)] recursive procedures with parameters can be encoded into parameterless recursive procedures with dynamic scoping, and vice-versa. \item[(2)] replication can be encoded into parameterless recursive procedures with static scoping, and vice-versa. \item[(3)]the languages from (1) are strictly more expressive than the languages from (2). \end{itemize} Furthermore, we show that behavioural equivalence is undecidable for the languages from (1), but decidable for the languages from (2). The undecidability result holds even if the process variables take values from a fixed finite domain", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-21, author = "{\'E}sik, Zolt{\'a}n and Kuich, Werner", title = "Formal Tree Series", institution = brics, year = 2002, type = rs, number = "RS-02-21", address = iesd, month = apr, note = "66~pp", abstract = "In this survey we generalize some results on formal tree languages, tree grammars and tree automata by an algebraic treatment using semirings, fixed point theory, formal tree series and matrices. The use of these mathematical constructs makes definitions, constructions, and proofs more satisfactory from an mathematical point of view than the customary ones. The contents of this survey paper is indicated by the titles of the sections: \begin{itemize} \item[1.] Introduction \item[2.] Preliminaries \item[3.] Tree automata and systems of equations \item[4.] Closure properties and a Kleene Theorem for recognizable tree series \item[5.] Pushdown tree automata, algebraic tree systems, and a Kleene Theorem \item[6.] Tree series transducers \item[7.] Full abstract families of tree series \item[8.] Connections to formal power series \end{itemize} ", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-20, author = "{\'E}sik, Zolt{\'a}n and Larsen, Kim G.", title = "Regular Languages Definable by {L}indstr{\"o}m Quantifiers (Preliminary Version)", institution = brics, year = 2002, type = rs, number = "RS-02-20", address = iesd, month = apr, note = "56~pp. Superseeded by the BRICS report \htmladdnormallink{RS-03-28}{http://www.brics.dk/RS/03/28/}", abstract = "In our main result, we establish a formal connection between Lindstr{\"o}m quantifiers with respect to regular languages and the double semidirect product of finite monoid-generator pairs. We use this correspondence to characterize the expressive power of Lindstr{\"o}m quantifiers associated with a class of regular languages", linkhtmlabs = "" } @techreport{BRICS-RS-02-19, author = "Bloom, Stephen L. and {\'E}sik, Zolt{\'a}n", title = "An Extension Theorem with an Application to Formal Tree Series", institution = brics, year = 2002, type = rs, number = "RS-02-19", address = iesd, month = apr, note = "51~pp. Appears in " # entcsctcs02 # " under the title {\em Unique Guarded Fixed Points in an Additive Setting}", abstract = "A grove theory is a Lawvere algebraic theory $T$ for which each hom-set $T(n,p)$ is a commutative monoid; composition on the right distrbutes over all finite sums: $(\sum_{i \in F} f_i) \cdot h= \sum_{i \in F} f_i \cdot h$. A matrix theory is a grove theory in which composition on the left and right distributes over finite sums. A matrix theory $M$ is isomorphic to a theory of all matrices over the semiring $S=M(1,1)$. Examples of grove theories are theories of (bisimulation equivalence classes of) synchronization trees, and theories of formal tree series over a semiring $S$. Our main theorem states that if $T$ is a grove theory which has a matrix subtheory $M$ which is an iteration theory, then, under certain conditions, the fixed point operation on $M$ can be extended in exactly one way to a fixedpoint operation on $T$ such that $T$ is an iteration theory. A second theorem is a Kleene-type result. Assume that $T$ is a iteration grove theory and $M$ is a sub iteration grove theory of $T$ which is a matrix theory. For a given collection $\Sigma$ of scalar morphisms in $T$ we describe the smallest sub iteration grove theory of $T$ containing all the morphisms in $M \cup\Sigma $", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-18, author = "Brodal, Gerth St{\o}lting and Fagerberg, Rolf", title = "Cache Oblivious Distribution Sweeping", institution = brics, year = 2002, type = rs, number = "RS-02-18", address = daimi, month = apr, note = "Appears in " # lncs2380 # ", pages 426--438", abstract = "We adapt the distribution sweeping method to the cache oblivious model. Distribution sweeping is the name used for a general approach for divide-and-conquer algorithms where the combination of solved subproblems can be viewed as a merging process of streams. We demonstrate by a series of algorithms for specific problems the feasibility of the method in a cache oblivious setting. The problems all come from computational geometry, and are: orthogonal line segment intersection reporting, the all nearest neighbors problem, the 3D maxima problem, computing the measure of a set of axis-parallel rectangles, computing the visibility of a set of line segments from a point, batched orthogonal range queries, and reporting pairwise intersections of axis-parallel rectangles. Our basic building block is a simplified version of the cache oblivious sorting algorithm Funnelsort of Frigo et al., which is of independent interest" } @techreport{BRICS-RS-02-17, author = "Madsen, Bolette Ammitzb{\o}ll and Byskov, Jesper Makholm and Skjernaa, Bjarke", title = "On the Number of Maximal Bipartite Subgraphs of a Graph", institution = brics, year = 2002, type = rs, number = "RS-02-17", address = daimi, month = apr, note = "7~pp", abstract = "We show new lower and upper bounds on the number of maximal induced bipartite subgraphs of graphs with $n$ vertices. We present an infinite family of graphs having $105^{n/10} \approx 1.5926^n$ such subgraphs, which improves an earlier lower bound by Schiermeyer (1996). We show an upper bound of $n\cdot 12^{n/4} \approx n\cdot 1.8613^n$ and give an algorithm that lists all maximal induced bipartite subgraphs in time proportional to this bound. This is used in an algorithm for checking 4-colourability of a graph running within the same time bound", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-16, author = "Srba, Ji{\v{r}}{\'\i}", title = "Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds", institution = brics, year = 2002, type = rs, number = "RS-02-16", address = daimi, month = apr, note = "33~pp. To appear in {\em Acta Informatica}", abstract = "In this paper we study bisimilarity problems for simple process algebras. In particular, we show PSPACE-hardness of the following problems: \begin{enumerate} \item strong bisimilarity of Basic Parallel Processes (BPP), \item strong bisimilarity of Basic Process Algebra (BPA), \item strong regularity of BPP, and \item strong regularity of BPA. \end{enumerate} We also demonstrate NL-hardness of strong regularity problems for the normed subclasses of BPP and BPA.\bibpar Bisimilarity problems for simple process algebras are introduced in a general framework of process rewrite systems, and a uniform description of the new techniques used for the hardness proofs is provided", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-15, author = "Nielsen, Jesper Makholm", title = "On the Number of Maximal Independent Sets in a Graph", institution = brics, year = 2002, type = rs, number = "RS-02-15", address = daimi, month = apr, note = "10~pp", abstract = "We show that the number of maximal independent sets of size {\em exactly} $k$ in any graph of size $n$ is at most $\lfloor n/k \rfloor ^{k-(n\bmod k)} (\lfloor n/k \rfloor+1)^{n\bmod k}$. For maximal independent sets of size {\em at most} $k$ the same bound holds for $k\leq n/3$. For $k>n/3$ a bound of approximately $3^{n/3}$ is given. All the bounds are exactly tight and improve Eppstein (2001) who give the bound $3^{4k-n}4^{n-3k}$ on the number of maximal independent sets of size at most $k$, which is the same for $n/4 \leq k \leq n/3$, but larger otherwise. We give an algorithm listing the maximal independent sets in a graph in time proportional to these bounds (ignoring a polynomial factor), and we use this algorithm to construct algorithms for 4- and 5- colouring running in time ${\cal O}(1.7504^n)$ and ${\cal O}(2.1593^n)$, respectively", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-14, author = "Berger, Ulrich and Oliva, Paulo B.", title = "Modified Bar Recursion", institution = brics, year = 2002, type = rs, number = "RS-02-14", address = daimi, month = apr, note = "23~pp. To appear in {\em Lecture Notes in Logic}", abstract = "We introduce a variant of Spector's bar recursion (called ``modified bar recursion'') in finite types to give a realizability interpretation of the classical axiom of countable choice allowing for the extraction of witnesses from proofs of $\Sigma_1$ formulas in classical analysis. As a second application of modified bar recursion we present a bar recursive definition of the fan functional. Moreover, we show that modified bar recursion exists in ${\cal M}$ (the model of strongly majorizable functionals) and is not S1-S9 computable in ${\cal C}$ (the model of total functionals). Finally, we show that modified bar recursion defines Spector's bar recursion primitive recursively", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-13, author = "Brodal, Gerth St{\o}lting and Lyngs{\o}, Rune B. and {\"O}stlin, Anna and Pedersen, Christian N. S.", title = "Solving the String Statistics Problem in Time $O(n\log n)$", institution = brics, year = 2002, type = rs, number = "RS-02-13", address = daimi, month = mar, note = "28~pp. Shorter version appears in " # lncs2380 # ", pages 728--739", abstract = "The string statistics problem consists of preprocessing a string of length~$n$ such that given a query pattern of length~$m$, the maximum number of non-overlapping occurrences of the query pattern in the string can be reported efficiently. Apostolico and Preparata introduced the minimal augmented suffix tree (MAST) as a data structure for the string statistics problem, and showed how to construct the MAST in time ${\cal O}(n\log^2 n)$ and how it supports queries in time~${\cal O}(m)$ for constant sized alphabets. A subsequent theorem by Fraenkel and Simpson stating that a string has at most a linear number of distinct squares implies that the MAST requires space~${\cal O}(n)$. In this paper we improve the construction time for the MAST to ${\cal O}(n\log n)$ by extending the algorithm of Apostolico and Preparata to exploit properties of efficient joining and splitting of search trees together with a refined analysis", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-12, author = "Danvy, Olivier and Goldberg, Mayer", title = "There and Back Again", institution = brics, year = 2002, type = rs, number = "RS-02-12", address = daimi, month = mar, note = "ii+11~pp. Appears in " # acmicfp02 # ", pages 230--234. This report supersedes the earlier report BRICS RS-01-39", abstract = "We present a programming pattern where a recursive function traverses a data structure---typically a list---at return time. The idea is that the recursive calls get us there (typically to a base case) and the returns get us back again {\em while traversing the data structure}. We name this programming pattern of traversing a data structure at return time ``There And Back Again'' (TABA).\bibpar The TABA pattern directly applies to computing a symbolic convolution. It also synergizes well with other programming patterns, e.g., dynamic programming and traversing a list at double speed. We illustrate TABA and dynamic programming with Catalan numbers. We illustrate TABA and traversing a list at double speed with palindromes and we obtain a novel solution to this traditional exercise.\bibpar A TABA-based function written in direct style makes full use of an Algol-like control stack and needs no heap allocation. Conversely, in a TABA-based function written in continuation-passing style, the continuation acts as a list iterator. In general, the TABA pattern saves one from constructing intermediate lists in reverse order", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-11, author = "Christensen, Aske Simon and M{\o}ller, Anders and Schwartzbach, Michael I.", title = "Extending Java for High-Level Web Service Construction", institution = brics, year = 2002, type = rs, number = "RS-02-11", address = daimi, month = mar, note = "54~pp. To appear in {\em ACM Transactions on Programming Languages and Systems}", abstract = "We incorporate innovations from the {\tt} project into the Java language to provide high-level features for Web service programming. The resulting language, JWIG, contains an advanced session model and a flexible mechanism for dynamic construction of XML documents, in particular XHTML. To support program development we provide a suite of program analyses that at compile-time verify for a given program that no run-time errors can occur while building documents or receiving form input, and that all documents being shown are valid according to the document type definition for XHTML 1.0.\bibpar We compare JWIG with Servlets and JSP which are widely used Web service development platforms. Our implementation and evaluation of JWIG indicate that the language extensions can simplify the program structure and that the analyses are sufficiently fast and precise to be practically useful", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-10, author = "Kohlenbach, Ulrich", title = "Uniform Asymptotic Regularity for {M}ann Iterates", institution = brics, year = 2002, type = rs, number = "RS-02-10", address = daimi, month = mar, note = "17~pp. Appears in {\em Journal of Mathematical Analysis and Applications}, 279(2):531--544, 2003.", abstract = "In a previous paper we obtained an effective quantitative analysis of a theorem due to Borwein, Reich and Shafrir on the asymptotic behavior of general Krasnoselski-Mann iterations for nonexpansive self-mappings of convex sets $C$ in arbitrary normed spaces. We used this result to obtain a new strong uniform version of Ishikawa's theorem for bounded $C$. In this paper we give a qualitative improvement of our result in the unbounded case and prove the uniformity result for the bounded case under the weaker assumption that $C$ contains a point $x$ whose Krasnoselski-Mann iteration $(x_n)$ is bounded.\\ We also consider more general iterations for which asymptotic regularity is known only for uniformly convex spaces (Groetsch). We give uniform effective bounds for (an extension of) Groetsch's theorem which generalize previous results by Kirk/Martinez-Yanez and the author", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-9, author = "{\"O}stlin, Anna and Pagh, Rasmus", title = "One-Probe Search", institution = brics, year = 2002, type = rs, number = "RS-02-9", address = daimi, month = feb, note = "17~pp. Appears in " # lncs2380 # ", pages 439--450", abstract = "We consider dictionaries that perform lookups by probing a {\em single word\/} of memory, knowing only the size of the data structure. We describe a randomized dictionary where a lookup returns the correct answer with probability $1-\epsilon$, and otherwise returns ``don't know''. The lookup procedure uses an expander graph to select the memory location to probe. Recent explicit expander constructions are shown to yield space usage much smaller than what would be required using a deterministic lookup procedure. Our data structure supports efficient {\em deterministic\/} updates, exhibiting new probabilistic guarantees on dictionary running time", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-8, author = "Cramer, Ronald and Fehr, Serge", title = "Optimal Black-Box Secret Sharing over Arbitrary Abelian Groups", institution = brics, year = 2002, type = rs, number = "RS-02-8", address = daimi, month = feb, note = "19~pp. Appears in " # lncs2442 # ", pages 272--287", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-7, author = "Ing{\'o}lfsd{\'o}ttir, Anna and Christensen, Anders Lyhne and Hansen, Jens Alsted and Johnsen, Jacob and Knudsen, John and Rasmussen, Jacob Illum", title = "A Formalization of Linkage Analysis", institution = brics, year = 2002, type = rs, number = "RS-02-7", address = iesd, month = feb, note = "vi+109~pp", abstract = "In this report a formalization of genetic linkage analysis is introduced. Linkage analysis is a computationally hard biomathematical method, which purpose is to locate genes on the human genome. It is rooted in the new area of bioinformatics and no formalization of the method has previously been established. Initially, the biological model is presented. On the basis of this biological model we establish a formalization that enables reasoning about algorithms used in linkage analysis. The formalization applies both for single and multi point linkage analysis. We illustrate the usage of the formalization in correctness proofs of central algorithms and optimisations for linkage analysis. A further use of the formalization is to reason about alternative methods for linkage analysis. We discuss the use of MTBDDs and PDGs in linkage analysis, since they have proven efficient for other computationally hard problems involving large state spaces. We conclude that none of the techniques discussed are directly applicable to linkage analysis, however further research is needed in order to investigated whether a modified version of one or more of these are applicable", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-6, author = "Aceto, Luca and {\'E}sik, Zolt{\'a}n and Ing{\'o}lfsd{\'o}ttir, Anna", title = "Equational Axioms for Probabilistic Bisimilarity (Preliminary Report)", institution = brics, year = 2002, type = rs, number = "RS-02-6", address = iesd, month = feb, note = "22~pp. Appears in " # lncs2422 # ", pages 239--253", abstract = "This paper gives an equational axiomatization of probabilistic bisimulation equivalence for a class of finite-state agents previously studied by Stark and Smolka ((2000) {\em Proof, Language, and Interaction: Essays in Honour of Robin Milner}, pp.~571--595). The axiomatization is obtained by extending the general axioms of iteration theories (or iteration algebras), which characterize the equational properties of the fixed point operator on ($\omega$-)\-continuous or monotonic functions, with three axiom schemas that express laws that are specific to probabilistic bisimilarity. Hence probabilistic bisimilarity (over finite-state agents) has an equational axiomatization relative to iteration algebras", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-5, author = "Crazzolara, Federico and Winskel, Glynn", title = "Composing {S}trand Spaces", institution = brics, year = 2002, type = rs, number = "RS-02-5", address = daimi, month = feb, note = "30~pp", abstract = "The strand space model for the analysis of security protocols is known to have some limitations in the patterns of nondeterminism it allows and in the ways in which strand spaces can be composed. Its successful application to a broad range of security protocols may therefore seem surprising. This paper gives a formal explanation of the wide applicability of strand spaces. We start with an extension of strand spaces which permits several operations to be defined in a compositional way, forming a process language for building up strand spaces. We then show, under reasonable conditions how to reduce the extended strand spaces to ones of a traditional kind. For security protocols we are mainly interested in their safety properties. This suggests a strand-space equivalence: two strand spaces are equivalent if and only if they have essentially the same sets of bundles. However this equivalence is not a congruence with respect to the strand-space operations. By extending the notion of bundle we show how to define the strand-space operations directly on ``bundle spaces''. This leads to a characterisation of the largest congruence within the strand-space equivalence. Finally, we relate strand spaces to event structures, a well known model for concurrency.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-4, author = "Danvy, Olivier and Nielsen, Lasse R.", title = "Syntactic Theories in Practice", institution = brics, year = 2002, type = rs, number = "RS-02-4", address = daimi, month = jan, note = "34~pp. This revised report supersedes the earlier BRICS report RS-01-31", abstract = "The evaluation function of a syntactic theory is canonically defined as the transitive closure of (1) decomposing a program into an evaluation context and a redex, (2) contracting this redex, and (3) plugging the contractum in the context. Directly implementing this evaluation function therefore yields an interpreter with a worst-case overhead, for each step, that is linear in the size of the input program. We present sufficient conditions over a syntactic theory to circumvent this overhead, by replacing the composition of (3) plugging and (1) decomposing by a single ``refocusing'' function mapping a contractum and a context into a new context and a new redex, if there are any. We also show how to construct such a refocusing function, we prove its correctness, and we analyze its complexity.\bibpar We illustrate refocusing with two examples: a programming-language interpreter and a transformation into continuation-passing style. As a byproduct, the time complexity of this program transformation is mechanically changed from quadratic in the worst case to linear", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-3, author = "Danvy, Olivier and Nielsen, Lasse R.", title = "On One-Pass {CPS} Transformations", institution = brics, year = 2002, type = rs, number = "RS-02-3", address = daimi, month = jan, note = "18~pp", abstract = "We bridge two distinct approaches to one-pass CPS transformations, i.e., CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a syntactic theory of the $\lambda$-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use Church encoding, Reynolds's defunctionalization, and an implementation technique for syntactic theories, refocusing, developed in the second author's PhD thesis.\bibpar This work is directly applicable to transforming programs into monadic normal form", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-2, author = "Nielsen, Lasse R.", title = "A Simple Correctness Proof of the Direct-Style Transformation", institution = brics, year = 2002, type = rs, number = "RS-02-2", address = daimi, month = jan, note = "11~pp", abstract = "We build on Danvy and Nielsen's first-order program transformation into continuation-passing style (CPS) to present a new correctness proof of the converse transformation, i.e., a one-pass transformation from CPS back to direct style. Previously published proofs were based on, e.g., a one-pass higher-order CPS transformation, and were complicated by having to reason about higher-order functions. In contrast, this work is based on a one-pass CPS transformation that is both compositional and first-order, and therefore the proof simply proceeds by structural induction on syntax", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-02-1, author = "Brabrand, Claus and M{\o}ller, Anders and Schwartzbach, Michael I.", title = "The {\tt } Project", institution = brics, year = 2002, type = rs, number = "RS-02-1", address = daimi, month = jan, note = "36~pp. This revised report supersedes the earlier BRICS report RS-00-42", abstract = "We present the results of the {\tt } project, which aims to design and implement a high-level domain-specific language for programming interactive Web services.\bibpar A fundamental aspect of the development of the World Wide Web during the last decade is the gradual change from static to dynamic generation of Web pages. Generating Web pages dynamically in dialogue with the client has the advantage of providing up-to-date and tailor-made information. The development of systems for constructing such dynamic Web services has emerged as a whole new research area.\bibpar The {\tt } language is designed by analyzing its application domain and identifying fundamental aspects of Web services inspired by problems and solutions in existing Web service development languages. The core of the design consists of a session-centered service model together with a flexible template-based mechanism for dynamic Web page construction. Using specialized program analyses, certain Web specific properties are verified at compile-time, for instance that only valid HTML 4.01 is ever shown to the clients. In addition, the design provides high-level solutions to form field validation, caching of dynamic pages, and temporal-logic based concurrency control, and it proposes syntax macros for making highly domain-specific languages. The language is implemented via widely available Web technologies, such as Apache on the server-side and JavaScript and Java Applets on the client-side. We conclude with experience and evaluation of the project", linkhtmlabs = "", linkps = "", linkpdf = "" }