waashk/acm huggingface dataset:
deriving algorithms from type inference systems: application to strictness analysis  the role of non-standard type inference in static program analysis has been much studied recently. early work emphasised the efficiency of type inference algorithms and paid little attention to the correctness of the inference system. recently more powerful inference systems have been investigated but the connection with efficient inference algorithms has been obscured. the contribution of this paper is twofold: first we show how to transform a program logic into an algorithm and, second, we introduce the notion of lazy types and show how to derive an efficient algorithm or strictness analysis.  chris hankin daniel le metayer
an o(n2log n) time algorithm for the minmax angle triangulation  we show that a triangulation of a set of n points in the plane that minimizes the maximum angle can be computed in time o(n2 log n) and space o(n). in the same amount of time and space we can also handle the constrained case where edges are prescribed. the algorithm iteratively improves an arbitrary initial triangulation and is fairly easy to implement.  herbert edelsbrunner tiow seng tan roman waupotitsch
alternation and the power of nondeterminism  while nondeterminism is widely beleived to be more powerful than determinism in various contexts (the most famous being the conjecture that np strictly contains p), no proof of the added power of nondeterminism is available for any significant issue. the weaker conjecture (than np strictly contains p) that there is a language accepted by a nondeterministic linear time bounded multitape turing machine that cannot be accepted by a deterministic linear time bounded multi-tape tm still seems quite hard (paul 1982). the aim of this paper is to show how the existance of the polynomial-time hierarchy of meyer and stockmeyer(1972) and the related concept of alternation (chandra, kozen and stockmeyer(1981)) can be exploited to prove the power of nondeterminism over determinism in some contexts. it is hoped that this approach may be useful in proving stronger results.  ravi kannan
safe fusion of functional expressions  large functional programs are often constructed by decomposing each big task into smaller tasks which can be performed by simpler functions. this hierarchical style of developing programs has been found to improve programmers' productivity because smaller functions are easier to construct and reuse. however, programs written in this way tend to be less efficient. unnecessary intermediate data structures may be created. more function invocations may be required.  to reduce such performance penalties, wadler proposed a transformation algorithm, called deforestation, which could automatically fuse certain composed expressions together in order to eliminate intermediate tree-like data structures. however, his technique is only applicable to a subset of first-order expressions.  this paper will generalise the deforestation technique to make it applicable to all first-order and higher- order functional programs. our generalisation is made possible by the adoption of a model for safe fusion which views each function as a producer and its parameters as consumers. through this model, static program properties are proposed to classify producers and consumers as either safe or unsafe. this classification is used to identify sub-terms that can be safely fused/eliminated. we present the generalised transformation algorithm as a set of syntax-directed rewrite rules, illustrate it with examples, and provide an outline of its termination proof.  wei-ngan chin
embedded implicational dependencies and their inference problem  it is shown that the general inference problem for embedded implicational dependencies (eids) is undecidable. for the more important case of finite inference (i.e., inference for finite data bases), the problem is not even recursively enumerable (r.e.); rather, it is complete in co-r.e. these results hold even for typed eids without equality, as well as for (untyped) template dependencies. the case for typed template dependencies remains open. the complexity of the inference problem for full dependencies has also been characterized - it is complete in exponential time for full implicational dependencies, and even for full typed template dependencies.  ashok k. chandra harry r. lewis johann a. makowsky
a confluent calculus of macro expansion and evaluation  syntactic abbreviations or macros provide a powerful tool to increase the syntactic expressiveness of programming languages. the expansion of these abbreviations can be modeled with substitutions. this paper presents an operational semantics of macro expansions and evaluation where substitutions are handled explicitly. the semantics is defined in terms of a confluent, simple, and intuitive set of rewriting rules. the resulting semantics is also a basis for developing correct implementations.  ana bove laura arbilla
an  wlog logn lower bound for routing in optical networks  optical communication is likely to significantly speed up parallel computation because the vast bandwidth of the optical medium can be divided to produce communication networks of very high degree. however, the problem of contention in high-degree networks makes the routing problem in these networks theoretically (and practically) difficult. in this paper we examine valiant's h-relation routing problem, which is a fundamental problem in the theory of parallel computing. the h-relation routing problem arises both in the direct implementation of specific parallel algorithms on distributed-memory machines and in the general simulation of shared memory models such as the pram on distributed-memory machines. in an h  -relation routing problem each processor has up to h messages that it wishes to send to other processors and each processor is the destination of at most h messages. we present a lower bound for routing an h-relation (for any h > 1) on a complete optical network of size n. our lower bound applies to any randomized distributed algorithm for this task. specifically. we show that the expected number of communication steps required to route an arbitrary h-relation is  wh+loglogn . this is the first  known lower bound for this problem which does not restrict the class of algorithms under consideration.  leslie ann goldberg mark jerrum philip d. mackenzie
soft typing with conditional types  we present a simple and powerful type inference method for dynamically typed languages where no type information is supplied by the user. type inference is reduced to the problem of solvability of a system of type inclusion constraints over a type language that includes function types, constructor types, union, intersection, and recursive types, and conditional types. conditional types enable us to analyze control flow using type inference, thus facilitating computation of accurate types. we demonstrate the power and practicality of the method with examples and performance results from an implementation.  alexander aiken edward l. wimmers t. k. lakshman
an internal semantics for modal logic  in kripke semantics for modal logic, "possible worlds" and the possibility relation are both primitive notions. this has both technical and conceptual shortcomings. from a technical point of view, the mathematics associated with kripke semantics is often quite complicated. from a conceptual point of view, it is not clear how to use kripke structures to model knowledge and belief, where one wants a clearer understanding of the notions that are primitive in kripke semantics. we introduce modal structures as models for modal logic. we use the idea of possible worlds, but by directly describing the "internal semantics" of each possible world. it is much easier to study the standard logical questions, such as completeness, decidability, and compactness, using modal structures. furthermore, modal structures offer a much more intuitive approach to modelling knowledge and belief.  r fagin m y vardi
bounds on the greedy routing algorithm for array networks  we extend previous work on greedy routing for array networks by providing bounds on the average delay and the average number of packets in the system. we analyze the dynamic routing problem, where packets are generated at each node according to a poisson process. each packet is sent to a destination chosen uniformly at random. packets are routed greedily, first moving to the correct column and then to the correct row. packets require unit time to travel across a directed edge between nodes; only a single packet can cross an edge at any given time, and packets waiting for an edge are buffered. our bounds are based on comparisons with computationally more simple queueing networks, and the methods used are generally applicable to other network systems. a primary contribution of the paper is a new lower bound technique that also improves on the previous lower bounds by stamoulis and tsitsiklis for heavily loaded hypercube networks. [11] on heavily loaded array networks, our lower and upper bounds differ by only a small constant factor.  we further examine extensions of the problem where our methods prove useful. for example, we consider variations where edges can have different transmission rates or the destination distribution is non-uniform. in particular, we study to what extent optimally configured array networks outperform the standard array network.  michael mitzenmacher
nodes and arcs, the ideal structural primitives for language?  for a language to be reasonably small while providing referencing facilities which are adequate for direct natural expression, it is necessary that all operands be built from a small number of primitive structural types. for the referencing capabilities to be used in a clearly readable way the structure of the data must accurately reflect the structure of the conceptual objects being modeled without representational distortions. for objects from a small set of primitive structural types to be combined in a way that accurately reflects the structure of many kinds of object it is necessary that the structural primitives have a minimum of internal structure. these considerations and others indicate that nodes and arcs of directed graphs are probably a permanent optimum choice of structural primitives for a comprehensive programming and system description language. they provide a highly "plastic material" which can be "shaped and hardened" by declarations to accurately model the structure of many kinds of parts of different problem environments. current major languages emphasize function but distort the structure in system descriptions. accurate structural description simplifies application programs by eliminating irrelevant representational conventions and providing higher level, declarative information about the problem environment enabling the computer to be more helpful. it provides a basis for combining the advantages of many languages, leading to simpler and more coherently designed software systems. accurate description of preexisting data and systems can ease many interfacing and compatibility problems. the dawn language based on the above ideas is described briefly. it is a general language with a fully integrated semantic data model for data base and system control. a number of interdependencies among various kinds of language improvement are also described. the process of eliminating representational irrelevancies can probably be completed soon since those remaining are becoming sparse and objectively identifiable when similar language constructs are compared.  edward s. lowry
institutions: abstract model theory for specification and programming  there is a population explosion among the logical systems used in computing science. examples include first-order logic, equational logic, horn- clause logic, higher-order logic, infinitary logic, dynamic logic, intuitionistic logic, order-sorted logic, and temporal logic; moreover, there is a tendency for each theorem prover to have its own idiosyncratic logical system. the concept of institution is introduced to formalize the informal notion of "logical system." the major requirement is that there is a satisfaction relation between models and sentences that is consistent under change of notation. institutions enable abstracting away from syntactic and semantic detail when working on language structure "in-the-large"; for example, we can define language features for building large logical system. this applies to both specification languages and programming languages. institutions also have applications to such areas as database theory and the semantics of artificial and natural languages. a first main result of this paper says that any institution such that signatures (which define notation) can be glued together, also allows gluing together theories (which are just collections of sentences over a fixed signature). a second main result considers when theory structuring is preserved by institution morphisms. a third main result gives conditions under which it is sound to use a theorem prover for one institution on theories from another. a fourth main result shows how to extend institutions so that their theories may include, in addition to the original sentences, various kinds of constraint that are useful for defining abstract data types, including both "data" and "hierarchy" constraints. further results show how to define institutions that allow sentences and constraints from two or more institutions. all our general results apply to such "duplex" and "multiplex" institutions.  joseph a. goguen rod m. burstall
on the degree of boolean functions as real polynomials  every boolean function may be represented as a real polynomial. in this paper we characterize the degree of this polynomial in terms of certain combinatorial properties of the boolean function.  our first result is a tight lower bound of (log n) on the degree needed to represent any boolean function that depends on n variables.  our second result states that for every boolean function f the following measures are all polynomially related:(1) the decision tree complexity of f. (2) the degree of the polynomial representing f. (3) the smallest degree of a polynomial approximating f in the lmax norm.  noam nisan mario szegedy
on the power of one-way communication  in this paper, a very simple model of parallel computation is considered, and the question of how restricting the flow of data to be one way compares with two-way flow is studied. it is shown that the one-way version is surprisingly very powerful in that it can solve problems that seemingly require two-way communication. whether or not one-way communication is strictly weaker than two-way is an open problem, although the conjecture in this paper is in the positive. it is shown, however, that proving this conjecture is at least as hard as some well- known open problems in complexity theory.  jik h. chang oscar h. ibarra anastasios vergis
computing the minimum hausdorff distance for point sets under translation  we consider the problem of computing a translation that minimizes the hausdorff distance between two sets of points. for points in @@@@1 in the worst case there are &amp;ominus;(mn) translations at which the hausdorff distance is a local minimum, where m is the number of points in one set and n is the number in the other. for points in @@@@2 there are &amp;ominus;(mn(m \\+ n)) such local minima. we show how to compute the minimal hausdorff distance in time  (mn log mn) for points in @@@@1 and in time  m2n2α( ;mn)) for points in @@@@2. the results for the one-dimensional case are applied to the problem of comparing polygons under general affine transformations, where we extend the recent results of arkin et al on polygon resemblance under rigid body motion. the two-dimensional case is closely related to the problem of finding an approximate congruence between two points sets under translation in the plane, as considered by alt et al.  daniel p. huttenlocher klara kedem
time-space-optimal string matching (preliminary report)  in this paper we describe a new linear-time string-matching algorithm requiring neither dynamic storage allocation nor other high-level capabilities. the algorithm can be implemented to run in linear time even on a six-head two-way finite automaton. moreover, the automaton requires only "{ @@@@}- branching" [1]. (decisions depend on which of the six scanned pattern or text symbols and positions are the same, but not on the particular symbols or how many symbols there are. hence the same algorithm works even for an infinite alphabet.) a "real-time" implementation is possible on such a multihead finite automaton with a few more heads.  zvi galil joel seiferas
speedups of deterministic machines by synchronous parallel machines  this paper presents the new speedups dtime(t) @@@@ atime(t/log t) and dtime(t) @@@@ pram-time(@@@@t). these improve the results of hopcroft, paul, and valiant that dtime(t) @@@@ dspace(t/log t), and of paul and reischuk that dtime(t) @@@@ atime(t log log t/log t). the new approach unifies not only these two previous results, but also the result of paterson and valiant that size(t) @@@@ depth(o(t/log t)).  patrick w. dymond martin tompa
a framework for combining analysis and verification  we present a general framework for combining program verification and program analysis. this framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. more importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. in other words, our framework explores synergistic interaction between verification and analysis.  in this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. the framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. further, it has some important features:  it is flexible: any number of assertions can be used anywhere;  it is open: it can employ an arbitrary analyzer;  it is modular: we reason with conditional correctness of assertions;  it is incremental: it can be tuned for the accuracy/efficiency tradeoff.  nevin heintze joxan jaffar r
the competitiveness of on-line assignments  consider the on-line problem where a number of servers are ready to provide service to a set of customers. each customer's job can be handled by any of a subset of the servers. customers arrive one-by- one and the problem is to assign each customer to an appropriate server in a manner that will balance the load on the servers. this problem can be modeled in a natural way by a bipartite graph where the vertices of one side (customers) appear one at a time and the vertices of the other side (servers) are known in advance. we derive tight bounds on the competitive ratio in both deterministic and randomized cases. let n denote the number of servers. in the deterministic case we provide an on-line algorithm that achieves a competitive ratio of k = [log2 n] (up to an additive 1) and prove that this is the best competitive ratio that can be achieved by any deterministic on-line algorithm. in a similar way we prove that the competitive ratio for the randomized case is k=ln(n) (up to an additive 1). we conclude that for this problem, randomized algorithms differ from deterministic ones by precisely a constant factor.  yossi azar joseph naor raphael rom
equational theories and database constraints  we present a novel way to formulate database dependencies as sentences of first-order logic, using equational statements instead of horn clauses. dependency implication is directly reduced to equational implication. our approach is powerful enough to express functional and inclusion dependencies, which are the most common database constraints. we present a new proof procedure for these dependencies. we use our equational formulation to derive new upper and lower bounds for the complexity of their implication problems.  s s cosmadakis p c kanellakis
a complexity theory based on boolean algebra  a projection of a boolean function is a function obtained by substituting for each of its variables a variable, the negation of a variable, or a constant. reducibilities among computational problems under this relation of projection are considered. it is shown that much of what is of everyday relevance in turing-machine-based complexity theory can be replicated easily and naturally in this elementary framework. finer distinctions about the computational relationships among natural problems can be made than in previous formulations and some negative results are proved.  s. skyum l. g. valiant
countable nondeterminism and random assignment  four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. these comprise an operational semantics, two state transformation semantics based on the egli-milner and smyth orders, respectively, and a weakest precondition semantics. their equivalence is proved. a hoare-like proof system for total correctness is also introduced and its soundness and completeness in an appropriate sense are shown. finally, the recursion theoretic complexity of the notions introduced is studied. admission of countable nondeterminism results in a lack of continuity of various semantic functions, and this is shown to be necessary for any semantics satisfying appropriate conditions. in proofs of total correctness, one resorts to the use of (countable) ordinals, and it is shown that all recursive ordinals are needed.  k. r. apt g. d. plotkin
a model and temporal proof system for networks of processes  a model and a sound and complete proof system for networks of processes in which component processes communicate exclusively through messages is given. the model, an extension of the trace model, can describe both synchronous and asynchronous networks. the proof system uses temporal-logic assertions on sequences of observations --- a generalization of traces. the use of observations (traces) makes the proof system simple, compositional and modular, since internal details can be hidden. the expressive power of temporal logic makes it possible to prove temporal properties (safety, liveness, precedence, etc.) in the system. the proof system is language- independent and works for both synchronous and asynchronous networks.  van nguyen david gries susan owicki
parametric pattern router  this paper presents a new pattern router based on an enumeration scheme which sequentially produces alternative paths for a pin pair. first, we represent a pattern or shape of a route by a sequence of symbols representing directions of constituent line segments. then, we investigate a condition that a sequence of symbols represents a valid pattern. we also count all valid patterns.  given two points, we can specify any route between them by a pattern of the route and lengths of segments. if we vary their lengths as parameters, then we can generate various routes. therefore, the parametric pattern router with all possible patterns can always find a path between two points if one exists. the user of the router may define a set of admissible routing patterns according to circumstances.  tetsuo asano
space-time tradeoffs and first order problems in a model of programs  we introduce a model of programs for comparison-based problems. this model gives a measure of space usage and is "uniform". we first obtain upper and lower bounds on the selection problems which demonstrate the tradeoffs between time and space. we next introduce the class of first order problems and characterize them semantically. a surprisingly simple classification of first order problems into three complexity classes is shown. finally we extend the first order problems to the weak second order problems and show that these can be solved in polynomial time by programs in our model augmented with push-down stores.  c. k. yap