Formalization of the pumping lemma for context-free languages
Marcus Vinícius Midena Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Bacelar Almeida
Abstract
Open-access reader
Marcus Vinícius Midena Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Bacelar Almeida
Abstract
Open-access reader
Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.
OpenAlex reports 1 citations for this work. Citation counts describe recorded attention and do not establish research quality.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.
Key concepts: Pumping lemma for regular languages, Lemma (botany), Context-free language, Context (archaeology), Computer science, Abstract family of languages, Formal language, Programming language