Email Gateway (Aug 22 2022 at 18:41): Email Gateway (Aug 22 2022 at 18:41):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Dear All,
Last week, after a short talk about my research, some experts in Isabelle
suggested me to make my developments in the theory of formal languages more
algorithmic, because my original approach was non-constructive (a bad habit
from classical mathematics). After reading the tutorial "Defining Recursive
Functions in Isabelle/HOL" I reformulated my definitions and I proved some
classical theorems.
For me it was a nice exercise in order to remember the theory of formal
languages. Nevertheless, I do not know if my results are already in some
library in Isabelle/HOL. If this is the case, I would prefer to use the
library. This constructive approach will allow me to do both computations
and proof in Isabelle. Before, I did the computations in SAGE.
My algorithmic definition of Dyck paths:
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-language-theory/blob/master/DyckPathsDef.thy
The classical results that I proved (exercises in any course of
introduction to formal languages):
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-language-theory/blob/master/DyckPathsCharacterization1.thy
Thank you for the previous suggestions. Any new suggestion or comment is
welcome.
Sincerely yours,
José Manuel Rodriguez Caballero
Last updated: Nov 21 2024 at 12:39 UTC