Search

We introduce a single-set axiomatisation of cubical ω -categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical ω -categories, and their variants with connections and inverses, and the corresponding cubical ω -categories. We also report on the formalisation of cubical ω -categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation. [ABSTRACT FROM AUTHOR]

Reaction systems are a model of computing aiming to formalize biochemistry by capturing the qualitative relations between the species, and explicitly discarding any accounts of multiplicity. From the point of view of the formal language theory, this situates them in the realm of set rewriting. In this work, we propose a series of extensions of reaction systems to use strings. These extensions form a spectrum in the sense that all of them honor the hallmark features of the original model: the threshold principle and the non-permanency principle. We thoroughly discuss the details of the structure and the behavior of these variants, and commence studying their expressive power by comparing them to some classic models of computing. [ABSTRACT FROM AUTHOR]

In this paper, we develop computing machinery within the framework of the String Multiset Rewriting calculus (SMSR), as defined by Barbuti et al. [4], to solve the SAT problem in linear time regarding the number of variables of a given conjunctive normal form. This shows that SMSR can be considered a computational model capable of significantly reducing the time requirement of classical decision problems. [ABSTRACT FROM AUTHOR]

We apply Context-free Grammars (CFG) to measure the structural information content of a symbolic music string. CFGs are appropriate to this domain because they highlight hierarchical patterns, and their dictionary of rules can be used for compression. We adapt this approach to estimate the conditional Kolmogorov complexity of a string with a concise CFG of another string. Thus, a related string may be compressed with the production rules for the first string. We then define an information distance between two symbolic music strings, and show that this measure can separate genres, composers and musical styles. Next, we adapt our approach to a model-selection problem, expressing the model as a CFG with restricted size, generated from a set of representative strings. We show that a well-generated CFG for a composer identifies characteristic patterns that can significantly compress other pieces from the same composer, while not being useful on pieces from different composers. We identify further opportunities of this approach, including using CFGs for generating new music in the style of a composer. [ABSTRACT FROM AUTHOR]

This paper shows how to construct coherent presentations (presentations by generators, relations and relations among relations) of monoids admitting a right-noetherian Garside family. Thereby, it resolves the question of finding a unifying generalisation of the following two distinct extensions of construction of coherent presentations for Artin-Tits monoids of spherical type: to general Artin-Tits monoids, and to Garside monoids. The result is applied to some monoids which are neither Artin-Tits nor Garside. [ABSTRACT FROM AUTHOR]

The model of Spiking Neural P systems (SNP systems) is a widespread computational model in the area of membrane computing. It has numerous applications, especially related to machine learning. Most of these applications require a custom variant of SNP systems, differing by the rule form and by semantics. The model of network of cells and the formal framework for SNP systems were developed to help the analysis of such custom models, to compare and relate them to each other and to other models of computing. The model specifies the data structure, the rules and the update procedure, while the formal framework concentrates on how the input, output and the choice of the update strategy are handled. Together, these concepts specify a concrete instance of a network of cells that strongly bisimulates the desired model, thus making easier the process of the creation of new models and the extension of existing ones. Since the formal framework is rather generic, it might be slightly complex to use it for concrete cases. This paper provides a tutorial that explains the model of networks of cells and the basic concepts used in the formal framework for SNP systems. It gives a series of examples for the analysis of existing models, their bisimulation and their extension by different features. [ABSTRACT FROM AUTHOR]

Block tridiagonal matrices arise in applied mathematics, physics, and signal processing. Many applications require knowledge of eigenvalues and eigenvectors of block tridiagonal matrices. In this paper, we derive specific formulas for characteristic polynomials, and eigenvalues for a class of block tridiagonal matrices. We apply the results to determine the charactristic polynomial of some block Toeplitz symmetric tridiagonal matrices and give the explicit eigenvalues. Particularly, when the blocks are diagonal matrices, the eigenvalues are calculated explicitly. [ABSTRACT FROM AUTHOR]

The asymmetric encryption methods are based on difficult problems in mathematics. Let G be a group, A group word in G on a set Γ of generators is a string where. The word problem in a group G with respect to a subset Γ is the question of telling whether two words in Γ are equal. It is known that in general the word problem is undecidable, meaning that there is no algorithm to solve it. In this paper, we introduce a cryptosystem based on the word problem in a group G. [ABSTRACT FROM AUTHOR]

We explain the foundations of a new class of formal languages for the construction of large Feynman diagrams which contribute to solutions of all combinatorial Dyson–Schwinger equations in a given strongly coupled gauge field theory. Then we build a new Hopf algebraic structure on non-perturbative production rules which leads us to formulate the halting problem for the corresponding replacing–gluing graph grammars in our formal graph languages on the basis of Manin's renormalization Hopf algebra. In addition, we apply topology of graphons to associate a complexity parameter to this new class of graph grammars. At the final step, we address some applications of our new formal language platform to Quantum Field Theory. The first application concerns the constructive role of non-perturbative graph languages in dealing with quantum gauge symmetries in the context of the Hopf ideals generated by Slavnov–Taylor or Ward–Takahashi identities. The second application concerns the importance of the complexities of non-perturbative replacing–gluing graph grammars in formulating a new generalization of the circuit complexity on the space of Dyson–Schwinger equations. We provide a geometric interpretation of non-perturbative circuit complexities. The third application concerns the impact of non-perturbative replacing–gluing graph grammars in providing some new tools for the computation of the Kolmogorov complexity of Dyson–Schwinger equations. [ABSTRACT FROM AUTHOR]

The well-known pumping lemma for regular languages states that, for any regular language L, there is a constant p (depending on L) such that the following holds: If w ∈ L and | w | ≥ p , then there are words x ∈ V ∗ , y ∈ V + , and z ∈ V ∗ such that w = x y z and x y t z ∈ L for t ≥ 0 . The minimal pumping constant mpc (L) of L is the minimal number p for which the conditions of the pumping lemma are satisfied. We investigate the behaviour of mpc with respect to operations, i. e., for an n-ary regularity preserving operation ∘ , we study the set g ∘ mpc (k 1 , k 2 , ... , k n) of all numbers k such that there are regular languages L 1 , L 2 , ... , L n with mpc (L i) = k i for 1 ≤ i ≤ n and mpc (∘ (L 1 , L 2 , ... , L n) = k . With respect to Kleene closure, complement, reversal, prefix and suffix-closure, circular shift, union, intersection, set-subtraction, symmetric difference,and concatenation, we determine g ∘ mpc (k 1 , k 2 , ... , k n) completely. Furthermore, we give some results with respect to the minimal pumping length where, in addition, | x y | ≤ p has to hold. [ABSTRACT FROM AUTHOR]

Let K and L be two languages over Σ and Γ (with Γ ⊂ Σ ), respectively. Then, the L-reduction of K, denoted by K % L , is defined by { u 0 u 1 ⋯ u n ∈ (Σ - Γ) ∗ ∣ u 0 v 1 u 1 ⋯ v n u n ∈ K , v i ∈ L (1 ≤ i ≤ n) } . This is extended to language classes as follows: K % L = { K % L ∣ K ∈ K , L ∈ L } . In this paper, we investigate the computing powers of K % L in which K ranges among various classes of INS j i and min- LIN , while L is taken as DYCK and F , where INS j i : the class of insertion languages of weight (j, i), min- LIN : the class of minimal linear languages, DYCK : the class of Dyck languages, and F : the class of finite languages. The obtained results include: INS 1 1 % DYCK = RE INS i 0 % F = INS j 1 % F = CF (for i ≥ 3 and j ≥ 1 ) INS 2 0 % DYCK = INS 2 0 min- LIN % F 1 = LIN where RE , CF , LIN , F 1 are classes of recursively enumerable, of context-free, of linear languages, and of singleton languages over unary alphabet, respectively. Further, we provide a very simple alternative proof for the known result min- LIN % DYCK 2 = RE . We also show that with a certain condition, for the class of context-sensitive languages CS , there exists no K such that K % DYCK = CS , which is in marked contrast to the characterization results mentioned above for other classes in Chomsky hierarchy. It should be remarked from the viewpoint of molecular computing theory that the notion of L-reduction is naturally motivated by a molecular biological functioning well-known as RNA splicing occurring in most eukaryotic genes. [ABSTRACT FROM AUTHOR]

We propose a new type of computing devices based on grammatical formulation augmented by multiset storages, called chemical reaction regular grammars (CRRGs), and investigate some formal language theoretic characterizations of CRRGs including their generative capabilities. Shortly, a CRRG is a regular grammar with multisets, while its computational capability exhibits very intriguing aspects depending on the manners of rule applications. Firstly, we show that the class of languages (denoted by CRRL λ ) generated by CRRGs coincides with the class of languages accepted by chemical reaction automata (Okubo and Yokomori in Nat Comput 15(2): 215–224, 2016), whose implication is that the computing power of CRRGs is also equivalent to that of several known devices introduced from different motivations such as Petri nets (Peterson in ACM Comput Surv 9(3):223–252, 1977) and partially blind 1-way multicounter machines (Greibach in Theor Comput Sci 7:311–324, 1979). Second, a new manner of rewriting strategy is integrated into CRRGs and we show that CRRGs working in maximal-sequential manner can generate any recursively enumerable language, which is an unexpected result with a surprise. In contrast, it is also shown that regulated controls due to regular sets and matrix constraints do not enhance the computing power of CRRGs. Third, for each k ≥ 1 a subclass of languages k- CRRL λ is considered, where k is the number of different symbols for multisets of CRRGs. We show that the class of languages is a full principal semi-AFL, which is obtained from a characterization result that L is in k- CRRL λ iff L = h (g - 1 (B k) ∩ R) for some homomorphisms g, h, a regular set R, where B k is a paritally balanced language over k-symbol alphabet. [ABSTRACT FROM AUTHOR]

Generalization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t ′ is a term t ′ ′ of which t and t ′ are substitution instances. The dual of most general equational unifiers is that of least general equational generalizers, i.e., most specific anti-instances modulo equations. In a previous work, we extended the classical untyped generalization algorithm to: (1) an order-sorted typed setting with sorts, subsorts, and subtype polymorphism; (2) work modulo equational theories, where function symbols can obey any combination of associativity, commutativity, and identity axioms (including the empty set of such axioms); and (3) the combination of both, which results in a modular, order-sorted equational generalization algorithm. However, Cerna and Kutsia showed that our algorithm is generally incomplete for the case of identity axioms and a counterexample was given. Furthermore, they proved that, in theories with two identity elements or more, generalization with identity axioms is generally nullary, yet it is finitary for both the linear and one-unital fragments, i.e., either solutions with repeated variables are disregarded or the considered theories are restricted to having just one function symbol with an identity or unit element. In this work, we show how we can easily extend our original inference system to cope with the non-linear fragment and identify a more general class than one–unit theories where generalization with identity axioms is finitary. [ABSTRACT FROM AUTHOR]

In this paper we consider the model of single insertion-deletion systems that at each step insert or delete a single symbol in a context-free manner (i.e. at any position in the word). The corresponding operation is performed if the word contains a set of permitting (that have to be present in the word) and/or forbidding (that must not be present in the word) strings of some size. The main result of this paper states that if forbidding strings of size 2 and permitting strings of size 1 are used then computational completeness can be achieved; moreover, checking for a single permitting symbol is sufficient. We also show that in the case of systems having rules with forbidding conditions only, all regular languages can be obtained. Finally, we show the computational non-completeness in the case of systems using rules with forbidding strings of size 1 (single symbols) and permitting strings of any finite size. [ABSTRACT FROM AUTHOR]

The paper introduces a new type of rules into Natural Deduction, elimination rules by composition. Elimination rules by composition replace usual elimination rules in the style of disjunction elimination and give a more direct treatment of additive disjunction, multiplicative conjunction, existence quantifier and possibility modality. Elimination rules by composition have an enormous impact on proof-structures of deductions: they do not produce segments, deduction trees remain binary branching, there is no vacuous discharge, there is only few need of permutations. This new type of rules fits especially to substructural issues, so it is shown for Lambek Calculus, i.e. intuitionistic non-commutative linear logic and to its extensions by structural rules like permutation, weakening and contraction. Natural deduction formulated with elimination rules by composition from a complexity perspective is superior to other calculi. [ABSTRACT FROM AUTHOR]

For a regular language L, let Var (L) be the minimal number of nonterminals necessary to generate L by right linear grammars. Moreover, for natural numbers k 1 , k 2 , ... , k n and an n-ary regularity preserving operation f, let g f Var (k 1 , k 2 , ... , k n) be the set of all numbers k such that there are regular languages L 1 , L 2 , ... , L n such that Var (L i) = k i for 1 ≤ i ≤ n and Var (f (L 1 , L 2 , ... , L n)) = k . We completely determine the sets g f Var for the operations reversal, Kleene-closures + and ∗ , and union; and we give partial results for product and intersection. [ABSTRACT FROM AUTHOR]

The integration of autonomous robots in real applications is a challenge. It needs that the behaviour of these robots is proved to be safe. In this paper, we focus on the real-time software embedded on the robot, and that supports the execution of safe and autonomous behaviours. We propose a methodology that goes from the design of component-based software architectures using a Domain Specific Language, to the analysis of the real-time constraints that arise when considering the safety of software applications. This methodology is supported by a code generation toolchain that ensures that the code eventually executed on the robot is consistent with the analysis performed. This methodology is applied on a ground robot exploring an area. Categories (2), (3) [ABSTRACT FROM AUTHOR]

This paper presents a counterexample for the open conjecture whether innermost joinability of all critical pairs ensures confluence of innermost terminating term rewriting systems. We then show that innermost joinability of all normalized instances of the critical pairs is a necessary and sufficient condition. Using this condition, we give a decidable sufficient condition for confluence of innermost terminating systems. Finally, we enrich the condition by introducing the notion of left-stable rules. As a corollary, confluence of innermost terminating left-weakly-shallow TRSs is shown to be decidable. [ABSTRACT FROM AUTHOR]

We relate the operad FMan controlling the algebraic structure on the tangent sheaf of an F-manifold (weak Frobenius manifold) defined by Hertling and Manin to the operad PreLie of pre-Lie algebras: for the filtration of PreLie by powers of the ideal generated by the Lie bracket, the associated graded object is FMan. [ABSTRACT FROM AUTHOR]

We investigate the padded version of reduction, an extension of multifraction reduction as defined in arXiv:1606.08991 , and connect it both with ordinary reduction and with the so-called Property H. As an application, we show that all Artin–Tits groups of sufficiently large type satisfy some weakened version Conjecture A padded of Conjecture A , thus showing that the reduction approach is relevant for these groups. [ABSTRACT FROM AUTHOR]

We construct finite coherent presentations of plactic monoids of type A. Such coherent presentations express a system of generators and relations for the monoid extended in a coherent way to give a family of generators of the relations amongst the relations. Such extended presentations are used for representations of monoids, in particular, it is a way to describe actions of monoids on categories. Moreover, a coherent presentation provides the first step in the computation of a categorical cofibrant replacement of a monoid. Our construction is based on a rewriting method introduced by Squier that computes a coherent presentation from a convergent one. We compute a finite coherent presentation of a plactic monoid from its column presentation and we reduce it to a Tietze equivalent one having Knuth's generators. [ABSTRACT FROM AUTHOR]

Autostackability for finitely presented groups is a topological property of the Cayley graph combined with formal language theoretic restrictions, that implies solvability of the word problem. The class of autostackable groups is known to include all asynchronously automatic groups with respect to a prefix-closed normal form set, and all groups admitting finite complete rewriting systems. Although groups in the latter two classes all satisfy the homological finiteness condition F P ∞ , we show that the class of autostackable groups includes a group that is not of type F P 3 . We also show that the class of autostackable groups is closed under graph products and extensions. [ABSTRACT FROM AUTHOR]

Graph grammars extend the theory of formal languages in order to model distributed parallelism in theoretical computer science. We show here that to certain classes of context-free and context-sensitive graph grammars one can associate a Lie algebra, whose structure is reminiscent of the insertion Lie algebras of quantum field theory. We also show that the Feynman graphs of quantum field theories are graph languages generated by a theory dependent graph grammar. [ABSTRACT FROM AUTHOR]