A Computational Interpretation of Context-Free Expressions

DOI10.1007/978-3-319-71237-6_19MaRDI QIDQ5056002zbMATH OpenOpenAlexFDO

Authors Martin Sulzmann, Peter J. Thiemann

Publication date 9 December 2022

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1708.07366

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Formal languages and automata (68Q45)

Abstract: We phrase parsing with context-free expressions as a type inhabitation problem where values are parse trees and types are context-free expressions. We first show how containment among context-free and regular expressions can be reduced to a reachability problem by using a canonical representation of states. The proofs-as-programs principle yields a computational interpretation of the reachability problem in terms of a coercion that transforms the parse tree for a context-free expression into a parse tree for a regular expression. It also yields a partial coercion from regular parse trees to context-free ones. The partial coercion from the trivial language of all words to a context-free expression corresponds to a predictive parser for the expression.

Recommendations

• Certified CYK parsing of context-free languages
• Grammar Analysis and Parsing by Abstract Interpretation
• Simple, functional, sound and complete parsing for all context-free grammars
• Regular expression containment, coinductive axiomatization and computational interpretation
• Parsing with derivatives

Cites work

• Algebra and Coalgebra in Computer Science
• Automata, Languages and Programming
• Coalgebraic characterizations of context-free languages
• Derivatives of Regular Expressions
• scientific article; zbMATH DE number 1183236 (Why is no real title available?)
• scientific article; zbMATH DE number 1407672 (Why is no real title available?)
• scientific article; zbMATH DE number 5254145 (Why is no real title available?)
• Parsing with derivatives
• Programming Languages and Systems
• Regular expression containment, coinductive axiomatization and computational interpretation
• Resource usage verification.

This page was built for publication: A Computational Interpretation of Context-Free Expressions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5056002)