waashk/dblp huggingface dataset:
towards imperative modules: reasoning about invariants and sharing of mutable state. imperative and object-oriented programs make ubiquitous use of shared mutable objects. updating a shared object can and often does transgress a boundary that was supposed to be established using static constructs such as a class with private fields. this paper shows how auxiliary fields can be used to express two state-dependent encapsulation disciplines: ownership, a kind of separation, and friendship, a kind of sharing. a methodology is given for specification and modular verification of encapsulated object invariants and shown sound for a class-based language. as an example the methodology is used to specify iterators, which are problematic for previous ownership systems.
logic of subtyping. we introduce new modal logical calculi that describe subtyping properties of cartesian product and disjoint union type constructors as well as mutually recursive types defined using those type constructors.basic logic of subtyping s extends classical propositional logic by two new binary modalities ⊗ and ⊕. an interpretation of s is a function that maps standard connectives into set-theoretical operations (intersection, union, and complement) and modalities into cartesian product and disjoint union type constructors. this allows s to capture many subtyping properties of the above type constructors. we also consider logics sρ and sρω that incorporate into s mutually recursive types over arbitrary and well-founded universes correspondingly.the main results are completeness of the above three logics with respect to appropriate type universes. in addition, we prove cut elimination theorem for s and establish decidability of s and sρω.
a metric index for approximate string matching. we present a radically new indexing approach for approximate string matching. the scheme uses the metric properties of the edit distance and can be applied to any other metric between strings. we build a metric space where the sites are the nodes of the suffix tree of the text, and the approximate query is seen as a proximity query on that metric space. this permits us finding the occ occurrences of a pattern of length m, permitting up to r differences, in a text of length n over an alphabet of size σ, in average time o(m1+ε + occ) for any ε > 0, if r = o(m/logσm) and m > ((1 + ε)/ε)logσ n. the index works well up to r < (3 - √2)m/logσm, where it achieves its maximum average search complexity o(m1+√2+ε + occ). the construction time of the index is o(m1+√2+ε nlog n) and its space is o(m1+√2+εn). this is the first index achieving average search time polynomial in m and independent of n, for r = o(m/logσm). previous methods achieve this complexity only for r = o(m/logσ n). we also present a simpler scheme needing o(n) space.
average complexity of exact and approximate multiple string matching. we show that the average number of characters examined to search for r random patterns of length m in a text of length n over a uniformly distributed alphabet of size σ cannot be less than ω(n logσ(rm)/m). when we permit up to k insertions, deletions, and/or substitutions of characters in the occurrences of the patterns, the lower bound becomes ω(n(k + logσ(rm))/m). this generalizes previous single-pattern lower bounds of yao (for exact matching) and of chang and marr (for approximate matching), and proves the optimality of several existing multipattern search algorithms.
exponential transient length generated by a neuronal recurrence equation. we study the sequences generated by neuronal recurrence equations of the form x(n) = 1[σj=1k ajx(n - j) - θ], where k is the size of memory (k represents the number of previous states x(n - 1), x(n - 2),...,x(n - k) which intervene in the calculation of x(n)). we are interested in the number of steps (transient length) from an initial configuration to the cycle, where the length of the cycle represents the period. we show that under certain hypotheses it is possible to build a neuronal recurrence equation of memory size (s + 1)6m, whose dynamics contains an evolution of transient length (s + 1)(3m + 1 + lcm(p0, p1,...,ps-1,3m-1)) and a cycle of length (s + 1) lcm(p0, p1,....,ps-1), where lcm denotes the least common multiple and p0, p1,....,ps-1 are prime numbers lying between 2m and 3m.
small fast universal turing machines. we present deterministic polynomial time universal turing machines (utms) with state-symbol pairs of (3, 11), (5, 7), (6, 6), (7, 5) and (8, 4). these are the smallest known utms that simulate turing machines in polynomial time.
the stack-size of tries: a combinatorial study. in this paper, we introduce a class of extended binary trees that resembles all possible tree-structures of binary tries. assuming a uniform distribution of those trees we prove that for being the number of internal nodes the average stack-size is given by . since this result is quite similar to that for ordinary extended binary trees an attempt to find an explanation for that similarity using a quantitative level is made.
fast string matching by using probabilities: on an optimal mismatch variant of horspool's algorithm. the string matching problem, i.e. the task of finding all occurrences of one string as a substring of another one, is a fundamental problem in computer science. recently, this problem received a great deal of attention due to numerous applications in computational biology. in this paper we address a modified version of horspool's string matching algorithm using the probabilities of the different symbols to speed up the search. we show that the modified algorithm has a linear average running time; a precise asymptotical representation of the running time will be proven. a comparison of the average running time of the modified algorithm with well-known results for the original method shows that a substantial speed up for most of the symbol distributions has been achieved. finally, we show that the distribution of the symbols can be approximated to a high precision using a random sample of sublinear size.
note on ramsey theorems for spatial graphs. to show that ramsey theorem for spatial graphs without local knots does not hold in general, we construct a spatial embedding of kn;n which has no local knots on edges and which contains any subdivision of a given nonsplittable 2-component link.
completing prefix codes in submonoids. let m be a submonoid of the free monoid a*, and let x ⊆ m be a variable length code (for short a code). x is weakly m-complete if any word in m is a factor of some word in x* [j. néraud, c. selmi, free monoid theory: maximality and completeness in arbitrary submonoids, internat. j. algorithms comput. 13(5) (2003) 507-516]. given a code x ⊆ m, we are interested in the construction of a weakly m-complete code that contains x, if it exists. in the case where m and x are regular sets, the existence of such a code has been established [j. néraud, completing a code in a regular submonoid of the free monoid, in acts of mcu'2004, lecture notes in computer sciences, vol. 3354, springer, berlin, 2005, pp. 281-291; j. néraud, on the completion of codes in submonoids with finite rank, fund. inform., to appear]. actually, this result lays upon a method of construction that preserves the regularity of sets. as well known, any regular (or finite) code may be embedded into a regular (finite) prefix code that is complete in a*: instance: a regular submonoid m of a*, and a regular (or finite) prefix code x ⊆ m. question: does a weakly m-complete regular (finite) prefix code containing x exist?
locally complete sets and finite decomposable codes. we are interested in the concept of locally complete set: a subset x of the free monoid is locally complete if a code y a exists, with y a, x y, and such that both the sets of xand y have the same sets of factors. our contribution is based on the three following results: * a characterization of local completeness for very thin sets in terms of morphic images. * a polynomial time algorithm for deciding whether a finite code is locally complete. * a polynomial time algorithm for deciding whether a finite maximal code is decomposable
density via duality. we present an unexpected correspondence between homomorphism duality theorems and gaps in the poset of graphs and their homomorphisms. this gives a new proof of the density theorem for undirected graphs and solves the density problem for directed graphs.
learning erasing pattern languages with queries. a pattern is a finite string of constant and variable symbols. the non-erasing language generated by a pattern is the set of all strings of constant symbols that can be obtained by substituting non-empty strings for variables. in order to build the erasing language generated by a pattern, it is also admissible to substitute the empty string.the present paper deals with the problem of learning erasing pattern languages within angluin's model of learning with queries. moreover, the learnability of erasing pattern languages with queries is studied when additional information is available. the results obtained are compared with previously known results in case non-erasing pattern languages have to be learned.first, when regular pattern languages have to be learned, it is shown that the learnability results for the non-erasing case remain valid, if the proper superclass of all erasing regular pattern languages is the object of learning. second, in the general case, serious differences have been observed. for instance, it turns out that arbitrary erasing pattern languages cannot be learned in settings in which, in the non-erasing case, even polynomially many queries will suffice.
query automata over finite trees. a main task in document transformation and information retrieval is locating subtrees satisfying some pattern. therefore, unary queries, i.e., queries that map a tree to a set of its nodes, play an important role in the context of structured document databases. the motivation of this work is to understand how the natural and well-studied computation model of tree automata can be used to compute such queries. we define a query automaton (qa) as a deterministic two-way finite automaton over trees that has the ability to select nodes depending on the state and the label at those nodes. we study qas over ranked as well as over unranked trees. unranked trees differ from ranked ones in that there is no bound on the number of children of nodes. we characterize the expressiveness of the different formalisms as the unary queries definable in monadic second-order logic (mso). in contrast to the ranked case, special stay transitions had to be added to qas over unranked trees to capture mso. we establish the complexity of the non-emptiness, containment, and equivalence of qas to be complete for exptime.
multimodal logic programming. we give a framework for developing the least model semantics, fixpoint semantics, and sld-resolution calculi for logic programs in multimodal logics whose frame restrictions consist of the conditions of seriality (i.e. ∀x ∃y ri (x, y)) and some classical first-order horn clauses. our approach is direct and no special restriction on occurrences of □i and ♦i is required. we apply our framework for a large class of basic serial multimodal logics, which are parametefized by an arbitrary combination of generalized versions of axioms t, b, 4, 5 (in the form, e.g. 4 : □iϕ → □j □kϕ) and i: □i ϕ → □j ϕ. another part of the work is devoted to programming in multimodal logics intended for reasoning about multidegree belief, for use in distributed systems of belief, or for reasoning about epistemic states of agents in multiagent systems. for that we also use the framework, and although these latter logics belong to the mentioned class of basic serial multimodal logics, the special sld-resolution calculi proposed for them are more efficient.
leader election in plane cellular automata, only with left-right global convention. we give a linear time algorithm to elect a leader. this problem originated in networking and distributed computing research. given a graph, its vertices represent processors (here finite state machines), and its edges communication lines (here synchronous). the leader election problem consists in finding a protocol for a family of graphs which, upon iteration, distinguishes a vertex, edge or cycle by a special state called leader. here, the graphs are only required to be connected, and without holes. we describe the algorithm on a special class of planar graphs, prove its correctness and show how it extends to other classes.
nondeterministic regular expressions as solutions of equational systems. we define the class of the linear systems whose solution is expressible as a tuple of nondeterministic regular expressions when they are interpreted as trees of actions rather than as sets of sequences. we precisely characterize those systems that have a regular expression as "canonical" solution, and show that any regular expression can be obtained as a canonical solution of a system of the defined class.
an approximate a* algorithm and its application to the scs problem. in this paper we deal with algorithm a* and its application to the problem of finding the shortest common supersequence of a set of sequences. a* is a powerful search algorithm which may be used to carry out concurrently the construction of a network and the solution of a shortest path problem on it. we prove a general approximation property of a* which, by building a smaller network, allows us to find a solution with a given approximation ratio. this is particularly useful when dealing with large instances of some problem. we apply this approach to the solution of the shortest common supersequence problem and show its effectiveness.
a concurrent lambda calculus with futures. we introduce a new lambda calculus with futures, λ(fut), that models the operational semantics of concurrent statically typed functional programming languages with mixed eager and lazy threads such as alice ml, a concurrent extension of standard ml. λ(fut) is a minimalist extension of the call-by-value λ-calculus that is sufficiently expressive to define and combine a variety of standard concurrency abstractions, such as channels, semaphores, and ports. despite its minimality, the basic machinery of λ(fut) is sufficiently powerful to support explicit recursion and call-by-need evaluation.we present a static type system for λ(fut) and distinguish a fragment of λ(fut) that we prove to be uniformly confluent. this result confirms our intuition that reference cells are the sole source of indeterminism. this fragment assumes the absence of so called handle errors that violate the single assignment assumption of λ(fut)'s handled future-construct.finally, we present a linear type system for λ(fut) by which to prove the absence of handle errors. our system is rich enough to type definitions of the above mentioned concurrency abstractions. consequently, these cannot be corrupted in any (not necessarily linearly) well-typed context.
on point covers of c-oriented polygons. let s be any family of n c-oriented polygons of the two-dimensional euclidean plane e2, i.e., bounded intersection of halfplanes whose normal directions of edges belong to a fixed collection of c distinct directions. let (s) denote the packing number of s, that is the maximum number of pairwise disjoint objects of s. let (s) be the transversal number of s, that is the minimum number of points required so that each object contains at least one of those points. we provide linear-time algorithms t(n, c) = &thgr;(nc) for &agr;-fat c-oriented polytopes, translates or homothets of ed proving that g(2, c) = o(&agr;)d, g(2, c)&le;dd and g(2, c)&le;(3d3/2)d respectively
validating firewalls using flow logics. the ambient calculus is a calculus of computation that allows active processes to communicate and to move between sites. a site is said to be a protective firewall whenever it denies entry to all attackers not possessing the required passwords. we devise a computationally sound test for validating the protectiveness of a proposed firewall and show how to perform the test in polynomial time. the first step is the definition of a flow logic for analysing the flow of control in mobile ambients; it amounts to a syntax-directed specification of the acceptability of a control flow estimate. the second step is to define a hardest attacker and to determine whether or not there exists a control flow estimate that shows the inability of the hardest attacker to enter; if such an estimate exists, then none of the infinitely many attackers can enter unless they contain at least one of the passwords, and consequently the firewall cannot contain any trap doors.
secure multiparty computations without computers. many simple calculations can be done easier without computers than by using them. we show that the same holds for secure multiparty computations if the function to be computed is simple enough. our starting point is an observation of bert den boer: a multiparty computation of a logical and-gate can be performed by five simple playing cards. we show that by using a reasonable amount of cards many useful functions can be computed in such way that each input stays private.
computational complexity of uniform quantum circuit families and quantum turing machines. deutsch proposed two sorts of models of quantum computers, quantum turing machines (qtms) and quantum circuit families (qcfs). in this paper we explore the computational powers of these models and re-examine the claim of the computational equivalence of these models often made in the literature without detailed investigations. for this purpose, we formulate the notion of the codes of qcfs and the uniformity of qcfs by the computability of the codes. various complexity classes are introduced for qtms and qcfs according to constraints on the error probability of algorithms or transition amplitudes. their interrelations are examined in detail. for monte carlo algorithms, it is proved that the complexity classes based on uniform qcfs are identical with the corresponding classes based on qtms. however, for las vegas algorithms, it is still open whether the two models are equivalent. we indicate the possibility that they are not equivalent. in addition, we give a complete proof of the existence of a universal qtm efficiently simulating multi-tape qtms. we also examine the simulation of various types of qtms such as multi-tape qtms, single tape qtms, stationary, normal form qtms (snqtms), and qtms with the binary tapes. as a result, we show that these qtms are computationally equivalent to one another as computing models implementing not only monte carlo algorithms but also exact (or error-free) ones
uniformity of quantum circuit families for error-free algorithms. in order to establish the computational equivalence between quantum turing machines (qtms) and quantum circuit families (qcfs) using yao's quantum circuit simulation of qtms, we have previously introduced the class of uniform qcfs based on an infinite set of elementary gates, which has been shown to be computationally equivalent to polynomial-time qtms up to bounded error simulation. however, the complexity classes zqp and eqp introduced by bernstein and vazirani for qtms do not appear to equal their counterparts for uniform qcfs. recently, we have introduced a subclass of uniform qcfs, the class of finitely generated uniform qcfs, and showed that they are perfectly equivalent to the class of polynomial-time qtms in the sense that both classes can be exactly simulated with each other. here, we further investigate the power of uniform qcfs comparing with that of finitely generated uniform qcfs in detail. we obtain the following results: (i) if a permutation mf: |x)〉 ↦ |f(x)〉 can be implemented with zero error by a uniform qcf, then both f and f-1 can be exactly computed by uniform qcfs. (ii) the quantum fourier transform (qft) of any order cannot be implemented with zero error by any finitely generated uniform qcf, while it has been shown, in contrast, by mosca and zalka that the qft of any order can be exactly implemented by a uniform qcf.
a gap property of deterministic tree languages. we show that a tree language recognized by a deterministic parity automaton is either hard for the co-büchi level and therefore cannot be recognized by a weak alternating automaton, or is on a very low level in the hierarchy of weak alternating automata. a topological counterpart of this property is that a deterministic tree language is either π11 complete (and hence nonborel), or it is on the level π30 of the borel hierarchy. we also give a new simple proof of the strictness of the hierarchy of weak alternating automata.
complexity in the case against accuracy estimation. some authors have repeatedly pointed out that the use of the accuracy, in particular for comparing classifiers, is not adequate. the main argument concerns some assumptions of seldom validity or correctness underlying the use of this criterion. in this paper, we study the computational burden of the accuracy's replacement for building and comparing classifiers, using the framework of inductive logic programming. replacement is investigated in three ways: completion of the accuracy with an additional requirement, replacement of the accuracy with a bi-criterion recently introduced from statistical decision theory: the receiver operating characteristic analysis, and replacement of the accuracy by a single criterion. we prove very hard results for most of the possible replacements. a first result shows that allowing the arbitrary multiplication of clauses appears to be totally useless. "arbitrary" is to be taken in its broadest meaning, in particular exponential. the second point is the sudden appearance of the negative result, which is not a function of the criteria's demands. the third point is the equivalence in difficulty of all these different criteria. in contrast, the single accuracy's optimization appears to be tractable in this framework.
on domain-partitioning induction criteria: worst-case bounds for the worst-case based. one of the most popular induction scheme for supervised learning is also one of the oldest. it builds a classifier in a top-down fashion, following the minimization of a so-called index criterion. while numerous papers have reported experiments on this scheme, little has been known on its theoretical aspect until recent works on decision trees and branching programs using a powerful classification tool: boosting.in this paper, we look at this problem from a worst-case computational (rather than informational) standpoint. our conclusions for the ranking of these indexes minimization follow almost exactly that of boosting (with matching upper and lowerbounds), and provide extensions to more classes of boolean formulas such as decision lists, multilinear polynomials and symmetric functions. our results also exhibit a strong worst-case for the induction scheme, as we build particularly hard samples for which the replacement of most index criteria, or the class of concept representation, even when producing the same ranking as boosting does for the indexes, makes no difference at all for the concept induced. this is clearly not a limit of previous analyses, but a consequence of the induction scheme.
an optimal online algorithm for scheduling two machines with release times. we present a deterministic online algorithm for scheduling two parallel machines when jobs arrive over time and show that it is (1/2) (5&minus;v5) 1.38198-competitive. the best previously known algorithm is (3/2)-competitive. our upper bound matches a previously known lower bound, and thus our algorithm has the best possible competitive ratio. we also present a lower bound of 1.21207 on the competitive ratio of any randomized online algorithm for any number of machines. this improves a previous result of 4 &minus; 2v2 ?1.17157. copyright 2001 elsevier science b.v.