Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: practice: software

Topic: Differentiating Regex

James Fairbanks (Apr 16 2020 at 19:13):

Apparently you can "differentiate" a regex and get an efficient algorithm for matching them. This sounds like CT in disguise, http://matt.might.net/articles/implementation-of-regular-expression-matching-in-scheme-with-derivatives/ but I don't know how. Paging Dr. @Jules Hedges for a lensology consult.

sarahzrf (Apr 16 2020 at 19:14):

if it;s the same thing as this https://en.wikipedia.org/wiki/Brzozowski_derivative

sarahzrf (Apr 16 2020 at 19:15):

then it's the adjoint to day convolution

sarahzrf (Apr 16 2020 at 19:15):

but i was just leaving so i cant explain in detail rn :|

sarahzrf (Apr 16 2020 at 19:15):

day convolution in this case is concatenation of languages, though

sarahzrf (Apr 16 2020 at 19:16):

so this is the closed monoidal structure on the powerset of strings

sarahzrf (Apr 16 2020 at 19:18):

err sorry i was actually thinking of this https://en.wikipedia.org/wiki/Quotient_of_a_formal_language
but they are closely related

Gershom (Apr 17 2020 at 01:12):

Not deeply categorical but getting closer is rutten’s usage in discrete coinductive differential stream calculus https://www.cwi.nl/~janr/papers/files-of-papers/tcs308.pdf

sarahzrf (Apr 17 2020 at 01:19):

ok now i can say a bit more

sarahzrf (Apr 17 2020 at 01:20):

in (0, 0)-categories—i.e., sets (well, more or less)—the equivalent to taking the category of presheaves is taking the powerset

sarahzrf (Apr 17 2020 at 01:21):

the equivalent to the yoneda embedding is $x \mapsto \{x\}$ and the equivalent of the yoneda lemma is $x \in S \iff \{x\} \subseteq S$

sarahzrf (Apr 17 2020 at 01:21):

now, a monoidal (0, 0)-category is just a monoid

sarahzrf (Apr 17 2020 at 01:23):

if you take the monoid Σ* of strings on some alphabet Σ, then day convolution on its "(0, 1)-category of presheaves" (powerset ordered under inclusion) looks like $L \otimes K \triangleq \{s_1 s_2 \mid s_1 \in L, s_2 \in K\}$

sarahzrf (Apr 17 2020 at 01:25):

this is not symmetric monoidal—it's not a commutative monoid—so when i say it's closed i mean it has 2 different internal homs

sarahzrf (Apr 17 2020 at 01:27):

one satisfying $L \otimes K \subseteq O \iff L \subseteq K \multimap O$ and the other satisfying $L \otimes K \subseteq O \iff K \subseteq L \mathrel{\hat\multimap} O$

sarahzrf (Apr 17 2020 at 01:27):

these are the "quotients of a formal language" in that wikipedia article

sarahzrf (Apr 17 2020 at 01:28):

the brzozowski derivative is in particular the quotient of something by a singleton language—i.e., by the result of yoneda-embedding some string

sarahzrf (Apr 17 2020 at 01:30):

so the derivative of L with respect to a string s is gonna be $y(s) \mathrel{\hat\multimap} L$

sarahzrf (Apr 17 2020 at 01:32):

incidentally, the | operator in regex is coproduct in this (0, 1)-category, and kleene star is taking the free monoid of something :-)

Philip Zucker (Apr 17 2020 at 03:32):

Following a link chain from Gershom's suggestion: https://ir.cwi.nl/pub/28550/ Rutten's recent textbook on coalgebra. has some category theory, automata, derivatives, what have you. Pretty interesting looking

Matteo Capucci (he/him) (Apr 17 2020 at 08:22):

Jeez, this thread is mind-blowing.

Matteo Capucci (he/him) (Apr 17 2020 at 08:23):

Is it just me or Brzozowski's derivative looks suspisciously like localization of a ring? Which, incidentally, is used by algebraic geometers to talk about derivatives

Matteo Capucci (he/him) (Apr 17 2020 at 08:26):

@sarahzrf I love your "low dimensional" category theory, it's incredible how seemingly advanced machinery was hiding in plain sight down in the $(0,0)$/$(0,1)$ world

Jules Hedges (Apr 17 2020 at 10:17):

Pretty!

sarahzrf (Apr 17 2020 at 13:39):

come see my talk for the ACT seminar on the 6th then :-)

sarahzrf (Apr 17 2020 at 13:39):

unless i procrastinate too hard on making slides and have to bail :sob:

sarahzrf (Apr 17 2020 at 14:00):

regarding kleene star being free monoid:

sarahzrf (Apr 17 2020 at 14:01):

a monoid $M$ has morphisms $I \to M$ and $M \otimes M \to M$; at level (0, 1), this is all you need, because there can be only one choice for those morphisms, and all diagrams commute automatically—being a monoid is a property of an element in a monoidal proset, not a structure to equip it with

sarahzrf (Apr 17 2020 at 14:02):

the tensor unit in our monoidal proset is $y(\varepsilon)$, empty-string language

sarahzrf (Apr 17 2020 at 14:04):

so a language $L$ is a monoid if both

1. $y(\varepsilon) \subseteq L$, or equivalently $\varepsilon \in L$
2. $L \otimes L \subseteq L$

sarahzrf (Apr 17 2020 at 14:05):

i.e., if it parses the empty string and it parses any concatenation of things in itself

sarahzrf (Apr 17 2020 at 14:06):

then the sub-proset of P(Σ*) whose elements are the monoids is reflective—has a left adjoint to its inclusion, "taking the free monoid"

sarahzrf (Apr 17 2020 at 14:07):

the property is that for all languages $L$ and languages that are monoids $M$, we have $F(L) \subseteq M \iff L \subseteq M$

sarahzrf (Apr 17 2020 at 14:08):

and of course L* is always a monoid for any L, so we can restrict it to a function of the right type; it is monotone; and it's not hard to check that it satisfies the property i just wrote

sarahzrf (Apr 17 2020 at 14:09):

so it's takng the free monoid!

sarahzrf (Apr 17 2020 at 14:10):

alternatively, observe that it literally is defined the same way as this construction of free monoids
image.png

Jesse Sigal (Apr 17 2020 at 15:04):

@sarahzrf wow, the "low dimensional" explanation is really cool. Have you seen this paper?

Change Actions: Models of Generalised Differentiation (https://arxiv.org/abs/1902.05465)

It gives a framework in which the derivative of regular expressions fit.

sarahzrf (Apr 17 2020 at 15:09):

i have not :eyes:

sarahzrf (Apr 17 2020 at 15:10):

also: hey neat to see you again :)

sarahzrf (Apr 17 2020 at 15:10):

you should come see my talk too

Jesse Sigal (Apr 17 2020 at 15:17):

sarahzrf said:

also: hey neat to see you again :)

Indeed, same :D

Jesse Sigal (Apr 17 2020 at 15:17):

Yep, ACT@UCR is on my google calendar :+1:

sarahzrf (Apr 17 2020 at 15:25):

for the record: the reason i had such a ready-made rant about this topic is that i've literally gone and formalized bits of it in coq before
image.png

sarahzrf (Apr 17 2020 at 15:26):

(language there is defined by Definition language : Type := PSh str.)

Christian Williams (Apr 17 2020 at 21:26):

This is great. The terminology coincides with the derivative of combinatorial species, which is also exponentiating by a representable: $y(c)\Rightarrow S \simeq S(c\otimes -)$. http://bergeron.math.uqam.ca/wp-content/uploads/2013/11/book.pdf

It's also useful for algebraic data types http://strictlypositive.org/calculus/;
and the derivative of operads describes variable binding, e.g. $\mathrm{abs}:(y(1)\Rightarrow L)\to L$. https://homepages.inf.ed.ac.uk/gdp/publications/Abstract_Syn.pdf

@Conor McBride, do you have any thoughts as to how this notion of regex derivative is connected to the derivative of data types?

sarahzrf (Apr 17 2020 at 23:19):

i am reminded that the tangent bundle of a space is given by exponentiating it by a particular infinitesimal object

sarahzrf (Apr 17 2020 at 23:20):

that's a rather differential thing

sarahzrf (Apr 17 2020 at 23:20):

and representables are tiny, altho "infinitesimal" is maybe not appropriate here going by the definition im seeing when opening the nlab page again (it seems to be for cartesian closure), and anyway im not sure whether theyre infinitesimal here in addition to tiny, wld have to think about it

sarahzrf (Apr 18 2020 at 06:09):

re: derivative of operads, an operad is a monoid in species (where ⊗ is species composition), right?

sarahzrf (Apr 18 2020 at 06:09):

so derivative of species ~ derivative of operads?

sarahzrf (Apr 18 2020 at 06:10):

...oooooh that's the point you were making? >.<