Abstract

We work toward a practical, unified language formalism for structurally recursive languages by expressing the mathematical theories underlying context-free grammars with lookahead (CFGLA) in the Rocq theorem prover and leveraging CFGLA semantics to analyze interactions between between recursion and negative lookahead. We give examples of grammars with left-recursive negation cycles for the parsing expression grammar (PEG) variant due to Medeiros et al. and for the translation from PEG to CFGLA due to Miyazaki and Minamide. To study the interaction between left recursion and negative lookahead in a PEG context, we introduce FPEG, a left-recursive extension of PEG with Fitting semantics.

Degree

College and Department

Computational, Mathematical, and Physical Sciences; Computer Science

Rights

https://lib.byu.edu/about/copyright/