This document is also available as
PostScript
and
DVI.
 RS0155

PostScript,
PDF,
DVI.
Daniel Damian and Olivier Danvy.
A Simple CPS Transformation of ControlFlow Information.
December 2001.
18 pp. Appears in Logic Journal of the IGPL, 10(2):501515,
2002.
Abstract: We build on Danvy and Nielsen's firstorder program
transformation into continuationpassing style (CPS) to design a new CPS
transformation of flow information that is simpler and more efficient than
what has been presented in previous work. The key to simplicity and
efficiency is that our CPS transformation constructs the flow information in
one go, instead of first computing an intermediate result and then exploiting
it to construct the flow information.
More precisely, we show how to
compute controlflow information for CPStransformed programs from
controlflow information for directstyle programs and viceversa. As a
corollary, we confirm that CPS transformation has no effect on the
controlflow information obtained by constraintbased controlflow analysis.
The transformation has immediate applications in assessing the effect of the
CPS transformation over other analyses such as, for instance, bindingtime
analysis.
 RS0154

PostScript,
PDF,
DVI.
Daniel Damian and Olivier Danvy.
Syntactic Accidents in Program Analysis: On the Impact of the
CPS Transformation.
December 2001.
41 pp. To appear in the Journal of Functional Programming. This
report supersedes the earlier BRICS report RS0015.
Abstract: We show that a nonduplicating transformation into
continuationpassing style (CPS) has no effect on controlflow analysis, a
positive effect on bindingtime analysis for traditional partial evaluation,
and no effect on bindingtime analysis for continuationbased partial
evaluation: a monovariant controlflow analysis yields equivalent results on
a directstyle program and on its CPS counterpart, a monovariant bindingtime
analysis yields less precise results on a directstyle program than on its
CPS counterpart, and an enhanced monovariant bindingtime analysis yields
equivalent results on a directstyle program and on its CPS counterpart. Our
proof technique amounts to constructing the CPS counterpart of flow
information and of binding times.
Our results formalize and confirm a
folklore theorem about traditional bindingtime analysis, namely that CPS has
a positive effect on binding times. What may be more surprising is that the
benefit does not arise from a standard refinement of program analysis, as,
for instance, duplicating continuations.
The present study is
symptomatic of an unsettling property of program analyses: their quality is
unpredictably vulnerable to syntactic accidents in source programs, i.e., to
the way these programs are written. More reliable program analyses require a
better understanding of the effect of syntactic change.
 RS0153

PostScript,
PDF,
DVI.
Zoltán Ésik and Masami Ito.
Temporal Logic with Cyclic Counting and the Degree of
Aperiodicity of Finite Automata.
December 2001.
31 pp.
Abstract: We define the degree of aperiodicity of finite
automata and show that for every set of positive integers, the class
of finite automata whose degree of aperiodicity belongs to the
division ideal generated by is closed with respect to direct products,
disjoint unions, subautomata, homomorphic images and renamings. These closure
conditions define qvarieties of finite automata. We show that qvarieties
are in a onetoone correspondence with literal varieties of regular
languages. We also characterize as the cascade product of a
variety of counters with the variety of aperiodic (or counterfree) automata.
We then use the notion of degree of aperiodicity to characterize the
expressive power of firstorder logic and temporal logic with cyclic counting
with respect to any given set of moduli. It follows that when is
finite, then it is decidable whether a regular language is definable in
firstorder or temporal logic with cyclic counting with respect to moduli in
.
 RS0152

PostScript,
PDF,
DVI.
Jens Groth.
Extracting Witnesses from Proofs of Knowledge in the Random
Oracle Model.
December 2001.
23 pp.
Abstract: We prove that a 3move interactive proof system with
the special soundness property made noninteractive by applying the
FiatShamir heuristic is almost a noninteractive proof of knowledge in the
random oracle model. In an application of the result we demonstrate that the
DamgårdJurik voting scheme based on homomorphic threshold encryption is
secure against a nonadaptive adversary according to Canetti's definition of
multiparty computation security.
 RS0151

PostScript,
PDF,
DVI.
Ulrich Kohlenbach.
On Weak Markov's Principle.
December 2001.
10 pp. Appears in Mathematical Logic Quarterly, 48(suppl. 1):5965, 2002.
Abstract: We show that the socalled weak Markov's principle
(WMP) which states that every pseudopositive real number is positive is
underivable in
EHAAC. Since
allows to formalize (at least large parts of) Bishop's
constructive mathematics this makes it unlikely that WMP can be proved within
the framework of Bishopstyle mathematics (which has been open for about 20
years). The underivability even holds if the ineffective schema of full
comprehension (in all types) for negated formulas (in particular for free formulas) is added which allows to derive the law of excluded middle
for such formulas.
 RS0150

PostScript,
PDF,
DVI.
Jirí Srba.
Note on the Tableau Technique for Commutative Transition
Systems.
December 2001.
19 pp. Appears in Nielsen and Engberg, editors, Foundations of
Software Science and Computation Structures, FoSSaCS '02 Proceedings,
LNCS 2303, 2002, pages 387401.
Abstract: We define a class of transition systems called
effective commutative transition systems (ECTS) and show, by generalising a
tableaubased proof for BPP, that bisimilarity between any two states of such
a transition system is decidable. It gives a general technique for extending
decidability borders of strong bisimilarity for a wide class of
infinitestate transition systems. This is demonstrated for several process
formalisms, namely BPP process algebra, lossy BPP processes, BPP systems with
interrupt and timedarc BPP nets.
 RS0149

PostScript,
PDF,
DVI.
Olivier Danvy and Lasse R. Nielsen.
A FirstOrder OnePass CPS Transformation.
December 2001.
21 pp. To appear in Theoretical Computer Science. Extended
version of a paper appearing in Nielsen and Engberg, editors, Foundations of Software Science and Computation Structures, FoSSaCS '02
Proceedings, LNCS 2303, 2002, pages 98113.
Abstract: We present a new transformation of callbyvalue
lambdaterms into continuationpassing style (CPS). This transformation
operates in one pass and is both compositional and firstorder. Because it
operates in one pass, it directly yields compact CPS programs that are
comparable to what one would write by hand. Because it is compositional, it
allows proofs by structural induction. Because it is firstorder, reasoning
about it does not require the use of a logical relation.
This new CPS
transformation connects two separate lines of research. It has already been
used to state a new and simpler correctness proof of a directstyle
transformation, and to develop a new and simpler CPS transformation of
controlflow information.
 RS0148

PostScript,
PDF,
DVI.
Mogens Nielsen and Frank D. Valencia.
Temporal Concurrent Constraint Programming: Applications and
Behavior.
December 2001.
36 pp. Appears in Brauer, Ehrig, Karhumäki and Salomaa, editors,
Formal and Natural Computing, LNCS 2300, 2001, pages 298321.
Abstract: The ntcc calculus is a model of
nondeterministic temporal concurrent constraint programming. In this paper
we study behavioral notions for this calculus. In the underlying
computational model, concurrent constraint processes are executed in discrete
time intervals. The behavioral notions studied reflect the reactive
interactions between concurrent constraint processes and their environment,
as well as internal interactions between individual processes. Relationships
between the suggested notions are studied, and they are all proved to be
decidable for a substantial fragment of the calculus. Furthermore, the
expressive power of this fragment is illustrated by examples.
 RS0147

PostScript,
PDF,
DVI.
Jesper Buus Nielsen.
NonCommitting Encryption is Too Easy in the Random Oracle
Model.
December 2001.
20 pp.
Abstract: The noncommitting encryption problem arises in the
setting of adaptively secure cryptographic protocols, as the task of
implementing secure channels. We prove that in the random oracle model, where
the parties have oracle access to a uniformly random function, noncommitting
encryption can be implemented efficiently using any trapdoor
permutation.
We also prove that no matter how the oracle is
instantiated in practice the resulting scheme will never be noncommitting,
and we give a short discussion of the random oracle model in light of this.
 RS0146

PostScript,
PDF,
DVI.
Lars Kristiansen.
The Implicit Computational Complexity of Imperative Programming
Languages.
November 2001.
46 pp.
Abstract: During the last decade Cook, Bellantoni, Leivant and
others have developed the theory of implicit computational complexity, i.e. the theory of predicative recursion, tiered definition schemes, etcetera. We
extend and modify this theory to work in a context of imperative programming
languages, and characterise complexity classes like P, LINSPACE,
PSPACE and the classes in the Grzegorczyk hiearchy. Our theoretical
framework seems promising with respect to applications in engineering.
 RS0145

PostScript,
PDF.
Ivan B. Damgård and Gudmund Skovbjerg
Frandsen.
An Extended Quadratic Frobenius Primality Test with Average
Case Error Estimates.
November 2001.
43 pp.
Abstract: We present an Extended Quadratic Frobenius Primality
Test (EQFT), which is related to the MillerRabin test and the Quadratic
Frobenius test (QFT) by Grantham. EQFT is wellsuited for generating large,
random prime numbers since on a random input number, it takes time about
equivalent to 2 MillerRabin tests, but has much smaller error probability.
EQFT extends QFT by verifying additional algebraic properties related to the
existence of elements of order 3 and 4. We obtain a simple closed expression
that upper bounds the probability of acceptance for any input number. This in
turn allows us to give strong bounds on the averagecase behaviour of the
test: consider the algorithm that repeatedly chooses random odd bit
numbers, subjects them to iterations of our test and outputs the first
one found that passes all tests. We obtain numeric upper bounds for the error
probability of this algorithm as well as a general closed expression bounding
the error. For instance, it is at most for . Compared
to earlier similar results for the MillerRabin test, the results indicates
that our test in the average case has the effect of 9 MillerRabin tests,
while only taking time equivalent to about 2 such tests. We also give bounds
for the error in case a prime is sought by incremental search from a random
starting point. While EQFT is slower than the average case on a small set of
inputs, we present a variant that is always fast, i.e. takes time about 2
MillerRabin tests. The variant has slightly larger worst case error
probability than EQFT, but still improves on previous proposed tests.
 RS0144

PostScript,
PDF.
M. Oliver Möller, Harald Rueß, and
Maria Sorea.
Predicate Abstraction for Dense RealTime Systems.
November 2001.
27 pp. Appears in Asarin, Maler and Yovine, editors, Workshop on
Theory and Practice of Timed Systems, TPTS '02 Proceedings, ENTCS 65(6),
2002.
Abstract: We propose predicate abstraction as a means for
verifying a rich class of safety and liveness properties for dense realtime
systems. First, we define a restricted semantics of timed systems which is
observationally equivalent to the standard semantics in that it validates the
same set of calculus formulas without a nextstep operator. Then, we
recast the model checking problem
for a timed
automaton and a calculus formula in terms of
predicate abstraction. Whenever a set of abstraction predicates forms a
socalled basis, the resulting abstraction is strongly preserving in
the sense that validates iff the corresponding finite
abstraction validates this formula . Now, the abstracted system can
be checked using familiar calculus model checking.
Like the
region graph construction for timed automata, the predicate abstraction
algorithm for timed automata usually is prohibitively expensive. In many
cases it suffices to compute an approximation of a finite bisimulation by
using only a subset of the basis of abstraction predicates. Starting with
some coarse abstraction, we define a finite sequence of refined abstractions
that converges to a strongly preserving abstraction. In each step, new
abstraction predicates are selected nondeterministically from a finite basis.
Counterexamples from failed calculus model checking attempts can be
used to heuristically choose a small set of new abstraction predicates for
refining the abstraction.
 RS0143

PostScript,
PDF,
DVI.
Ivan B. Damgård and Jesper Buus
Nielsen.
From KnownPlaintext Security to ChosenPlaintext Security.
November 2001.
18 pp.
Abstract: We present a new encryption mode for block ciphers.
The mode is efficient and is secure against chosenplaintext attack (CPA)
already if the underlying symmetric cipher is secure against knownplaintext
attack (KPA). We prove that known (and widely used) encryption modes as CBC
mode and counter mode do not have this property. In particular, we prove that
CBC mode using a KPA secure cipher is KPA secure, but need not be CPA secure,
and we prove that counter mode using a KPA secure cipher need not be even KPA
secure. The analysis is done in a concrete security framework.
 RS0142

PostScript,
PDF,
DVI.
Zoltán Ésik and Werner Kuich.
Rationally Additive Semirings.
November 2001.
11 pp. Appears in Journal of Universal Computer Science,
8(2):173183, 2002.
Abstract: We define rationally additive semirings that are a
generalization of ()complete and ()continuous semirings.
We prove that every rationally additive semiring is an iteration semiring.
Moreover, we characterize the semirings of rational power series with
coefficients in , the semiring of natural numbers equipped with a
top element, as the free rationally additive semirings.
 RS0141

PostScript,
PDF,
DVI.
Ivan B. Damgård and Jesper Buus
Nielsen.
Perfect Hiding and Perfect Binding Universally Composable
Commitment Schemes with Constant Expansion Factor.
October 2001.
43 pp. Appears in Yung, editor, Advances in Cryptology: 22nd
Annual International Cryptology Conference, CRYPTO '02 Proceedings,
LNCS 2442, 2002, pages 581596.
Abstract: Canetti and Fischlin have recently proposed the
security notion universal composability for commitment schemes and
provided two examples. This new notion is very strong. It guarantees that
security is maintained even when an unbounded number of copies of the scheme
are running concurrently, also it guarantees nonmalleability, resilience to
selective decommitment, and security against adaptive adversaries. Both of
their schemes uses bits to commit to one bit and can be based on
the existence of trapdoor commitments and nonmalleable encryption.
We
present new universally composable commitment schemes based on the Paillier
cryptosystem and the OkamotoUchiyama cryptosystem. The schemes are
efficient: to commit to bits, they use a constant number of modular
exponentiations and communicates bits. Further more the scheme can be
instantiated in either perfectly hiding or perfectly binding versions. These
are the first schemes to show that constant expansion factor, perfect hiding,
and perfect binding can be obtained for universally composable
commitments.
We also show how the schemes can be applied to do
efficient zeroknowledge proofs of knowledge that are universally composable.
 RS0140

PostScript,
PDF,
DVI.
Daniel Damian and Olivier Danvy.
CPS Transformation of Flow Information, Part II:
Administrative Reductions.
October 2001.
9 pp. To appear in the Journal of Functional Programming.
Superseeded by the BRICS report RS0236.
Abstract: We characterize the impact of a linear betareduction
on the result of a controlflow analysis. (By ``a linear betareduction'' we
mean the betareduction of a linear lambdaabstraction, i.e., of a
lambdaabstraction whose parameter occurs exactly once in its body.)
As a corollary, we consider the administrative reductions of a Plotkinstyle
transformation into continuationpassing style (CPS), and how they affect the
result of a constraintbased controlflow analysis and in particular the
least element in the space of solutions. We show that administrative
reductions preserve the least solution. Since we know how to construct least
solutions, preservation of least solutions solves a problem that was left
open in Palsberg and Wand's paper ``CPS Transformation of Flow
Information.''
Therefore, together, Palsberg and Wand's article ``CPS
Transformation of Flow Information'' 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 controlflow information in one pass.
 RS0139

PostScript,
PDF,
DVI.
Olivier Danvy and Mayer Goldberg.
There and Back Again.
October 2001.
14 pp. To appear in the proceedings of the 2002 ACM SIGPLAN
International Conference on Functional Programming.
Abstract: We illustrate a variety of programming problems that
seemingly require two separate list traversals, but that can be efficiently
solved in one recursive descent, without any other auxiliary storage but what
can be expected from a control stack. The idea is to perform the second
traversal when returning from the first.
This programming technique
yields new solutions to traditional problems. For example, given a list of
length or , where is unknown, we can detect whether this list
is a palindrome in recursive calls and no heap allocation.
 RS0138

PostScript,
PDF,
DVI.
Zoltán Ésik.
Free De Morgan Bisemigroups and Bisemilattices.
October 2001.
13 pp. To appear in the journal Algebra Colloquium.
Abstract: We give a geometric representation of free De Morgan
bisemigroups, free commutative De Morgan bisemigroups and free De Morgan
bisemilattices, using labeled graphs.
 RS0137

PostScript,
PDF,
DVI.
Ronald Cramer and Victor Shoup.
Universal Hash Proofs and a Paradigm for Adaptive Chosen
Ciphertext Secure PublicKey Encryption.
October 2001.
34 pp.
Abstract: We present several new and fairly practical
publickey encryption schemes and prove them secure against adaptive chosen
ciphertext attack. One scheme is based on Paillier's Decision Composite
Residuosity (DCR) assumption, while another is based in the classical
Quadratic Residuosity (QR) assumption. The analysis is in the standard
cryptographic model, i.e., the security of our schemes does not rely on the
Random Oracle model.
We also introduce the notion of a universal hash
proof system. Essentially, this is a special kind of noninteractive
zeroknowledge proof system for an NP language. We do not show that universal
hash proof systems exist for all NP languages, but we do show how to
construct very efficient universal hash proof systems for a general class of
grouptheoretic language membership problems.
Given an efficient
universal hash proof system for a language with certain natural cryptographic
indistinguishability properties, we show how to construct an efficient
publickey encryption schemes secure against adaptive chosen ciphertext
attack in the standard model. Our construction only uses the universal hash
proof system as a primitive: no other primitives are required, although even
more efficient encryption schemes can be obtained by using hash functions
with appropriate collisionresistance properties. We show how to construct
efficient universal hash proof systems for languages related to the DCR and
QR assumptions. From these we get corresponding publickey encryption schemes
that are secure under these assumptions. We also show that the CramerShoup
encryption scheme (which up until now was the only practical encryption
scheme that could be proved secure against adaptive chosen ciphertext attack
under a reasonable assumption, namely, the Decision DiffieHellman
assumption) is also a special case of our general theory.
 RS0136

PostScript,
PDF.
Gerth Stølting Brodal, Rolf Fagerberg,
and Riko Jacob.
Cache Oblivious Search Trees via Binary Trees of Small Height.
October 2001.
20 pp. Appears in Eppstein, editor, The Thirteenths Annual
ACMSIAM Symposium on Discrete Algorithms, SODA '02 Proceedings, 2002,
pages 3948.
Abstract: We propose a version of cache oblivious search trees
which is simpler than the previous proposal of Bender, Demaine and
FarachColton and has the same complexity bounds. In particular, our data
structure avoids the use of weight balanced trees, and can be implemented
as just a single array of data elements, without the use of pointers. The
structure also improves space utilization.
For storing elements,
our proposal uses
times the element size of memory, and
performs searches in worst case memory transfers, updates in
amortized
memory transfers, and range queries
in worst case
memory transfers, where is the size of
the output.
The basic idea of our data structure is to maintain a
dynamic binary tree of height using existing methods, embed
this tree in a static binary tree, which in turn is embedded in an array in a
cache oblivious fashion, using the van Emde Boas layout of Prokop.
We
also investigate the practicality of cache obliviousness in the area of
search trees, by providing an empirical comparison of different methods for
laying out a search tree in memory.
The source code of the programs,
our scripts and tools, and the data we present here are available online
under ftp.brics.dk/RS/01/36/Experiments/.
 RS0135

PostScript,
PDF,
DVI.
Mayer Goldberg.
A General Schema for Constructing OnePoint Bases in the Lambda
Calculus.
September 2001.
8 pp.
Abstract: In this paper, we present a schema for constructing
onepoint bases for recursively enumerable sets of lambda terms. The novelty
of the approach is that we make no assumptions about the terms for which the
onepoint basis is constructed: They need not be combinators and they may
contain constants and free variables. The significance of the construction is
twofold: In the context of the lambda calculus, it characterises onepoint
bases as ways of ``packaging'' sets of terms into a single term; And in the
context of realistic programming languages, it implies that we can define a
single procedure that generates any given recursively enumerable set of
procedures, constants and free variables in a given programming language.
 RS0134

PostScript,
PDF.
Flemming Friche Rodler and Rasmus Pagh.
Fast Random Access to Wavelet Compressed Volumetric Data Using
Hashing.
August 2001.
31 pp. To appear in ACM Transactions on Graphics.
Abstract: We present a new approach to lossy storage of the
coefficients of wavelet transformed data. While it is common to store the
coefficients of largest magnitude (and let all other coefficients be zero),
we allow a slightly different set of coefficients to be stored. This brings
into play a recently proposed hashing technique that allows space efficient
storage and very efficient retrieval of coefficients. Our approach is applied
to compression of volumetric data sets. For the ``Visible Man'' volume we
obtain up to 80% improvement in compression ratio over previously suggested
schemes. Further, the time for accessing a random voxel is quite competitive.
 RS0133

PostScript,
PDF.
Rasmus Pagh and Flemming Friche Rodler.
Lossy Dictionaries.
August 2001.
14 pp. Short version appears in Meyer auf der Heide, editor, 9th
Annual European Symposium on Algorithms, ESA '01 Proceedings, LNCS 2161,
2001, pages 300311.
Abstract: Bloom filtering is an important technique for space
efficient storage of a conservative approximation of a set . The set
stored may have up to some specified number of ``false positive'' members,
but all elements of are included. In this paper we consider lossy
dictionaries that are also allowed to have ``false negatives'', i.e.,
leave out elements of . The aim is to maximize the weight of included keys
within a given space constraint. This relaxation allows a very fast and
simple data structure making almost optimal use of memory. Being more time
efficient than Bloom filters, we believe our data structure to be well suited
for replacing Bloom filters in some applications. Also, the fact that our
data structure supports information associated to keys paves the way for new
uses, as illustrated by an application in lossy image compression.
 RS0132

PostScript,
PDF.
Rasmus Pagh and Flemming Friche Rodler.
Cuckoo Hashing.
August 2001.
21 pp. Short version appears in Meyer auf der Heide, editor, 9th
Annual European Symposium on Algorithms, ESA '01 Proceedings, LNCS 2161,
2001, pages 121133.
Abstract: We present a simple and efficient dictionary with
worst case constant lookup time, equaling the theoretical performance of the
classic dynamic perfect hashing scheme of Dietzfelbinger et al. (Dynamic
perfect hashing: Upper and lower bounds. SIAM J. Comput., 23(4):738761,
1994). The space usage is similar to that of binary search trees, i.e.,
three words per key on average. The practicality of the scheme is backed by
extensive experiments and comparisons with known methods, showing it to be
quite competitive also in the average case.
 RS0131

PostScript,
PDF,
DVI.
Olivier Danvy and Lasse R. Nielsen.
Syntactic Theories in Practice.
July 2001.
37 pp. Extended version of an article to appear in the informal
proceedings of the Second International Workshop on RuleBased
Programming, RULE 2001 (Firenze, Italy, September 4, 2001). Superseeded by
the BRICS report RS024.
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 result in the context. Directly implementing this evaluation
function therefore yields an interpreter with a quadratic time factor over
its input. We present sufficient conditions over a syntactic theory to
circumvent this quadratic factor, and illustrate the method with two
programminglanguage interpreters and a transformation into
continuationpassing style (CPS). In particular, we mechanically change the
time complexity of this CPS transformation from quadratic to linear.
 RS0130

PostScript,
PDF,
DVI.
Lasse R. Nielsen.
A Selective CPS Transformation.
July 2001.
24 pp. Appears in Brookes and Mislove, editors, 27th Annual
Conference on the Mathematical Foundations of Programming Semantics,
MFPS '01 Proceedings, ENTCS 45, 2001. A preliminary version appeared in
Brookes and Mislove, editors, 17th Annual Conference on Mathematical
Foundations of Programming Semantics, MFPS '01 Preliminary Proceedings,
BRICS Notes Series NS012, 2001, pages 201222.
Abstract: The CPS transformation makes all functions
continuationpassing, uniformly. Not all functions, however, need
continuations: they only do if their evaluation includes computational
effects. In this paper we focus on control operations, in particular ``call
with current continuation'' and ``throw''. We characterize this involvement
as a control effect and we present a selective CPS transformation that makes
functions and expressions continuationpassing if they have a control effect,
and that leaves the rest of the program in direct style. We formalize this
selective CPS transformation with an operational semantics and a simulation
theorem à la Plotkin.
 RS0129

PostScript,
PDF,
DVI.
Olivier Danvy, Bernd Grobauer, and Morten
Rhiger.
A Unifying Approach to GoalDirected Evaluation.
July 2001.
23 pp. Appears in New Generation Computing, 20(1):5373,
November 2001. A preliminary version appeared in Taha, editor, 2nd
International Workshop on Semantics, Applications, and Implementation of
Program Generation, SAIG '01 Proceedings, LNCS 2196, 2001, pages 108125.
Abstract: Goaldirected evaluation, as embodied in Icon and
Snobol, is built on the notions of backtracking and of generating successive
results, and therefore it has always been something of a challenge to specify
and implement. In this article, we address this challenge using computational
monads and partial evaluation.
We consider a subset of Icon and we
specify it with a monadic semantics and a list monad. We then consider a
spectrum of monads that also fit the bill, and we relate them to each other.
For example, we derive a continuation monad as a Church encoding of the list
monad. The resulting semantics coincides with Gudeman's continuation
semantics of Icon.
We then compile Icon programs by specializing their
interpreter (i.e., by using the first Futamura projection), using
typedirected partial evaluation. Through various back ends, including a
runtime code generator, we generate ML code, C code, and OCaml byte code.
Bindingtime analysis and partial evaluation of the continuationbased
interpreter automatically give rise to C programs that coincide with the
result of Proebsting's optimized compiler.
 RS0128

PostScript,
PDF,
DVI.
Luca Aceto, Zoltán Ésik, and Anna
Ingólfsdóttir.
A Fully Equational Proof of Parikh's Theorem.
June 2001.
28 pp. Appears in RAIRO, Theoretical Informatics and
Applications, 36(2):129153, 2002, special issue devoted to selected papers
from FICS 2001 (A. Labella ed.).
Abstract: We show that the validity of Parikh's theorem for
contextfree languages depends only on a few equational properties of least
prefixed points. Moreover, we exhibit an infinite basis of term
equations of continuous commutative idempotent semirings.
 RS0127

PostScript,
PDF,
DVI.
Mario José Cáccamo and Glynn
Winskel.
A HigherOrder Calculus for Categories.
June 2001.
24 pp. Appears in Boulton and Jackson, editors, Theorem Proving
in Higher Order Logics: 14th International Conference, TPHOLs '01
Proceedings, LNCS 2152, 2001, pages 136153.
Abstract: A calculus for a fragment of category theory is
presented. The types in the language denote categories and the expressions
functors. The judgements of the calculus systematise categorical arguments
such as: an expression is functorial in its free variables; two expressions
are naturally isomorphic in their free variables. There are special binders
for limits and more general ends. The rules for limits and ends support an
algebraic manipulation of universal constructions as opposed to a more
traditional diagrammatic approach. Duality within the calculus and
applications in proving continuity are discussed with examples. The calculus
gives a basis for mechanising a theory of categories in a generic theorem
prover like Isabelle.
 RS0126

PostScript,
PDF,
DVI.
Ulrik Frendrup and Jesper Nyholm Jensen.
A Complete Axiomatization of Simulation for Regular CCS
Expressions.
June 2001.
18 pp.
Abstract: This paper gives axiomatizations of strong and weak
simulation over regular CCS expressions. The proof of completeness of the
axiomatization of strong simulation is inspired by Milner's proof of
completeness of his axiomatization for strong equivalence over regular CCS
expressions. Soundness and completeness of the axiomatization for weak
simulation is easily deduced from the corresponding result for the
axiomatization of strong simulation over regular CCS expressions.
 RS0125

PostScript,
PDF,
DVI.
Bernd Grobauer.
Cost Recurrences for DML Programs.
June 2001.
51 pp. Extended version of a paper appearing in Leroy, editor, Proceedings of the 6th ACM SIGPLAN International Conference on Functional
Programming, 2001, pages 253264.
Abstract: A cost recurrence describes an upper bound for the
running time of a program in terms of the size of its input. Finding cost
recurrences is a frequent intermediate step in complexity analysis, and this
step requires an abstraction from data to data size. In this article, we use
information contained in dependent types to achieve such an abstraction:
Dependent ML (DML), a conservative extension of ML, provides dependent types
that can be used to associate data with size information, thus describing a
possible abstraction. We systematically extract cost recurrences from
firstorder DML programs, guiding the abstraction from data to data size with
information contained in DML type derivations.
 RS0124

Zoltán Ésik and Zoltán L. Németh.
Automata on SeriesParallel Biposets.
June 2001.
15 pp. Appears in Kuich, Rozenberg and Salomaa, editors, 5th
International Conference, Developments in Language Theory, DLT '01 Revised
Papers, LNCS 2295, 2002, pages 217227. Superseded by the later report
BRICS RS0244.
Abstract: We provide the basics of a 2dimensional theory of
automata on seriesparallel biposets. We define recognizable, regular and
rational sets of seriesparallel biposets and study their relationship.
Moreover, we relate these classes to languages of seriesparallel biposets
definable in monadic secondorder logic.
 RS0123

PostScript,
PDF,
DVI.
Olivier Danvy and Lasse R. Nielsen.
Defunctionalization at Work.
June 2001.
45 pp. Extended version of an article appearing in Søndergaard,
editor, 3rd International Conference on Principles and Practice of
Declarative Programming, PPDP '01 Proceedings, 2001, pages 162174.
Abstract: We study practical applications of Reynolds's
defunctionalization technique, which is a wholeprogram transformation from
higherorder to firstorder functional programs. This study leads us to
discover new connections between seemingly unrelated higherorder and
firstorder specifications and their correctness proofs. We thus perceive
defunctionalization both as a springboard and as a bridge: as a springboard
for discovering new connections between the firstorder world and the
higherorder world; and as a bridge for transferring existing results between
firstorder and higherorder settings.
 RS0122

PostScript,
PDF,
DVI.
Zoltán Ésik.
The Equational Theory of Fixed Points with Applications to
Generalized Language Theory.
June 2001.
21 pp. Appears in Kuich, Rozenberg and Salomaa, editors, 5th
International Conference, Developments in Language Theory, DLT '01 Revised
Papers, LNCS 2295, 2002,pages 2136.
Abstract: We review the rudiments of the equational logic of
(least) fixed points and provide some of its applications for axiomatization
problems with respect to regular languages, tree languages, and
synchronization trees.
 RS0121

PostScript,
PDF,
DVI.
Luca Aceto, Zoltán Ésik, and Anna
Ingólfsdóttir.
Equational Theories of Tropical Semirings.
June 2001.
52 pp. To appear in Theoretical Computer Science. Extended
abstracts of parts of this paper have appeared in Honsell and Miculan,
editors, Foundations of Software Science and Computation Structures,
FoSSaCS '01 Proceedings, LNCS 2030, 2001, pages 4256 and in Gaubert and
Loiseau, editors, Workshop on MaxPlus Algebras and Their Applications
to DiscreteEvent Systems, Theoretical Computer Science, and Optimization,
MAXPLUS '01 Proceedings, IFAC (International Federation of Automatic
Control) IFAC Publications, 2001.
Abstract: This paper studies the equational theory of various
exotic semirings presented in the literature. Exotic semirings are semirings
whose underlying carrier set is some subset of the set of real numbers
equipped with binary operations of minimum or maximum as sum, and addition as
product. Two prime examples of such structures are the
semiring and the tropical semiring. It is shown that none of the
exotic semirings commonly considered in the literature has a finite basis for
its equations, and that similar results hold for the commutative idempotent
weak semirings that underlie them. For each of these commutative idempotent
weak semirings, the paper offers characterizations of the equations that hold
in them, decidability results for their equational theories, explicit
descriptions of the free algebras in the varieties they generate, and
relative axiomatization results.
 RS0120

PostScript,
PDF,
DVI.
Catuscia Palamidessi and Frank D.
Valencia.
A Temporal Concurrent Constraint Programming Calculus.
June 2001.
31 pp. Appears in Walsh, editor, 7th International Conference on
Principles and Practice of Constraint Programming, CP '01 Proceedings,
LNCS 2239, 2001, pages 302316.
Abstract: The tcc model is a formalism for reactive concurrent
constraint programming. In this paper we propose a model of temporal
concurrent constraint programming which adds to tcc the capability of
modeling asynchronous and nondeterministic timed behavior. We call this tcc
extension the ntcc calculus. The expressiveness of ntcc is illustrated by
modeling cells and asynchronous bounded broadcasting, by specifying temporal
requirements such as response and invariance, and by modeling timed systems
such as RCX controllers. We present a denotational semantics for modeling the
strongestpostcondition behavior of ntcc processes, and, based on this
semantics, we develop a proof system for proving linear temporal properties
of these processes.
 RS0119

PostScript,
PDF,
DVI.
Jirí Srba.
On the Power of Labels in Transition Systems.
June 2001.
23 pp. Full and extended version of Larsen and Nielsen, editors, Concurrency Theory: 12th International Conference, CONCUR '01 Proceedings,
LNCS 2154, 2001, pages 277291.
Abstract: In this paper we discuss the role of labels in
transition systems with regard to bisimilarity and model checking problems.
We suggest a general reduction from labelled transition systems to unlabelled
ones, preserving bisimilarity and satisfiability of mucalculus formulas. We
apply the reduction to the class of transition systems generated by Petri
nets and pushdown automata, and obtain several decidability/complexity
corollaries for unlabelled systems. Probably the most interesting result is
undecidability of strong bisimilarity for unlabelled Petri nets.
 RS0118

PostScript,
PDF.
Katalin M. Hangos, Zsolt Tuza, and Anders
Yeo.
Some Complexity Problems on Single Input Double Output
Controllers.
May 2001.
27 pp.
Abstract: We investigate the time complexity of constructing
single input double output state feedback controller structures, given the
directed structure graph of a system. Such a controller structure defines
a restricted type of partition of the graph . A necessary condition
has been found and two classes of graphs have been identified where the
search problem of finding a feasible partition is polynomially solvable
and, in addition, is not only necessary but also sufficient for the
existence of a partition. It is shown further that the decision problem
on two particular graph classes  defined in terms of forbidden subgraphs
 remains NPcomplete, but is polynomially solvable on the
intersection of those two classes. Moreover, for every natural number , a
stabilizing structure with Single Input Output controllers can be found
in polynomial time for the system in question, if it admits one.
 RS0117

PostScript,
PDF.
Claus Brabrand, Anders Møller, Steffan
Olesen, and Michael I. Schwartzbach.
LanguageBased Caching of Dynamically Generated HTML.
May 2001.
18 pp. Appears in World Wide Web Journal, 5(4):305323, 2002.
Abstract: Increasingly, HTML documents are dynamically
generated by interactive Web services. To ensure that the client is presented
with the newest versions of such documents it is customary to disable client
caching causing a seemingly inevitable performance penalty. In the
<bigwig> system, dynamic HTML documents are composed of higherorder
templates that are plugged together to construct complete documents. We show
how to exploit this feature to provide an automatic finegrained caching of
document templates, based on the service source code. A <bigwig>
service transmits not the full HTML document but instead a compact JavaScript
recipe for a clientside construction of the document based on a static
collection of fragments that can be cached by the browser in the usual
manner. We compare our approach with related techniques and demonstrate on a
number of realistic benchmarks that the size of the transmitted data and the
latency may be reduced significantly.
 RS0116

PostScript,
PDF,
DVI.
Olivier Danvy, Morten Rhiger, and
Kristoffer H. Rose.
Normalization by Evaluation with Typed Abstract Syntax.
May 2001.
9 pp. Appears in Journal of Functional Programming,
11(6):67368, November 2000.
Abstract: We present a simple way to implement typed abstract
syntax for the lambda calculus in Haskell, using phantom types, and we
specify normalization by evaluation (i.e., typedirected partial evaluation)
to yield this typed abstract syntax. Proving that normalization by evaluation
preserves types and yields normal forms then reduces to typechecking the
specification.
 RS0115

PostScript,
PDF,
DVI.
Luigi Santocanale.
A Calculus of Circular Proofs and its Categorical Semantics.
May 2001.
30 pp. Appears in Nielsen and Engberg, editors, Foundations of
Software Science and Computation Structures, FoSSaCS '02 Proceedings,
LNCS 2303, 2002, pages 129143.
Abstract: We present a calculus of proofs, the intended models
of which are categories with finite products and coproducts, initial algebras
and final coalgebras of functors that are recursively constructible out of
these operations, that is, bicomplete categories. The calculus
satisfies the cut elimination and its main characteristic is that the
underlying graph of a proof is allowed to contain a certain amount of cycles.
To each proof of the calculus we associate a system of equations which has a
meaning in every bicomplete category. We prove that this system admits
always a unique solution, and by means of this theorem we define the
semantics of the calculus.
 RS0114

PostScript,
PDF,
DVI.
Ulrich Kohlenbach and Paulo B. Oliva.
Effective Bounds on Strong Unicity in Approximation.
May 2001.
38 pp. A revised and numerically much improved version appeared in
Annals of Pure and Applied Logic, 121:138, 2003. Extended extended
abstract appears in Hofmann, editor, 3rd International Workshop on
Implicit Computational Complexity, ICC '01 Proceedings, BRICS Notes
Series NS013, 2001, pages 117122.
Abstract: In this paper we present another case study in the
general project of Proof Mining which means the logical analysis of prima
facie noneffective proofs with the aim of extracting new computationally
relevant data. We use techniques based on monotone functional interpretation
(developed by the first author) to analyze Cheney's simplification from 1965
of Jackson's original proof from 1921 of the uniqueness of the best
approximation of continuous functions by polynomials
of degree . Cheney's proof is noneffective in the sense
that it is based on classical logic and on the noncomputational principle
WKL (binary König Lemma). The result of our analysis provides the first
effective (in all parameters and ) uniform modulus of
uniqueness (a concept which generalizes `strong uniqueness' studied
extensively in approximation theory). Moreover, the extracted modulus has the
optimal dependency as follows from Kroo 78. The paper also
describes how the uniform modulus of uniqueness can be used to compute the
best approximations of a fixed with arbitrary precision,
and includes some remarks on the case of best Chebycheff approximation.
 RS0113

PostScript,
PDF,
DVI.
Federico Crazzolara and Glynn Winskel.
Events in Security Protocols.
April 2001.
30 pp. Appears in 8th ACM conference on Computer and
Communications Security, CCS '01 Proceedings, 2001, pages 96105.
Abstract: The events of a security protocol and their causal
dependency can play an important role in the analysis of security properties.
This insight underlies both strand spaces and the inductive method. But
neither of these approaches builds up the events of a protocol in a
compositional way, so that there is an informal spring from the protocol to
its model. By broadening the models to certain kinds of Petri nets, a
restricted form of contextual nets, a compositional eventbased semantics is
given to an economical, but expressive, language for describing security
protocols; so the events and dependency of a wide range of protocols are
determined once and for all. The net semantics is formally related to a
transition semantics, strand spaces and inductive rules, as well as trace
languages and event structures, so unifying a range of approaches, as well as
providing conditions under which particular, more limited, models are
adequate for the analysis of protocols. The net semantics allows the
derivation of general properties and proof principles which are demonstrated
in establishing an authentication property, following a diagrammatic style of
proof.
 RS0112

PostScript,
PDF,
DVI.
Torben Amtoft, Charles Consel, Olivier
Danvy, and Karoline Malmkjær.
The Abstraction and Instantiation of StringMatching Programs.
April 2001.
37 pp. Appears in Mogensen, Schmidt and Sudborough, editors, The
Essence of Computation: Complexity, Analysis, Transformation, LNCS 2556,
2002, pages 332357.
Abstract: We consider a naive, quadratic string matcher testing
whether a pattern occurs in a text, we equip it with a cache mediating its
access to the text, and we abstract the traversal policy of the pattern, the
cache, and the text. We then specialize this abstracted program with respect
to a pattern, using the offtheshelf partial evaluator Similix.
Instantiating the abstracted program with a lefttoright traversal policy
yields the lineartime behavior of Knuth, Morris and Pratt's string matcher.
Instantiating it with a righttoleft policy yields the lineartime behavior
of Boyer and Moore's string matcher.
 RS0111

PostScript,
PDF.
Alexandre David and M. Oliver Möller.
From HUPPAAL to UPPAAL: A Translation from
Hierarchical Timed Automata to Flat Timed Automata.
March 2001.
40 pp. Appears in Kutsche and Weber, editors, Fundamental
Approaches to Software Engineering: Fifth International Conference,
FASE '02 Proceedings, LNCS 2306, 2002, pages 218232, with the title Formal Verification of UML Statecharts with RealTime Extensions.
Abstract: We present a hierarchical version of timed automata,
equipped with data types, handshake synchronization, and local variables. We
describe the formal semantics of this hierarchical timed automata (HTA)
formalism in terms of a transition system.
We report on the
implementation of a flattening algorithm, that translates our formalism to a
network of UPPAAL timed automata. We establish a correspondence between
symbolic states of an HTA and its translations, and thus are able to make use
of UPPAAL's simulator and model checking engine.
This technique
is exemplified with a cardiac pacemaker model. Here, the overhead introduced
by the translation is tolerable. We give runtime data for deadlock checking,
timed reachability, and timed response analysis.
 RS0110

PostScript,
PDF,
DVI.
Daniel Fridlender and Mia Indrika.
Do we Need Dependent Types?
March 2001.
6 pp. Appears in Journal of Functional Programming,
10(4):409415, 2000. Superseeds BRICS Report RS9838.
Abstract: Inspired by Danvy, we describe a technique for
defining, within the HindleyMilner type system, some functions which seem to
require a language with dependent types. We illustrate this by giving a
general definition of zipWith for which the Haskell library provides a
family of functions, each member of the family having a different type and
arity. Our technique consists in introducing ad hoc codings for natural
numbers which resemble numerals in calculus.
 RS019

PostScript,
PDF.
Claus Brabrand, Anders Møller, and
Michael I. Schwartzbach.
Static Validation of Dynamically Generated HTML.
February 2001.
18 pp. Appears in Field and Snelting, editors, ACM
SIGPLANSIGSOFT Workshop on Program Analysis For Software Tools and
Engineering, PASTE '01 Proceedings, 2001, pages 3845.
Abstract: We describe a static analysis of <bigwig>
programs that efficiently decides if all dynamically computed XHTML documents
presented to the client will validate according to the official DTD. We
employ two interprocedural flow analyses to construct a graph summarizing the
possible documents. This graph is subsequently analyzed to determine validity
of those documents.
 RS018

PostScript,
PDF.
Ulrik Frendrup and Jesper Nyholm Jensen.
Checking for Open Bisimilarity in the Calculus.
February 2001.
61 pp.
Abstract: This paper deals with algorithmic checking of open
bisimilarity in the calculus. Most bisimulation checking algorithms are
based on the partition refinement approach. Unfortunately the definition of
open bisimulation does not permit us to use a partition refinement approach
for open bisimulation checking directly, but in the paper A Partition
Refinement Algorithm for the Calculus Marco Pistore and Davide
Sangiogi present an iterative method that makes it possible to check for open
bisimilarity using partition refinement. We have implemented the algorithm
presented by Marco Pistore and Davide Sangiorgi. Furthermore, we have
optimized this algorithm and implemented this optimized algorithm. The
timecomplexity of this algorithm is the same as the timecomplexity for the
first algorithm, but performance tests have shown that in many cases the
running time of the optimized algorithm is shorter than the running time of
the first algorithm.
Our implementation of the optimized open
bisimulation checker algorithm and a user interface have been integrated in a
system called the OBC Workbench. The source code and a manual for it is
available from www.cs.auc.dk/research/FS/ny/PRpi/.
 RS017

PostScript,
PDF,
DVI.
Gregory Gutin, Khee Meng Koh, Eng Guan
Tay, and Anders Yeo.
On the Number of QuasiKernels in Digraphs.
January 2001.
11 pp.
Abstract: A vertex set of a digraph is a kernel if is independent (i.e., all pairs of distinct vertices of
are nonadjacent) and for every there exists such that
. A vertex set of a digraph is a quasikernel if
is independent and for every there exist
such that either or In 1994, Chvátal and
Lovász proved that every digraph has a quasikernel. In 1996, Jacob and
Meyniel proved that, if a digraph has no kernel, then contains at
least three quasikernels. We characterize digraphs with exactly one and two
quasikernels, and, thus, provide necessary and sufficient conditions for a
digraph to have at least three quasikernels. In particular, we prove that
every strong digraph of order at least three, which is not a 4cycle, has at
least three quasikernels. We conjecture that every digraph with no sink has
a pair of disjoint quasikernels and provide some support to this conjecture.
 RS016

PostScript,
PDF,
DVI.
Gregory Gutin, Anders Yeo, and Alexey
Zverovich.
Traveling Salesman Should not be Greedy: Domination Analysis of
GreedyType Heuristics for the TSP.
January 2001.
7 pp.
Abstract: Computational experiments show that the greedy
algorithm (GR) and the nearest neighbor algorithm (NN), popular choices for
tour construction heuristics, work at acceptable level for the Euclidean TSP,
but produce very poor results for the general Symmetric and Asymmetric TSP
(STSP and ATSP). We prove that for every there is an instance of
ATSP (STSP) on vertices for which GR finds the worst tour. The same
result holds for NN. We also analyze the repetitive NN (RNN) that starts NN
from every vertex and chooses the best tour obtained. We prove that, for the
ATSP, RNN always produces a tour, which is not worse than at least
other tours, but for some instance it finds a tour, which is not worse than
at most other tours, . We also show that, for some instance of
the STSP on vertices, RNN produces a tour not worse than at most
tours. These results are in sharp contrast to earlier results by G.
Gutin and A. Yeo, and A. Punnen and S. Kabadi, who proved that, for the ATSP,
there are tour construction heuristics, including some popular ones, that
always build a tour not worse than at least tours.
 RS015

PostScript,
PDF.
Thomas S. Hune, Judi Romijn, Mariëlle
Stoelinga, and Frits W. Vaandrager.
Linear Parametric Model Checking of Timed Automata.
January 2001.
44 pp. Appears in Margaria and Yi, editors, Tools and Algorithms
for The Construction and Analysis of Systems: 7th International Conference,
TACAS '01 Proceedings, LNCS 2031, 2001, pages 174188.
Abstract: We present an extension of the model checker
UPPAAL capable of synthesize linear parameter constraints for the
correctness of parametric timed automata. The symbolic representation of the
(parametric) statespace is shown to be correct. A second contribution of
this paper is the identification of a subclass of parametric timed automata
(L/U automata), for which the emptiness problem is decidable, contrary to the
full class where it is know to be undecidable. Also we present a number of
lemmas enabling the verification effort to be reduced for L/U automata in
some cases. We illustrate our approach by deriving linear parameter
constraints for a number of wellknown case studies from the literature
(exhibiting a flaw in a published paper).
 RS014

PostScript,
PDF.
Gerd Behrmann, Ansgar Fehnker, Thomas S.
Hune, Kim G. Larsen, Paul Pettersson, and Judi Romijn.
Efficient Guiding Towards CostOptimality in UPPAAL.
January 2001.
21 pp. Appears in Margaria and Yi, editors, Tools and Algorithms
for The Construction and Analysis of Systems: 7th International Conference,
TACAS '01 Proceedings, LNCS 2031, 2001, pages 174188.
Abstract: In this paper we present an algorithm for efficiently
computing the minimum cost of reaching a goal state in the model of Uniformly
Priced Timed Automata (UPTA). This model can be seen as a submodel of the
recently suggested model of linearly priced timed automata, which extends
timed automata with prices on both locations and transitions. The presented
algorithm is based on a symbolic semantics of UTPA, and an efficient
representation and operations based on difference bound matrices. In analogy
with Dijkstra's shortest path algorithm, we show that the search order of the
algorithm can be chosen such that the number of symbolic states explored by
the algorithm is optimal, in the sense that the number of explored states can
not be reduced by any other search order. We also present a number of
techniques inspired by branchandbound algorithms which can be used for
limiting the search space and for quickly finding nearoptimal
solutions.
The algorithm has been implemented in the verification tool
Uppaal. When applied on a number of experiments the presented techniques
reduced the explored statespace with up to 90%.
 RS013

PostScript,
PDF.
Gerd Behrmann, Ansgar Fehnker, Thomas S.
Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits W. Vaandrager.
MinimumCost Reachability for Priced Timed Automata.
January 2001.
22 pp. Appears in Di Benedetto and SangiovanniVincentelli, editors,
Hybrid Systems: Computation and Control, Fourth International Workshop,
HSCC '01 Proceedings, LNCS 2034, 2001, 147161.
Abstract: This paper introduces the model of linearly priced
timed automata as an extension of timed automata, with prices on both
transitions and locations. For this model we consider the minimumcost
reachability problem: i.e. given a linearly priced timed automaton and a
target state, determine the minimum cost of executions from the initial state
to the target state. This problem generalizes the minimumtime reachability
problem for ordinary timed automata. We prove decidability of this problem by
offering an algorithmic solution, which is based on a combination of
branchandbound techniques and a new notion of priced regions. The latter
allows symbolic representation and manipulation of reachable states together
with the cost of reaching them.
 RS012

PostScript,
PDF,
DVI.
Rasmus Pagh and Jakob Pagter.
Optimal TimeSpace TradeOffs for NonComparisonBased Sorting.
January 2001.
ii+20 pp. Appears in Eppstein, editor, The Thirteenths Annual
ACMSIAM Symposium on Discrete Algorithms, SODA '02 Proceedings, 2002,
pages 918.
Abstract: We study the fundamental problem of sorting
integers of bits on a unitcost RAM with word size , and in particular
consider the timespace tradeoff (product of time and space in bits) for
this problem. For comparisonbased algorithms, the timespace complexity is
known to be . A result of Beame shows that the lower bound also
holds for noncomparisonbased algorithms, but no algorithm has met this for
time below the comparisonbased
lower bound.
We show
that if sorting within some time bound is possible, then time
can be achieved with high probability using space
, which is optimal. Given a deterministic priority queue using
amortized time per operation and space , we provide a
deterministic algorithm sorting in time
with
. Both results require that
. Using
existing priority queues and sorting algorithms, this implies that we can
deterministically sort timespace optimally in time for
, and with high probability for
.
Our
results imply that recent lower bounds for deciding element distinctness in
time are nearly tight.
 RS011

PostScript,
PDF,
DVI.
Gerth Stølting Brodal, Rolf Fagerberg,
Christian N. S. Pedersen, and Anna Östlin.
The Complexity of Constructing Evolutionary Trees Using
Experiments.
January 2001.
28 pp. Appears in Orejas, Spirakis and Leeuwen, editors, 28th
International Colloquium on Automata, Languages, and Programming,
ICALP '01 Proceedings, LNCS 2076, 2001, pages 140151.
Abstract: We present a tight upper and lower bound for
constructing evolutionary trees using experiments. We present an algorithm
which constructs an evolutionary tree of species using experiments in
time , where is the degree of the constructed tree. We
show by an explicit adversary argument that any algorithm for constructing an
evolutionary tree of species using experiments must perform
experiments, where is the degree of the constructed tree.
