waashk/dblp huggingface dataset:
amalgamation in the semantics of casl. we present a semantics for architectural specifications in the common algebraic specification language (casl), including an extended static analysis compatible with model-theoretic requirements. the main obstacle here is the lack of amalgamation for casl models. to circumvent this problem, we extend the casl logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. the extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. using these concepts, we develop the semantics at various levels in an institution-independent fashion. moreover, amalgamation for enriched casl means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for casl.
combination of constraint systems ii: rational amalgamation. in two earlier papers (baader, schulz, in: u. montanari, f. rossi (eds.), proc. cp'95 springer lecture notes in computer science, vol. 976, springer, berlin, pp. 380-397; theoret. comput. sci 192 (1998) 107-161), the concept of "free amalgamation" has been introduced as a general methodology for interweaving solution structures for symbolic constraints, and it was shown how constraint solvers for two components can be lifted to a constraint solver for the free amalgam. here we discuss a second general way for combining solution domains, called rational amalgamation. in praxis, rational amalgamation seems to be the preferred combination principle if the two solution structures to be combined are "rational" or "non-wellfounded" domains. it represents, e.g., the way how rational trees and rational lists are interwoven in the solution domain of prolog iii, and a variant has been used by w. rounds for combining feature structures and hereditarily finite non-wellfounded sets. we show that rational amalgamation is a general combination principle, applicable to a large class of structures. as in the case of free amalgamation, constraint solvers for two component structures can be combined to a constraint solver for their rational amalgam. from this algorithmic point of view, rational amalgamation seems to be interesting since the combination technique for rational amalgamation avoids one source of non-determinism that is needed in the corresponding scheme for free amalgamation. copyright 2001 elsevier science b.v.
primitive recursion for higher-order abstract syntax. higher-order abstract syntax is a central representation technique in logical frameworks which maps variables of the object language into variables of the meta-language. it leads to concise encodings, but is incompatible with functions defined by primitive recursion or proofs by induction. in this paper we propose an extension of the simply typed lambda-calculus with iteration and case constructs which preserves the adequacy of higher-order abstract syntax encodings. the well-known paradoxes are avoided through the use of a modal operator which obeys the laws of s4. in the resulting calculus many functions over higher-order representations can be expressede legantly. our central technical result, namely that our calculus is conservative over the simply typed lambda-calculus, is proved by a rather complex argument using logical relations. we view our system as an important first step towards allowing the methodology of lf to be employed effectively in systems based on induction principles such as alf, coq, or nuprl, leading to a synthesis of currently incompatible paradigms. copyright 2001 elsevier science b.v.
unique existence, approximate solutions, and countable choice. an existential statement seems to admit of a constructive proof without countable choice only if the object to be constructed is uniquely determined, or is intended as an approximate solution of the problem in question. this conjecture is substantiated by re-examining some basic tools of mathematical analysis from a choice-free constructive point of view, starting from dedekind cuts as an appropriate notion of real numbers. by establishing a fairly general version of the approximate intermediate value theorem, we also indicate that strong continuity is a practicable substitute for uniform continuity, where a mapping between metric spaces is called strongly continuous if two subsets of its domain are bounded away from each other whenever so are their images.
efficient data mappings for parity-declustered data layouts. the joint demands of high performance and fault tolerance in a large array of disks can be satisfied by a parity-declustered data layout. such a data layout is generated by partitioning the data on the disks into stripes and choosing a part of each stripe to hold redundant information. thus the data layout can be represented as a table of stripes. the data mapping problem is the problem of translating a data address into a disk identifier and an offset on that disk. recent work has yielded mappings that compute disks and offsets directly from data addresses without the need to store tables. in this paper, we show that parity-declustered data layouts based on commutative rings yield mappings with improved computational efficiency and wider applicability.
on the expressive power of monadic least fixed point logic. monadic least fixed point logic mlfp is a natural logic whose expressiveness lies between that of first-order logic fo and monadic second-order logic mso. in this paper, we take a closer look at the expressive power of mlfp. our results are: (1) mlfp can describe graph properties beyond any fixed level of the monadic second-order quantifier alternation hierarchy. (2) on strings with built-in addition, mlfp can describe at least all languages that belong to the linear time complexity class dlin. (3) settling the question whether addition-invariant mlfp = addition-invariant mso on finite strings or, equivalently, settling the question whether mlfp = mso on finite strings with addition would solve open problems in complexity theory: "=" would imply that ph = ptime whereas "≠" would imply that dlin ≠ linh. apart from this we give a self-contained proof of the previously known result that mlfp is strictly less expressive than mso on the class of finite graphs.
an arithmetic for polynomial-time computation. we define a restriction lha of heyting arithmetic ha with the property that all extracted programs are feasible. the restrictions consist in linearity and ramification requirements.
logical optimality of groundness analysis. in the context of the abstract interpretation theory, we study the relations among various abstract domains for groundness analysis of the logic programs. we reconstruct the well-known domain as a logical domain in a fully automatic way and we prove that it is the best abstract domain which can be set up from the property of groundness by applying logic operators only. we propose a new notion of optimality which precisely captures the relation between and its natural concrete domain. this notion enables us to discriminate between the various abstract domains for groundness analysis from a computational point of view and to compare their relative precision. finally, we propose a new domain for groundness analysis which has the advantage of being independent from the specific program and we show it optimality. copyright 2002 elsevier science b.v.
on some generalizations of the thue-morse morphism. in 1912, the norwegian mathematician axel thue was the first to describe an overlap-free binary infinite word. this word was generated by a morphism which is called, since the works of morse, the thue-morse morphism. here, we present two generalizations of the thue-morse morphism in the case of alphabets with more than two letters. the extension of the characteristic properties of the word of thue to the words generated by these morphisms is considered. one of these generalizations corresponds to the construction of prouhet and a link with the arshon words is given. in particular, we prove that if n is an even number then the n-letter arshon word is generated by morphism.
lyndon factorization of the prouhet words. prouhet words are a natural generalization, over alphabets with more than two letters, of the well known binary thue-morse word.we give a unique factorization of these words in a sequence of decreasing lyndon words, then generalizing such a decomposition given by ido and melançon for the thue-morse word.
a manifesto for the computational method. we promote the much maligned computational method. the computational method is a paradigm for proving mathematical results where the burden of doing the "grunt work" is given to our able research assistant, the computer. we assert that proofs using the computational method, also known as computer aided proofs, are here to stay. in fact, the use of a computer can make the analysis of complicated algorithms fun. we illustrate the usefulness of the method by analyzing a randomized algorithm for multi-processor scheduling with rejection. more specifically, we present a randomized algorithm which is 1.44127-competitive. the best previously known result is a 1.5-competitive algorithm.
online companion caching. this paper is concerned with online caching algorithms for the (n, k)-companion cache, defined by brehob et al. (j. scheduling 6 (2003) 149). in this model the cache is composed of two components: a k-way set-associative cache and a companion fully associative cache of size n. we show that the deterministic competitive ratio for this problem is (n + 1)(k + 1) - 1, and the randomized competitive ratio is o(log n log k) and ω(log n + log k).
new bounds for randomized busing. we consider anonymous secure communication, where parties not only wish to conceal their communications from outside observers, but also wish to conceal the very fact that they are communicating. we consider the bus framework introduced by beimel and dolev (j. cryptology 16 (2003) 25), where messages are delivered by a bus traveling on a random walk. we generalize this idea to consider more than one bus. we show that if w buses are allowed, then the expected delivery time for a message can be decreased from θ(n) to θ(n/√w) in the case of a complete graph. additionally, we introduce a class of graphs called r-partite directed collars and obtain analogous bounds on the expected delivery time for these graphs. we also propose several new features that resolve possible shortcomings in the systems proposed by beimel and dolev.
verification and refinement with fine-grained action-based concurrent objects. action-based concurrent object-oriented programs express autonomous behavior of objects through actions that, like methods, are attached to objects but, in contrast to methods, may execute autonomously whenever their guard is true. the promise is a streamlining of the program structure by eliminating the distinction between processes and objects and a streamlining of correctness arguments. in this paper we illustrate the use of action-based object-oriented programs and study their verification and their refinement from specifications, including the issue of non-atomic operations.
order-incompleteness and finite lambda reduction models. many familiar models of the untyped lambda calculus are constructed by order-theoretic methods. this paper provides some basic new facts about ordered models of the lambda calculus. we show that in any partially ordered model that is complete for the theory of β- or βη-conversion, the partial order is trivial on term denotations. equivalently, the open and closed term algebras of the untyped lambda calculus cannot be non-trivially partially ordered. our second result is a syntactical characterization, in terms of so-called generalized mal'cev operators, of those lambda theories which cannot be induced by any non-trivially partially ordered model. we also consider a notion of finite models for the untyped lambda calculus, or more precisely, finite models of reduction. we demonstrate how such models can be used as practical tools for giving finitary proofs of term inequalities.
towards a descriptive set theory for domain-like structures. this is a survey of results in descriptive set theory for domains and similar spaces, with the emphasis on the ω-algebraic domains. we try to demonstrate that the subject is interesting in its own right and is closely related to some areas of theoretical computer science. since the subject is still in its beginning, we discuss in detail several open questions and possible future development. we also mention some relevant facts of (effective) descriptive set theory.
a reducibility for the dot-depth hierarchy. hierarchies considered in computability theory and in complexity theory are related to some reducibilities in the sense that levels of the hierarchies are downward closed and have complete sets. in this paper we propose a reducibility having similar relationship to the brzozowski's dot-depth hierarchy and some its refinements. we prove some basic facts on the corresponding degree structure and discuss relationships of the reducibility to complexity theory (via the leaf-language approach).
l(a)=l(b)? a simplified decidability proof. we give a proof of decidability of the equivalence problem for deterministic pushdown automata, which simplifies that of s&eacute;nizergues (theoret. comput. sci. 251 (2000) 1).
the approximability of non-boolean satisfiability problems and restricted integer programming. in this paper we present improved approximation algorithms for two classes of maximization problems defined in barland et al. (j. comput. system sci. 57(2) (1998) 144). our factors of approximation substantially improve the previous known results and are close to the best possible. on the other hand, we show that the approximation results in the framework of barland et al. hold also in the parallel setting, and thus we have a new common framework for both computational settings. we prove almost tight non-approximability results, thus solving a main open question of barland et al.we obtain the results through the constraint satisfaction problem over multi-valued domains, for which we develop approximation algorithms and show non-approximability results. our parallel approximation algorithms are based on linear programming and random rounding; they are better than previously known sequential algorithms. the non-approximability results are based on new recent progress in the fields of probabilistically checkable proofs and multi-prover one-round proof systems.
vectorial languages and linear temporal logic. determining for a given deterministic complete automaton the sequence of visited states while reading a given word is the core of important problems with automata-based solutions, such as approximate string matching. the main difficulty is to do this computation efficiently. considering words as vectors and working on them using vectorial operations allows to solve the problem faster than using local operations.in this paper, we show first that the set of vectorial operations needed by an algorithm representing a given automaton depends on the language accepted by the automaton. we give precise characterizations for star-free, solvable and regular languages using vectorial algorithms. we also study classes of languages associated with restricted sets of vectorial operations and relate them with languages defined by fragments of linear temporal logic.finally, we consider the converse problem of constructing an automaton from a given vectorial algorithm. as a byproduct, we show that the satisfiability problem for some extensions of ltl characterizing solvable and regular languages is pspace-complete.
games with winning conditions of high borel complexity. we first consider infinite two-player games on pushdown graphs. in previous work, cachat et al. [solving pushdown games with a σ3-winning condition, in: proc. 11th annu. conf. of the european association for computer science logic, csl 2002, lecture notes in computer science, vol. 2471, springer, berlin, 2002, pp. 322-336] have presented a winning decidable condition that is σ3-complete in the borel hierarchy. this was the first example of a decidable winning condition of such borel complexity. we extend this result by giving a family of decidable winning conditions of arbitrary finite borel complexity. from this family, we deduce a family of decidable winning conditions of arbitrary finite borel complexity for games played on finite graphs. the problem of deciding the winner for these conditions is shown to be non-elementary.
on learning embedded midbit functions. a midbit function on l binary inputs x1,...,xl outputs the middle bit in the binary representation of x1+...+xl. we consider the problem of probably approximately correct (pac) learning embedded midbit functions, where the set s ⊂ {x1,...,xn} of relevant variables on which the midbit depends is unknown to the learner.to motivate this problem, we first point out that a result of green et al. implies that a polynomial time learning algorithm for the class of embedded midbit functions would immediately yield a fairly efficient (quasipolynomial time) (pac) learning algorithm for the entire complexity class acc. we then give two different subexponential learning algorithms, each of which learns embedded midbit functions under any probability distribution in 2√n log n time. finally, we give a polynomial time algorithm for learning embedded midbit functions under the uniform distribution.
approximate reasoning by similarity-based sld resolution. in (gerla and sessa, fuzzy logic and soft computing, kluwer, norwell, 1999, pp. 19-31) a methodology that allows to manage uncertain and imprecise information in the frame of the declarative paradigm of logic programming has been proposed. with this aim, a similarity relation r between function and predicate symbols in the language of a logic program is considered. approximate inferences are then possible since similarity relation allows us to manage alternative instances of entities that can be considered "equal" with a given degree. the declarative semantics of the proposed transformation technique of logic programs is analyzed. the notion of fuzzy least herbrand model is also introduced. in this paper the corresponding operational semantics is provided by introducing a modified version of sld resolution. this top-down refutation procedure overcomes failure situations in the unification process by using the similarity relation. a generalized notion of most general unifier provides a numeric value which gives a measure of the exploited approximation. in this way, the sld resolution is enhanced since it is possible both to handle uncertain or imprecise information, and to compute approximate answer substitutions, with an associated approximation-degree, when failures of the exact inference process occur. it can lead to the implementation of a more general prolog interpreter, without detracting from the elegance of the language.
smaller solutions for the firing squad. in this paper we improve the bounds on the complexity of solutions to the firing squad problem, also known as the firing synchronization problem. in the firing synchronization problem we consider a one-dimensional array of n identical finite automata. initially all automata are in the same state except for one automaton designated as the initiator for the synchronization. our results hold for the original problem, where the initiator may be located at either endpoint, and for the variant where any one of the automata may be the initiator, called the generalized problem. in both cases, the goal is to define the set of states and transition rules for the automata so that all machines enter a special fire state simultaneously and for the first time during the final round of the computation. in our work we improve the construction for the best known minimal-time solution to the generalized problem by reducing the number of states needed and give non-minimal-time solutions to the original and generalized problem that use fewer states than the corresponding minimal-time solutions.
from rewrite rules to bisimulation congruences. the dynamics of many calculi can be most clearly defined by a reduction semantics. to work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. this paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. general definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. they give rise to bisimulation congruences. as a test of the theory it is shown that bisimulation for a fragment of ccs is recovered. the transitions generated for a fragment of the ambient calculus of cardelli and gordon, and for ski combinators, are also discussed briefly.
optimal insertion in deterministic dawgs. in this paper, we present an on-line algorithm for adding words (strings) in deterministic directed acyclic word graphs (dawgs) i.e. acyclic deterministic finite-state automata (dfas). the proposed algorithm performs optimal insertion, meaning that if applied to a minimal dawg, the dawg after the insertion will also be minimal. the time required to add a new word is o(n) with respect to the size of the dawg. repetitive application of the proposed insertion algorithm can be used to construct minimal deterministic dawgs incrementally, although the algorithm is not time-efficient for building minimal dawgs from a set of words: to build a dawg of n words this way, o(n2) time is required. however, the algorithm is quite useful in cases where existing minimal dawgs have to be updated rapidly (e.g. speller dictionaries), since each word insertion traverses only a limited portion of the graph and no additional minimization operation is required. this makes the process very efficient to be used on-line. this paper provides a proof of correctness for the algorithm, a calculation of its time-complexity and experimental results.
tight bounds for online class-constrained packing. we consider class-constrained packing problems, in which we are given a set of bins, each having a capacity v and c compartments, and n items of m different classes and the same (unit) size. we need to fill the bins with items, subject to capacity constraints, such that items of different classes are placed in separate compartments; thus, each bin can contain items of at most c distinct classes. we consider two optimization goals. in the class-constrained bin-packing problem (ccbp), our goal is to pack all the items in a minimal number of bins; in the class-constrained multiple knapsack problem (ccmk), we wish to maximize the total number of items packed in m bins, for m > 1. the ccbp and ccmk problems model fundamental resource allocation problems in computer and manufacturing systems. both are known to be strongly np-hard.in this paper we derive tight bounds for the online variants of these problems. we first present a lower bound of (1 + α) on the competitive ratio of any deterministic algorithm for the online ccbp, where α ∈ (0,1) depends on v, c, m and n. we show that this ratio is achieved by the algorithm first-fit. we then consider the temporary ccbp, in which items may be packed for a bounded time interval (that is unknown in advance). we obtain a lower bound of v/c on the competitive ratio of any (deterministic or randomized) algorithm. we show that this ratio is achieved by all any-fit algorithms. finally, tight bounds are derived for the online ccmk and the temporary ccmk problems.