search

noughtmare / parsing-ddgs

Parsing Data-Dependent Grammars using Derivatives
0 stars 0 forks source link

Which properties do we want to prove? #13

Open noughtmare opened 1 month ago

noughtmare commented 1 month ago

The main advantage of a type theoretic formalization of parsing (as opposed to an operational automata-based formalization) is that it makes it easier to reason about our parsers. But which things do we actually want to know?

The main properties I can think of are basic algebraic properties like commutativity of the union of languages and related semiring laws. We also want to know that our fixed points are proper fixed points (#12).

One other important property is ambiguity (#3, #4, #10). That will be necessary to prove linear time complexity (#5). However, I don't think that will make it into the paper as that still seems very difficult to me.

Are there other properties we would want to prove?

noughtmare commented 1 month ago

In particular, what property characterizes the nullability of the fixed point operator. I wanted to propose:

νfix : ν (fix₀ P) ↔ ν (P ⊘)

However, that does not seem to be provable.