A Computational Interpretation of Context-Free Expressions

TL;DR

This paper presents a novel computational approach to parsing with context-free expressions by framing it as a type inhabitation problem, utilizing reachability and coercion concepts to interpret parse trees.

Contribution

It introduces a new type-theoretic framework for parsing that reduces containment problems to reachability and employs proofs-as-programs for interpretation.

Findings

Containment reduces to reachability via canonical states

A coercion transforms parse trees between expressions

Predictive parsing corresponds to partial coercion

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.