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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/17642 |
| Date | 18 January 2016 |
| Creators | RAMOS, Marcus Vinícius Midena |
| Contributors | http://lattes.cnpq.br/1825502153580661, QUEIROZ, Ruy José Guerra Barretto de |
| Publisher | Universidade Federal de Pernambuco, Programa de Pos Graduacao em Ciencia da Computacao, UFPE, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.0028 seconds