Grammar Transformation to Chomsky Normal Form

Stream: new members

[Ramneet Singh]

I'd like to certify the algorithm for transforming any context-free grammar to Chomsky Normal Form. The inspiration for this is https://www.mathnet.ru/links/316b2bdc8ebee2d0774a0b54eb0f1f33/tisp24.pdf. The overall plan is to define five individual transformations and show that they are semantics preserving, i.e., don't change the language of a context-free grammar. I will then show that if put in a particular sequence, the transformations are guaranteed to terminate by well-founded induction on some measure.

I'm a little lost on formalising this in Lean (I'm using Version 3.50). I imagine I'll need to define a type for context-free grammars and then define functions corresponding to transformations. I am also confused about showing termination in Lean, since it doesn't hesitate to use the Axiom of Choice in its proofs which might make them non-computable. Specific advice or pointers to appropriate learning resources would both be appreciated. Thank you in advance for any help.

[Martin Dvořák]

Please consider making it on top of my library:
https://github.com/madvorak/grammars
Normal forms of grammars are something I just started planning implementing.
I am willing to provide any support you will need.

[Martin Dvořák]

Please, don't be scared of my code. In just a few days, I will release a technical report documenting it.

[Martin Dvořák]

My version of Lean is 3.41.0 but I suppose I can update it if it makes a difference for you.

[Martin Dvořák]

Martin Dvořák said:

Please, don't be scared of my code. In just a few days, I will release a technical report documenting it.

https://arxiv.org/abs/2302.06420

[Eric Wieser]

The computability package does not declare any syntactic sugar for the Kleene star

This is actually false as of the last few weeks, docs#has_kstar

[Martin Dvořák]

I had no idea! Is it a backport from mathlib4?

[Eric Wieser]

No, port-status#computability/language isn't in mathlib4 at all yet

[Martin Dvořák]

Thanks for the info! I will consider updating my project to the newest version of mathlib3.

[Martin Dvořák]

With the update, I should probably wait for what @Ramneet Singh as the first user of my library prefers.
Do you want me to synchronize the main branch with the current version of mathlib?

[Ramneet Singh]

@Martin Dvořák It's very kind of you to ask. Yes I do think that would be helpful. But I have to say, I'm a complete beginner at Lean so it might take me a few weeks to get started actually using the library.

[Martin Dvořák]

Any news? @Ramneet Singh

[Ramneet Singh]

'm not very far along, I've just defined context free grammars. I'm struggling to define a function which generates a fresh non-terminal symbol that hasn't been used in the rules before.

[Martin Dvořák]

(already answering your PM)