waashk/dblp huggingface dataset:
polynat in per models. the polymorphic lambda-calculus can be modelled using pers on a partial combinatory algebra. we say that the type of natural numbers (polynat) is polymorphically standard in such a model if the interpretation of the type only contains (the interpretations of) the church numerals. we show that this is not always the case by constructing an explicit counterexample. on the other hand, when the pca has either (strong) equality or weak equality plus a form of continuity, we show polynat is standard.
explicit test sets for iterated morphisms in free monoids and metabelian groups. for checking equivalence of any two word morphisms, restricted on a subset (language), it suffices to do this for a finite subset of the language, the so-called finite test set. a way of effectively obtaining a finite test set for a special class of languages, the so-called iterated morphisms, is presented here together with an explicit upper bound for its size. the method can be extended to free metabelian groups, and to certain other metabelian groups.
universal coalgebra: a theory of systems. in the semantics of programming, finite data types such as finite lists, have traditionally been modelled by initial algebras. later final coalgebras were used in order to deal with infinite data types. coalgebras, which are the dual of algebras, turned out to be suited, moreover, as models for certain types of automata and more generally, for (transition and dynamical) systems. an important property of initial algebras is that they satisfy the familiar principle of induction. such a principle was missing for coalgebras until the work of aczel (1988) on a theory of non-wellfounded sets, in which he introduced a proof principle nowadays called coinduction. it was formulated in terms of bisimulation, a notion originally stemming from the world of concurrent programming languages (milner, 1980; park, 1981). using the notion of coalgebra homomorphism, the definition of bisimulation on coalgebras can be shown to be formally dual to that of congruence on algebras (aczel and mendler, 1989). thus the three basic notions of universal algebra: algebra, homomorphism of algebras, and congruence, turn out to correspond to: coalgebra, homomorphism of coalgebras, and bisimulation, respectively. in this paper, the latter are taken as the basic ingredients of a theory called universal coalgebra. some standard results from universal algebra are reformulated (using the afore mentioned correspondence) and proved for a large class of coalgebras, leading to a series of results on, e.g., the lattices of subcoalgebras and bisimulations, simple coalgebras and coinduction, and a covariety theorem for coalgebras similar to birkhoff''s variety theorem.
behavioural differential equations: a coinductive calculus of streams, automata, and power series. we present a theory of streams (infinite sequences), automata and languages, and formal power series, in terms of the notions of homomorphism and bisimulation, which are the cornerstones of the theory of (universal) coalgebra. this coalgebraic perspective leads to a unified theory, in which the observation that each of the aforementioned sets carries a so-called final automaton structure, plays a central role. finality forms the basis for both definitions and proofs by coinduction, the coalgebraic counterpart of induction. coinductive definitions take the shape of what we have called behavioural differential equations, after brzozowski's notion of input derivative. a calculus is developed for coinductive reasoning about all of the afore mentioned structures, closely resembling calculus from classical analysis.
a tutorial on coinductive stream calculus and signal flow graphs. this paper presents an application of coinductive stream calculus to signal flow graphs. in comparison to existing approaches, which are usually based on z-transforms (a discrete version of laplace transforms) and transfer functions, the model presented in these notes is very elementary. the formal treatment of flow graphs is interesting because it deals with two fundamental phenomena in the theory of computation: memory (in the form of register or delay elements) and infinite behaviour (in the form of feedback).
elements of generalized ultrametric domain theory. a generalized ultrametric space is an ordinary ultrametric space in which the distance need not be symmetric, and where different elements may have distance 0. our interest in generalized ultrametric spaces is primarily motivated by the following observations: 1. (possibly nondeterministic) transition systems can be naturally endowed with a generalized ultrametric that captures their operational behavior in terms of simulations; 2. the category of generalized ultrametric spaces contains both the categories of preorders and of ordinary ultrametric spaces as full subcategories. a theory of generalized ultrametric spaces is developed along the lines of the work by smyth and plotkin (1982) and america and rutten (1989), such that its restriction to preorders and ordinary ultrametric spaces yields (more and less) familiar facts. our work has in common with other recent work along the same lines---by flagg and kopperman, and wagner---that it is directly based on lawvere''s v-categorical interpretation of metric spaces, and uses results on quasimetrics by smyth. it is different in being far less general, and consequently a number of new results, specific for generalized ultrametric spaces, is obtained. in particular, domain equations are solved by means of metric adjoint pairs, and the notions of (generalized) totally-boundedness and bifinite (or `sfu'') domain are introduced and characterized.
application of kolmogorov complexity and universal codes to identity testing and nonparametric testing of serial independence for time series. we show that kolmogorov complexity and such its estimators as universal codes (or data compression methods) can be applied for hypotheses testing in a framework of classical mathematical statistics. the methods for identity testing and nonparametric testing of sérial independence for time series are suggested.
on the p-np problem over real matrix rings. we prove that p ≠ dnp over rings of matrices with real elements in a restricted blum-shub-smale computational model. the restriction is that machines can use only two constants (zero-matrix and identity matrix) in computations. also we show that in the unrestricted blum-shub-smale model p = dnp over real matrix rings iff p = dnp over the non-ordered real ring and the same is true for the equality p = np. the latter assertion implies that p ≠ np over real matrix rings.
the structure of subword graphs and suffix trees of fibonacci words. we use automata-theoretic approach to analyze properties of fibonacci words. the directed acyclic subword graph (dawg) is a useful deterministic automaton accepting all suffixes of the word. we show that dawg's of fibonacci words have particularly simple structure. our main result is a unifying framework for a large collection of relatively simple properties of fibonacci words. the simple structure of dawgs of fibonacci words gives in many cases simplified alternative proofs and new interpretation of several well-known properties of fibonacci words. in particular, the structure of lengths of paths corresponds to a number-theoretic characterization of occurrences of any subword. using the structural properties of dawg's it can be easily shown that for a string ω we can check if ω is a subword of a fibonacci word in time o(|ω|) and o(1) space. compact dawg's of fibonacci words show a very regular structure of their suffix trees and show how the suffix tree for the fibonacci word grows (extending the leaves in a very simple way) into the suffix tree for the next fibonacci word.
multiple points of tilings associated with pisot numeration systems. this paper deals with a kind of aperiodic tilings associated with pisot numeration systems, originally due to w.p. thurston, in the formulation of s. akiyama. we treat tilings whose generating pisot units β are cubic and not totally real. each such tiling gives a numeration system on the complex plane; we can express each complex number z in the following form: z = ck α-k + ck-1 α-k+1 +...+ c1 α-1 + c0 + c-1 α1 + c-2 α2 +..., where α is a conjugate of β, and c-m c-m+1... ck-1 ck is the β-expansion of some real number for any integer m. we determine the set of complex numbers which have three or more representations. this is equivalent to determining the triple points of the tiling, which is shown to be a collection of model sets (or cut-and-project sets). we also determine the set of complex numbers with eventually periodic representations.
combinatorics and algorithms for low-discrepancy roundings of a real sequence. we discuss the problem of computing all the integer sequences obtained by rounding an input sequence of n real numbers such that the discrepancy between the input sequence and each output binary sequence is less than one. the problem arises in the design of digital halftoning methods in computer graphics. we show that the number of such roundings is at most n + 1 if we consider the discrepancy with respect to the set of all subintervals, and give an efficient algorithm to report all of them. then, we give an optimal method to construct a compact graph to represent the set of global roundings satisfying a weaker discrepancy condition.
bias and pathology in minimax search. this article presents the results of experiments designed to gain insight into the effect of the minimax algorithm on the error of a heuristic evaluation function. two types of effect of minimax are considered: (a) evaluation accuracy (are the minimax backed-up values more accurate than the heuristic values themselves?), and (b) decision accuracy (are moves played by deeper minimax search better than those by shallower search?). the experiments were performed in the king-rook-king (krk) chess endgame and in randomly generated game trees. the results show that, counter-intuitively, evaluation accuracy may decline with search depth, whereas at the same time decision accuracy improves with depth. in the article, this is explained by the fact that minimax in combination with a noisy evaluation function introduces a bias into the backed-up evaluations, which masks the evaluation effectiveness of minimax, but this bias still permits decision accuracy to improve with depth. this observed behaviour of minimax in the krk endgame is discussed in the light of previous studies of pathology in minimax. it is shown that explaining the behaviour of minimax in an actual chess endgame in terms of previously known results requires special care.
on an optimal propositional proof system and the structure of easy subsets of taut. in this paper we develop a connection between optimal propositional proof systems and structural complexity theory--specifically, there exists an optimal propositional proof system if and only if there is a suitable recursive presentation of the class of all easy (polynomial time recognizable) subsets of taut. as a corollary we obtain the result that if there does not exist an optimal propositional proof system, then for every theory t there exists an easy subset of taut which is not t-provably easy.
ordering default theories and nonmonotonic logic programs. first-order theories are ordered under logical entailment based on the amount of information derived from theories. in default logic, on the other hand, a theory contains default information as well as definite information. to order default theories, distinguishing different sorts of information is necessary to assess the information content of a default theory. for this purpose, we first introduce a multi-valued interpretation of default theories using a ten-valued bilattice. it distinguishes between definite and credulous/skeptical default information derived from a theory, and is used for ordering default theories based on their information contents. we then apply the technique to order nonmonotonic logic programs under the answer set semantics. the results of this paper provide a method for comparing default theories or nonmonotonic logic programs in a manner different from the conventional extension/model-based viewpoint. moreover, they have important application to induction from nonmonotonic theories.
learning elementary formal systems with queries. the elementary formal system (efs) is a kind of logic programs which directly manipulates strings, and the learnability of the subclass called hereditary efss (hefss) has been investigated in the frameworks of the pac-learning, query-learning, and inductive inference models. the hierarchy of hefs is expressed by hefs(m,k,t,r), where m, k, t and r denote the number of clauses, the occurrences of variables in the head, the number of atoms in the body, and the arity of predicate symbols. the present paper deals with the learnability of hefs in the query learning model using equivalence queries and additional queries such as membership, predicate membership, entailment membership, and dependency queries. we show that the class hefs(*, k, t, r) is polynomial-time learnable with the equivalence and predicate membership queries and the class hefs(*,k,*,r) with termination property is polynomial-time learnable with the equivalence, entailment membership, and dependency queries for the unbounded parameter *. a lowerbound on the number of queries is presented. we also show that the class hefs(*,k,t,r) is hard to learn with the equivalence and membership queries under the cryptographic assumptions. furthermore, the learnability of the class of unions of regular pattern languages, which is a subclass of hefss, is investigated. the bounded unions of regular pattern languages are polynomial-time predictable with membership query. however, all unbounded unions of regular pattern languages are not polynomial-time predictable with membership queries if neither are the dnf formulas.
on dart-free perfectly contractile graphs. the dart is a graph obtained from a 4-clique by removing one edge and adding a pendant vertex adjacent to one vertex of degree three. an even pair is pair of vertices such that every chordless path between them has even length. a graph is perfectly contractile if every induced subgraph has a sequence of even-pair contractions that leads to a clique. we show that the dart-free graphs satisfy the conjecture of everett and reed about the forbidden structures for perfectly contractile graphs. our proof yields a polynomial-time algorithm to recognize dart-free perfectly contractile graphs.
uni-transitional watson-crick d0l systems. the phenomenon known as watson-crick complementarity is basic both in the experiments and theory of dna computing. while the massive parallelism of dna strands makes exhaustive searches possible, complementarity constitutes a powerful computational tool. it is also very fruitful to view complementarity as a language-theoretic operation: "bad" words obtained through a generative process are replaced by their complementary ones. this idea seems particularly suitable for lindenmayer systems. d0l systems augmented with a specific complementarity transition, watson-crick d0l systems, have turned out to be a most interesting model and have already been extensively studied. a language is generated by a watson-crick d0l system as a sequence of words. consequently, the systems can be applied also to compute functions in a natural way. in the present paper, attention is focused on uni-transitional systems, where at most one complementarity transition takes place in the generated sequence. in spite of their seeming simplicity, uni-transitional systems represent a vast extension of ordinary d0l systems. this becomes apparent in their capacity of defining functions. quite remarkably, all basic decision problems for uni-transitional systems are algorithmically equivalent among themselves, as well as equivalent to a celebrated open problem. we investigate also a simpler case of systems with regular triggers, as well as pose some open problems.
composition sequences for functions over a finite domain. diverse problems ranging from many-valued logics to finite automata can be expressed as questions concerning compositions of functions over a finite domain. we develop a theory dealing with the depth and complete depth of such functions. interconnections with synchronizable finite automata are also discussed. many of the very basic problems turn out to be np-hard. also several open problems are pointed out.
connections between subwords and certain matrix mappings. parikh matrices recently introduced have turned out to be a powerful tool in the arithmetizing of the theory of words. in particular, many inequalities between (scattered) subword occurrences have been obtained as consequences of the properties of the matrices. this paper continues the investigation of parikh matrices and subword occurrences. in particular, we study certain inequalities, as well as information about subword occurrences sufficient to determine the whole word uniquely. some algebraic considerations, facts about forbidden subwords, as well as some open problems are also included.
independence of certain quantities indicating subword occurrences. when words are characterized in terms of numerical quantities, awkward considerations due to the noncommutativity of words are avoided. the numerical quantity investigated in this paper is |w|u, the number of occurrences of a word u as a (scattered) subword of a word w. parikh matrices recently introduced have these quantities as their entries. according to the main result in this paper, no entry in a parikh matrix, no matter how high the dimension, can be computed in terms of the other entries. consequences concerning various inference problems between numbers |w|u themselves, as well as of the word w from these numbers, are obtained.
watson-crick d0l systems: the power of one transition. we investigate the class of functions computable by uni-transitional watson-crick d0l systems: only one complementarity transition is possible during each derivation. the class is characterized in terms of a certain min-operation applied to z-rational functions. we also exhibit functions outside the class, and show that the basic decision problems are equivalent or harder than a celebrated open problem. for instance, the latter alternative applies to the growth-bound problem for functions in the class.
on the state complexity of reversals of regular languages. we compare the number of states between minimal deterministic finite automata accepting a regular language and its reversal (mirror image). in the worst case the state complexity of the reversal is 2n for an n-state language. we present several classes of languages where this maximal blow-up is actually achieved and study the conditions for it. in the case of finite languages the maximal blow-up is not possible but still a surprising variely of different growth types can be exhibited.
decidability of edt0l structural equivalence. we show that a tree pushdown automaton can verify, for an arbitrary nondeterministically constructed structure tree t, that t does not correspond to any valid derivation of a given edt0l grammar. in this way we reduce the structural equivalence problem for edt0l grammars to deciding emptiness of the tree language recognized by a tree pushdown automaton, i.e., to the emptiness problem for context-free tree languages. thus we establish that structural equivalence for edt0l grammars can be decided effectively. the result contrasts the known undecidability result for et0l structural equivalence.
reductions in binary search trees. we analyze two bottom-up reduction algorithms over binary trees that represent replaceable data within a certain system, assuming the binary search tree (bst) probabilistic model. these reductions are based on idempotent and nilpotent operators, respectively. in both cases, the average size of the reduced tree, as well as the cost to obtain it, is asymptotically linear with respect to the size of the original tree. additionally, the limiting distributions of the size of the trees obtained by means of these reductions satisfy a central limit law of gaussian type.
the rectangle complexity of functions on two-dimensional lattices. let x be a non-empty set. let f:z2x. all vectors which occur have integer coefficients, and for =(a1,a2), =(b1,b2) we write or < if ajbj or aj < bj for j=1,2, respectively. let >0. a -block is a set of the form b(){z2| < +}. a -pattern is the restriction of f to some -block. the total number of distinct -patterns is called the -complexity of f. a conjecture of the authors implies that f is periodic if there is a >0 such that the -complexity of f does not exceed b1b2. in this paper, we prove the statement for b=(n,2) where n is any positive integer.
m-balanced words: a generalization of balanced words. consider to construct an infinite sequence, or an infinite word, from a finite set of letters such as each letter is distributed with "good balance," that is, as evenly as possible, when the densities of letters are provided. such words have been applied to many scheduling and routing problems in various areas. concerning the balancedness of words, the notions of regularity and balanced words have been exploited. however, it is known that there does not always exist a balanced word for given densities of letters. in this paper, we introduce a new notion called m-balanced words, which gives a measure of "well balancedness" for any words with any densities of letters. we derive some properties of m-balanced words and give a set of algorithms generating well balanced words. we further give a few examples of applications to simple network scheduling problems.
on the equational definition of the least prefixed point. we propose a method to axiomatize by equations the least prefixed point of an order preserving function. we discuss its domain of application and show that the boolean modal µ-calculus has a complete equational axiomatization. the method relies on the existence of a "closed structure" and its relationship to the equational axiomatization of action logic is made explicit. the implication operation of a closed structure is not monotonic in one of its variables; we show that the existence of such a term that does not preserve the order is an essential condition for defining by equations the least prefixed point. we stress the interplay between closed structures and fixed point operators by showing that the theory of boolean modal µ-algebras is not a conservative extension of the theory of modal µ-algebras. the latter is shown to lack the finite model property.
on the design of a constructive algorithm to solve the multi-peg towers of hanoi problem. this paper describes a placement strategy to compute a set of ``good'' locations where visual sensing will be most effective. throughout this paper it is assumed that a {\em polygonal 2-d map} of a workspace is given as input. this polygonal map --- also known as a {\em floor plan} or {\em layout} --- is used to compute a set of locations where expensive sensing tasks (such as 3-d image acquisition) could be executed. a map-building robot, for example, can visit these locations in order to build a full 3-d model of the workspace.the sensor placement strategy relies on a randomized algorithm that solves a variant of the {\em art-gallery problem}~\cite{oro87,she92,urr97}: find the minimum set of guards inside a polygonal workspace from which the entire workspace boundary is visible. to better take into account the limitations of physical sensors, the algorithm computes a set of guards that satisfies incidence and range constraints. although the computed set of guards is not guaranteed to have minimum size, the algorithm does compute with high probability a set whose size is at most a factor $\bigo{ (n + h) \cdot \log(c \ (n + h) ) }$ from the optimal size $c$, where $n$ is the number of edges in the input polygonal map and $h$ the number of obstacles in its interior (holes).