waashk/dblp huggingface dataset:
regular binoid expressions and regular binoid languages. a bisemigroup consists of a set of elements and two associative operations. a bimonoid is a bisemigroup which has an identity to each associative operation. a binoid is a bimonoid which has the same identity to the two associative operations. in a previous paper, we introduced these three notions, and studied formal languages over free binoids (which are subsets of a free binoid where any element of a free binoid is denoted by its standard form which is a sequence of symbols). in this paper, we introduce a class of expressions called regular binoid expressions and show that any binoid language denoted by a regular binoid expression can be regarded to be a set of the standard forms of elements of a free binoid which can be recognized as a regular (monoid) language.
equivalence of regular binoid expressions and regular expressions denoting binoid languages over free binoids. a free binoid σ*(○, •) over a finite alphabet σ is a free algebra generated by σ with two independent associative operators, ○ and •. it has also the same identity λ to both operations. any element of σ*(○, •) is denoted uniquely by a sequence of symbols from the extended alphabet e(σ) = σ ∪ {○, • (,)}, and any subset of a free binoid is called a binoid language. the set of regular binoid expressions are introduced so that all languages denoted by regular binoid expressions are those which contain finite binoid languages, and closed under five operations, ∪, ○-concatenation, •-concatenation, ○-closure and •-closure. it is shown that for any regular (monoid) expression denoting a binoid language r, there exists a regular binoid expression denoting r. this result together with the main result in a previous paper implies that the class of binoid languages denoted by binoid regular expressions is the same as the class of binoid languages denoted by regular expressions over free binoids.
on the lengths of symmetry breaking-preserving games on graphs. given a graph g, we consider a game where two players, a and b, alternatingly, color edges of g in red and in blue, respectively. let lsym(g) be the maximum number of moves in which b is able to keep the red and the blue subgraphs isomorphic, if a plays optimally to destroy the isomorphism. this value is a lower bound for the duration of any avoidance game on g under the assumption that b plays optimally. we prove that if g is a path or a cycle of odd length n, then ω(logn) ≤ lsym(g) ≤ o(log2 n). the lower bound is based on relations with ehrenfeucht-fraïssé games from model theory. we also consider complete graphs and prove that lsym(kn) = o(1).
a typed context calculus. this paper develops a typed calculus for contexts i.e., lambda terms with "holes". in addition to ordinary lambda terms, the calculus contains labeled holes, hole abstraction and context application for manipulating first-class contexts. the primary operation for contexts is hole-filling, which captures free variables. this operation conflicts with substitution of the lambda calculus, and a straightforward mixture of the two results in an inconsistent system. we solve this problem by defining a type system that precisely specifies the variable-capturing nature of contexts and that keeps track of bound variable renaming. these mechanisms enable us to define a reduction system that properly integrates&brg;-reduction and hole-filling. the resulting calculus is church-rosser and the type system has the subject reduction property. we believe that the context calculus will serve as a basis for developing a programming language with advanced features that call for manipulation of open terms. copyright 2001 elsevier science b.v.
efficient reconfiguration algorithms of de bruijn and kautz networks into linear arrays. in this paper, we prove the existence of ranking and unranking algorithms on d-ary de bruijn and kautz graphs. a ranking algorithm takes as input the label of a node and returns the rank r of that node in a hamiltonian path (06r6n - 1, where n is the order of the considered graph). an unranking algorithm takes as input an integer r (06r6n - 1) and returns the label of the rth ranked node in a hamiltonian path. our results generalize results given by annexstein for binary de bruijn graphs. the key of our framework is based on a recursive construction of hamiltonian paths in de bruijn and kautz graphs. the construction uses suitable uniform homomorphisms of de bruijn and kautz graphs of diameter d on de bruijn graphs of diameter d - 1. our ranking and unranking algorithms have sequential time complexity in o(d2), where d is the length of node labels.
a non-hausdorff quaternion multiplication. we denote by (s3)' the barycentric subdivision of the minimal model s3 of the three-dimensional sphere in the category of finite posets and order-preserving functions, op(x) is the poset obtained by reversing the order relations in a poset x. we describe a finite model of a quaternion multiplication in the form of a morphism op(s3)' × (s3)' → s3 that restricts to weak homotopy equivalences on the axes. for such multiplications a version of hopf's construction can be defined that yields finite models of non-trivial homotopy classes.
a coalgebraic approach to the semantics of the ambient calculus. recently, various process calculi have been introduced which are suited for the modelling of mobile computation and in particular the mobility of program code; a prominent example is the ambient calculus. due to the complexity of the involved spatial reduction, there is--in contrast to the situation in standard process algebra--up to now no satisfying coalgebraic representation of a mobile process calculus. here, we discuss a coalgebraic denotational semantics for the ambient calculus, viewed as a step towards a generic coalgebraic framework for modelling mobile systems. crucial features of our modelling are a set of gsos style transition rules for the ambient calculus, a hardwiring of the so-called hardening relation in the functorial signature, and a set-based treatment of hidden name sharing. the formal representation of this framework is cast in the algebraic-coalgebraic specification language cocasl.
on quasi orders of words and the confluence property. we investigate the confluence property, that is, the property of a language to contain, for any two words of it, one which is bigger, with respect to a given quasi order on the respective free monoid, than each of the former two. this property is investigated mainly for regular and context-free languages. as a consequence of our study, we give an answer to an old open problem raised by haines concerning the effective regularity of the sets of subwords. namely, we prove that there are families with a decidable emptiness problem for which the regularity of the sets of subwords is not effective.
many aspects of defect theorems. we give a survey and a unified presentation of the defect theorem, its generalizations and recent aspects of interest. in its basic form, the defect theorem states that if a set of n words satisfies a nontrivial relation, then these words can be expressed simultaneously as products of at most n - 1 words. in other words, dependency of words causes a defect effect. there does not exist just one defect theorem, but several ones depending on the restrictions that are put to the n - 1 words. the defect theorem is closely related to equations of words, and in this way to the compactness theorem for systems of word equations.
mathematics based on incremental learning - excluded middle and inductive inference. learning theoretic aspects of mathematics and logic have been studied by many authors. they study how mathematical and logical objects are algorithmically "learned" (inferred) from finite data. although they study mathematical objects, the objective of the studies is learning. in this paper, a mathematics whose foundation itself is learning theoretic will be introduced. it is called limit-computable mathematics. it was originally introduced as a means for "proof animation", which is expected to make interactive formal proof development easier. although the original objective was not learning theoretic at all, learning theory is indispensable for our research. it suggests that logic and learning theory are related in a still unknown but deep new way.
uniform characterizations of polynomial-query learnabilities. we consider the exact learning in the query model. we deal with all types of queries introduced by angluin: membership, equivalence, superset, subset, disjointness and exhaustiveness queries, and their weak (or restricted) versions where no counterexample is returned. for each of all possible combinations of these queries, we uniformly give complete characterizations of boolean concept classes that are learnable using a polynomial number of polynomial-sized queries. our characterizations show the equivalence between the learnability of a concept class c using queries and the existence of a good query for any subset h of c which is guaranteed to reject a certain fraction of candidate concepts in h regardless of the answer. as a special case for equivalence queries alone, our characterizations directly correspond to the lack of the approximate fingerprint property, which is known to be a sufficient and necessary condition for the learnability using equivalence queries.
towards the animation of proofs - testing proofs by examples. in this paper, we introduce the notion of proof animation, which is a new application of the principle of "curry-howard isomorphism" to formal proof development. logically, proof animation is merely a contrapositive of "proofs as programs", which is an application of curry-howard isomorphism to formal program development. nonetheless, this new perspective is completely different. the motivation, aims, problems, and a prototype tool under development are presented in this paper. we also discuss possibility of "proof engineering" guided by the curry-howard isomorphism. copyright 2002 elsevier science b.v.
a characterization of periodicity of bi-infinite words. a finite word is called bordered if it has a proper prefix which is also a suffix of that word. costa proves in [theoret. comput. sci. 290(3) (2003) 2053-2061] that a bi-infinite word w is of the form ωf g fω, for some finite words f and g, if, and only if, there is a factorization w = suv, with u ∈ a* such that every factor s'uv', with s' ≤ s and v' ≤ v, is bordered. we present a shorter proof of that result in this paper.
the wide window string matching algorithm. generally, current string matching algorithms make use of a window whose size is equal to pattern length. in this paper, we present a novel string matching algorithm named ww (for wide window) algorithm, which divides the text into [n/m] overlapping windows of size 2m - 1. in the windows, the algorithm attempts m possible occurrence positions in parallel. it firstly searches pattern suffixes from middle to right with a forward suffix automaton, shifts the window directly when it fails, otherwise, scans the corresponding prefixes backward with a reverse prefix automaton. theoretical analysis shows that ww has optimal time complexity of o(n) in the worst, o(n/m) best and o(n(logσm)/m) for average case. experimental comparison of ww with existing algorithms validates our theoretical claims for searching long patterns. it further reveals that ww is also efficient for searching short patterns.
on the independence of equations in three variables. we prove that an independent system of equations in three variables with a nonperiodic solution and at least two equations consists of balanced equations only. for that, we show that the intersection of two different entire systems contains only balanced equations, where an entire system is the set of all equations solved by a given morphism. furthermore, we establish that two equations which have a common nonperiodic solution have the same set of periodic solutions or are not independent.
improved algorithms for two single machine scheduling problems. in this paper, we investigate two single machine scheduling problems. the first problem addresses a class of the two-stage scheduling problems in which the first stage is job production and the second stage is job delivery. for the case that jobs are processed on a single machine and delivered by a single vehicle to one customer area, with the objective of minimizing the time when all jobs are completed and delivered to the customer area and the vehicle returns to the machine, an approximation algorithm with a worst-case ratio of 5/3 is known and no approximation can have a worst-case of 3/2 unless p = np. we present an improved approximation algorithm with a worst-case ratio of 53/35, which only leaves a gap of 1/70. the second problem is a single machine scheduling problem subject to a period of maintenance. the objective is to minimize the total completion time. the best known approximation algorithm has a worst-case ratio of 20/17 we present a polynomial time approximation scheme.
counting bordered and primitive words with a fixed weight. a word w is primitive if it is not a proper power of another word, and w is unbordered if it has no prefix that is also a suffix of w. we study the number of primitive and unbordered words w with a fixed weight, that is, words for which the parikh vector of w is a fixed vector. moreover, we estimate the number of words that have a unique border.
on unique factorizations of primitive words. we give a short proof of a result by weinbaum [unique sunwords in nonperiodic words, proc. amer. math. soc. 109(3) (1990) 615-619] stating that each primitive word of length at least 2 has a conjugate w' = uv such that both u and v have a unique position in the cyclic word of w. we emphasize the connection of weinbaum's result to the critical factorization theorem.
on the bandwidth of a hamming graph. the bandwidth of the hamming graph (the product, (kn)d, of complete graphs) has been an open question for many years. recently berger-wolf and rheingold [1] pointed out that the bandwidth of a numbering of the hamming graph may be interpreted as a measure of the effects of noise in the multi-channel transmission of data with that numbering. they also gave lower and upper bounds for it. in this paper we present better lower and upper bounds, showing that the bandwidth of kn)d is asymptotic to √(2/πd)nd as d → ∞.
uniqueness logic. a uniqueness type system is used to distinguish values which are referenced at most once from values which may be referenced an arbitrary number of times in a program. uniqueness type systems are used in the clean and mercury programming languages to provide efficiently updatable data-structures and i/o without compromising referential transparency.in this paper we establish a curry-howard-lambek equivalence between a form of uniqueness types and a 'resource-sensitive' logic. this logic is similar to intuitionistic linear logic, however the modality, which moderates the structural rules in the antecedent in the same way as !, is introduced via the dual ? rules. we discuss the categorical proof theory and models of this new logic, as well as its computational interpretation.
turning back time in markovian process algebra. product-form solutions in markovian process algebra (mpa) are constructed using properties of reversed processes. the compositionality of mpas is directly exploited, allowing a large class of hierarchically constructed systems to be solved for their state probabilities at equilibrium. the paper contains new results on both reversed stationary markov processes as well as mpa itself and includes a mechanisable proof in mpa notation of jackson's theorem for product-form queueing networks. several examples are used to illustrate the approach.
algorithms for multi-level graph planarity testing and layout. in this paper we consider the problems of testing a multi-level graph for planarity and laying out or, drawing, a multi-level graph in a clear way. we introduce a new abstraction of a common integer linear programming formulation of the problems that we call a vertex-exchange graph. we demonstrate how this concept can be used to solve the problems by providing clear and simple algorithms for testing a multi-level graph for planarity and laying out a multi-level graph when planar.
some complexity results for polynomial rational expressions. it is known that any languages of level 3/2 of the straubing-thérien hierarchy can be written as a polynomial expression, that is, a finite union of languages of the form a0*b1a*1 ... b*kak where the ai and bi are subsets of the alphabet. in this paper we prove that such a polynomial expression for a 3/2-level language can be of exponential size. more precisely we exhibit an n-state minimal automaton recognizing a level 3/2 language for which the shortest polynomial expresion has exponential size in n.
pspace-completeness of sliding-block puzzles and other problems through the nondeterministic constraint logic model of computation. we present a nondeterministic model of computation based on reversing edge directions in weighted directed graphs with minimum in-flow constraints on vertices. deciding whether this simple graph model can be manipulated in order to reverse the direction of a particular edge is shown to be pspace-complete by a reduction from quantified boolean formulas. we prove this result in a variety of special cases including planar graphs and highly restricted vertex configurations, some of which correspond to a kind of passive constraint logic. our framework is inspired by (and indeed a generalization of) the "generalized rush hour logic" developed by flake and baum [theoret. comput. sci. 270(1-2) (2002) 8951.we illustrate the importance of our model of computation by giving simple reductions to show that several motion-planning problems are pspace-hard. our main result along these lines is that classic unrestricted sliding-block puzzles are pspace-hard, even if the pieces are restricted to be all dominoes (1 × 2 blocks) and the goal is simply to move a particular piece. no prior complexity results were known about these puzzles. this result can be seen as a strengthening of the existing result that the restricted rush hourtm puzzles are pspace-complete [theoret. comput. sci. 270(1-2) (2002) 895], of which we also give a simpler proof. we also greatly strengthen the conditions for the pspace-hardness of the warehouseman's problem [int. j. robot. res. 3(4) (1984) 76], a classic motion-planning problem. finally, we strengthen the existing result that the pushing-blocks puzzle sokoban is pspace-complete [in: proc. internat. conf. on fun with algorithms, elba, italy, june 1998, pp. 65-76.], by showing that it is pspace-complete even if no barriers are allowed.
separable equilibrium state probabilities via time reversal in markovian process algebra. the reversed compound agent theorem (rcat) is a compositional result that uses markovian process algebra (mpa) to derive the reversed process of certain interactions between two continuous time markov chains at equilibrium. from this reversed process, together with the given, forward process, the joint state probabilities can be expressed as a product-form, although no general algorithm has previously been given. this paper first generalises rcat to multiple (more than two) cooperating agents, which removes the need for multiple applications and inductive proofs in cooperations of an arbitrary number of processes. a new result shows a simple stochastic equivalence between cooperating, synchronised processes and corresponding parallel, asynchronous processes. this greatly simplifies the proof of the new, multi-agent theorem, which includes a statement of the desired product-form solution itself as a product of given state probabilities in the parallel components. the reversed process and product-form thus derived rely on a solution to certain rate equations and it is shown, for the first time, that a unique solution exists under mild conditions--certainly for queueing networks and g-networks.
characterising fs domains by means of power domains. fs domains can be characterised using the upper or lower power domain construction. in these characterisations, separation by the elements of a finite set is replaced by separation by a continuous non-deterministic function with finite image. this notion of separation can be formalised in many different, but equivalent ways.
canonical substitutions tilings of ammann-beenker type. we present a large class of parallelogram tilings that have two important features in common with the ammann-beenker tiling: they can be constructed by canonical projection from z4 ⊂ r4 to a plane, and they admit substitution rules.
contractivity of linear fractional transformations. one possible approach to exact real arithmetic is to use linear fractional transformations (lfts) to represent real numbers and computations on real numbers. recursive expressions built from lfts are only convergent (i.e., denote a well-defined real number) if the involved lfts are sufficiently contractive. in this paper, we define a notion of contractivity for lfts. it is used for convergence theorems and for the analysis and improvement of algorithms for elementary functions.
on log-tape isomorphisms of complete sets. in this paper we study $\log n$-tape computable reductions between sets and investigate conditions under which $\log n$-tape reductions between sets can be extended to $\log n$-tape computable isomorphisms of these sets. as an application of these results we obtain easy to check necessary and sufficient conditions that sets complete under $\log n$-tape reductions in nl, csl, p, np, ptape, etc. are $\log n$-tape isomorphic to the previously known complete sets in the respective classes. as a matter of fact, all the "known" complete sets for nl, csl, p, np, ptape, etc. are now easily seen to be, respectively, $\log n$-tape isomorphic. these results strengthen and extend substantially the previously known results about polynomial time computable reductions and isomorphisms of np and ptape complete sets. furthermore, we show that any set complete in csl, ptape, etc. must be dense and therefore, for example, cannot be over a single letter alphabet.
a non-topological view of dcpos as convergence spaces. the category top of topological spaces is not cartesian closed, but can be embedded into the cartesian closed category conv of converyence spaces. it is well known that the category dcpo of dcpos and scott continuous functions can be embedded into top, and so into conv, by considering the scott topology. we propose a different, "cotopological" embedding of dcpo into conv, which, in contrast to the topological embedding, preserves products. if x is a cotopological dcpo, i.e. a dcpo with the cotopological conv-structure, and y is a topological space, then [x → y] is again topological, and conversely, if x is a topological space, and y a cotopological complete lattice, then [x → y] is again a cotopological complete lattice. for a dcpo d, the topological and the cotopological convergence structures coincide if and only if d is a continuous dcpo. moreover, cotopological dcpos still enjoy some of the properties which characterise continuous dcpos. for instance, all cotopological complete lattices are injective spaces (in conv) w.r.t. topological subspace embeddings.
relations between diagonalization, proof systems, and complexity gaps. in this paper we study diagonal processes over time-bounded computations of one-tape turing machines by diagonalizing only over those machines for which there exist formal proofs that they operate in the given time bound. this replaces the traditional &ldquo;clock&rdquo; in resource bounded diagonalization by formal proofs about running times and establishes close relations between properties of proof systems and existence of sharp time bounds for one-tape turing machine complexity classes. furthermore, these diagonalization methods show that the gap theorem for resource bounded computations does not hold for complexity classes consisting only of languages accepted by turing machines for which it can be formally proven that they run in the required time bound.