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: theory: category theory

Topic: Categorical models for abstract symbols

Ben Logsdon (Aug 21 2023 at 19:26):

I would like to find a categorical models for the programming langauge feature described below, which I call symbols. This idea is discussed in Part XIII of "Practical Foundations for Programming Languages" by Robert Harper, but I don't currently know whether my formulation below is equivalent to his.

There is some countably infinite type $\mathcal{S}$ of symbols. This type has decidable equality; there is some function $\_=\_ : \mathcal{S} \to \mathtt{Bool}$ which determines whether two symbols are the same. Besides this, symbols have no internal structure (i.e. no structure available to the user of the language). Since $\_=\_$ is the only primitive function available which eliminates symbols, all deterministic functions $\mathcal{S} \to A$ for any type $A$ should be almost-everywhere constant, i.e. constant on all but finitely many inputs.

There is a special (nondeterministic) function $\bullet$, which I pronounce "symbolgen". Each time $\bullet$ is evaluated, it produces a fresh symbol (i.e. a symbol that has never been produced before). In this way, $\bullet$ can be seen as an idealization of the process of generating a random string of bits---so idealized that it is downright impossible to generate the same symbol twice.

So...do you know of any categorical formulations of this feature or a similar one? Since it involves nondeterminism, it feels like it could be modeled by (something like) a Markov category, with $\bullet$ interpreted as a single nondeterministic function $\mathbf{1} \to \mathcal{S}$. I am especially interested in how this feature would interact with standard programming language features, such as inductive types.

To give a bit of context of this question...there are many purposes of this feature, but one of them is to serve as an abstract account of names (e.g. names of functions in a module system) which doesn't rely on some underlying structure, such as representing names as strings. Another application is to represent capabilities and access control explicitly---possession of a given symbol by a piece of code can indicate that that code is authorized to access certain information or modify data in a certain way. This is why it's important that $\bullet$ never yields the same symbol twice; if I generate a symbol to serve as a guard for some data I want to protect, I want to be sure that no one else will be able to generate that symbol later.

If no references seem to surface, then I'll sit down and puzzle through it myself, but I'm wondering if there is any existing work on this or a similar problem.

Spencer Breiner (Aug 21 2023 at 19:40):

Maybe not quite what you're looking for, but if you haven't seen them already you should look at [[nominal sets]].

Ryan Wisnesky (Aug 23 2023 at 01:34):

perhaps obvious, but you could implement it with a monad on top of stlc

Tobias Fritz (Aug 23 2023 at 04:09):

You may be interested in @Dario Stein 's Probabilistic Programming Semantics for Name Generation and the references to Stark's $\nu$-calculus given there.

Tobias Fritz (Aug 23 2023 at 04:17):

Also very relevant could be Section 25 in Dario's thesis, which describes a Markov category of nominal sets.

Tobias Fritz (Aug 23 2023 at 05:11):

I've been toying around a bit myself with similar ideas and constructed a different Markov category of nominal sets. I'm not sure to what extent the following is reasonable from the programming perspective, so take it as merely an idea that may or may not be worth considering further.

Let me start with some background on nominal sets. Fix an infinite set $\mathbb{A}$, whose elements are thought of as basic variable names. Let $G := S(\mathbb{A})$ be its group of finite permutations. Then let's say that a pre-nominal set is simply a $G$-set, i.e. a set $X$ together with a homomorphism from $G$ to permutations on $X$. The idea is that $X$ could e.g. be a set of expressions in your language, where the $G$-action keeps track of how these expressions change upon changing the names of variables. The support of an $x \in X$ is the smallest $B \subseteq \mathbb{A}$ such that $\pi|_B = \mathrm{id}_B$ for $\pi \in G$ implies $\pi x = x$. If you think of $x$ as an expression in your language, then this means that the support is the set of names that actually appear in it. Now a nominal set is a pre-nominal set $X$ such that every $x \in X$ has finite support. If $X$ is a nominal set, then for any $x, y \in X$, there is $\pi \in G$ such that $\pi x$ and $y$ have disjoint support: you can always rename the variables in an expression such that they become disjoint from those appearing in another one.

If $X$ and $Y$ are nominal sets, then the same considerations also apply to functions $X \to Y$, since these form a $G$-set of their own. We can now define a Markov category as follows:

• Objects are nominal sets. (Or even pre-nominal sets, either should work.)
• The morphisms $X \to Y$ are $G$-orbits of finitely supported functions from $X$ to $Y$.
• Composition is by choosing representatives of disjoint support and composing those. In the programming interpretation, you compose two functions by first making sure that the variable names appearing in them are disjoint, and then you compose them as ordinary functions. This is analogous to how composition of stochastic matrices assumes stochastic independence (as reflected in the fact that one multiplies probabilities).
• Similarly for the monoidal structure: choose representatives of disjoint support and then take the usual Cartesian product of functions.
• The Markov category structure is the obvious one, given by the diagonal maps $X \to X \times X$.

My hypothesis is that this Markov category provides a sensible way to talk about the sort of nondeterminism that you want to model. But I'm not sufficiently familiar with programming language theory to confidently assert this.

Sam Staton (Aug 23 2023 at 17:16):

Hi @Tobias Fritz, curious category. I've mainly considered the Kleisli category of the name generation monad on nominal sets for this kind of name generation. So I'm wondering whether your category has different properties as a Markov category? Or is there another reason that you propose it?

At first I thought your category might be very similar to the Kleisli category of the name generation monad, but $\mathbf{Nom}(\mathbb{A},T(2))=2$, whereas I think $\mathcal C(\mathbb{A},2)$ has many elements for your category $\mathcal C$.

Also. I tried calculating $\mathbb{A}\xrightarrow{\bullet\otimes id_{\mathbb{A}}}\mathbb{A}\times\mathbb{A}\xrightarrow{[=]}2$, to check whether it was equal to $\mathbb{A}\xrightarrow ! 1 \xrightarrow {false}2$. I couldn't get it, but maybe I misunderstood your definition, or made a mistake. Or maybe you didn't want this?

Tobias Fritz (Aug 24 2023 at 02:53):

Hi Sam! The simple reason for me to come up with this category was that I had just learned about nominal sets and hadn't heard of the name generation monad :sweat_smile: So for anyone else reading this: @Sam Staton is the real expert here on these things!

So far, I haven't thought about this category at all other than its definition, so I don't know what properties it has. I agree with your calculations though. In particular, yes, the composite $\mathbb{A}\xrightarrow{\bullet\otimes id_{\mathbb{A}}}\mathbb{A}\times\mathbb{A}\xrightarrow{[=]}2$ is not constant false, and not even constant. So somehow this category keeps track of more fine-grained information than the Kleisli category of the name generation monad: the resulting composite morphism $\mathbb{A} \to 2$ remembers that you had picked one fresh name, but it doesn't remember which one.

Tobias Fritz (Aug 24 2023 at 03:00):

So I don't really know what to make of this category. But given that the definition is pretty simple and natural (to anyone who knows about nominal sets), I think that there has to be some sensible interpretation or operational account of it. Would you agree with this expectation?

Here's an incomplete attempt at finding such an interpretation. Think of $\mathbb{A}$ as the set of bank notes in circulation; this set is infinite for all practical purposes, so let's formalize it as an infinite set. Then a typical morphism $\mathbb{A} \to 2$ could be represented by something like "given a bank note $x \in \mathbb{A}$, answer yes if and only if $x$ has ever passed through my wallet". Then there is a definite fact of the matter about how many notes have passed through my wallet, but no definite fact of the matter about which ones, since the morphism really is the entire orbit of such a predicate.

In general, it looks like a morphism in this category has the power to treat finitely many names as special. But for every morphism, these finitely many special names are required to be fresh (due to composition being defined in terms of disjoint support).

Sam Staton (Aug 26 2023 at 16:53):

Thanks Tobias. It's an interesting that you can have this "intensional" model -- I haven't seen it before.

As you probably know there are two monoidal closed structures on nominal sets. You used the cartesian closed one (finitely supported functions) as part of your construction. But I think if you'd used the other one, it would have been close to the usual name generation monad.

Tobias Fritz (Aug 27 2023 at 02:46):

Thanks, I didn't know this! I suppose that the "other one" is the monoidal structure called separated product, right? I'm not sure how this gives a Markov category, because there are no diagonals $X \to X \ast X$?

Ben Logsdon (Aug 31 2023 at 19:37):

Thanks all for the responses and discussion! The references and ideas here seem to be exactly what I was looking for. It will take me some time to absorb all the details here, but I have a few follow-up questions:

1. Is there a good reference (or section in one of the references mentioned above) that talks about the name-generation monad on the category of nominal sets? I haven't seen it so far in my reading.
2. What is the other monoidal closed structure on nominal sets (alternatively, where can I read about it)?
   Thanks again; this was very helpful for me.

Tom Hirschowitz (Sep 04 2023 at 16:53):

What's a finitely supported function, concretely? Or maybe before that, what's the action of permutations on functions that you consider? (Sorry for the naive question...)

Tobias Fritz (Sep 04 2023 at 16:57):

If $X$ and $Y$ are $G$-sets, then the action on functions is such that a group element $g \in G$ acts on a function $f : X \to Y$ by producing the new function $g \cdot f$ defined by $(g \cdot f)(x) = g \cdot f(g^{-1} \cdot x)$. This $G$-set of functions is the exponential object $Y^X$ in the category of $G$-sets, see Proposition 3.9.

Tobias Fritz (Sep 04 2023 at 17:00):

A function $f$ is finitely supported if there is finite $S \subseteq \mathbb{A}$ such that if $g$ is any group element that acts like the identity outside of $S$, then also $g \cdot f = f$. I think of this as saying something like "only the variable names in $S$ appear in the definition of $f$".

Tobias Fritz (Sep 04 2023 at 17:01):

So, any equivariant function $X \to Y$ is finitely supported, since we can even take $S = \emptyset$. For a non-equivariant example, any constant function $\mathbb{A} \to \mathbb{A}$ is finitely supported.

Tom Hirschowitz (Sep 05 2023 at 07:58):

Thanks! Do you mean "acts like the identity on $S$", or am I confused? Is it right that the point of your category is to include more morphisms than the usual equivariant maps?

Tobias Fritz (Sep 05 2023 at 08:34):

I do mean "identity outside of S". If you think of S as the set of variables names that occur in f, then permuting other variable names that do not occur in f doesn't do anything, but permuting those that do occur in f will generally result in a different expression.

Tobias Fritz (Sep 05 2023 at 08:35):

But yes, the idea is to include more morphisms than the equivariant ones, constructing an interesting-looking Markov category like that. The equivariant morphisms are precisely those that are deterministic in the Markov cats sense

Tom Hirschowitz (Sep 05 2023 at 09:02):

Tobias Fritz said:

I do mean "identity outside of S". If you think of S as the set of variables names that occur in f, then permuting other variable names that do not occur in f doesn't do anything, but permuting those that do occur in f will generally result in a different expression.

Sorry for being so thick, but "permuting variable names that do not occur in f" sounds to me like being identity on $S$. Let me explain how I'm thinking so that maybe you can pinpoint where I'm derailing.

You seem to be saying that if g only permutes variable names that do not occur in f, then
$g \cdot f = f$, but

only permuting variable names that do not occur in f

is the same as

leaving variable names in $$S$$ unchanged

ie

being identity on $$S$$.

Where is this wrong?!

Tobias Fritz (Sep 05 2023 at 09:23):

D'oh, of course you're right, and I've been very confused :grimacing: Looks like my explanation was fine, but my statement of the condition was off. Thanks for the correction!

Tom Hirschowitz (Sep 05 2023 at 09:31):

Oh ok! Thanks for the explanation then :big_smile: