# Formalising parallel parsing (ValiantAgda code updates)

September 15, 2023

Professor of Computer Science

September 15, 2023

One of the lunch discussions during the recent ICFP 2023 week was about parallel parsing and I was then inspired to look up the Agda code of this paper:

"Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda"

Jean-Philippe Bernardy, Patrik Jansson

http://arxiv.org/abs/1601.07724

"Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda"

Jean-Philippe Bernardy, Patrik Jansson

http://arxiv.org/abs/1601.07724

The basic idea is to compute a (sparse, upper triangular) matrix whose position (i,j) contains the parses from position i to j in the input string. The fact that it works is fascinating! The formalisation is an exercise in working with block matrices in several layers and keeping few requirements on the final matrix elements in the "leaves" but still synthesizing the necessary properties on the way up the "quad tree".

The Agda code was originally published on github in 2016 (using Agda version 2.4.2.3 and agda-stdlib-0.9) but as usual with code written in a living language (Agda) it did not type check anymore. It took almost two hours to figure out the changes needed to bring it up to date with current Agda 2.6.3 and stdlib 1.7.3:

https://github.com/DSLsofMath/ValiantAgda

There were a number of (arguably minor) changes needed:

https://github.com/DSLsofMath/ValiantAgda

There were a number of (arguably minor) changes needed:

- Three renamings / moves in stdlib:
- Relation/Binary/On.agda -> Relation/Binary/Construct/On.agda
- Relation.Binary.EqReasoning -> Relation.Binary.Reasoning.Setoid
- Algebra.FunctionProperties -> Algebra.Definitions

- records need new modifier eta-equality to allow for pattern-matching (with eta-equality) on the constructor.
- IsCommutativeMonoid record rationalised in the library (the hint was a bit indirect: “The record type IsCommutativeMonoid does not have the fields isSemigroup, identityˡ but it would have the field isMonoid …”.)

It would be interesting to investigate what it wold take to build tool support for this kind of code refactoring. The only tool support I had was the error messages from (current) Agda and the full repository history of stdlib on github.