@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-94-48, author = "Godskesen, Jens Chr{.} and Larsen, Kim G.", title = "Synthesizing Distinguishing Formulae for Real Time Systems", institution = brics, year = 1994, type = rs, number = "RS-94-48", address = iesd, month = dec, note = "21~pp. Extended abstract appears in " # lncs969 # ", pages 519--528", abstract = "This paper describes a technique for generating diagnostic information for the {\sl timed} bisimulation equivalence and the {\sl timed} simulation preorder. More precisely, given two (parallel) networks of regular real--time processes, the technique will provide a logical formula that differentiates them in case they are not timed (bi)similar. Our method may be seen as an extension of the algorithm by {\v C}er{\=a}ns for deciding timed bisimilarity in that information of time--quantities has been added sufficient for generating distinguishing formulae. The technique has been added to the automatic verification tool {\sc Epsilon} and applied to various examples.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-47, author = "Larsen, Kim G. and Steffen, Bernhard and Weise, Carsten", title = "A Constraint Oriented Proof Methodology based on Modal Transition Systems", institution = brics, year = 1994, type = rs, number = "RS-94-47", address = iesd, month = dec, note = "13 pp", abstract = "In this paper, we present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are {\em projective views}, {\em separation of proof obligations}, {\em Skolemization} and {\em abstraction}. The method is even applicable to real time systems.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-46, author = "Beimel, Amos and G{\'a}l, Anna and Paterson, Mike", title = "Lower Bounds for Monotone Span Programs", institution = brics, year = 1994, type = rs, number = "RS-94-46", address = daimi, month = dec, note = "14~pp. Appears in " # ieeefocs95 # ", pages 674--681", abstract = "The model of span programs is a linear algebraic model of computation. Lower bounds for span programs imply lower bounds for contact schemes, symmetric branching programs and for formula size. Monotone span programs correspond also to linear secret-sharing schemes. We present a new technique for proving lower bounds for monotone span programs. The main result proved here yields quadratic lower bounds for the size of monotone span programs, improving on the largest previously known bounds for explicit functions. The bound is asymptotically tight for the function corresponding to a class of 4-cliques.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-45, author = "Andersen, J{\o}rgen H. and Kristoffersen, K{\aa}re J. and Larsen, Kim G. and Niedermann, Jesper", title = "Automatic Synthesis of Real Time Systems", institution = brics, year = 1994, type = rs, number = "RS-94-45", address = iesd, month = dec, note = "17 pp. Appears in " # lncs944 # ", pages 535--546", abstract = "This paper presents a method for automatically constructing real time systems directly from their specifications. The model--construction problem is considered for implicit specifications of the form: \[ (A_1\,{\mid }\,\ldots\,{\mid}\,A_n\,{\mid}\,X) \,\,\mbox {{\sf sat}}\,\, S \] where $S$ is a real time (logical) specification, $A_1\ldots A_n$ are given (regular) timed agents and the problem is to decide whether there exists (and if possible exhibit) a real time agent $X$ which when put in parallel with $A_1\ldots A_n$ will yield a network satisfying $S$. The method presented proceeds in two steps: first, the implicit specification of $X$ is transformed into an equivalent direct specification of $X$; second, a model for this direct specification is constructed (if possible) using a direct model construction algorithm. A prototype implementation of our method has been added to the real time verification tool EPSILON.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-94-44, author = "Agerholm, Sten", title = "A {HOL} Basis for Reasoning about Functional Programs", institution = brics, year = 1994, type = rs, number = "RS-94-44", address = daimi, month = dec, note = "PhD thesis. viii+224 pp", abstract = "Domain theory is the mathematical theory underlying denotational semantics. This thesis presents a formalization of domain theory in the Higher Order Logic (HOL) theorem proving system along with a mechanization of proof functions and other tools to support reasoning about the denotations of functional programs. By providing a fixed point operator for functions on certain domains which have a special undefined (bottom) element, this extension of HOL supports the definition of recursive functions which are not also primitive recursive. Thus, it provides an approach to the long-standing and important problem of defining non-primitive recursive functions in the HOL system.\bibpar Our philosophy is that there must be a direct correspondence between elements of complete partial orders (domains) and elements of HOL types, in order to allow the reuse of higher order logic and proof infrastructure already available in the HOL system. Hence, we are able to mix domain theoretic reasoning with reasoning in the set theoretic HOL world to advantage, exploiting HOL types and tools directly. Moreover, by mixing domain and set theoretic reasoning, we are able to eliminate almost all reasoning about the bottom element of complete partial orders that makes the LCF theorem prover, which supports a first order logic of domain theory, difficult and tedious to use. A thorough comparison with LCF is provided.\bibpar The advantages of combining the best of the domain and set theoretic worlds in the same system are demonstrated in a larger example, showing the correctness of a unification algorithm. A major part of the proof is conducted in the set theoretic setting of higher order logic, and only at a late stage of the proof domain theory is introduced to give a recursive definition of the algorithm, which is not primitive recursive. Furthermore, a total well-founded recursive unification function can be defined easily in pure HOL by proving that the unification algorithm (defined in domain theory) always terminates; this proof is conducted by a non-trivial well-founded induction. In such applications, where non-primitive recursive HOL functions are defined via domain theory and a proof of termination, domain theory constructs only appear temporarily.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-94-43, author = "Aceto, Luca and Jeffrey, Alan~S.~A.", title = "A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours (Revised Version)", institution = brics, year = 1994, type = rs, number = "RS-94-43", address = iesd, month = dec, note = "18 pp. Appears in {\em Theoretical Computer Science} vol.~152(2) pages 251--268, December 1995", abstract = "One of the most satisfactory results in process theory is Milner's axiomatization of strong bisimulation for regular CCS. This result holds for open terms with finite-state recursion. Wang has shown that timed bisimulation can also be axiomatized, but only for closed terms without recursion. In this paper, we provide an axiomatization for timed bisimulation of open terms with finite-state recursion.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-42, author = "Breslauer, Dany and G{\c{a}}sieniec, Leszek", title = "Efficient String Matching on Coded Texts", institution = brics, year = 1994, type = rs, number = "RS-94-42", address = daimi, month = dec, note = "20 pp. Appears with the title {\em Efficient String Matching on Packed Texts} in " # lncs937 # ", pages 27--40 and in {\em RAIRO Informatique Th{\'e}orique et Applications}, 30(6):521--544, 1996", abstract = "The so called ``four Russians technique'' is often used to speed up algorithms by encoding several data items in a single memory cell. Given a sequence of $n$ symbols over a constant size alphabet, one can encode the sequence into $O(n / \lambda)$ memory cells in $O(\log\lambda )$ time using $n / \log\lambda$ processors.\bibpar This paper presents an efficient CRCW-PRAM string-matching algorithm for coded texts that takes $O(\log\log(m/\lambda))$ time making only $O(n / \lambda)$ operations, an improvement by a factor of $\lambda= O(\log n)$ on the number of operations used in previous algorithms. Using this string-matching algorithm one can test if a string is square-free and find all palindromes in a string in $O(\log\log n)$ time using $n / \log\log n$ processors.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-41, author = "Miltersen, Peter Bro and Nisan, Noam and Safra, Shmuel and Wigderson, Avi", title = "On Data Structures and Asymmetric Communication Complexity", institution = brics, year = 1994, type = rs, number = "RS-94-41", address = daimi, month = dec, note = "17 pp. Appears in " # acmstoc95 # ", pages 103--111. Appears also in {\em Journal of Computer and System Sciences}, 57(1):37--49, 1998", abstract = "In this paper we consider two party communication complexity when the input sizes of the two players differ significantly, the ``asymmetric'' case. Most of previous work on communication complexity only considers the total number of bits sent, but we study tradeoffs between the number of bits the first player sends and the number of bits the second sends. These types of questions are closely related to the complexity of static data structure problems in the cell probe model. We derive two generally applicable methods of proving lower bounds, and obtain several applications. These applications include new lower bounds for data structures in the cell probe model. Of particular interest is our ``round elimination'' lemma, which is interesting also for the usual symmetric communication case. This lemma generalizes and abstracts in a very clean form the ``round reduction'' techniques used in many previous lower bound proofs.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-40, author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna", title = "{CPO} Models for {GSOS} Languages --- Part {I}: Compact {GSOS} Languages", institution = brics, year = 1994, type = rs, number = "RS-94-40", address = iesd, month = dec, note = "70 pp. An extended abstract of the paper appears in: {\em Proceedings of CAAP~'95}, LNCS 915, 1995, pages 439--453. Full version also appears in {\em Information and Computation}, 129(2):107--141, September 1996.", abstract = "In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail and Meyer. The canonical model used for this purpose will be Abramsky's domain of synchronization trees, and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder. In the process of establishing the full abstraction result, we also obtain several general results on the bisimulation preorder (including a complete axiomatization for it), and give a novel operational interpretation of GSOS languages", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-39, author = "Damg{\aa}rd, Ivan B. and Goldreich, Oded and Wigderson, Avi", title = "Hashing Functions can Simplify Zero-Knowledge Protocol Design (too)", institution = brics, year = 1994, type = rs, number = "RS-94-39", address = daimi, month = nov, note = "18 pp", abstract = "In {\em Crypto93}, Damg{\aa}rd showed that any constant-round protocol in which the verifier sends only independent, random bits and which is zero-knowledge against the {\em honest} verifier can be transformed into a protocol (for the same problem) that is zero-knowledge {\em in general}. His transformation was based on the interactive hashing technique of Naor, Ostrovsky, Venkatesan and Yung, and thus the resulting protocol had very large round-complexity.\bibpar We adopt Damg{\aa}rd's methods, using ordinary hashing functions, instead of the abovementioned interactive hashing technique. Typically, the protocols we derive have much lower round-complexity than those derived by Damg{\aa}rd's transformation. As in Damg{\aa}rd's transformation, our transformation preserves statistical/perfect zero-knowledge and does not rely on any computational assumptions. However, unlike Damg{\aa}rd's transformation, the new transformation is not applicable to argument systems or to proofs of knowledge", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-38, author = "Damg{\aa}rd, Ivan B. and Knudsen, Lars Ramkilde", title = "Enhancing the Strength of Conventional Cryptosystems", institution = brics, year = 1994, type = rs, number = "RS-94-38", address = daimi, month = nov, note = "12 pp", abstract = "We look at various ways of enhancing the strength of conventional cryptosystems such as DES by building a new system which has longer keys and which uses the original system as a building block. We propose a new variant of two-key triple encryption which is not vulnerable to the meet in the middle attack by van Oorschot and Wiener. Under an appropriate assumption on the security of DES, we can prove that our system is at least as hard to break as single DES", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-37, author = "van Oosten, Jaap", title = "Fibrations and Calculi of Fractions", institution = brics, year = 1994, type = rs, number = "RS-94-37", address = daimi, month = nov, note = "21 pp. Appears in {\em Journal of Pure and Applied}, 146(1):77--102, 2000", abstract = "Given a fibration ${\cal E}\rightarrow\cal B$ and a class $\Sigma$ of arrows of $\cal B$, one can construct the free fibration (on $\cal E$ over $\cal B$ such that all reindexing functors over elements of $\Sigma$ are equivalences.\bibpar In this work I give an explicit construction of this, and study its properties. For example, the construction preserves the property of being fibrewise discrete, and it commutes up to equivalence with fibrewise exact completions. I show that mathematically interesting situations are examples of this construction. In particular, subtoposes of the effective topos are treated.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-36, author = "Razborov, Alexander A.", title = "On provably disjoint {{\bf NP}}-pairs", institution = brics, year = 1994, type = rs, number = "RS-94-36", address = daimi, month = nov, note = "27 pp", abstract = "In this paper we study the pairs $(U,V)$ of disjoint {\bf NP}-sets representable in a theory $T$ of Bounded Arithmetic in the sense that $T$ proves $U \cap V = \emptyset$. For a large variety of theories $T$ we exhibit a natural disjoint {\bf NP}-pair which is complete for the class of disjoint {\bf NP}-pairs representable in $T$. This allows us to clarify the approach to showing independence of central open questions in Boolean complexity from theories of Bounded Arithmetic initiated in [1]. Namely, in order to prove the independence result from a theory $T$, it is sufficient to separate the corresponding complete {\bf NP}-pair by a (quasi)poly-time computable set. We remark that such a separation is obvious for the theory ${\cal S}(S_2) + {\cal S}\Sigma^b_2 - PIND$ considered in [1], and this gives an alternative proof of the main result from that paper.\bibpar [1] A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of Bounded Arithmetic. To appear in {\em Izvestiya of the RAN}, 1994. ", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-35, author = "Brodal, Gerth St{\o}lting", title = "Partially Persistent Data Structures of Bounded Degree with Constant Update Time", institution = brics, year = 1994, type = rs, number = "RS-94-35", address = daimi, month = nov, note = "24~pp. Appears in {\em Nordic Journal of Computing}, 3(3):238--255, 1996", abstract = "The problem of making bounded in-degree and out-degree data structures partially persistent is considered. The node copying method of Driscoll {\it et al.\/} is extended so that updates can be performed in {\em worst-case\/} constant time on the pointer machine model. Previously it was only known to be possible in amortised constant time [Driscoll89]. The result is presented in terms of a new strategy for Dietz and Raman's dynamic two player pebble game on graphs. It is shown how to implement the strategy and the upper bound on the required number of pebbles is improved from $2b+2d+O(\sqrt{b})$ to $d+2b$, where $b$ is the bound of the in-degree and $d$ the bound of the out-degree. We also give a lower bound that shows that the number of pebbles depends on the out-degree $d$.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-94-34, author = "Andersen, Henrik Reif and Stirling, Colin and Winskel, Glynn", title = "A Compositional Proof System for the Modal $\mu$-Calculus", institution = brics, year = 1994, type = rs, number = "RS-94-34", address = daimi, month = oct, note = "18~pp. Appears in " # lics9 # ", pages 144--153. Superseeded by BRICS Report RS-98-40", abstract = "We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal $\mu$-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal $\mu$-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-33, author = "Sassone, Vladimiro", title = "Strong Concatenable Processes: An Approach to the Category of Petri Net Computations", institution = brics, year = 1994, type = rs, number = "RS-94-33", address = daimi, month = oct, note = "40 pp. Workshop version appears in " # nwpt6 # ", pages 385--399 with the title {\em An Approach to the Category of Net Computations}. Revised version appears in " # lncs915 # ", pages 334--348 with the title {\em On the Category of {P}etri Net Computations}", abstract = "We introduce the notion of {\it strong concatenable process\/} for Petri nets as the least refinement of non-sequential (concatenable) processes which can be expressed abstractly by means of a {\it functor\/} ${\cal Q}[\_]$ from the category of Petri nets to an appropriate category of symmetric strict monoidal categories with free non-commutative monoids of objects, in the precise sense that, for each net~$N$, the strong concatenable processes of~$N$ are isomorphic to the arrows of~${\cal Q}[N]$. This yields an axiomatization of the causal behaviour of Petri nets in terms of symmetric strict monoidal categories.\bibpar In addition, we identify a {\it coreflection\/} right adjoint to ${\cal Q}[\_]$ and we characterize its replete image in the category of symmetric monoidal categories, thus yielding an abstract description of the category of net computations", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-32, author = "Aiken, Alexander and Kozen, Dexter and Wimmers, Ed", title = "Decidability of Systems of Set Constraints with Negative Constraints", institution = brics, year = 1994, type = rs, number = "RS-94-32", address = daimi, month = oct, note = "33 pp. Appears in {\em Information and Computation}, 122(1):30-44, October 1995", abstract = "Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general systems of positive set constraints have appeared. In this paper we consider systems of mixed positive and negative constraints, which are considerably more expressive than positive constraints alone. We show that it is decidable whether a given such system has a solution. The proof involves a reduction to a number-theoretic decision problem that may be of independent interest.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-31, author = "Nisan, Noam and Ta-Shma, Amnon", title = "Symmetric Logspace is Closed Under Complement", institution = brics, year = 1994, type = rs, number = "RS-94-31", address = daimi, month = sep, note = "8 pp", abstract = "We present a Logspace, many-one reduction from the undirected st-connectivity problem to its complement. This shows that $SL = co - SL$", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-30, author = "Husfeldt, Thore", title = "Fully Dynamic Transitive Closure in Plane Dags with one Source and one Sink", institution = brics, year = 1994, type = rs, number = "RS-94-30", address = daimi, month = sep, note = "26 pp. Appears in " # lncs979 # ", pages 199--212", abstract = "We give an algorithm for the Dynamic Transitive Closure Problem for planar directed acyclic graphs with one source and one sink. The graph can be updated in logarithmic time under arbitrary edge insertions and deletions that preserve the embedding. Queries of the form `is there a directed path from $u$ to $v$?' for arbitrary vertices $u$ and $v$ can be answered in logarithmic time. The size of the data structure and the initialisation time are linear in the number of edges.\bibpar The result enlarges the class of graphs for which a logarithmic (or even polylogarithmic) time dynamic transitive closure algorithm exists. Previously, the only algorithms within the stated resource bounds put restrictions on the topology of the graph or on the delete operation. To obtain our result, we use a new characterisation of the transitive closure in plane graphs with one source and one sink and introduce new techniques to exploit this characterisation.\bibpar We also give a lower bound of $\Omega(\log n/\log\log n)$ on the amortised complexity of the problem in the cell probe model with logarithmic word size. This is the first dynamic directed graph problem with almost matching lower and upper bounds.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-RS-94-29, author = "Cramer, Ronald and Damg{\aa}rd, Ivan B.", title = "Secure Signature Schemes Based on Interactive Protocols", institution = brics, year = 1994, type = rs, number = "RS-94-29", address = daimi, month = sep, note = "24~pp. Appears in " # lncs963 # ", pages 297--310", abstract = "A method is proposed for constructing from interactive protocols digital signature schemes secure against adaptively chosen message attacks. Our main result is that practical secure signature schemes can now also be based on computationally difficult problems other than factoring, such as the discrete logarithm problem.\bibpar More precisely, given only an interactive protocol of a certain type as a primitive, we can build a (non-interactive) signature scheme that is secure in the strongest sense of Goldwasser, Micali and Rivest (GMR): not existentially forgeable under adaptively chosen message attacks. There are numerous examples of primitives that satisfy our conditions, e.g. Feige-Fiat-Shamir, Schnorr, Guillou-Quisquater, Okamoto and Brickell-Mc.Curley.\bibpar In fact, the existence of one-way group homomorphisms is a sufficient assumption to support our construction. As we also demonstrate that our construction can be based on claw-free pairs of trapdoor one-way permutations, our results can be viewed as a generalization of the GMR signature scheme", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-28, author = "Goldreich, Oded", title = "Probabilistic Proof Systems", institution = brics, year = 1994, type = rs, number = "RS-94-28", address = "Department of Applied Mathematics and Computer Science, Weizmann Institute of Science, Rehovot, Israel", month = sep, note = "19 pp", abstract = "Various types of {\em probabilistic} proof systems have played a central role in the development of computer science in the last decade. In this exposition, we concentrate on three such proof systems --- {\em interactive proofs}, {\em zero-knowledge proofs}, and {\em probabilistic checkable proofs} --- stressing the essential role of randomness in each of them.\bibpar This exposition is an expanded version of a survey written for the proceedings of the International Congress of Mathematicians ({\em ICM94}) held in Zurich in 1994. It is hope that this exposition may be accessible to a broad audience of computer scientists and mathematians.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-27, author = "Bra{\"u}ner, Torben", title = "A Model of Intuitionistic Affine Logic from Stable Domain Theory (Revised and Expanded Version)", institution = brics, year = 1994, type = rs, number = "RS-94-27", address = daimi, month = sep, note = "19 pp. Full version of paper appearing in " # lncs820 # ", pages 340--351. This report is a revised and expanded version of DAIMI IR-118", abstract = "Girard worked with the category of coherence spaces and continuous stable maps and observed that the functor that forgets the linearity of linear stable maps has a left adjoint. This fundamental observation gave rise to the discovery of Linear Logic. Since then, the category of coherence spaces and linear stable maps, with the comonad induced by the adjunction, has been considered a canonical model of Linear Logic. Now, the same phenomenon is present if we consider the category of pre dI domains and continuous stable maps, and the category of dI domains and linear stable maps; the functor that forgets the linearity has a left adjoint. This gives an alternative model of Intuitionistic Linear Logic. It turns out that this adjunction can be factored in two adjunctions yielding a model of Intuitionistic Affine Logic; the category of pre dI domains and affine stable functions. It is the goal of this paper to show that this category is actually a model of Intuitionistic Affine Logic, and to show that this category moreover has properties which make it possible to use it to model convergence/divergence behaviour and recursion.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-26, author = "Riis, S{\o}ren", title = "Count($q$) versus the Pigeon-Hole Principle", institution = brics, year = 1994, type = rs, number = "RS-94-26", address = daimi, month = aug, note = "3 pp. Appears in {\em Archive for Mathematical Logic\/} 36(3):157--188 (1997) (expanded to a selfcontained paper)", abstract = "For each $p \leq 2$ there exist a model ${M\!\!I}^{*}$ of $I\Delta_{0}(\alpha)$ which satisfies the Count($p$) principle. Furthermore if $p$ contain all prime factors of $q$ there exist $n,r \in{M\!\!I}^{*}$ and a bijective map $f \in{\rm Set}({M\!\!I}^{*})$ mapping $\{1,2,...,n\}$ onto $\{1,2,...,n+q^{r}\}$. \bibpar A corollary is a complete classification of the Count($q$) versus Count($p$) problem. Another corollary solves an open question by M. Ajtai.", linkhtmlabs = "", linkdvi = "", linkps = "" } @techreport{BRICS-RS-94-25, author = "Riis, S{\o}ren", title = "Bootstrapping the Primitive Recursive Functions by 47 Colors", institution = brics, year = 1994, type = rs, number = "RS-94-25", address = daimi, month = aug, note = "5 pp. Improved version appears in {\em Decrete Mathematics} 169(1--3):269--272 (1997) under the title {\em Bootstrapping the Primitive Recursive Functions by Only 27 Colors}", abstract = "I construct a concrete coloring of the 3 element subsets of $I\!N$. It has the property that each homogeneous set $\{s_{1},s_{2},...,s_{u}\}, u \geq s_{1}$ has its elements spread so much apart that $F_{\omega}(s_{i})