cubical
cubical copied to clipboard
agda
Suggestion for application of SIP
Define the type of finite automata, and then characterize its equality using SIP. This should give one of the several notions of automata equivalence known from the literature. (The "right" one?) Like for categories, I expect that perhaps there should be two notions, where one is that of "univalent automaton". Then two of the traditional notions of equivalence should collapse to one (maybe).
Are you aware of https://git.sr.ht/~jorge-jbs/theory-of-computation? I haven't really looked at the code yet, but it seems very much related to your suggestion
Btw, the place to discuss this is over on the Agda Zulip: https://agda.zulipchat.com/#narrow/stream/260790-cubical/topic/Theory.20of.20computation
The reason I chose this place and not a mailing list, or twitter, or a blog, or Zulip is that I feel that the majority of examples of SIP given in both my lecture notes and the Cubical Agda library are mathematical rather than computational. This is fine with me given my love of maths. But if we want to attract computer scientists too, as I believe we do, we should add lots of interesting and useful applications of univalence to computer science. I believe automata theory is a natural and appealing example for a general audience of computer scientists.
Edit: Moreover, there are lots of work on automata theory developed in the language of categories, not only recently in the coalgebra community, but also since a long time ago with the work of Eilenberg, in addition to the traditional computer science references given in the above link, in a nice cross fertilization with maths. It would be nice to have the Cubical Agda library to represent this cross fertilization in a new way .
Yeah, I totally agree that we need more CS applications of univalence and HITs. I only meant to refer the discussion about the particular formalization that I linked in my previous message to the already existing Zulip conversation about it. Sorry for the confusion, I think we can leave this issue open until someone has done what you suggest
I am on the process of learning about SIP. Maybe a good candidate is the final coalgebra as a structure? https://github.com/niccoloveltri/final-pfin
