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.
My Petri-net paper is out!
http://arxiv.org/abs/2005.05108
I hope it will be of interest to some people in this chat, and I am very eager to get feedback, especially regarding the proper place of all this in the theory of Petri nets. I have been interested in Petri nets for many years, but it's a huge field and most of it I cannot grasp, so I feel a bit awkward writing about it as if I were an expert.
Here is the title and abstract:
Elements of Petri nets and processes
We present a formalism for Petri nets based on polynomial-style finite-set configurations and etale maps. The formalism supports both a geometric semantics in the style of Goltz and Reisig (processes are etale maps from graphs) and an algebraic semantics in terms of free coloured props: the Segal space of P-processes is shown to be the free coloured prop-in-groupoids on P. There is also an unfolding semantics \`a la Winskel, which bypasses the classical symmetry problems. Since everything is encoded with explicit sets, Petri nets and their processes have elements. In particular, individual-token semantics is native, and the benefits of pre-nets in this respect can be obtained without the need of numberings. (Collective-token semantics emerges from rather drastic quotient constructions \`a la Best--Devillers, involving taking $\pi_0$ of the groupoids of states.)
Wow, this looks great. Looking forward to reading it!
Here is the main point of the paper, which is just a definition: I define Petri nets to be diagrams of finite sets where is the set of transitions, is the set of places, and and are the sets of incoming and outgoing arcs of transitions. In particular, for a transition , the fibres and are explicit sets, and they are not necessarily subsets of . It is only a slight modification of the usual definition. I like to call them whole-grain Petri nets. In fact the key point is to replace the usual notion of multiset (in terms of multiplicity functions) with the representable analogue where a multiset on is an element in the finite slice . In this sense, the definition can be seen as modifying the classical definition by replacing the free-commutative-monoid monad with the free-symmetric-monoidal-category monad --- but the definition is still just a configuration of finite sets! It can also be seen as a version of pre-nets, but without numberings. Once I have told you this, and since you are category theorists, I am afraid there are no more surprises, and maybe you will think it is all trivial.
(You might also say that changing the definition is cheating. But if you follow the development of the theory, there is always an escape route you can take if you don't like it: at any point you can take and get back to classical theory. My own opinion is that you should delay this as much as possible, because groupoids are so much cooler than sets.)
I like this idea. It definitely seems more natural than the way we've been doing it, ie with , which I always found awkward.
From this definition the theory develops quite naturally. There is a natural notion of etale map: they are maps between diagrams where the middle squares are pullbacks. There is a lot of recycling of a formalism for directed graphs I developed some years ago in connection with properads [Graphs, hypergraphs, and properads (2016)]. 'Graph' now means directed acyclic graph admitting open-ended edges.
A process of a Petri net P is just an etale map from a graph. There is a natural symmetric monoidal Segal space of processes, and it is shown to be the free prop-in-groupoids on P. Maybe that's the main theorem. (One can also extract a 1-categorical version of this.)
A digraphical species is a presheaf on the category of elementary graphs. The elementary graphs are the connected graphs without inner edges, so the only possibilities are: the unit graph (one edge, no nodes), and the (m,n)-corollas. A digraphical species is also called a coloured bi-collection. They are the kind of structure underlying props and properads -- and the kind of stuff you generate free props and properads from. The next key point is that there is a restricted-Yoneda embedding from whole-grain Petri nets to digraphical species. The image is shown to consist of the flat digraphical species -- that just means those whose symmetric-group actions are free. The free prop-in-groupoids has an explicit description in terms of graphs, easily seen to agree with the Segal space of processes.
All this is precisely analogous to the way polynomial endofunctors embed into ordinary coloured species (coloured collections). That was my motivation for doing all this.
One can also say that whole-grain Petri nets sit in between ordinary Petri nets and pre-nets in the same way as polynomial monads sit in between symmetric operads and non-symmetric operads.
In this sense, the definition can be seen as modifying the classical definition by replacing the free-commutative-monoid monad with the free-symmetric-monoidal-category monad --- but the definition is still just a configuration of finite sets!
I (and I guess a few other people) had the idea to do something nearly exactly like this not too long ago. I think this presentation is much cleaner than what I would have come up with though
Joe Moeller said:
I like this idea. It definitely seems more natural than the way we've been doing it, ie with , which I always found awkward.
I wouldn't say that one is more natural or more awkward; they're just different. The ones are presentations of commutative monoidal categories. I suspect the ones Joachim is talking about are presentation of symmetric monoidal categories.
Mike Shulman, Jade Master, Fabio Genovese and I are writing a paper about this latter kind. Mike's preferred description is different than what Joachim just described, but I bet they're just different ways to formalize the same concept. This is just a guess; I'll check it.
Yes definitely, but I think commutative monoidal categories are inherently awkward, so this is an extension of that opinion.
I don't like words like "awkward" very much: they're too vague. Commutative monoidal categories show up when one is taking the "collective token philosophy", i.e. when doesn't care at all about switching two tokens in the same place. Symmetric monoidal categories show up when one is taking the individual token philosophy. They're both important.
For example, in applications to chemical reaction theory it's good to take the collective token philosophy.
Anyway, in the paper with all those coauthors, we're going to show how these two philosophies fit together.
So, now we have to read Joachim's paper and see how to adjust our paper to take it into account. If he's done everything we were going to do, that means less work for me! But I'm afraid that's probably not true.
Joe Moeller said:
In this sense, the definition can be seen as modifying the classical definition by replacing the free-commutative-monoid monad with the free-symmetric-monoidal-category monad --- but the definition is still just a configuration of finite sets!
I (and I guess a few other people) had the idea to do something nearly exactly like this not too long ago. I think this presentation is much cleaner than what I would have come up with though
I think that Sassone thought of the symmetric-monoidal-category monad ten years ago, but he didn't follow up on it, as far as I know. Personally I am fond of the fact that one can avoid the monad, and just talk about configurations of finite sets.
When you say I suppose it is the commutative-monoid monad, like in Meseguer-Montanari?
Does this definition actually make Petri nets into a presheaf category on the (two spans sharing feet) category?
Joachim Kock said:
I think that Sassone thought of the symmetric-monoidal-category monad ten years ago, but he didn't follow up on it, as far as I know.
I don't think he really quite managed to work this out.
When you say I suppose it is the commutative-monoid monad, like in Meseguer-Montanari?
Yes, that's the notation for the commutative monoid monad that I use in all my papers on Petri nets.
More generally for any commutative monoid I use for the set of finite linear combinations of elements of a set with coefficients in . The most famous case is a group ring like when our set is a group.
So we have when is finite but not otherwise.
John Baez said:
Mike Shulman, Jade Master, Fabio Genovese and I are writing a paper about this latter kind. Mike's preferred description is different than what Joachim just described, but I bet they're just different ways to formalize the same concept. This is just a guess; I'll check it.
I look forward to hear about that!
I am very much aware that maybe I mostly like the whole-grain formalism because it fits into my way of thinking in terms of polynomial functors. Not everybody thinks like that! I hope to get in contact with real users of Petri nets, and hear what they think.
Here is the main point of the paper, which is just a definition: I define Petri nets to be diagrams of finite sets where is the set of transitions, is the set of places, and and are the sets of incoming and outgoing arcs of transitions.
Interestingly this is the approach I took back when I wanted to have Petri nets be the objects of a topos - Joe may remember that. But then I decided I didn't like the morphisms in that topos.
I don't remember that.
I do remember there being a category of Petri nets with undesirable morphisms.
I was really excited about this particular approach because you can think of these diagrams as objects in a presheaf topos.
But then there are morphisms that squash down two elements of or ("arcs") to one.
So I'm curious what Joachim's morphisms between Petri nets are!
Joe Moeller said:
Does this definition actually make Petri nets into a presheaf category on the (two spans sharing feet) category?
Depends on the maps you allow. I am not an expert, but it is not so clear to me what general maps of SITOS diagrams (so as to have a presheaf category) would mean. I think the nice maps are the etale maps, and then it is no longer a presheaf category. At the end of my paper I also consider some more general maps called rational maps, consisting of certain spans: a little backwards correction map before the main part which is a forward etale map.
John Baez said:
I don't like words like "awkward" very much: they're too vague. Commutative monoidal categories show up when one is taking the "collective token philosophy", i.e. when doesn't care at all about switching two tokens in the same place. Symmetric monoidal categories show up when one is taking the individual token philosophy. They're both important.
I am struggling to understand the significance of these two 'philosophies'. Lacking a philosophical education in Petri nets, I just followed my instinct: even if I were not interested in sets (arcs or tokens) other than their number and kind, my instinct would still be to deal with them as actual sets. And then take of some groupoids at some point.
John Baez said:
So, now we have to read Joachim's paper and see how to adjust our paper to take it into account. If he's done everything we were going to do, that means less work for me! But I'm afraid that's probably not true.
I am sure it is not true, because I do very little. Judging from the composition of your team, I am probably only scratching the surface of what you are doing.
John Baez said:
So I'm curious what Joachim's morphisms between Petri nets are!
They are morphisms of SITOS diagrams where the middle squares are pullbacks. They are called etale maps.
Both the diagrams and the etale maps are from my properads paper https://arxiv.org/abs/1407.3744
The digraphical species are also from that paper.
Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all, while the people at Statebox applying Petri nets to industrial process use the individual token philosophy (Petri nets as presentations of free strict symmetric monoidal categories), because for them switching two people counts as doing something.
I'll have to think about what etale maps actually are in concrete low-brow terms, before I can mentally process what you did. But it sounds interesting!
@John Baez, is the following true?
John Baez said:
Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all, while the people at Statebox applying Petri nets to industrial process use the individual token philosophy (Petri nets as presentations of free strict symmetric monoidal categories), because for them switching two people counts as doing something.
yeah I think of this collective token philosophy as a big part of what makes petri nets interesting as a model of mass action. The idea that the molecules of a given species are interchangeable and the concentrations are uniform over space are pretty important. Outside of chemistry this assumption is used in the SIR epidemics modeling. If you don't take the collective token approach then you can't approximate the dynamics with simple ODEs.
If you are asking about the reachability relation then the individual token philosophy makes sense as an extension of vanilla petri nets, but in the chemical setting, distinguishing between tokens really doesn't make any sense from the perspective of the underlying chemistry. If you want to distinguish between molecules of the same species, you need a spatial model that talks about concentration as a function of position. Or your definition of "species" is too coarse.
Daniel Geisler said:
John Baez, is the following true?
- Free commutative monoidal categories - unlabeled combintorial structures
- Free strict symmetric monoidal categories - labeled combintorial structures
What is a (un)labelled combintorial structure?
Joachim Kock said:
Joe Moeller said:
Depends on the maps you allow. I am not an expert, but it is not so clear to me what general maps of SITOS diagrams (so as to have a presheaf category) would mean. I think the nice maps are the etale maps, and then it is no longer a presheaf category.
Do you know for sure that WGPNs with etale maps are not a presheaf category (on any domain category), or just that they are not a presheaf category in this particular way? (I ask because the BGMS notion of net is a presheaf category, albeit in a slightly non-obvious way; so if yours are not then it would give an easy proof that the two are different.)
James Fairbanks said:
John Baez said:
Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all, while the people at Statebox applying Petri nets to industrial process use the individual token philosophy (Petri nets as presentations of free strict symmetric monoidal categories), because for them switching two people counts as doing something.
yeah I think of this collective token philosophy as a big part of what makes petri nets interesting as a model of mass action. The idea that the molecules of a given species are interchangeable and the concentrations are uniform over space are pretty important. Outside of chemistry this assumption is used in the SIR epidemics modeling. If you don't take the collective token approach then you can't approximate the dynamics with simple ODEs.
If you are asking about the reachability relation then the individual token philosophy makes sense as an extension of vanilla petri nets, but in the chemical setting, distinguishing between tokens really doesn't make any sense from the perspective of the underlying chemistry. If you want to distinguish between molecules of the same species, you need a spatial model that talks about concentration as a function of position. Or your definition of "species" is too coarse.
Another way to understand this is that, if you were to assign types to places, your places would all have type unit in the collective token philosophy.
This also highlights very well why the collective token philosphy does not work well in many compsci applications. There your places do not have type unit, and being tokens terms of that type you need to distinguish between tokens in an execution.
John Baez said:
I'll have to think about what etale maps actually are in concrete low-brow terms, before I can mentally process what you did. But it sounds interesting!
I should have said that: they are just the maps that preserve in/out arities on transitions.
Or maybe I should not have said it --- I also hope you will read the paper :-)
Daniel Geisler said:
Free commutative monoidal categories - unlabeled combinatorial structures
Free strict symmetric monoidal categories - labeled combinatorial structures
@Fabrizio Genovese said:
What is a (un)labelled combinatorial structure?
I picked the terms up from Philippe Flajolet's work and suspect it is in Combinatorial Analytics. A common example is the unlabeled integer partitions and labeled set partitions/Bell numbers. The different labeled set partitions map into the integer partitions.
Mike Shulman said:
Joachim Kock said:
Joe Moeller said:
Depends on the maps you allow. I am not an expert, but it is not so clear to me what general maps of SITOS diagrams (so as to have a presheaf category) would mean. I think the nice maps are the etale maps, and then it is no longer a presheaf category.Do you know for sure that WGPNs with etale maps are not a presheaf category (on any domain category), or just that they are not a presheaf category in this particular way? (I ask because the BGMS notion of net is a presheaf category, albeit in a slightly non-obvious way; so if yours are not then it would give an easy proof that the two are different.)
It is not a topos because there is no terminal object. A terminal object would amount to a finite-map classifier in Set.
(It would be an -topos if we copied over the definition to -groupoids and demanded the two middle maps to belong to a bounded local class, just like polynomial functors over -groupoids form an -topos is just the middle maps are demanded to belong to a bounded local class (see [Gepner-Haugseng-Kock]).)
On the other hand, WGPetri is locally a topos, in the sense that every slice of WGPetri is a topos. (This follows since the etale maps are really an example of the Joyal-Moerdijk axiomatic notion of class of etale maps.) In particular, pre-nets (In the sense of Bruni-Meseguer-Montanari-Sassone) form a topos (at least if we allow infinite nets), because pre-nets are WG Petri nets with an etale map to the Petri net obtained by gluing together all the elementary graphs at a single place (i.e. one transition for each (m,n)). (Just like nonsymmetric sequences are polynomial endofunctors cartesian over the free-monoid monad.)
Yes, I think you can see it this way
In symmetric monoidal categories different permutations of an object are distinct, while in commutative monoidal categories they are not.
Joachim Kock said:
My Petri-net paper is out!
It's interesting that you have Morse functions in your formalism. I'm wondering if this musing by @Jules Hedges could be formulated under this. :thinking:
I sometime use the phrase "future alien [wizard] mathematics". Usually I mean it for hypothetical stuff involving *taking the topology of syntax seriously*. For example if you're using surface diagrams to denote computer programs, then it's using Morse theory to study programming
- julesh (@_julesh_)morse theory seems really cool
but i dont think i know enough diff geo to learn it :upside_down:
You don't really need diff geo in this case.
You should start from discrete Morse theory, that's combinatorics ;)
what does discrete morse theory do
It starts from a combinatorial CW complex (for example, the face poset of a regular CW complex, or a simplicial complex) and gives you criteria for deleting cells without changing the homotopy type.
interesting
The thought bubble I had was that Petri nets are already used to model programs, so Jules' vision could emerge if you could do Morse theory there.
James Fairbanks said:
I think of this collective token philosophy as a big part of what makes petri nets interesting as a model of mass action. The idea that the molecules of a given species are interchangeable and the concentrations are uniform over space are pretty important. Outside of chemistry this assumption is used in the SIR epidemics modeling. If you don't take the collective token approach then you can't approximate the dynamics with simple ODEs.
Hi James, all this is very interesting. I have some questions, if you don't mind. In these models for chemical reactions or epidemics,
1) is it correct that you are talking about Petri nets with rates?
2) is it correct that you are interested in markings where there are millions of tokens?
3) do you ever talk about events or concurrency?
4) do you ever play the token game and look at firing sequences or unfolding?
5) what is your actual use of monoidal categories semantics?
That would be a great starting point for me to try to understand what tiny little corner of Petri net theory I am actually working in. Maybe I need to rewrite the introduction of my paper to better delimit its potential interest.
I hope to see you again in the break-out rooms soon!
Daniel Geisler said:
- Free commutative monoidal categories - unlabeled combintorial structures
- Free strict symmetric monoidal categories - labeled combintorial structures
That sounds like a very good analogy to me. (But I might have to revise my opinion over the coming days...)
As a further analogy in this directions, the relation between ordinary generating functions and exponential generating functions.
And as an addition to the reference to [Flajolet-Sedgewick], let me add the theory of combinatorial species. That's built on the idea of labelled combinatorial structures -- the objects are really sets equipped with a structure, not just iso-classes of such things. But it is also a great tool to deal with unlabelled structures, through fix-point calculus and cycle index series.
Where combinatorial species are 'structures that sets can have', I see Petri nets as '(local) structures that graphs can have'. (These graphs are the processes.) Graphs decorated with Petri nets exist both in the collective- and the individual-token viewpoints, but in the collective-token viewpoint these graphs do not work as arrows in categories.
Joachim Kock said:
It is not a topos because there is no terminal object. A terminal object would amount to a finite-map classifier in Set.
Excellent, thanks! So our categories are definitely different.
Amar Hadzihasanovic said:
It starts from a combinatorial CW complex (for example, the face poset of a regular CW complex, or a simplicial complex) and gives you criteria for deleting cells without changing the homotopy type.
That's fine, but in this thread I should probably point out that the Morse functions in my paper are not the discrete Morse functions from the theory of simplicial complexes! I have an explicit warning in my paper. Maybe it is silly of me to call them Morse functions, it's just that I rely on intuition from cobordism categories.
Fabrizio Genovese said:
This also highlights very well why the collective token philosophy does not work well in many compsci applications. There your places do not have type unit, and being tokens terms of that type you need to distinguish between tokens in an execution.
What's a "type unit"? I don't understand the last sentence here, in part because of that and in part because the chunk after "and" isn't grammatical (as far as I can tell). But I think I understand the basic idea in a vague way, and I'd like to understand it the way you do.
It should be read as "the type of each place is the unit (i.e. terminal/singleton) type".
@Joachim Kock - here's a lazy request: could you describe your etale maps between your whole-grain Petri nets in a very lowbrow undergraduate-style way?
Say I have two of them:
and
Is an etale map from the first to the second a function from to , a function from to , a function from to and a function from to obeying some property?
John Baez said:
Joachim Kock - here's a lazy request: could you describe your etale maps between Petri nets in a very lowbrow undergraduate-style way?
It's a map of diagrams from one SITOS diagram to another. So it maps transitions to transitions and places to places. It also maps arcs to arcs, and all incidences must be preserved. So far these are just the maps in the presheaf category Joe described. The etale condition says that a transition with m incoming arcs and n outgoing arc must map to another transition with this same interface.
Yay! That's what I was hoping! This extra "etale" condition is what I hadn't considered when I discarded a similar idea.
i guess regardless of whether this category forms a topos, we know it forms a sitos :thinking:
Without that extra condition on the morphisms you get a very cute little presheaf topos of Petri nets, but it's not useful in applications.
So, I said goodbye to it and moved on.
Your category sounds a lot more reasonable.
Petri nets are a bit complicated to consider. Let's first consider graphs. Actually let's just consider trees. Then etale maps send nodes with n inputs to nodes with n inputs. From the viewpoint of operads you would not think of other maps. For trees, the pullback condition actually forces etale maps to be injections (because trees are connected and simply connected) -- see my tree paper https://arxiv.org/abs/0807.2874, which was the first restaurant in the chain. For graphs it is essential to allow etale maps that are not injective, because if you cut an edge which is not a bridge, then the corresponding cover duplicates that edge. For Petri nets it is even more essential to consider etale maps, because you would like to run around in the net for a long time. In all three cases, the correct notion is just the pullback condition! And after that, all arguments are with pullbacks :-)
Joachim Kock said:
That's fine, but in this thread I should probably point out that the Morse functions in my paper are not the discrete Morse functions from the theory of simplicial complexes! I have an explicit warning in my paper. Maybe it is silly of me to call them Morse functions, it's just that I rely on intuition from cobordism categories.
Yes, sorry, I didn't want to be confusing :D I looked at the corresponding section of your paper only after replying. It seems fine to call it a Morse function, in any case.
Ah wow. I am very impressed by this paper :)
John Baez said:
Without that extra condition on the morphisms you get a very cute little presheaf topos of Petri nets, but it's not useful in applications.
So, I said goodbye to it and moved on.
The full presheaf category is curious. In the case of trees (where the shape is A <- M -> N -> A), I never found any use of the general presheaf maps. But just this Spring, David Myers and David Spivak discovered that the general presheaf maps are the natural transformations of Dirichlet functors! (And that Dirichlet functors are the contravariant polynomial functors.) I find it amazing!
(For the SITOS diagrams, I used the general maps in the case of graphs. They are not directly useful for props or properads, but they turned out to be useful for technical purposes, to describe an adjunction with closed graphs, and to deal with paths and convexity of graphs.)
What are Dirchlet functors and contravariant polynomial functors?
Mike Shulman said:
What are Dirchlet functors and contravariant polynomial functors?
Briefly, where a polynomial functor is a sum of representable functors, a Dirichlet functor is a sum of corepresentable functors.
See Myers-Spivak: Dirichlet Functors are Contravariant Polynomial Functors
http://arxiv.org/abs/2004.04183
Oh, I see - they really are like categorified Dirichlet series, sorta kinda.
John Baez said:
Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all
[snip]
I think I am fine with the idea that in some situations the natural questions to ask concern the number of tokens instead of the set of tokens.
Another example found in some places is that of some school boys, collecting money for a present to their math(?) teacher. Each boy contributes 1 pound, but when buying the present not all the money is spent. Does it then make sense to ask whose pounds were spent?
But I am still struggling with the philosophy part. Is it never useful to consider the groupoid of states instead of only it isomorphism class, even if you are only interested in number?
I am not trying to impose the individual-token philosophy on anyone. I would just like to understand why my groupoid intuition does not work in this case. Instinctively, when I see a natural number, I think it should be a set, and when I see a natural-number linear combination I think it should be a span. I learned this from reading the Baez-Dolans.
If you set 10 hydrogens loose on 5 oxigens, are you never interested in how they pair up? I understand that the answer is 'no' from a macroscopic viewpoint. But is it never useful to think about some sum of histories, or at least care about whether the two hydrogen atoms from the same molecule remain together when they become a water molecule?
From what I read here, the answer is no: it is not relevant.
Maybe I am just being silly or naive, thinking that I can transfer intuition from concurrency to something as different as chemical reactions, where there are billions of tokens. Maybe it is never relevant to consider a single firing of a transition, or care about which events depend causally on which others. Could it be that the very idea of process -- in the Goltz-Reisig sense I consider in my paper -- is irrelevant in this context?
I hope it does not sound like I am stubborn. Only slow.
I am not sure how this connects to the mathematical discussion, but sometimes people do care about which oxygen atoms go where. It comes up if you use isotopes to study biochemistry. Then you need to know whether the O2 that plants give off is the O from the CO2 they breathe or from the H2O they drink. (I think it's from the H2O, but don't quote me.) I think it's mostly the carbon atoms that are important to keep track of. The group that includes Jakob Andersen study this kind of thing with their computational models.
I think that if you care about which molecule matches up with the other, you are taking a single token philosophy. You still have processes in chemistry it’s just not distinguishable to say which molecules went where, if you could, then it wouldn’t be mass action. It would be a different model of chemical theory.
I think the atomic isotopes issue is best thought of as different species for the different isotopes
In biochemistry you have this spatial structure too so you can think of cells as machines for enforcing the violation of mass action assumptions. They have a lot of complex processes going on to ensure that things don’t become uniformly distributed.
John Baez said:
Fabrizio Genovese said:
This also highlights very well why the collective token philosophy does not work well in many compsci applications. There your places do not have type unit, and being tokens terms of that type you need to distinguish between tokens in an execution.
What's a "type unit"? I don't understand the last sentence here, in part because of that and in part because the chunk after "and" isn't grammatical (as far as I can tell). But I think I understand the basic idea in a vague way, and I'd like to understand it the way you do.
What I mean is that places do not have type unit
. unit
is the type with just one term. So two terms of this type are always the same term and you can't really distinguish between them. I'd say my last sentence is grammatical tho. I parse it like this:
(and (being tokens terms of that type)) (you need to distinguish between tokens in an execution.)
The only part I am not 100% sure about is "being tokens terms of that type", which I interpret as equivalent to "given that tokens are terms of that type". I've found some sentences that were of this form in some books though, so I assumed it's a thing in English.
I think if you transpose "being" and "tokens", it becomes clear.
There your places do not have type
unit
, and, tokens being terms of that type, you need to distinguish between tokens in an execution.
Yes, that's probably the confusing part. Transposing "tokens" and "being" like that sounds way more natural in English, but feels very unnatural in my first language, so probably that's the source of confusion :slight_smile:
Yes, "being tokens of that type" isn't grammatical in English unless it's part of something like "the aforementioned items being tokens of that type". That's what was throwing me.