Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages

Autor: Marcus Vinícius Midena Ramos, Ruy J. G. B. de Queiroz, José B. Almeida, Nelma Moreira
Přispěvatelé: Universidade do Minho
Rok vydání: 2019
Předmět:
formalization
General Computer Science
Property (programming)
Computer science
0102 computer and information sciences
02 engineering and technology
computer.software_genre
01 natural sciences
Formal proof
Theoretical Computer Science
Formal language
0202 electrical engineering
electronic engineering
information engineering
Coq
non-context-free languages
Lemma (mathematics)
intersection
Science & Technology
Programming language
Intersection (set theory)
Proof assistant
Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing)
020207 software engineering
Engenharia Eletrotécnica
Eletrónica e Informática [Engenharia e Tecnologia]
closure
pumping lemma
Pumping lemma for regular languages
010201 computation theory & mathematics
Computer Science::Programming Languages
Pumping lemma for context-free languages
computer
Engenharia e Tecnologia::Engenharia Eletrotécnica
Eletrónica e Informática
Zdroj: LSFA
Repositório Científico de Acesso Aberto de Portugal
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
ISSN: 1571-0661
Popis: Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma for Context-Free Languages states a property that is valid for all context-free languages, which makes it a tool for showing the existence of non-context-free languages. This paper presents a formalization, extending the previously formalized Lemma, of the fact that several well-known languages are not context-free. Moreover, we build on those results to construct a formal proof of the well-known property that context-free languages are not closed under intersection. All the formalization has been mechanized in the Coq proof assistant.
(undefined)
Databáze: OpenAIRE
Externí odkaz: