Bar-Hillel Theorem Mechanization in Coq
Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verifica- tion, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theo- rem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.
This volume of Lecture Notes in Computer Science contains the papers presented at the 22nd International Conference on Developments in Language Theory (DLT 2018) organized by the Algorithmic “Oritatami” Self-Assembly Laboratory as part of the 100th Anniversary Commemorative Events of University of Electro-Communications (UEC) in Fuchu, Tokyo, Japan, during September 10–14, 2018.
The DLT conference series is one of the major international conference series in language theory and related areas. Since its establishment by G. Rozenberg and A. Salomaa in Turku (1993), it had been held every other year in Magdeburg (1995), Thessaloniki (1997), Aachen (1999), and Vienna (2001). In 2002, the DLT conference was held in Kyoto, for the first time outside Europe. Since then, the DLT conferences have been held in and outside Europe alternately: Szeged (2003), Auckland (2004), Palermo (2005), Santa Barbara (2006), Turku (2007), Kyoto (2008), Stuttgart (2009), London (2010), Milan (2011), Taipei (2012), Marne-la-Vallée (2013), Ekaterinburg (2014), Liverpool (2015), Montréal (2016), and Liège (2017). Thus, it returned to Japan after an absence of 10 years.
The series of International Conference on Developments in Language Theory (DLT) provides a forum for presenting current developments in formal languages and automata. Its scope is very general and includes, among others, the following topics and areas: combinatorial and algebraic properties of words and languages; grammars, acceptors, and transducers for strings, trees, graphs, arrays; algebraic theories for automata and languages; codes; efficient text algorithms; symbolic dynamics; decision problems; relationships to complexity theory and logic; picture description and anal- ysis; polyominoes and bidimensional patterns; cryptography; concurrency; cellular automata; bio-inspired computing; and quantum computing.
There were 84 qualified submissions, among which three were withdrawn, from 28 countries: Australia, Austria, Belgium, Canada, China, Czech Republic, Finland, France, Germany, Hungary, India, Israel, Italy, Japan, Latvia, Luxembourg, Norway, Paraguay, Poland, Portugal, Qatar, Republic of Korea, Russia, Slovakia, South Africa, Sweden, the UK, and the USA. Each of the 81 submissions was reviewed by at least three reviewers and thoroughly discussed by the Program Committee (PC). The committee decided to accept 39 papers for oral presentation. The volume also includes the abstracts or full papers of the six invited talks given by Tomohiro I., Bakhadyr Khoussainov, Alexander Okhotin, Dominique Perrin, Marinella Sciortino, and Andrew Winslow.
We warmly thank all the invited speakers and all authors of the submitted papers for making DLT 2018 successful. As the PC chair, I, Shinnosuke Seki, would like to express my cordial gratitude to the members of the PC and the external reviewers for reviewing the papers, participating in the selection process, and helping to maintain the high standard of the DLT conferences. We appreciate the help of the EasyChair con- ference system for facilitating our work of organizing DLT 2018 very much. We would
like to thank the editorial staff of Springer, and in particular Alfred Hofmann, Anna Kramer, Christine Reiss, and Raghuram Balasubramanian for their guidance and help during the process of publishing this volume. We also would like to thank Norio Takano, the mayor of Fuchu, the staff of Fuchu City Office, and all the citizens of the city for letting us use their Baltic hall as a venue for DLT 2018. Last but not the least, we are grateful to the Organizing Committee members: Szilard Zsolt Fazekas, Satoshi Kobayashi, Kohei Maruyama, Yusei Masuda, Reoto Morita, Shiho Sugimoto, Yuki Ubukata, and Fumie Watanabe.
DLT 2018 was financially supported by the National Institute of Information and Communications Technology (NICT), the Telecommunications Advancement Foun- dations (TAF), Japan Society for the Promotion of Science (JSPS) as Grant-in-Aid for Young Scientists (A) No. 16H05854 and Grant-in-Aid for Challenging Research (Exploratory) No. 18K19779 to Shinnosuke Seki, Kubota Information Technology, and the University of Electro-Communications. We would like to express our sincere gratitude for their philanthropic support.
We are all looking forward to DLT 2019 at the University of Warsaw in Poland.
September 2018 Mizuho Hoshi Shinnosuke Seki
The textbook contains the basic information of formal logical systems. It is Boolean functions, Post’s theorem on functional completeness, the k-valued logic, derivatives of Boolean functions, axiomatic calculi for propositions, for predicates, for sequentions, for resolutions. Programming language Prolog and axiomatic programming language OBJ3 are introduced. Problems of monadic logic, of finite automata and of the represented by them languages, of temporal logic are considered. Many examples are shown. It is put in a basis of the book long-term experience of teaching by authors the discipline «Discrete mathematics» at the business informatics faculty, at the computer science faculty of National research university Higher school of economics, and at the automatics and computer technique faculty of National research university Moscow power engineering institute. The book is intended for the students of a bachelor degree, trained at the computer science faculties in the directions 09.03.01 Informatics and computational technique, 09.03.02 Informational systems and technologies, 09.03.03 Applied informatics, 09.03.04 Software Engineering, and also for IT experts and developers of software products.
Concepts of the theory of algorithmic languages and methods of broadcasting and also processing of data and their organization are considered. Statement of material is followed by practical examples. The grant is intended for students of the higher educational institutions studying in the Applied Mathematics and Applied Mathematics and Informatics directions. Contains the subjects studied in disciplines "The theory of computing processes and structures", "The theory of algorithmic languages", "Mathematical fundamentals of informatics". It can be used as lecture material, on a practical training, when performing course and theses and also as means of self-education
We consider linear dynamical systems with a structure of a multigraph. The vertices are associated to linear spaces and the edges correspond to linear maps between those spaces. We analyse the asymptotic growth of trajectories (associated to paths along the multigraph), the stability and the stabilizability problems. This generalizes the classical linear switching systems and their recent extensions to Markovian systems, to systems generated by regular languages, etc. We show that an arbitrary system can be factorized into several irreducible systems on strongly connected multigraphs. For the latter systems, we prove the existence of invariant (Barabanov) multinorm and derive a method for its construction. The method works for a vast majority of systems and finds the joint spectral radius (Lyapunov exponent). Numerical examples are presented and applications to the study of fractals, attractors, and multistep methods for ODEs are discussed.
In this work are considered a theoretical basis, which can help approach the implementation of the tool for analyze the source code of the program in Perl.
in this work the development of a tool for the Perl programming language source code analysis for algorithm visualizationis considered . A theoretical basis is considered, which can help approach the implementation of the tool and analyze the source code of the program in Perl. An overview of the existing visualization tools for source code programs is made, on the basis of which we formulated the requirements for the developed software. The tools for the analysis of program code are considered. The application that reads from a file the program text and builds a diagram that can be edited and then saved to a fileis designed, implemented and tested
The Hilbert series is one of the most important algebraic invariants of innite-dimensional graded associative algebra. The noncommutative Groebner basis machine reduces the prob- lem of nding Hilbert series to the case of monomial algebra. We apply both noncommutative and commutative Groebner bases theory as well as the theory of formal languages to provide a new method for symbolic computation of Hilbert series of graded associative algebras. Whereas in general the problem of computation oh such a Hilbert series is known to be algorithmically unsolvable, we have describe a general class of algebras (called homologically unambiguous) with unambiguous context-free set of relations for which our method give eective algorithms. Unlike previously known methods, our algorithm is applicable to algebras with irrational Hilbert series and produces an alge- braic equation which denes the series. The examples include innitely presented monomials algebras as well as nitely presented algebras with irrational Hilbert series such that the associated monomial algebras are homologically unambiguous.
We present a new structural lemma for deterministic con- text free languages. From the first sight, it looks like a pumping lemma, because it is also based on iteration properties, but it has significant distinctions that makes it much easier to apply. The structural lemma is a combinatorial analogue of KC-DCF-Lemma (based on Kolmogorov complexity), presented by Li and Vit ́anyi in 1995 and corrected by Glier in 2003. The structural lemma allows not only to prove that a language is not a DCFL, but discloses the structure of DCFLs Myhill-Nerode classes.
We consider regular realizability problems, which consist in verifying whether the intersection of a regular language which is the problem input and a fixed language (filter) which is a parameter of the problem is nonempty. We study the algorithmic complexity of regular realizability problems for context-free filters. This characteristic is consistent with the rational dominance relation of CF languages. However, as we prove, it is more rough. We also give examples of both P-complete and NL-complete regular realizability problems for CF filters. Furthermore, we give an example of a subclass of CF languages for filters of which the regular realizability problems can have an intermediate complexity. These are languages with polynomially bounded rational indices.
We consider certain spaces of functions on the circle, which naturally appear in harmonic analysis, and superposition operators on these spaces. We study the following question: which functions have the property that each their superposition with a homeomorphism of the circle belongs to a given space? We also study the multidimensional case.
We consider the spaces of functions on the m-dimensional torus, whose Fourier transform is p -summable. We obtain estimates for the norms of the exponential functions deformed by a C1 -smooth phase. The results generalize to the multidimensional case the one-dimensional results obtained by the author earlier in “Quantitative estimates in the Beurling—Helson theorem”, Sbornik: Mathematics, 201:12 (2010), 1811 – 1836.
We consider the spaces of function on the circle whose Fourier transform is p-summable. We obtain estimates for the norms of exponential functions deformed by a C1 -smooth phase.