Abstract In this thesis, we will study very small full trios and full AFLs inside the family of context-free languages. Especially, we are interested in the existence of the smallest nontrivial full trios and full AFLs. This is an old research subject, and it has not been studied much since the 1970s. A conjecture by Autebert et al. states that there does not exist a nontrivial minimal full trio inside the family of context-free languages (2) (see also (1)). First, we will show that there does not exist a nontrivial minimal full trio or a nontrivial minimal full AFL with respect to the bounded context-free languages. This result solves another old conjecture stated by Autebert et al. (1). Then we will try to generalize our result to also concern unbounded context-free languages. We will make some progress, but the problem still remains open.

We present a term rewriting procedure based on congruence closure that can be used with arbitrary equational theories. This procedure is motivated by the pragmatic need to prove equations in equational theories where confluence can not be achieved. The procedure uses context free grammars to represent equivalence classes of terms. The procedure rewrites grammars rather than terms and uses congruence closure to maintain certain congruence properties of the grammar. Grammars provide concise representations of large term sets. Infinite term sets can be represented with finite grammars and exponentially large term sets can be represented with linear sized grammars.

No description available.

The composition and reuse of existing textual languages is a frequently re-occurring problem. One possibility of composing textual languages lies on the level of parser specifications which are mainly based on context-free grammars and regular expressions. Unfortunately most mainstream parser generators provide proprietary specification languages and usually do not provide strong abstractions for reuse. New forms of parser generators do support modular language development, but they can often not be easily integrated with existing legacy applications. To support modular language development based on mainstream parser generators, in this paper we apply the Invasive Software Composition (ISC) paradigm to parser specification languages by using our Reuseware framework. Our approach is grounded on a platform independent metamodel and thus does not rely on a specific parser generator.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-08-08T13:11:15Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) / Made available in DSpace on 2016-08-08T13:11:15Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) Previous issue date: 2016-03-28 / CAPEs / Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different such tools are being increasingly used in order to accelerate and simplify proof checking, and the Coq proof assistant is one of the most known and used. Language and automata theory is a well-established area of mathematics, relevant to computer science foundations and information technology. In particular, context-free language theory is of fundamental importance in the analysis, design and implementation of computer programming languages. This work describes a formalization effort, using the Coq proof assistant, of fundamental results of the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. To achieve this, several steps had to be fulfilled, including (i) understanding of the characteristics, importance and benefits of mathematical formalization, specially in computer science, (ii) familiarization with the underlying mathematical theories used in proof assistants, (iii) familiarization with the Coq proof assistant, (iv) review of the strategies used in the informal proofs of the main results of the context-free language theory and finally (iv) selection and adequation of the representation and proof strategies adopted in order the achieve the desired objectives. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the remarkable result that is the formalization of the Pumping Lemma for context-free languages. The perspectives for the further development of this work are diverse and can be grouped in three different areas: inclusion of new devices and results, code extraction and general enhancements of its libraries. / Assistentes de prova são ferramentas de software que são usadas na mecanização da construção e da validação de provas na matemática e na ciência da computação, e também no desenvolvimento de programas certificados. Diferentes ferramentas estão sendo usadas de forma cada vez mais frequente para acelerar e simplificar a verificação de provas, e o assistente de provas Coq é uma das mais conhecidas e utilizadas. A teoria de linguagens e de autômatos é uma área bem estabelecida da matemática, com relevância para os fundamentos da ciência da computação e a tecnologia da informação. Em particular, a teoria das linguagens livres de contexto é de fundamental importância na análise, no projeto e na implementação de linguagens de programação de computadores. Este trabalho descreve um esforço de formalização, usando o assistente de provas Coq, de resultados fundamentais da teoria clássica das gramáticas e linguagens livres de contexto. Estes incluem propriedades de fechamento (união, concatenação e estrela de Kleene), simplificação gramatical (eliminação de símbolos inúteis, de símbolos inacessíveis, de regras vazias e de regras unitárias), a existência da Forma Normal de Chomsky para gramáticas livres de contexto e o Lema do Bombeamento para linguagens livres de contexto. Para alcançar estes resultados, diversas etapas precisaram ser cumpridas, incluindo (i) o entendimento das características, da importância e dos benefícios da formalização matemática, especialmente na ciência da computação, (ii) a familiarização com as teorias matemáticas fundamentais utilizadas pelos assistentes de provas, (iii) a familiarização com o assistente de provas Coq, (iv) a revisão das estratégias usadas nas provas informais dos principais resultados da teoria das linguagens livres de contexto e, finalmente, (v) a seleção e adequação das estratégias de representação e prova adotadas para permitir o alcance dos resultados pretendidos. O resultado é um importante conjunto de bibliotecas cobrindo os principais resultados da teoria das linguagens livres de contexto, com mais de 500 lemas e teoremas totalmente provados e verificados. Esta é provavelmente a formalização mais abrangente da teoria clássica das linguagens livres de contexto jamais feita no assistente de provas Coq, e inclui o importante resultado que é a formalização do Lema do Bombeamento para linguagens livres de contexto. As perspectivas para novos desenvolvimentos a partir deste trabalho são diversas e podem ser agrupadas em três áreas diferentes: inclusão de novos dispositivos e resultados, extração de código e aprimoramentos gerais das suas bibliotecas.

The composition and reuse of existing textual languages is a frequently re-occurring problem. One possibility of composing textual languages lies on the level of parser specifications which are mainly based on context-free grammars and regular expressions. Unfortunately most mainstream parser generators provide proprietary specification languages and usually do not provide strong abstractions for reuse. New forms of parser generators do support modular language development, but they can often not be easily integrated with existing legacy applications. To support modular language development based on mainstream parser generators, in this paper we apply the Invasive Software Composition (ISC) paradigm to parser specification languages by using our Reuseware framework. Our approach is grounded on a platform independent metamodel and thus does not rely on a specific parser generator.

Le problème de séparation pour une classe de langages S est le suivant : étant donnés deux langages L1 et L2, existe-t-il un langage appartenant à S qui contient L1, en étant disjoint de L2 ? Si les langages à séparer sont des langages réguliers, le problème de séparation pour la classe S est plus général que le problème de l'appartenance à cette classe, et nous fournit des informations plus détaillées sur la classe. Ce problème de séparation apparaît dans un contexte algébrique sous la forme des parties ponctuelles, et dans un contexte profini sous la forme d'un problème de séparation topologique. Pour quelques classes de langages spécifiques, ce problème a été étudié en utilisant des méthodes profondes de la théorie des semigroupes profinis.Dans cette thèse, on s'intéresse, dans un premier temps, à la décidabilité de ce problème pour plusieurs sous-classes des langages réguliers. Dans un second temps, on s'intéresse à obtenir un langage séparateur, s'il existe, ainsi qu'à la complexité de ces problèmes.Nous établissons une approche générique pour prouver que le problème de séparation est décidable pour une classe de langages donnée. En utilisant cette approche, nous obtenons la décidabilité du problème de séparation pour les langages testables par morceaux, les langages non-ambigus, les langages localement testables, et les langages localement testables à seuil. Ces classes correspondent à des fragments de la logique du premier ordre, et sont parmi lesclasses de langages réguliers les plus étudiées. De plus, cette approche donne une description d'un langage séparateur, pourvu qu'il existe. / The separation problem, for a class S of languages, is the following: given two input languages, does there exist a language in S that contains the first language and that is disjoint from the second langage ?For regular input languages, the separation problem for a class S subsumes the classical membership problem for this class, and provides more detailed information about the class. This separation problem first emerged in an algebraic context in the form of pointlike sets, and in a profinite context as a topological separation problem. These problems have been studied for specific classes of languages, using involved techniques from the theory of profinite semigroups.In this thesis, we are not only interested in showing the decidability of the separation problem for several subclasses of the regular languages, but also in constructing a separating language, if it exists, and in the complexity of these problems.We provide a generic approach, based on combinatorial arguments, to proving the decidability of this problem for a given class. Using this approach, we prove that the separation problem is decidable for the classes of piecewise testable languages, unambiguous languages, and locally (threshold) testable languages. These classes are defined by different fragments of first-order logic, and are among the most studied classes of regular languages. Furthermore, our approach yields a description of a separating language, in case it exists.