waashk/dblp huggingface dataset:
a functional correspondence between monadic evaluators and abstract machines for languages with computational effects. we extend our correspondence between evaluators and abstract machines from the pure setting of the λ-calculus to the impure setting of the computational λ-calculus. we show how to derive new abstract machines from monadic evaluators for the computational λ-calculus. starting from (1) a generic evaluator parameterized by a monad and (2) a monad specifying a computational effect, we inline the components of the monad in the generic evaluator to obtain an evaluator written in a style that is specific to this computational effect. we then derive the corresponding abstract machine by closure-converting, cps-transforming, and defunctionalizing this specific evaluator. we illustrate the construction with the identity monad, obtaining the cek machine, and with a lifted state monad, obtaining a variant of the cek machine with error and state.in addition, we characterize the tail-recursive stack inspection presented by clements and felleisen as a lifted state monad. this enables us to combine this stack-inspection monad with other monads and to construct abstract machines for languages with properly tail-recursive stack inspection and other computational effects. the construction scales to other monads--including one more properly dedicated to stack inspection than the lifted state monad--and other monadic evaluators.
scheduling with timed automata. in this work, we present timed automata as a natural tool for posing and solving scheduling problems. we show how efficient shortest path algorithms for timed automata can find optimal schedules for the classical job-shop problem. we then extend these results to synthesize adaptive scheduling strategies for problems with uncertainty in task durations.
model checking of systems with many identical timed processes. over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, petri nets, lossy channel systems, context-free and push-down processes. we present a method for deciding reachability properties of networks of timed processes. such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. to our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in "two dimensions": they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz real-valued clocks. we illustrate our method by showing how it can be used to automatically verify fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes.finally, we show undecidability of the recurrent state problem: given a state in a timed network, check whether there is a computation of the network visiting the state infinitely often. this implies undecidability of model checking for any temporal logic which is sufficiently expressive to encode the recurrent state problem, such as ptl, ctl, etc.
computational topology for isotopic surface reconstruction. new computational topology techniques are presented for surface reconstruction of 2-manifolds with boundary, while rigorous proofs have previously been limited to surfaces without boundary. this is done by an intermediate construction of the envelope (as defined herein) of the original surface. for any compact c2-manifold m embedded in r3, it is shown that its envelope is c1,1. then it is shown that there exists a piecewise linear (pl) subset of the reconstruction of the envelope that is ambient isotopic to m, whenever m is orientable. the emphasis of this paper is upon the formal mathematical proofs needed for these extensions. (practical application examples have already been published in a companion paper.) possible extensions to non-orientable manifolds are also discussed. the mathematical exposition relies heavily on known techniques from differential geometry and topology, but the specific new proofs are intended to be sufficiently specialized to prompt further algorithmic discoveries.
reductions for non-clausal theorem proving. this paper presents the tas methodology as a new framework for generating non-clausal automated theorem provers. we present a complete description of the atp for classical propositional logic, named tas-d, but the ideas, which make use of implicants and implicates can be extended in a natural manner to first-order logic, and non-classical logics. the method is based on the application of a number of reduction strategies on subformulas, in a rewrite-system style, in order to reduce the complexity of the formula as much as possible before branching. specifically, we introduce the concept of complete reduction, and extensions of the pure literal rule and ofthe collapsibility theorems; these strategies allow to limit the size ofthe search space. in addition, tas-d is a syntactical countermodel construction. as an example of the power of tas-d we study a class of formulas which has linear proofs (in the number of branchings) when either resolution or dissolution with factoring is applied. when applying our method to these formulas we get proofs without branching. in addition, some experimental results are reported. copyright 2001 elsevier science b.v.
a symbolical algorithm on additive basis and double-loop networks. a double-loop digraph g = g(n; s1, s2), with gcd(n, s1, s2) = 1, has the set of vertices v = zn and the adjacencies are given by u → u + si (mod n) i = 1, 2. the diameter of g, denoted by d(n; s1, s2), is known to be lower bounded by lb(n) with d(n) = min1 ≤ s1 < s2 < n, gcd(n, s1, s2)=1 d(n; s1, s2) ≥ ⌈ √3n ⌉ - 2 = lb(n). this lower bound is known to be sharp. for a fixed n ∈ n, some algorithms to find d(n) and steps 1 ≤ α < β < n such that d(n; α, β) = d(n) are known through the bibliography, being of numerical nature all of them.in this paper we propose a symbolic algorithm on the following problem: given a number of vertices n0 ∈ n, find if possible an infinite family of tiqht double-loop digraphs g(x) = g(n(x); s1(x), s2(x)) such that n(x0) = n0 and d(x) = d(n(x); s1(x),s2(x)) = lb(n(x)) ∀x ≥ x0. this family is parameterized by the integer x with n(x) ∈ z and s1(x); s2(x) ∈ z/(n(x)). as a direct consequence of such an explicit family of digraphs g(x), we also have an additive basis {s1(x), s2(x)} which covers the elements of z/(n(x)) with optimal order.the time cost of this algorithm is o(√n0 log n0), in the worst case.
iteration and coiteration schemes for higher-order and nested datatypes. this article studies the implementation of inductive and coinductive constructors of higher kinds (higher-order nested datatypes) in typed term rewriting, with emphasis on the choice of the iteration and coiteration constructions to support as primitive. we propose and compare several well-behaved extensions of system fω with some form of iteration and coiteration uniform in all kinds. in what we call mendler-style systems, the iterator and coiterator have a computational behavior similar to the general recursor, but their types guarantee termination. in conventional-style systems, monotonicity witnesses are used for a notion of monotonicity defined uniformly for all kinds. our most expressive systems gmitω and gitω of generalized mendler, resp. conventional (co)iteration encompass martin, gibbons and bailey's efficient folds for rank-2 inductive types. strong normalization of all systems considered is proved by providing an embedding of the basic mendler-style system mitω into system fω
competitive facility location: the voronoi game. we consider a competitive facility location problem with two players. players alternate placing points, one at a time, into the playing arena, until each of them has placed n points. the arena is then subdivided according to the nearest-neighbor rule, and the player whose points control the larger area wins. we present a winning strategy for the second player, where the arena is a circle or a line segment. we permit variations where players can play more than one point at a time, and show that the first player can ensure that the second player wins by an arbitrarily small margin.
games on triangulations. we analyze several perfect-information combinatorial games played on planar triangulations. we introduce three broad categories of such games--constructing, transforming, and marking triangulations--and several specific games within each category. in various situations of each game, we develop polynomial-time algorithms to determine who wins a given game position under optimal play, and to find a winning strategy. along the way, we show connections to existing combinatorial games such as kayles and nimstring (a variation on dots-and-boxes).
towards compatible triangulations. we state the following conjecture: any two planar n-point sets that agree on the number of convex hull points can be triangulated in a compatible manner, i.e., such that the resulting two triangulations are topologically equivalent. we first describe a class of point sets which can be triangulated compatibly with any other set (that satisfies the obvious size and shape restrictions). the conjecture is then proved true for point sets with at most three interior points. finally, we demonstrate that adding a small number of extraneous points (the number of interior points minus three) always allows for compatible triangulations. the linear bound extends to point sets of arbitrary size and shape.
the plurality problem with three colors and more. the plurality problem is a game between two participants: paul and carole. we are given n balls, each of them is colored with one out of c colors. at any step of the game, paul chooses two balls and asks whether they are of the same color, whereupon carole answers yes or no. the game ends when paul either produces a ball a of the plurality color (meaning that the number of balls colored like a exceeds those of the other colors), or when paul states that there is no plurality. how many questions lc(n) does paul have to ask in the worst case?for c = 2, the problem is equivalent to the well-known majority problem which has already been solved (combinatorica 11 (1991) 383-387). in this paper we show that 3 ⌊n/2⌋-2 ≤ l3(n) ≤ ⌊5n/3⌋ - 2. moreover, for any c ≤ n, we show that surprisingly the naive algorithm for the plurality problem is asymptotically optimal.
words whose complexity satisfies lim p(n)/n = 1. in this paper, we study the infinite words such that limn p(n)/n = 1, by using the rauzy graphs. we show that the infinite evolution of the graphs of these infinite words can be characterized by a rather simple condition, which ensures that the graphs with more than one right special factor appear rarely, so that makes the complexity very small.
the thue-morse word contains circular 5/2+ power free words of every length. a word is circular 5/2+ power free if none of its conjugates has period less than 2/5 of its length. we show that the thue-morse word contains words of every length which are circular 5/2+ power free.
correspondence and translation for heterogeneous data. data integration often requires a clean abstraction of the different formats in which data are stored, and means for specifying the correspondences/relationships between data in different worlds and for translating data from one world to another. for that, we introduce in this paper a middleware data model that serves as a basis for the integration task, and a declarative rules language for specifying the integration. we show that using the language, correspondences between data elements can be computed in polynomial time in many cases, and may require exponential time only when insensitivity to order or duplicates are considered. furthermore, we show that in most practical cases the correspondence rules can be automatically turned into translation rules to map data from one representation to another. thus, a complete integration task (derivation of correspondences, transformation of data from one world to the other, incremental integration of a new bulk of data, etc.) can be specified using a single set of declarative rules.
avoiding slack variables in the solving of linear diophantine equations and inequations. in this paper, we present an algorithm for solving directly linear diophantine systems of both equations and inequations. here directly means without adding slack variables for encoding inequalities as equalities. this algorithm is an extension of the algorithm due to contejean and devie (1994) for solving linear diophantine systems of equations, which is itself a generalization of the algorithm of fortenbacher (clausen and fortenbacher, 1989) for solving a single linear diophantine equation. all the nice properties of the algorithm of contejean and devie are still satisfied by the new algorithm: it is complete, i.e. provides a (finite) description of the set of solutions, it can be implemented with a bounded stack, and it admits an incremental version. all of these characteristics enable its integration in the clp paradigm. &mdash;authors' abstract
limiting partial combinatory algebras. from every partial combinatory algebra a we construct another partial combinatory algebra a-lim(a). in a-lim(a), every representable partial numerical function φ(n) is exactly of the form limtζ(t, n) for some representable partial numerical function ζ(t, n) of a. the partial combinatory algebra a-lim(a) is a quotient of a by a partial equivalence relation, and is equipped with a limit structure in the sense that each element of a-lim(a) is the limit of a countable sequence of a-elements. in this paper, we discuss the limit structures for a in terms of barendregt's range property (if the range of a combinator is finite, then it is a singleton). moreover, we repeat the construction a-lim(-) transfinite times to interpret infinitary λ-calculi. finally, we attempt to interpret type-free λµ-calculus by introducing another partial applicative structure which has an asynchronous application operator that allows a parallel limit operation.
self-stabilizing timestamps. the problem of implementing self-stabilizing timestamps with bounded values is investigated and a solution is found which is applied to the l-exclusion problem and to the multiwriter atomic register problem. thus we get self-stabilizing solutions to these two well-known problems. a new type of weak timestamps is identified here, and some evidence is brought to show its usefulness.
random lattices, threshold phenomena and efficient reduction algorithms. two new lattice reduction algorithms are presented and analyzed. these algorithms, called the schmidt reduction and the gram reduction, are obtained by relaxing some of the constraints of the classical lll algorithm. by analyzing the worst case behavior and the average case behavior in a tractable model, we prove that the new algorithms still produce "good" reduced basis while requiring fewer iterations on average. in addition, we provide empirical tests on random lattices coming from applications, that confirm our theoretical results about the relative behavior of the different reduction algorithms.
the optimal lll algorithm is still polynomial in fixed dimension. in this paper, we consider the open problem of the complexity of the lll algorithm in the case when the approximation parameter of the algorithm has as its extreme value 1. this case is of interest because the output is then the strongest lovász-reduced basis. experiments reported by lagarias and odlyzko (j. acm 32(1) (1985) 229) seem to show that the algorithm remains polynomial in average. however, no bound better than a naive exponential order one is established for the worst-case complexity of the optimal lll algorithm, even for fixed small dimension (higher than 2). here, we prove that, for any fixed dimension n, the number of iterations of the lll algorithm is linear with respect to the size of the input. it is easy to deduce from vallée (j. algorithms 12 (1991) 556) that the linear order is optimal. moreover in 3 dimensions, we give a tight bound for the maximum number of iterations and we characterize precisely the output basis. our bound also improves the known one for the usual (non-optimal) lll algorithm.
an assertion-based proof system for multithreaded java. besides the features of a class-based object-oriented language, java integrates concurrency via its thread classes, allowing for a multithreaded flow of control. the concurrency model includes synchronous message passing, dynamic thread creation, shared-variable concurrency via instance variables, and coordination via reentrant synchronization monitors.to reason about safety properties of multithreaded java programs, we introduce an assertional proof method for a multithreaded sublanguage of java, covering the mentioned concurrency issues as well as the object-based core of java. the verification method is formulated in terms of proof-outlines, where the assertions are layered into local ones specifying the behavior of a single instance, and global ones taking care of the connections between objects. we establish the soundness and the relative completeness of the proof system. from an annotated program, a number of verification conditions are generated and handed over to the interactive theorem prover pvs.
on canonical number systems. let p(x)=pdxd++p0z[x] be such that d1,pd=1,p02 and n={0,1,...,p01}. we are proving in this note a new criterion for the pair {p(x),n} to be a canonical number system. this enables us to prove that if p2,...,pd1,i=1dpi0 and p0>2i=1d|pi|, then {p(x),n} is a canonical number system.
self-stabilizing l-exclusion. our work presents a self-stabilizing solution to the l-exclusion problem. this problem is a well-known generalization of the mutual-exclusion problem in which up to l, but never more than l, processes are allowed simultaneously in their critical sections. self-stabilization means that even when transient failures occur and some processes crash, the system finally resumes its regular and correct behavior. the model of communication assumed here is that of shared memory, in which processes use single-writer multiple-reader regular registers. copyright 2001 elsevier science b.v.
a structural approach to reversible computation. reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. most foundational work on reversible computing to date has focussed on simulations of low-level machine models. by contrast, we develop a more structural approach. we show how high-level functional programs can be mapped compositionally (i.e. in a syntax-directed fashion) into a simple kind of automata which are immediately seen to be reversible. the size of the automaton is linear in the size of the functional term. in mathematical terms, we are building a concrete model of functional computation. this construction stems directly from ideas arising in geometry of interaction and linear logic--but can be understood without any knowledge of these topics. in fact, it serves as an excellent introduction to them. at the same time, an interesting logical delineation between reversible and irreversible forms of computation emerges from our analysis.
identification of genetic networks by strategic gene disruptions and gene overexpressions under a boolean model. analysis of the interactions between genes by systematic gene disruptions and gene overexpressions is an important topic in molecular biology. this paper analyses the problem of identifying a genetic network from the data obtained by multiple gene disruptions and overexpressions in regard to the number of experiments and the complexity of experiments. an experiment consists of simultaneous gene disruptions and overexpressions and the complexity of an experiment is the number of genes disrupted or overexpressed. we define a genetic network as a boolean network and show a series of algorithms which describe methods for identifying the underlying genetic network by such experiments. some lower bounds on the number of experiments required for the identification are also proved for some cases.
a simple greedy algorithm for finding functional relations: efficient implementation and average case analysis. inferring functional relations from relational databases is important for the discovery of scientific knowledge because many experimental data are represented in the form of tables and many rules are represented in the form of functions. a simple greedy algorithm has been known as an approximation algorithm for this problem. this paper presents an efficient implementation of the algorithm. this paper also shows that the algorithm can identify an exact solution for simple functions if input data for each function are generated uniformly at random and the size of the domain is bounded by a constant. results of computational experiments using artificially generated data are presented to verify the approach.
towards a semantics of proofs for non-commutative logic: multiplicatives and additives. interpretation of proofs of the multiplicative-additive fragment of non-commutative logic, by using bimodules on coherent spaces and bilinear functions.
computing the similarity of two sequences with nested arc annotations. we present exact algorithms for the np-complete longest common subsequence problem for sequences with nested arc annotations, a problem occurring in structure comparison of rna. given two sequences of length at most n and nested arc structure, one of our algorithms determines (if existent) in o(3.31k1+k2 ċ n) time an arc-preserving subsequence of both sequences, which can be obtained by deleting (together with corresponding arcs) k1 letters from the first and k2 letters from the second sequence. a second algorithm shows that, (in case of a four letter alphabet) we can find a length l arc-annotated subsequence in o(12lċlċn) time. this means that the problem is fixed-parameter tractable when parameterized by the number of deletions as well as when parameterized by the subsequence length. our findings complement known approximation results which give a quadratic time factor-2-approximation for the general and polynomial time approximation schemes for restricted versions of the problem. in addition, we obtain further fixed-parameter tractability results for these restricted versions.
the power of reachability testing for timed automata. the computational engine of the verification tool uppall consists of a collection of efficient algorithms for the analysis of teachability properties of systems. model-checking of properties other than plain reachability ones may currently be carried out in such a tool as follows. given a property φ to model-check, the user must provide a test automaton tφ for it. this test automaton must be such that the original system s has the property expressed by φ precisely when none of the distinguished reject states of tφ can be reached in the synchronized parallel composition of s with tφ. this raises the question of which properties may be analysed by uppaal in such a way. this paper gives an answer to this question by providing a complete characterization of the class of properties for which model-checking can be reduced to reachability testing in the sense outlined above. this result is obtained as a corollary of a stronger statement pertaining to the compositionality of the property language considered in this study. in particular, it is shown that our language is the least expressive compositional language that can express a simple safety property stating that no reject state can ever be reached.finally, the property language characterizing the power of reachability testing is used to provide a definition of characteristics properties with respect to a timed version of the ready simulation preorder, for nodes of τ-free, deterministic timed automata.