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.
Lê Thành Dũng (Tito) Nguyễn (Oct 07 2022 at 04:09):I'm not sure what's the best / most appropriate way to advertise this, but in connection with Gordon Plotkin's future Topos Institute Berkeley Seminar talk https://topos.site/berkeley-seminar/ I would like to announce that I have obtained a characterization of what he calls the "nonuniformly definable" functions in the simply typed λ-calculus, making essential use of the results (https://arxiv.org/abs/2206.08413) that he's going to present in the talk (at least according to his abstract).
While I have not yet finished writing a paper on it I have had the opportunity to present my discovery at a seminar of the University of Warsaw recently:
https://www.mimuw.edu.pl/aktualnosci/seminaria/transducer-model-simply-typed-l-definable-functions
As said in the above abstract, the characterisation uses an automaton model, in line with my work with Cécilia Pradic on "implicit automata in typed λ-calculi". See our first paper on the topic
https://hal.science/hal-02476219/document
for a brief introduction to the perspective we've been developing, or Chapter 1 of my PhD thesis defended last year
https://nguyentito.eu/thesis.pdf
for a more lengthy overview of this research programme. (In fact the result I'm announcing here positively answers Conjecture 1.4.3 in my thesis.)
Lê Thành Dũng (Tito) Nguyễn (Oct 07 2022 at 04:11):While I'm at it, let me mention that I also know a way to prove Prof. Plotkin's result using the standard set-theoretic semantics of the simply typed λ-calculus instead of Scott domains, by adapting Statman's approach from the following paper https://www.sciencedirect.com/science/article/pii/S0168007204000661
Lê Thành Dũng (Tito) Nguyễn (Oct 07 2022 at 04:16):I also have some slides from an older talk (I hadn't yet proved my conjecture) geared towards an audience of automata theorists, but which may still be helpful to understand what it is I'm talking about: https://nguyentito.eu/updated-stlc-transducer.pdf
Lê Thành Dũng (Tito) Nguyễn (Mar 21 2023 at 12:36):Hmm, so I still haven't managed to properly write up the proof that I announced a few months ago (yay ADHD…) but I have a new preprint with Mikołaj Bojańczyk – again on automata, this time with a bit of category theory too – which has just been accepted for presentation at SYCO 11!
https://hal.science/hal-03985883/document
Title: Algebraic Recognition of Regular Functions
Abstract: We consider regular string-to-string functions, i.e. functions that are recognized by copyless streaming string transducers, or any of their equivalent models, such as deterministic two-way automata. We give yet another characterization, which is very succinct: finiteness-preserving functors from the category of semigroups to itself, together with a certain output function that is a natural transformation.
Semigroups are like monoids, but possibly without a unit element. Our result is analogous to the following classical theorem: a set of words over a finite alphabet, in other words a function from a finitely generated free monoid to {yes,no}, is a regular language – described by some regular expression, or equivalently recognized by some finite-state automaton – if and only if it factors through a homomorphism to a finite semigroup. Or to a finite monoid, but for our generalization to string-to-string functions, there are good technical reasons to work with semigroups instead.