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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
References
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley Longman Publishing Co. Inc., Boston (1986)
Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundam. Inf. 33(4), 309–338 (1998)
Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)
Frisch, A., Cardelli, L.: Greedy regular expression matching. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 618–629. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27836-8_53
Grabmayer, C.: Using proofs by coinduction to find “Traditional” proofs. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 175–193. Springer, Heidelberg (2005). https://doi.org/10.1007/11548133_12
Henglein, F., Nielsen, L.: Regular expression containment: coinductive axiomatization and computational interpretation. In: Proceedings of POPL 2011, pp. 385–398. ACM (2011)
Krishnaswami, N.R.: A typed, algebraic approach to parsing (2017). https://www.cl.cam.ac.uk/nk480/parsing.pdf
Lu, K.Z.M., Sulzmann, M.: An implementation of subtyping among regular expression types. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 57–73. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30477-7_5
Marriott, K., Stuckey, P.J., Sulzmann, M.: Resource usage verification. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 212–229. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40018-9_15
Might, M., Darais, D., Spiewak, D.: Parsing with derivatives: a functional pearl. In: Proceedings of ICFP 2011, pp. 189–195. ACM (2011)
Reps, T.: Program analysis via graph reachability. In: Proceedings of ILPS 1997, pp. 5–19. MIT Press, Cambridge, MA, USA (1997)
Sulzmann, M., Lu, K.Z.M.: A type-safe embedding of XDuce into ML. Electron. Notes Theor. Comput. Sci. 148(2), 239–264 (2006)
Winter, J., Bonsangue, M.M., Rutten, J.J.M.M.: Coalgebraic characterizations of context-free languages. Log. Methods Comput. Sci. 9(3), 1–39 (2013)
Acknowledgments
We thank the APLAS’17 reviewers for their constructive feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Sulzmann, M., Thiemann, P. (2017). A Computational Interpretation of Context-Free Expressions. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-71237-6_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-71236-9
Online ISBN: 978-3-319-71237-6
eBook Packages: Computer ScienceComputer Science (R0)