A mechanisation of some context-free language theory in HOL4

Select |


Barthwal, Aditi; Norrish, Michael

Barthwal, Aditi; Norrish, Michael


Journal Article

Journal of Computer and System Sciences




We describe the mechanisation of some foundational results in the theory of context-free languages (CFLs), using the HOL4 system. We focus on pushdown automata (PDAs). We show that two standard acceptance criteria for PDAs (“accept-by-empty-stack? and “accept-by-final-state?) are equivalent in power. We are then able to show that the pushdown automata (PDAs) and context-free grammars (CFGs) accept the same languages by showing that each can emulate the other. With both of these models to hand, we can then show a number of basic, but important results. For example, we prove the basic closure properties of the context-free languages such as union and concatenation. Along the way, we also discuss the varying extent to which textbook proofs (we follow Hopcroft and Ullman) and our mechanisations diverge: sometimes elegant textbook proofs remain elegant in HOL; sometimes the required mechanisation effort blows up unconscionably.

context-free languages, language theory



Barthwal, Aditi; Norrish, Michael. A mechanisation of some context-free language theory in HOL4. Journal of Computer and System Sciences. 2014-03-01; 80(2):346--362. https://doi.org/10.1016/j.jcss.2013.05.003

Loading citation data...

Citation counts
(Requires subscription to view)