Strong Normalization for Well-Typed Parsing Expression Grammars
Resumo
Parsing Expression Grammars (PEGs) are a deterministic formalism for describing syntax that has gained wide adoption in practice. A natural question is whether a PEG parser always terminates: could a grammar send a parser into an infinite loop? We show that this is not the case for well-typed PEGs, using a logical-relations argument inspired by the well-known strong normalization proof for the simply typed 𝜆-calculus. The proof is mechanized in the Agda proof assistant.
Palavras-chave:
Parsing Expression Grammars, Strong Normalization, Logical Relations, Agda, Proof Mechanization
Referências
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. 2018. POPLMark Reloaded: Mechanizing Proofs by Logical Relations. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). Association for Computing Machinery, 1–1. DOI: 10.1145/3167102
Agda Team. 2024. Agda Standard Library. Version 2.2, [link].
Elton M. Cardoso, Regina De Paula, Daniel Pereira, Leonardo Reis, and Rodrigo Geraldo Ribeiro. 2023. Type-based Termination Analysis for Parsing Expression Grammars. In Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing (SAC). Association for Computing Machinery, Tallinn, Estonia, 1–8. DOI: 10.1145/3555776.3577620
Guilherme Daher, Elton Cardoso, Leonardo Reis, and Rodrigo Ribeiro. 2025. Pest control: A formal model of the Pest parser generator. In Proceedings of the XXIX Brazilian Symposium on Programming Languages (SBLP). SBC, Recife, Brazil. DOI: 10.5753/sblp.2025.10399
Nicolaas Govert de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75, 5 (1972), 381–392.
Sérgio Queiroz de Medeiros and Carlos Olarte. 2020. A Semantic Framework for PEGs. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (SLE). Association for Computing Machinery, 230–245. DOI: 10.1145/3426425.3426944
Bryan Ford. 2004. Parsing Expression Grammars: A Recognition-Based Syntactic Foundation. In Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). 111–122. DOI: 10.1145/964001.964011
Jean-Yves Girard, Yves Lafont, and Paul Taylor. 1989. Proofs and Types. Cambridge University Press.
Adam Koprowski and Henri Binsztok. 2010. TRX: A Formally Verified Parser Interpreter. In Proceedings of the 19th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 6012). 345–365. DOI: 10.1007/978-3-642-11957-6_19
Neelakantan R. Krishnaswami and Jeremy Yallop. 2019. A Typed, Algebraic Approach to Parsing. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Association for Computing Machinery, Phoenix, AZ, USA, 379–393. DOI: 10.1145/3314221.3314625
Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph. D. Dissertation. Chalmers University of Technology.
Rodrigo Ribeiro, Leonardo V. S. Reis, Samuel Feitosa, and Elton M. Cardoso. 2019. Towards Typed Semantics for Parsing Expression Grammars. In Proceedings of the XXIII Brazilian Symposium on Programming Languages (Salvador, Brazil) (SBLP ’19). Association for Computing Machinery, New York, NY, USA, 70–77. DOI: 10.1145/3355378.3355388
Natarajan Shankar and Zephyr Lucas. 2024. Robust Verification of PEG Parser Interpreters. In 2024 IEEE Security and Privacy Workshops (SPW). 180–188. DOI: 10.1109/SPW63631.2024.00022
William W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I. The Journal of Symbolic Logic 32, 2 (1967), 198–212. DOI: 10.2307/2271658
Philip Wadler, Wen Kokke, and Jeremy G. Siek. 2022. Programming Language Foundations in Agda. [link].
Agda Team. 2024. Agda Standard Library. Version 2.2, [link].
Elton M. Cardoso, Regina De Paula, Daniel Pereira, Leonardo Reis, and Rodrigo Geraldo Ribeiro. 2023. Type-based Termination Analysis for Parsing Expression Grammars. In Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing (SAC). Association for Computing Machinery, Tallinn, Estonia, 1–8. DOI: 10.1145/3555776.3577620
Guilherme Daher, Elton Cardoso, Leonardo Reis, and Rodrigo Ribeiro. 2025. Pest control: A formal model of the Pest parser generator. In Proceedings of the XXIX Brazilian Symposium on Programming Languages (SBLP). SBC, Recife, Brazil. DOI: 10.5753/sblp.2025.10399
Nicolaas Govert de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75, 5 (1972), 381–392.
Sérgio Queiroz de Medeiros and Carlos Olarte. 2020. A Semantic Framework for PEGs. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (SLE). Association for Computing Machinery, 230–245. DOI: 10.1145/3426425.3426944
Bryan Ford. 2004. Parsing Expression Grammars: A Recognition-Based Syntactic Foundation. In Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). 111–122. DOI: 10.1145/964001.964011
Jean-Yves Girard, Yves Lafont, and Paul Taylor. 1989. Proofs and Types. Cambridge University Press.
Adam Koprowski and Henri Binsztok. 2010. TRX: A Formally Verified Parser Interpreter. In Proceedings of the 19th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 6012). 345–365. DOI: 10.1007/978-3-642-11957-6_19
Neelakantan R. Krishnaswami and Jeremy Yallop. 2019. A Typed, Algebraic Approach to Parsing. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Association for Computing Machinery, Phoenix, AZ, USA, 379–393. DOI: 10.1145/3314221.3314625
Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. Ph. D. Dissertation. Chalmers University of Technology.
Rodrigo Ribeiro, Leonardo V. S. Reis, Samuel Feitosa, and Elton M. Cardoso. 2019. Towards Typed Semantics for Parsing Expression Grammars. In Proceedings of the XXIII Brazilian Symposium on Programming Languages (Salvador, Brazil) (SBLP ’19). Association for Computing Machinery, New York, NY, USA, 70–77. DOI: 10.1145/3355378.3355388
Natarajan Shankar and Zephyr Lucas. 2024. Robust Verification of PEG Parser Interpreters. In 2024 IEEE Security and Privacy Workshops (SPW). 180–188. DOI: 10.1109/SPW63631.2024.00022
William W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I. The Journal of Symbolic Logic 32, 2 (1967), 198–212. DOI: 10.2307/2271658
Philip Wadler, Wen Kokke, and Jeremy G. Siek. 2022. Programming Language Foundations in Agda. [link].
Publicado
08/09/2026
Como Citar
NASCIMENTO, Guilherme Augusto Anício Drummond do; CARDOSO, Elton Máximo; FEITOSA, Samuel da Silva; RIBEIRO, Rodrigo.
Strong Normalization for Well-Typed Parsing Expression Grammars. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 30. , 2026, São Paulo/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 46-53.
DOI: https://doi.org/10.5753/sblp.2026.27720.
