waashk/dblp huggingface dataset:
about frequencies of letters in generalized automatic sequences. we present some asymptotic results about the frequency of a letter appearing in a generalized unidimensional automatic sequence. next, we study multidimensional generalized automatic sequences and the corresponding frequencies.
scheduling jobs with agreeable processing times and due dates on a single batch processing machine. in this paper we study the problems of scheduling jobs with agreeable processing times and due dates on a single batch processing machine to minimize total tardiness, and weighted number of tardy jobs. we prove that the problem of minimizing total tardiness is np-hard even if the machine capacity is two jobs and we develop a pseudo-polynomial-time algorithm for an np-hard special case of this problem. we also develop a pseudo-polynomial-time algorithm for the np-hard problem of minimizing weighted number of tardy jobs, which suggests that this problem cannot be strongly np-hard unless p=np.
self-assembly of strings and languages. self-assembly is the process in which simple objects autonomously aggregate into large structures and it has become one of the major tools for nano-scale engineering. we propose in this paper a string-based framework inspired by the principle of self-assembly: two strings with a common overlap, say uv and vw, yield a string uvw; we say that string uvw has been assembled from strings uv and vw. the operation may be extended in a natural way also to sets of strings. we answer several questions: what is the assembly power of a given set of strings, can a given set of strings be generated through assembly and if so, what is a minimal generator for it?
on-line scheduling with delivery time on a single batch machine. we consider a single batch machine on-line scheduling problem with jobs arriving over time. a batch processing machine can handle up to b jobs simultaneously as a batch, and the processing time for a batch is equal to the longest processing time among the jobs in it. each job becomes available at its arrival time, which is not known in advance, and its characteristics, such as processing time and delivery time, become known at its arrival. once the processing of a job is completed we deliver it to the destination. the objective is to minimize the time by which all jobs have been delivered. in this paper, we deal with two variants: the unbound model where b is sufficiently large and the bounded model where b is finite. we provide on-line algorithms with competitive ratio 2 for the unbounded model and with competitive ratio 3 for the bounded model. for when each job has the same processing time, we provide on-line algorithms with competitive ratios (5+1)/2, and these results are the best possible.
degree distribution of the fkp network model. power laws, in particular power-law degree distributions, have been observed in real-world networks in a very wide range of contexts, including social networks, biological networks, and artificial networks such as the physical internet or abstract world wide web. recently, these observations have triggered much work attempting to explain the power laws in terms of new 'scale-free' random graph models. so far, perhaps the most effective mechanism for explaining power laws is the combination of growth and preferential attachment. in [a. fabrikant, e. koutsoupias, c.h. papadimitriou, heuristically optimized trade-offs: a new paradigm for power laws in the internet icalp 2002, in: lncs, vol. 2380, pp. 110-122], fabrikant, koutsoupias and papadimitriou propose a new 'paradigm' for explaining power laws, based on trade-offs between competing objectives. they also introduce a new, simple and elegant parametrized model for the internet, and prove some kind of power-law bound on the degree sequence for a wide range of scalings of the trade-off parameter. here we shall show that this model does not have the usual kind of power-law degree distribution observed in the real world: for the most interesting range of the parameter, neither the bulk of the nodes, nor the few highest degree nodes have degrees following a power law. we shall show that almost all nodes have degree 1, and that there is a strong bunching of degrees near the maximum.
on being a student of john reynolds. the editors of this volume asked me to put together a description of what it was like to be a ph.d. student of john c. reynolds. with the assistance of his other students, this is exactly what i have done. i have asked each of them to contribute their reminiscences on what it was like to work with john, to describe how they came to know john, and to say whatever they would like about how john affected their lives. these contributions will be found below, ordered by the year that each student formally finished his studies. all in all, this piece serves to document the very positive effect that working under john had for those of us lucky enough to work under him.
relational separation logic. in this paper, we present a hoare-style logic for specifying and verifying how two pointer programs are related. our logic lifts the main features of separation logic, from an assertion to a relation, and from a property about a single program to a relationship between two programs. we show the strength of the logic, by proving that the schorr-waite graph marking algorithm is equivalent to the depth-first traversal.
the girard-reynolds isomorphism (second edition). jean-yves girard and john reynolds independently discovered the second-order polymorphic lambda calculus, f2. girard additionally proved a representation theorem: every function on natural numbers that can be proved total in second-order intuitionistic predicate logic, p2, can be represented in f2. reynolds additionally proved an abstraction theorem: every term in f2 satisfies a suitable notion of logical relation; and formulated a notion of parametricity satisfied by well-behaved models. we observe that the essence of girard's result is a projection from p2 into f2, and that the essence of reynolds's result is an embedding of f2 into p2, and that the reynolds embedding followed by the girard projection is the identity. we show that the inductive naturals are exactly those values of type natural that satisfy reynolds's notion of parametricity, and as a consequence characterize situations in which the girard projection followed by the reynolds embedding is also the identity. an earlier version of this paper used a logic over untyped terms. this version uses a logic over typed term, similar to ones considered by abadi and plotkin and by takeuti, which better clarifies the relationship between f2 and p2. this paper uses colour to enhance its presentation. if the link below is not blue, follow it for the colour version. http://homepages.inf.ed.ac.uk/wadler
core algebra revisited. reynolds's work in parametric polymorphism when specialized to a particular example gives rise to the notion of the core of a category and its associated equational theory of core algebras.
on the relations between monadic semantics. we present a simple computational metalanguage with general recursive types and multiple notions of effects, through which a variety of concrete denotational semantics can be conveniently factored, by suitably interpreting the effects as monads. we then propose a methodology for relating two such interpretations of the metalanguage, with the aim of showing that the semantics they induce agree for complete programs. as a prototypical instance of such a relation, we use the framework to show agreement between a direct and a continuation semantics of the simple, untyped functional language from reynolds's original paper on the subject.
combining algebraic effects with continuations. we consider the natural combinations of algebraic computational effects such as side-effects, exceptions, interactive input/output, and nondeterminism with continuations. continuations are not an algebraic effect, but previously developed combinations of algebraic effects given by sum and tensor extend, with effort, to include commonly used combinations of the various algebraic effects with continuations. continuations also give rise to a third sort of combination, that given by applying the continuations monad transformer to an algebraic effect. we investigate the extent to which sum and tensor extend from algebraic effects to arbitrary monads, and the extent to which felleisen et al.'s c operator extends from continuations to its combination with algebraic effects. to do all this, we use dubuc's characterisation of strong monads in terms of enriched large lawvere theories.
flow analysis of lazy higher-order functional programs. in recent years much interest has been shown in a class of functional languages including haskell, lazy ml, sasl/krc/miranda, alfl, orwell, and ponder. it has been seen that their expressive power is great, programs are compact, and program manipulation and transformation is much easier than with imperative languages or more traditional applicative ones. common characteristics: they are purely applicative, manipulate trees as data objects, use pattern matching both to determine control flow and to decompose compound data structures, and use a ''lazy'' evaluation strategy. in this paper we describe a technique for data flow analysis of programs in this class by safely approximating the behavior of a certain class of term rewriting systems. in particular we obtain ''safe'' descriptions of program inputs, outputs and intermediate results by regular sets of trees. potential applications include optimization, strictness analysis and partial evaluation. the technique improves earlier work because of its applicability to programs with higher-order functions, and with either eager or lazy evaluation. the technique addresses the call-by-name aspect of laziness, but not memoization.
a few exercises in theorem processing. the realization of inference rules as the primitive operations of a type ''theorem'' in a type-safe programming language that has so well served lcf and its descendants may, it is suggested, be of interest aside from any immediate context of theorem proving or hardware or software verification. using the general ''conversions'' introduced by paulson, a couple of simple programming exercises with theorem data, imitative of list processing, are presented. an example of a potentially useful notational definition in the hol object language is given as an application.
a syntactic correspondence between context-sensitive calculi and abstract machines. we present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with ten calculi and machines for applicative order with an abort operation, normal order with generalized reduction and call/cc, the lambda-mu-calculus, delimited continuations, stack inspection, proper tail-recursion, and lazy evaluation. most of the machines already exist but they have been obtained independently and are only indirectly related to the corresponding calculi. all of the calculi are new and they make it possible directly to reason about the execution of the corresponding machines.
a bisimulation for dynamic sealing. we define @l"s"e"a"l, an untyped call-by-value @l-calculus with primitives for protecting abstract data by sealing, and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence. this provides a formal basis for reasoning about data abstraction in open, dynamic settings where static techniques such as type abstraction and logical relations are not applicable.
analyzing the environment structure of higher-order languages using frame strings. reasoning about program behaviour in programming languages based on the @l calculus requires reasoning in a unified way about control, data and environment structure. previous analysis work has done an inadequate job on the environment component of this task. we develop a new analytic framework, @dcfa, which is based on a new abstraction: frame strings, an enriched variant of procedure strings that can be used to model both control flow and environment allocation. this abstraction enables new environment-sensitive analyses and transformations that have not been previously attainable. we state the critical theorems needed to establish correctness of the entire technology suite, with their proofs.
a semantics for concurrent separation logic. we present a trace semantics for a language of parallel programs which share access to mutable data. we introduce a resource-sensitive logic for partial correctness, based on a recent proposal of o'hearn, adapting separation logic to the concurrent setting. the logic allows proofs of parallel programs in which ''ownership'' of critical data, such as the right to access, update or deallocate a pointer, is transferred dynamically between concurrent processes. we prove soundness of the logic, using a novel ''local'' interpretation of traces which allows accurate reasoning about ownership. we show that every provable program is race-free.
language equations with complementation: decision problems. systems of language equations of the form x"i=@f"i(x"1,...,x"n)(1=
attributed graph transformation with node type inheritance. the aim of this paper is to integrate typed attributed graph transformation with node type inheritance. borrowing concepts from object oriented systems, the main idea is to enrich the attributed type graph with an inheritance relation and a set of abstract nodes. in this way, a node type inherits the attributes and edges of all its ancestors. based on these concepts, it is possible to define abstract productions, containing abstract nodes. these productions are equivalent to a number of concrete productions, resulting from the substitution of the abstract node types by the node types in their inheritance clan. therefore, productions become more compact and suitable for their use in combination with meta-modelling. the main results of this paper show that attributed graph transformation with node type inheritance is fully compatible with the existing concept of typed attributed graph transformation.
context-dependent nondeterminism for pushdown automata. pushdown automata using a limited and unlimited amount of nondeterminism are investigated. moreover, nondeterministic steps are allowed only within certain contexts, i.e., in configurations that meet particular conditions. the relationships of the accepted language families with closures of the deterministic context-free languages (dcfl) under regular operations are studied. for example, automata with unbounded nondeterminism that have to empty their pushdown store up to the initial symbol in order to make a guess are characterized by the regular closure of dcfl. automata that additionally have to reenter the initial state are (almost) characterized by the kleene star closure of the union closure of the prefix-free deterministic context-free languages. pushdown automata with bounded nondeterminism are characterized by the union closure of dcfl in any of the considered contexts. proper inclusions between all language classes discussed are shown. finally, closure properties of these families under afl operations are investigated.
automated compositional proofs for real-time systems. we present a framework for formally proving that the composition of the behaviors of the different parts of a complex, real-time system ensures a desired global specification of the overall system. the framework is based on a simple compositional rely/guarantee circular inference rule, plus a methodology concerning the integration of the different parts into a whole system. the reference specification language is the trio metric linear temporal logic. the novelty of our approach with respect to existing compositional frameworks-most of which do not deal explicitly with real-time requirements-consists mainly in its generality and abstraction from any assumptions about the underlying computational model and from any semantic characterizations of the temporal logic language used in the specification. moreover, the framework deals equally well with continuous and discrete time. it is supported by a tool, implemented on top of the proof-checker pvs, to perform deduction-based verification through theorem-proving of modular real-time axiom systems. as an example of application, we show the verification of a real-time version of the old-fashioned but still relevant ''benchmark'' of the dining philosophers problem.
on some variations of two-way probabilistic finite automata models. rabin [m. rabin, probabilistic finite automata, information and control (1963) 230-245] initiated the study of probabilistic finite automata (pfa). rabin's work showed a crucial role of the gap in the error bound (for accepting and non-accepting computations) in the power of the model. further work resulted in the identification of qualitatively different error models (one-sided error, bounded and unbounded errors, no error etc.) karpinski and verbeek [m. karpinski, r. verbeek, there is no polynomial deterministic simulation of probabilistic space with two-way random-tape generator, information and control 67 (1985) 158-162] and nisan [n. nisan, on read-once vs. multiple access to randomness in logspace, in: proc. of fifth ieee structure in complexity theory, barcelona, spain, 1990, pp. 179-184] studied a model of probabilistic automaton in which the tape containing random bits can be read by a two-way head. they presented results comparing models with one-way vs. two-way access to randomness. dwork and stockmeyer [c. dwork, l. stockmeyer, interactive proof systems with finite state verifiers, ibm report rj 6262, 1988] and condon et al. [a. condon, et al., on the power of finite automata with both nondeterministic and probabilistic states, siam journal on computing (1998) 739-762] studied a model of 2-pfa with nondeterministic states (2-npfa). in this paper, we present some results about the above mentioned variations of probabilistic finite automata, as well as a model of 2-pfa augmented with a pebble studied in [b. ravikumar, some observations on two-way probabilistic finite automata, in: proc. of the foundations of software technology and theoretical computer science, 1992, pp. 392-403]. our observations indicate that these models exhibit subtle variations in their computational power. we also mention many open problems about these models. complete characterizations of their power will likely provide deeper insights about the role of randomness in space-bounded computations.
can abstract state machines be useful in language theory? the abstract state machine (asm) is a modern computation model. asms and asm based tools are used in academia and industry, albeit on a modest scale. they allow you to give high-level operational semantics to computer artifacts and to write executable specifications of software and hardware at the desired abstraction level. in connection with the 2006 conference on developments in language theory, we point out several ways that we believe abstract state machines can be useful to the dlt community.
events and modules in reaction systems. reaction systems are a formal model of interactions between biochemical reactions. they are based on the observation that two basic mechanisms behind the functioning of biochemical reactions are facilitation and inhibition. in this paper we continue the investigation of reaction systems, and in particular we introduce the notion of a module, and then we investigate the formation and evolution of modules. among others we prove that reaction systems can be viewed as self-organizing systems, where the organizing goal is to ensure a specific property of the set of all modules (of a state of a process).
synchronizing automata with a letter of deficiency 2. we present two infinite series of synchronizing automata with a letter of deficiency 2 whose shortest reset words are longer than those for synchronizing automata obtained by a straightforward modification of cerny's construction.
modeling adaptive behaviors in context unity. context-aware computing refers to a paradigm in which applications sense aspects of the environment and use this information to adjust their behavior in response to changing circumstances. in this paper, we present a formal model and notation (context unity) for expressing quintessential aspects of context-aware computations; existential quantification, for instance, proves to be highly effective in capturing the notion of discovery in open systems. furthermore, context unity treats context in a manner that is relative to the specific needs of an individual application and promotes an approach to context maintenance that is transparent to the application. in this paper, we construct the model from first principles, introduce its proof logic, and demonstrate how the model can be used as an effective abstraction tool for context-aware applications and middleware.
equivalence of simple functions. a partial function f:@s^*->@w^* is called a simple function if f(w)@?@w^* is the output produced in the leftmost derivation of a word w@?@s^* from a nonterminal of a simple context free grammar g with output alphabet @w. in this paper we present an efficient algorithm for testing the equivalence of simple functions. such functions correspond also to one-state deterministic pushdown transducers. our algorithm works in time polynomial with respect to |g|+v(g), where |g| is the size of the textual description of g, and v(g) is the maximum of the shortest lengths of words generated by nonterminals of g.
on the existence of prime decompositions. we investigate factorizations of regular languages in terms of prime languages. a language is said to be strongly prime decomposable if any way of factorizing it yields a prime decomposition in a finite number of steps. we give a characterization of the strongly prime decomposable regular languages and using the characterization we show that every regular language over a unary alphabet has a prime decomposition. we show that there exist non-regular unary languages that do not have prime decompositions. we also consider infinite factorizations of unary languages.
observational purity and encapsulation. practical specification languages for imperative and object-oriented programs, such as jml, eiffel, and spec#, allow the use of program expressions including method calls in specification formulas. for coherent semantics of specifications, and to avoid anomalies with runtime assertion checking, expressions in specifications and assertions are typically required to be weakly pure in the sense that their evaluation has no effect on the state of preexisting objects. for specification of large systems using standard libraries this restriction is impractical: it disallows many standard methods that mutate state for purposes such as caching or lazy initialization. calls of such methods can sensibly be used for specifications and annotations in contexts where their effects cannot be observed. this paper formalizes a notion of observational purity, justifies the use of weakly and observationally pure methods in specifications, and shows that a method is observationally pure if it simulates a weakly pure method.
the growth ratio of synchronous rational relations is unique. we introduce @a-synchronous relations for a rational number @a. we show that if a rational relation is both @a- and @a^'-synchronous for two different numbers @a and @a^', then it is recognizable. we give a synchronization algorithm for @a-synchronous transducers. we also prove the closure under boolean operations and composition of @a-synchronous relations.