Collected notes

The Rocq proof of linearity of the prefixed pikevm is out of scope.

To discuss

• Thesis format? Typst? -> possible, needs to check rules. People in general did it in Latex
• If we add ? and ?? and then prove equivalence between general quantifiers and expansion on the AST + usage of */*?/?/??, we could argue the same could have been done with anchors and look-arounds (which was proven to be equivalent). Maybe it is good to discuss where is the border between supporting directly vs through an equivalence. Is that why anchors were not implemented? -> the decision is to add ?/?? to PikeVM, then have all quantifiers through equivalence
  • It would seem adding them directing and doing the expansion in the bytecode is easier than doing an AST rewrite. But doing an AST rewrite can give good foundation for future proofs.
• Is there any way to do a shallow simplification and choose the exact subterms? I want it to compute the fuel and the bytecode for me. -> hard to answer, old question
• Does linden do “Linear Matching of the Capture Reset Property”? -> yes, through GroupReset and Check/Progress.

Action items

• Write an outline of the thesis
• Finish non-det proof
• Re-investigate the linearity of the prefixed pikevm