Algebraic aspects of domain theory / breaktime conversations: FW Lawvere (& others)

0:00 Thank you. Another instance of someone that Dana spotted early. Apparently Gordon came down to the water in 1974 and Dana told me after that he'd met this chap Gordon Popkin who had some really interesting ideas and I really ought to meet him, which unfortunately I didn't do until about 1984 because I've seen plenty of him. Since then, it's a good job that Gordon's speaking today, not later in the conference, because since he arrived with no slides, he's been busy writing slides and not eating and doing various things like that. Gordon writes slides, some of the time. He's already got 25, so he doesn't need to start. Gordon is going to go up there and break out of bed. Actually, I think I spotted Dana before he spotted me. I think probably about, although we met since before, I came across his work probably since he's hard to remember. I had a friend who was giving lectures in Oxford and I had a secret agent, Robert Bowen, who went to Oxford and sent me up to the studio and I was quite excited. I remember thinking, oh, I can do this last part too now, to the language. I never did this last part. But I remember that, kind of, through a little, like, insight. And these are good emotions one gets from time to time. And they stay with you. I certainly did a lot of work in the main theory after that. And as Edith Piaf used to say, quite afraid, I'm very happy to have done this work. And it's been very good for me. And one learns a lot. So, thanks, Dana. So, having said the positive stuff, one can expect the negative stuff. Uh-oh. I don't think there's any negative stuff here. So, this is sort of things that happen. So, domains, I suppose, probably like any bit of good mathematics, are a very rich subject. There's a bunch of aspects which kind of interact in interesting ways, and there's a lot of aspects of domains, mathematical things, well, for me, my intuition, I tend to think the order is one of the things like x, y, so there's order of theory, other people might take topology as primitive, in which case the order could be a derived concept, a specialization order, then there's what before was handling recursion,

2:30 I'll come back to the blue stuff later, if you can order. When you look at actual definitions on the scope, it means you have all kinds of more intimate axioms about them, like conditional upper bounds, or maybe you do representation theory, you worry about modularity, so you have that whole way of thinking. There's all the lattice theory, and of course they're what they're for, so you have to have a theory of computability, because otherwise you're talking rubbish. Topology as well as aspects of domains. I'm always kind of focusing I think here on what's good for a domain. Of course, all these arrows, two-way arrows, two-way arrows and domains have been good for those subjects to be used as well. For example, we heard some people have had domains that were good for topology yesterday. A universal algebra comes up with domains and in fact I'll say nothing about that in some sense because that's what the whole of my talk is about. Category theory is really good at all kinds of ways for organizing domains. For example, I think category theory, personally, first, is a useful device for organizing and understanding the solution of domain equations. That was from an early paper of Daniels, colored yellow, I think, with the marks there. Daniel tried to build a mirror, so that's a reason. Followed by other kind of forays into the sea. A bunch of reasons, but again, I'm really thinking of it now as a kind of way to putability in a nice way, following Martin's, the whole process of mathematics to mean theory, no, I don't mean mathematics. Then, when you're doing, when you're applying equations to other things, depending on how other things come up, so thinking of probabilistic computation, certainly you get interactions with measure theory.

5:00 Once you've done all that, you should actually try to... So we can talk about type theory, logic, and programming languages, but again that's more applications and more we want to focus actually on the mathematics that's going on here. And what I wanted to pick out was just the algebraic, because as you can see from the blue comments, algebra enters into at least three ways. So the first thing was something I did quite early on, which was Dana had his, actually the very first thing he had before anything else that most people know is the idea of Scud domains. And they were good because they had all the subtle, less theoretic axioms, dealt with the theory of computability, dealt with inverse limits and everything. I wanted to ask myself the question, what's the kind of minimum thing, what's the minimum thing you need to know about domains in order to do the main, get the main results, name of the main type of constructors and to solve recursive domain equations. So the answer is CPO's Pleiade bottom. I need order. I need some kind of soups. And the minimum kind of soups you need is omega soups of increasing chains. That's a nice fixed minimum thing. But if you're a topologist, you like to have a little bit more. You like to have soups of all directed sets. But actually they're useless. You only ever use the chains. But, unless you're doing topology. It depends what you're writing. Useless. It's kind of an uneasy relationship. I kind of always want to bring that out. I don't know if it's a contradiction, but there's something uneasy going on. I don't know quite what my mind is on properly there. In some sense it doesn't matter. It's kind of a joke because whatever your framework is, one thing is that the domains that come out are very special. And all these different notions just collapse into one. So you can't actually see any difference. So it's almost like religious. A useless discussion about useless things, but in some sense, this bounded thing, this bounded soup has somehow an alter-wave idea in a way that arbitrary soups does not, and I will come across why, just in terms of properties and things like that. The next experience I had was, I don't know, an interesting one, when I did work in power domains, so power domains and stock domains are real good, because you don't get stock domains, well, stock domains I thought at the time were real good. Obviously one of them is not good.

7:30 We came across something called strongly bifinite domains and had a notion of power domain there. It was quite a complex representation, thinking of Gaddi as a power domain and a domain D, which is going to be a bifinite object. It's a collection of subsets of some kind, a particular kind we had mentioned briefly by Martinus. It's going to be Lawson compact, with another axiom as well, which is kind of a strange axiom. And that was a fine experience, and then later on working with Maskewicz... I found that in some sense all of that work was completely unnecessary. What's our car remains for? Well, if we're doing non-determinism, why do we care about doing non-determinism if we care about binary choice, just to do A or B? What are the properties of binary choice? There are semi-elastices. So all we need is a way of constructing semi-elastices, free semi-elastices, and that's all that you use in semantics. You actually don't need to know anything about what it actually looks like, but of course you want to. So in some sense the logical way of doing it would be to talk about all of this and then to do representation theory in the case where SFP, the three semilattices look like such and such. That would be nice. The next example is kind of worse. It's better and worse. So probabilistic power domains, they have a nice theoretical characterisation. You basically want to say that the probabilistic power of the domain is the collection of measures ordered somehow, but you're not really doing including algebra, you're doing lattice theories, you're doing replace measures by combinations, including continuity, and I give you a nice definition which applies in the category of DCPOs, Directed Complete Cartoon Orders. The corresponding subclass, in this case the only continuous ones, they're the algebras for a certain kind of algebraic theory, and I'll show you what it is later. The only problem is that the definition works for all CPOs, both definitions work for all CPOs, and they probably don't go inside. So it's a question of which you prefer, and again it's a religious question because they all do consent wherever they actually get used. So one can take the topological and measurement theory as a quote from one hand or an algebraic approach from the other. And what I want to look at here is just to see what the algebraic approach is and what does that mean in these various cases.

10:00 The technology will always... So there's kind of two reasons why there might be some interest in my talk. One is just seeing what these various algebraic phenomena are, and the other will be seeing how to deal with them. Well, the technology of how to deal with algebra is long-er theories. That's kind of clear. Though here I want to do them in a domain-theoretic setting, so it's going to have to be enriched log-error theories. That's fine. But what I wanted to do was kind of connect that up with how these guys are presented sort of naively. Scott didn't say it's a log-error theory of a certain kind, he just said here's some axioms. And they certainly don't look like equational axioms. So the question is, what's the equation of logic for a process? What's the equation of logic for all of the CPOs? Do we have a uniform answer to that question? The answer is, well, we have a uniform answer for what a lot of your theories are of that kind, and from that we can extract what the equation of theory ought to be in each case. And as you'll see, there are some surprises. There's obvious things that you think it should be, and it isn't. So that insofar as there are any surprises in this talk. That's what there is, it's not much of a surprise. So, let me just go through, probably not as briefly as I would like, the equation of logic of logarithms. This is not, I'm not assuming you don't know this. The only point of doing this is I want to establish a particular kind of notation which is going to be convenient, in which I can vary. So first of all I'll establish it in a familiar setting and then I'll vary it. With variation then it would be so painful. So, we start off with the signature. It's a set of sigma constant symbols, every constant symbol is an arity, we have the variables, I deliberately want the variables to be a countable set and this is an enumeration of all of them, v1, v2, v3, this makes life a bit easier at some point, we have the terms, They are formed in the obvious way. We have context. One doesn't usually have to follow a context in a single sort of equation, but I wanted a simple one that I can elaborate on later. Contexts are just sequences of variables with equations. Normally you would just say an equation is t equals u. I want to quantify with the context. For all the values of the x's, t equals u. And then we axiomatize the notion of t being provable from the t equals u being provable given an axiomatic system.

12:30 And the rules are obvious rules, I'll just repeat a couple of them here, actually I managed to get one in the wrong, anyway the first one says to improve the ti equals the ui is to improve f of the t so that f of the u is, another rule could be that if t equals u is an equation, and for every variable in delta I have a gamma term that has to be given by, that's what I was thinking about from delta to gamma, I just need to think of it as a substitution, which for every delta variable gives me a gamma term. Okay, we're by gamma term and the term is all available inside gamma, then I can prove that t-sigma equals u-sigma. If you look at that gamma trans-tel delta-sigma, it makes no sense, but the point is it will make, the correspondence will make sense. We're talking about that pattern coming in different ways. You might think to yourselves, why might that make sense? Internal thought. Anyway, so you get the theory. You can make up a lot of your theory. So the logic of the theory corresponding to that data. Objects are natural numbers. Anamorphism from end to end is an integral of terms. Actually not quite, because you have to take the equivalence class of terms one over the equation of theory. That's what the little brackets mean. And the variables from t1 to tn are precisely d1 to dn, as far as we can have that in relation to the tedious translation between variables and natural numbers. You could just say the variables equals natural numbers, but that's in some fashion. I can't bring myself to do that. It's breaking some category distinction or something. Anyway, the law of use theory is the representation between invariant and the definition of the law of use theory is in category L with finite products. As a map from N-Op to L, bijective and objects are preserved as finite products. I should say what N is. N, well it's basically the category of finite sets, the category of finite sets is too big. So you take a small equivalent, so here the objects are natural numbers and amorphous and from N to N is any function from 1 through N to 1 through N. So that's that. This is all very cute once you get to this point.

15:00 I'm trying to put up the learning factor from L to Z. These models are alphabets, so note in particular that a of n is a of 1 to the power of n. So models are determined by a single set and some stuff on it. Then one theory we proved is that models... The original theory is set to the same as an algebra which I didn't even bother to spell out anywhere and the next thing you can prove is that the category and the equation of theories, I've only not told you what the morphisms are, would be interpretations, is equivalent to the category of LaBierre theories, which is the obvious morphism of LaBierre theories. Now, to prove that, the whole thing, to prove the equivalent part of it is you have to show that for every LaBierre theory there is a corresponding equation of theories. And there's another thing I want to show you, because this will turn out to be a thing which gets elaborated, so this is very trivial, it just says if you've got any morphism from F to N along your series, for your signature sigma, for every N, you put in a symbol F, sorry, for every J from 1 through N, you put in a symbol FJ, and every function, so the arity of FJ is N, the domain of your N, and you have as many of them as are specified in the target, and that's it. And then the equations just described the category and how that's all there. So, the kind of fun way I want you to look at this slide is, suppose miraculously that you knew about Lafayette's Theories. This is hard to believe that such a person would know about Lafayette's Theories and didn't know about Equation of Logic. How could we invent Equation of Logic? Well, this is how we would do it. And maybe that won't be clear to you, but it will be clear when we see how that works and how it is. So there's a forgetful function for models of elements set to set that has a left adjoint, you get 1 out of TL, that's a planetary one that preserves filter co-limits or directed co-limits.

17:30 I've just named the t of the union of the x's and the union of the x's. The union of the t of the x's is the t of the union of the x's. And that's kind of a good enough example to think about to get an idea of what's going on. So for example, if there's a free group, the free group on any set x is the union of the free group on finite subsets of x. That's sort of the way of thinking. And then we carry on with a model-to-balance set, the same as TL for us. Theoretical theories over set is equivalent to the category of finite monads over set, and so we get the conclusion that equatorial and globular theories and finite monads are equivalent, so that's a kind of classical critique picture, which can go further. Instead of taking models as well as sets, you can take models as well as other categories, like top, so you can take topological groups. So what generalities are there? I'm sure the most generalities I don't know. But the ones I do know is that we've got the forgetful puncture from model and C to C, and in case C is locally financially presentable, that has a left adjunct. And don't worry about what locally financially presentable means, because it will come out in examples. Once you've seen some examples of autospeed, you'll like that. But one thing I could say is that it's a categorical analog of being an algebraic lattice. Algebraic and complete lattice, I'm going to say. Okay, but ... An example here would be to take power domains. As I said, that's just in theory of second lattices. STL is non-empty finite subsets. We're only the CPO. TL is the power domain I was talking about earlier in these two illustrations. For D-CPO, it's again the power domain which restricts it to bifind domains. Only points to notice are that 2 and 3 are not examples of the general thing I said.

20:00 It's further up here. Because omega-CPO is not locally presentable, whether it is locally presentable or not good enough. All of this, O, is not presented as something seriously awful. Both the monads exist. It's all B-C-P-O-s. Oh, I see. No, no, no, there's an intrinsic problem. You'll see the problem coming out. It's nothing to do with how nice they are. It's just, what would you mean? E-A-R, because that's true for the, well, I don't know, if there's an objection, I don't know what it would be for, because that's anyway a fragment of omega-C-P-O, so that's just going to the intersection. For only a CPO, it's okay by general nonsense. For DCPO, it's okay anyway by calculation, which is kind of what I'm trying to acknowledge. There should be some general nonsense there which works better. So that's the WOMI diversity discussion. I'll come back to the topos discussion at the end. But a kind of criticism of this is... There are other power domains. Actually, you'd like sometimes to say bottom is less than something, or other power domains, like the upper power domain, let's say like x or y is less than, get to the next, as you want to see in equations. So this is, this is fine as far as it goes, but it's totally, it's totally equational. I want to get beyond equations, or at least beyond equations from a set point of view. So here are some reasons to think about why you might want any equations. You might want them because of the bottom. You might want them because of the other two power domains, the upper and the lower. You might want them because you're doing Scott domains. A typical thing Scott would say is, I've got x and y, and I know that the two classes aren't quite what I might want, but I'll have conditionally complete ones.

22:30 So I'll have soups of upper bounded pairs. And later on, when stability became important, one would tell the notions of domain, and one would typically want meets of upper bounded pairs. And just a thought here, I'm literally on one of my domains where you have two orders of one, so an exercise for those of you who find this topic interesting would be to figure out what bi-equational logic is. Let's start off, so I want to do it, I mean, one could do it systematically, that's part of the lobby of theory, but let's do it non-systematically by just looking at examples and seeing what equation logic would be like for those. And then, what difficulties are we going to get? So let's think of conditional upper bounds. So x or y with the subscript z means, it means the least upper bound of x or y when x and y are bounded by z. Now how are we going to do that? With the signature, well we take an itinerary operation bounded soup z, x, y. But the trick is, if this thing is not 3, I'm going to say that to the degree that the arity is the shape that the arguments have to be in. The arity is that triangle there. And what about the axioms? We like to say typically that if x and y are less than z, then x is less than the bx of zxy. So again, there's more to the axioms. You might think the axioms are just t less than or equal to u, people have done lots of any equation of logic and that's what they always did. But from this point of view, they always made a mistake, because they didn't allow this kind of axiom, which are conditional on assertions about variables, or this kind of arity, and that's what you have to do. If you're in trouble about a term of your alphabet B, S, T, U, V, is that a well-formed term? Well, it is if you can prove that U is less than T. What does it mean to prove that U is T? Well, that means U and T must be terms. But we just have that problem. So the concepts of being a well-formed term and the concepts of being less than each other are actually recursive. You can't just, as we defined initially, have a bunch of terms. And then you have to have a mutually recursive definition.

25:00 So we have this cycle of judgments, basic judgments here being well-formed terms, and yes, some are equal. So the small problem of the easier cycle of judgments, what are the judgments of? They can't be termed any longer because we don't know what the terms are. Okay, it's like problems, but we get around that by a little technical trick. Signature has two aspects. It has a degree, that tells you the speed, and an arity, that tells you the shape. So the arity is a partial order on 1 dot blah blah blah. Then what you do is you just regard that as a signature of the old kind, the sigma d kind, and that gives you a notion of term, most of which will be wildly illegal, but we'll call these things free terms. This is a well-known trick which is used in type theory for dependent types, which is this kind of thing happening all the time. Okay, and then a context will now be a pair, now you can see why I wanted a sequence of variables and a bunch of order assertions on those variables. All of these are going to be a t less than you can do with a gamma before it, but on a gamma remember we'll have some order of circumstances on it. We've just been seeing that for all x, y, z, x is less than y, z is less than something, and something else is less than something else. So, creating a trap to unfold you. Then, for the formal system, Here's a couple of the rules that are readable. The first thing, suppose I want to prove that f of some t's is a well-formed term. Well, prove that the t's must be in the shape of the adjective. So it's easy enough to define something as given in the IOT, I substitute the t's for the corresponding numbers in the IOT, that gives me a partial order of terms, that gives me a function of order assertions that I have to prove, that's just an abbreviation for that list of order assertions, order assertions, and how about proving t sigma is less than u sigma, well I want to use,

27:30 A well-formed, I want to use an n-equation, a t is less than u given delta, but another cut here, n-equation might not be an n-equation, because to be a real n-equation, you have to be a relation between terms. But to be a relation between terms, and we're back in the cycle, you actually have to verify that it's a well-formed n-equation. Okay, so I've written a well-formed equation there, and at the bottom I've said what it is to be a well-formed equation, it's just a variation of sigma t and u, it has to be well-formed terms in the delta context. You have to prove that, and you have to prove what? Q, I totally forgot. Anyway, you do a substitution in delta sigma, and you have to prove that's a well-formed substitution. That's right, I think for delta, delta is kind of a quantifier. So the quantifier says there are some x's that have to prove that everything in a substitute can be prepared with terms, and there's some restrictions that have to prove that they satisfy the restrictions. So that's a bunch of assertions of the same kind of truth. So there's some abbreviations there, but all that's actually being done in the way of judgements is well-proven terms and less than or equal to. Okay, so this is a very involved system. Everything depends on itself. You don't even know what an axiom system is, it's just a set of things, some of which might be valid. But here's one theorem about this system which at least makes one feel a bit happier. Suppose I can actually prove some judgment j in this axiom system. Well, then it turns out that that's true if and only if there's a sequence of axioms i1 through im. So if I take ik, then I can prove ik is a well-formed axiom in terms of the previous ones, and then I can prove the judgment relative to all the i's. So, this is really, it's natural, but I hope you'll agree with me, it's not entirely simple, so this is why it's nice, what you might, if you didn't know anything about, oh no, I should say it a bit more, sorry, it's a bit more of a non-simplistic one, I'll probably rush over this, but we should say what sigma algebras are. It turns out, well they're very easy enough, for each function of a sigma varied to a, the monotone map is the right kind, q to the a to the q, the number of q to the a is the set of all monotone functions made to q, it must be a monotone function, so everything must be monotone, or in the jargon it must be cos-enriched. But, you can't actually interpret terms, because most terms you try to interpret will break, because

30:00 The conditions will be well formed. You can't interpret key terms, you might think, because it'll break. At some point you won't satisfy the conditions, but you can't interpret well-formed terms either without knowing that you're modeling the action system. You can't know you're modeling the action system. So there's another horrible loop here, so the only way I've figured out to break it, I've got a feeling there must be something fit here anyway, is that you just go ahead and you do interpret key terms, and if it breaks, it's tough, it's broken, okay? This interpretation is just powerful. And then once you've done that, then you say that A makes the axioms untrue. If the axiom is true, in other words, whenever you put in values from the carrier A, then such that the previous is satisfied, then the interpretation of T and U do not break down. Two points you get, one is less than the other. Even less true. Any idea where the hell you were going, you might have given up at this point. It's such a complicated system, how do you know it's the right one? It's just a system that fits with some examples. So that's why I love your theories as a group, because they're a clear pattern piece of mathematics that we're trying to prove things equivalent to. So what are we going to do now? So this is a brief overview of some things. So we have to talk about finite three objects in a category. Well, I'll just say they're just like the finite objects in a domain. An object A is less than some object X, we use the morphism F. It's actually already less than some place, a lot of morphism there, essentially unique. A is finite, you're not going to use it. So in post-ed, I say it's finite because that's a fancier notion of arity, which we've already seen coming up.

32:30 And the general notion is you just, not be refused to find in terms, there's only actually power in which case that's what we want, the analog of power. So power is, A power is, A power of an object Y is... Some things such as that, isomorphism holds naturally in X and the A-co-tensor of an object Y in the same at-boss category is an object Y to the A such as that, isomorphism holds, but it's not going to be an enriched isomorphism. So it's just what they were before except that I think monotony now has to be. So we'll put these ingredients together to make our enriched theories. It's actually sort of supposed to be the category of all final post-sets, but that's too big, so you just take the skeleton of it. So the skeleton I'm going to take is that the objects are the post-sets whose carrier is 1 to n, or something like that. So that's what a post-set is. And then you just take the appropriate analog L, it has to have a co-tensor relative to the post-set, and that function has to be bijective knowledge, because you have co-tensors. Here's the construction of the Longmuir theory from the equation of theory. You have a bunch of terms. T is amorphism. If you can see on the right-hand side, you can prove all the TIs are well-formed terms in the context which says about the variables that the shape of the arguments is the P-N shape. Success. The T's are in the shape of the Q.

35:00 And then, to make this thing in order and structured, a tuple of t is less than a tuple of u, so that's a good point. So it's a thing that you would expect to do. What's to see? Nothing much to say after that, except that everything chugs along perfectly medley. Things come out as they should. In other words, we did the right thing in this particular formulation of theory. This is meant to be an algebra. Algebras are just as before except now they've been preserved with the co-tensors. That gives you the models and you get that the axi-algebras are isomorphic equivalent to the models. I haven't checked this out in detail yet. I'm a little bit scared about it. Everything else comes to mind. And the theories are equivalent to the Lovier plus theories. And you can do your monads again. It turns out TL is actually infinitely possible. All that means is an exponent on the morphisms here, and that's the equivalence of algebras and monads. So you have that equivalence that we had before for cos, equational logic, Lockyer theories, and Monads. They're all equivalent, so that gives you the right form of inequational logic. So that's good. So the general philosophy really would be to work backwards. If this works for any locally found exemptible V, it's only a question of finding the equation of logic and I might put up a little slide showing how, if we thought about this in the first place, how would we have discovered an equation of logic? Well, we would have just followed out that question, you see. Now, what's the Morphism of the Laverne plus T? F is going to be a Morphism from Trump. Finite poset P, the M doesn't matter, the finite poset Q, now how are we going to say that in terms of operations, well for each element in Q we're going to have an operation F, it should be FI, but I don't even know what the M there is, A, but the arity is going to have to be PN, and there's no way to make the arity simple, so we'd have to have some signature which would allow the arity of that shape, now having that is just going to tell you

37:30 The elements in Q is not going to tell you the relationship, so we're going to need some judgment unless you talk about that, so we'd have to do less than or equal to. We are going to need to do less than or equal to as if we were to come straight out of it at once. And of course we still haven't done the work, but it's here where we should have gone. What else do I want to say? Again, you get this fluidicity for any category there, C, N, E, L, F, E, category, meaning post-category that is, appropriate in registration. And again, only the CPO ain't one, but it's one in the next rank up. DCPO ain't one at any rank, and I actually don't know whether it's okay here. I presume it is, I just haven't slaved through the detailed copies to find out. I don't really like to either, but I really would like to know some mathematics here. One knows more things. I guess I'll come back to that itself. But not automatically those things about the category of algebras, but I'll come back to that when I've got examples of what I was talking about. One could do things here if one wanted. One could take, for example, whatever your favourite notion of power domain is, you could take it in the Scott domain. Because the Scott domain is a category of algebras, and I could put it in for the C there. I could put general principles in it and that's okay. So that's an idea that Dana suggested to me once, but this would be a sort of systematic way of looking at it. I wanted to investigate such things. So in fact, there is indeed a power domain factor over Scott domains. Contrary to what we all thought, but what we don't know is whether there's any. So let's anyway go back to Omega CPO. I said to you that was algebraic, but I said it and I didn't prove it. But, so what kind of algebra would it be? So Omega CPO has a single infinitory operator, oh, yeah, I know that story. It's got a single infinitory operator, SU, which is increasing sequence of elements in the algebra. Now suppose I want to axiomatize that. So this is now meant to be... and axiomatization in the cos sense. So equals is just an abbreviation for less than or equal and greater than or equal.

40:00 Then it turns out... So now I'm saying he's got it in. So anyway, they have these laws. And there's now two statements, it turns out these two equations actually ties the notion of being of this kind of infinity law. Namely the infinity law of a constant is a constant and the infinity law of x not blah blah blah is the same as the infinity law of x1 blah blah blah. Yes, so how are we going to do this in Fin3 stuff? Well, we'll have to go to the countable from Fin3. Well, what does countable mean? Well, Fin3, for example, would mean something to do with directed things. That's where two things come together. But he just made the analogous thing with all things coming together. So then it turns out the countably presentable process or the countably infinite one. Very easy to see that one. And I'm not going to spell it out, but there's a fair bit of evidence that we fit it to be an inequality of logic, just like what we had before, except the n could be infinite. It's the models of this theory in post-set, so by their own principles, it's locally-accountably, yeah, locally-accountably automatically, so it's automatically all. I'll come back to this I-O-E thing in a second. Now, this is the imperative that there's nothing missing here. There's nothing missing. Where? From the theory. You just have two axes. Okay? It's kind of cute. You'd have to run it right around that thing, right? So, we have a monad. Now, if the monad is commutated, we know that our category of algebras will be closed. And it turns out it is, and that just corresponds to the following fact about soups, that they'll have a doubly increasing sequence of x's than commutated soups in other words.

42:30 But I would also like to know a bit more, you know, I actually do know, of course. So I'd like actually the tensors to be the products in order to like be the same continuity. But that just turns out to be this last thing here, and that's true too. So these are well-loved miracles, but this is why they appear systematically. So, I guess the point about what I've been saying in the last few seconds is that everyone's known everything I've said for a power, if you think you're going to get CTOs. The only point I've had to make is, not only have you known it forever, but it is trivial. It was always trivial. And these are trivialities. So, I want to come back now... Why do these things come back? What? What forces them to be these things? Oh, yes, yes, yes. I'll answer that question later if she doesn't know what the question is, she won't answer it. Okay, actually I've almost finished that one. So what else did I want to say? I want to talk about only the CPO logic. So, yeah, I was looking back to that in a while. I want to talk about the motivation. Now the motivation is what I mentioned very early, which is an alleged probabilistic computation of algebraic theory. So what do we ask in this probabilistic computation? Let me just concentrate on that one. As I said, measure theoretically we know what they are, but algebraically it turns out to be that, well, you can probably present it in various ways if you want in the presentation. The funny, the strange thing about here is that you can't separate out bottom and the rest of the algebra so you can only know that it's kind of, well, one way to do it is to pretend that this is your point of study. And you can operate with sigma lambda i for every kind of convex combination, every proper convex combination. It's convenient not to let any of the lambdas be zero. I don't know if any of the lambdas have been zero. But anyway, what you do is sigma lambda, sigma lambda mu, that's an obvious kind of collecting, actually a kind of generalization of associativity you might think of it as, sort of. You can add up in any order, that's what 3 says as a permutation of what you meant, and 4 says that it's constant, it's constant.

45:00 Now what 5 says, which is slightly gravely written, it's interesting, it says that x is the least y in which you toss a random coin and the probability of half do x and the probability of half start all over again. So that's an intuitive axiom, and that's why one needs the logic. So, that's the motivation. So, the next bit is, so what's the logic going to be? I said it earlier, I said it earlier in various things, but the simplest one of them was that omega CpO is not quite that representable. And the reason is kind of clear, if you look at this little diagram here at the top, That's the co-limits of all little finite formals. Map 1 into omega plus 1 will send infinity, but that map doesn't factor through any of the places, because infinity doesn't turn up until the end. So if 1 isn't finite, then nothing is the only thing that will be finite. Okay, now, let's see, what do we know about it? And that T is a cantable monad, cantably. So we know that Omega C is cantably presented, is locally cantably presented. We always said that you do a lecture in the sense of mathematical fun, so this is really the only mathematical content of the lecture, which was, I wanted to try to identify the locally cantable, the cantably presentable objects. Now, we know by general, by general nonsense that the locally counter-presentable objects are retracts of co-equalizers of free, what you do is you take a counter-presentable object from the release maps of, and you get an object R.

47:30 So, the question is what the hell is it? Try and sketch what they are. Then I'll stop. We have the idea here, so this will look at the main thing. Well, I didn't say what omega p is, so that's easy enough. So, p is a coset and we want to make it canonically into something with limits of omega, increasing omega chains. We just sort of shove them in. So, what we've been able to do with that would be increasing omega chains, so a, blah, blah, blah, blah, a1, a2, a3, increasing. What happens if there's some b that's less than some a? Well, we should shove that in as well. So, we really need some notion of ideal. So there are corrective ideals which are generated by chemical changes. And B-items and M-items are actually algebraic from the appropriate flavor of algebraic. Anyway, these F and G are continuous but that's the same as monotone functions on the P and underlying P. So to say that is to say that for all F and P, one of them is A of P, F A equals G A. Well what is F A and G A? Well basically it just suits. The first sup is Vm, the second sup is Cm. So that's to say that sup Vm equals sup Cm. So that's to say that Vm is less than sup Cm, and Cm is less than sup Vm. So we're going to address these kinds of infinitary conditions, that an A is less than a sup of B. And that's what we're going to correspond to. That's going to be as we're explicit. So, let's say a condition in a partial order is a pair of A, B with A's in P and B's out, increasing sequence of the P's, and we'll say that a condition, a nomadic condition in partial order is a pair of P and C, where P is a partial order that sees a set of conditions on it.

50:00 Well, anamorphism is just something that also preserves the conditions. Determines a condition in partial order when we just say all the relations between elements and soups that exist in the partial order. So U of P is just PC where C is all the ALS soups being true in P. And then it turns out that that's how we get a function from omega CPU to a condition in the omega condition process and it has a left-hat joint. How do you construct a left-hat joint? It's just like this. It's exactly the same as you constructed the previous hat joint except you have to take care of the conditions. So we'd say that a C ideal is just like before, except it has extra things in it that we've never seen, it says it should have extra things in it. Okay, then for each x the least such C ideal, and what else? For each a and p you can take the least ideal and continue it, then I only have three c's, it's just under the least collection of C ideals, continue the eight and close up with that. Yes, that's right. So that is the CPO determined by a condition CPO, and we have a condition martial order, which is a partial order, and now let's just turn that into a definition, let's just say that Q is explicitly countably presentable if it is high of such an infinitary set of conditions. Now, this whole thing has been set up in such a way as to take care of the co-equalizer. The whole technology was set up to do that. So, it's hardly surprising. This proposition has to be true or else we've just screwed up and basically we're doing mathematics. It's an absolute mistake. The r could be given by a co-evaluator diagram of that kind, if you only make it so that it can't be identical. And that's a verification. What was the theorem? Well, it doesn't get to work. All of these things are presentable, and once you've got that, that's your characterization that P is presentable, if only it's explicitly presentable. So that's kind of nice in itself to abstract, but it relates well to standard notions.

52:30 It turns out that everything at the sommelier continues when it is explicitly presentable. There's many things, but I can't be reversed as easy counterexamples. Counterexamples imply counterexamples in general, but not conversely. So that seems to be the reason for this one. It's going to get in. Equational logic. And by now we don't actually need to give an equation of logic. All we actually need is to look at the lobbyer situation and we just have to see what we need to work on. I'd like to have an answer, let's see what it would be. So we take as additives the QC's I think, the standard for the objects, and we need the less stands, but now we also have to make assertions that say the conditions meet our infinities too. So it's going to be just like, what's the result of all of that? The result is it's going to be exactly infinity of posts in equation of logic plus the use of soup as a kind of logical symbol. So that's the end of the domain theory really. I just want to mention some possible directions for future research. It might be interesting. So a long time ago, I know it's David, I should give him a birthday present. A long time ago I asked him for a birthday present. In which we have everything that one could possibly want, the best domain theoretic toy possible, which is Cartesian, Gauss, Cattery, etc. with all three, and now I'd like only a CPU algorithm and I know what to ask for and what algorithms of that kind please, and solution of domain equations, also solution of anything polymorphic like a notion of computability, and that's really all I could think of. But we know that this is just out of the window, we don't know anything of that kind to me. I mean, the standards aren't the probabilistic part, I mean, we know nothing like that, let alone computability. So the thought might be, take all of the previous mathematics and do it in a topos. What would that be? Because it cannot be done. I don't know enough to know. And then do it in the exact topos. In terms of the equation of logic, a fun thing to do is to look at various equation of logics. For example, the equation of logic for cats might be interesting. And it's easy enough, I think I may have got a lot shown now, but it's easy enough to see what the judgement should be just looking at the fundamental presentable categories.

55:00 And John would like to do, who actually has been teaching me about this subject for a very few years, would like to very abstractly explain what an equation of logic for a general V might be. How far can you get? So, yeah, well, last slide is the last slide. Okay, see you then. The result of our retracts just adds more relations to your presentation? No, it adds more elements too. It turns out that you're making conditions between things which themselves are directed soups of things. Actually, no, no. Between things which are, you have to take an allothenol branching tree. The way to describe these objects is infinite soups of infinite soups of infinite soups. That's an allothenol branching tree well around a tree with infinite soups of each thing. So you have to describe those things as well and then talk about conditions between them. The difference is 40. There is an equation of logic going back to Leibniz, which over an arbitrary base category perfectly corresponds to monads. Nobody tried to make some deductive system on it, but it would be interesting. Everything is an object of the base category. Or just, yeah, just no notion of size at all. Without any notion, without any restrictions of size. Well, that could be an edit of whether it's finite or not. But Witten did not.

57:30 Sorry, I'm just disappearing myself. Thank you very much for your time and we'll be in touch about the project for next year. Thanks very much.

1:00:00 Thank you very much, I didn't mean to talk much else, you've got a bit more time.

1:02:30 Assuming that they exist. Is that your recollection about that? Well, I know where I have wrote about that. I think it may even be in one of these Warhol's volumes. Because it's in order to prove a statement of Lee's, namely that under such and such circumstances this is a function of x alone. All the invariant functions are actually functions on this quotient space. Well, that's not the way he expresses it, but it's a function of... It only depends on... I don't remember Lee's formulation, because that's not up to our standards. So one way of making it into our standards is to assume that you have a quotient, For a vector field, say, it has a function. There are arbitrary values, but it's a constant, which is constant on the orbit, invariant on the action. So, therefore, quotient is evidently a universal principle. Well, in other words, you know, an abstract notion could have... I mean, I know definitely a point where we use the productivity. That's the paper with Gonzalo in the Durham proceedings.

1:05:00 But that's a different kind of potion. Is it just gluing open sets or is it actually a quotient bound by group action for proving that projective space is... So, I know it's in... that aspect of it is in the Dora mode. Dumb people would be concerned with conformal manifolds. I think it's just conformal manifolds. I would just remind you that I've done a lot of past discussions on monads and the rules. Monads might have various kinds of categories of heritages of support, and there was a particular I was wondering whether the answer to the saying was the same. I suppose that in other subjects it seems that if you have a monad, it's very much considered a generality, but supported on projected heritages. Then the underlying function of the algorithm is to preserve ethics or something like that, which wouldn't be truly general. No, no, exactly. Maybe we don't preserve all columns if it's an atom, if it's supported by an atom or something. Yes, it's an important class. Project is not enough for preserving columns. How about the same thing? Yeah, yeah. Oh, good. I don't quite remember what is in the recent paper with Gonzalo where we explicitly worked with atoms in connection with different equations to prove that there is a further edge on the thought that the forgetful countries' research limits are poor.

1:07:30 Thank you for watching. Actually, the money, I think the money is coming from you. No, I didn't hear you. I wasn't listening to you. Actually, only half of you, only half of you. We're going to have more choices to see what we're going to do. Last week, I just woke up and I thought, you know, I just woke up and I thought, you know, of course, I said to myself, that's quite embarrassing. Of course, I'm talking about the beer and the beer and the beer and the beer and the beer and the beer and the beer. From what Anders was saying, there's actually quite a lot of geometrical stuff in these objects. Thank you very much. Thank you for your attention. What you call SUD, a separate work on ramified design of objects, the use of it as a tool of analysis. This should be one. That's true. With one hand. Which you touched on explicitly. Yeah. It sounds like a good idea. It's all around. You're having even more money. Does he have any money? I don't think so. I mean, certainly what you're saying about the extreme richness of the subject, the number of angles, the approach of the subject, because it's about two years, but even there you're here for four hours. Before, I didn't get very much about it. I don't mind it, you know, about how, what a terrible thing it was. I think it was that since we had no free agents, it was more about how you actually... Yeah, I've been there for three years.

1:10:00 Actually, I thought we wanted to come to that, but since we've got one hour left, I'm not going to do that. It's also not a very high-speed lecture, which is not necessarily a good idea, because it's not a very high-speed lecture. It's really not so high-speed. I was going to come to that, but I actually went off to the train station, so I'm going to stay around. I just thought that looked just as the ones in yellow. It always turned out that the heads of the main ones were the ones in yellow. Which one is true? I mean, the main thing is true. And that's what you were saying. Thank you for your attention. We have to decide on a name for this meeting, for this workshop. Oh my god. Excellent. And I can't really call it that. If I were you, it would be a lovely week. Certainly. I don't think you'd be very... Would you dare? No, no, I wouldn't dare. Don't worry. I wouldn't use the word how they are named in such circumstances, don't worry, but they're being serious. The University of France actually said that before they could formally give us a grant and start printing programs, we do actually have to choose a title, so I thought I'd consumpt you on that, and I'll then impose our name. So any suggestions for the time you'll receive?

1:12:30 It's very good to see you again. I'm sorry to have you much too short. We're going to come for this thing that we're cooking up for the bill next year. I'm sure we'll see you on another one. In Firenze. In Firenze, yes. We think probably in November. He was just asking about the appropriate title. Yes, we've been asked to give a title in order to give a grant. Some of the ideas that we like are philosophical or counter-theory, yes, but that isn't something that's hard to like in the provision. I think that's one of the things that makes it a bit punchier than that. Punchier, yeah. Philosophical ramifications of category theory is fine. It's fine by me. Yes, I think it is. Well, I imagine you were a teacher, weren't you? Yeah, yes, I was. Well, I'm a pilot for the Ferdinand Morosky Institute. I was at their meeting on the development of the mathematics of mathematical physics in the 1950s and 1940s. That was quite interesting. Where were the wrong turnings taken? Particularly, I'd like to talk to you about that. I said that Hilbert space was solved, that the functional aspects were solved in Hilbert space, didn't they? I'm trying to persuade them that that was the structure of the dynamics as well as the mechanics, which of course was solved in Hilbert space. I just feel that when you open this ennoyment book, it comes with a piece of information that you can investigate with a question. Well, there's a meeting on this subject in the district mathematics meeting. There's quite a few people who might have something useful to say. I would never say we did it, though. Yeah, yeah, sure, yeah. In fact, it's a good setting of conceptual flying. They all fell down in awe in front of this supreme thing. Did he already have that reputation? By 1930, I think so.

1:15:00 After he moved to the States, we had this talk about the linear ranking of mathematicians. He was the greatest, you see. Nobody else was contention for a second. They used to talk about it. I'm afraid some of us do. I'm really rather busy when you come because Eduardo Dubuc is visiting. Who is he? That's the one thing I like to say. Did he say that? No, he didn't. I don't really know it. He worked out or dug into historical sources about some very specific issues. Well, if I find out anything about, you know, how human space was so tied to the physicists, or the other interesting things about the wrong trainings that were taken in the mass, the creation of the mass that was, as it were, taken on by the mathematics. In the States, there were three or four great mathematicians whose main interest was really quantum mechanics. But they all disagreed among one another, and we talked to some of them. What about what Marshall Stone said? Mackey was one, George Mackey, and then Irving Evers Siegel.

1:17:30 This is the former husband of Hosea. Yeah, Hosea McLean. What is Hilbert? Hilbert? Yes, David Hilbert. No, but he was four. Yeah, but I mean... But he was still alive. Yeah, and he wrote about mathematical physics, but he didn't take up Hilbert space as a tool in... I don't think Hilbert himself ever did. The same thing went on in von Neumann's lecture and von Göttingen's, as to quantum mathematics and so on. Please, what is your book? Please tell me what is your book. The only thing I know of Hilbert is the thing which Colin covers, which is very interesting. No, I don't think he was very productive after he wrote that book. I think Stone says somewhere that the whole idea, you see, that the use of the homomorphism condition on the dual, you see, the fact that you take algebras, you know, to algebras of functions, and then these have some algebraic structure, so if you again consider homomorphism to be such structures, they should come from... The original geometric maps. It's basic principle, you see. But of course the pure double dual is much too big, but the idea of the poison specifically ringing the morphisms, which has played a big role in Stone's actual work, but I think it was suggested by von Leibniz. So if it's true and phenomenal, really well as a genius or something, you know, at least, at least he had, he had the right idea, he had the right insight and suggested it to the person who really worked it out. In fact, because, because the trouble is that... Since the algebraic topologists, as we were saying yesterday, have not tended to go in the other direction, we take the ideals as the basic structure, as long as the geometry is very geometric. Yeah, yeah. Topologists as well, I think. Well, that was already then. They were usually going, you know, in trouble, you know. Yeah, very interesting. Well, I look forward to very much to seeing you again, so have a safe journey. Yes. Enjoy your camping holiday.

1:20:00 Camping holiday? Well, you know, it's an awesome city, isn't it? My daughter lives in some city and has a house. Oh, so you are actually, you know, laid back in luxury in that case. Oh, yes. Thank you for your attention. I'll say hello to the family. Thank you for your attention. It's really terrible. It's seven in the morning and I'm playing the violin. At least you're quite near the airport. And you're going to have to spend long shifts of energy. It's going to mean you're going to have to leave the airport by about 5.30 or so. On the other hand, it also means that I can get a night out. That's just what I'll do. Instead of staying here tomorrow night, I'll check out of my hotel tomorrow. I'll just stash my bags and then go home after a coffee and get up and go home and catch some trouble. Anyway, we're going to get a very good night's sleep tonight. ... in a space where they're in connection with each other, and it at the same time connects up two mathematics with algebra and topology and geometry.

1:22:30 And at the same time, because of the rich mathematical structure associated with the main theory, it's had a hand in inspiring programming languages and type disciplines and reasoning. However, today, computation is becoming increasingly distributed, and I think one can say that we lack that global mathematical guidance that domain theory would give. Domain theory has not played a great part in the theories of concurrency.

1:25:00 We see a rather fragmented world. We can see a variety of models and a variety of process and to try and put some form on that world, I think that one can say that recently there's been an increasing use of causal models or independence models like country nets and event structures. In which one's concerned with computation paths which have quite a lot of structure that consists of say patterns and events related but where the relations of cause and dependency and independence between these events. And these have been used in a variety of different situations. Often they've been rediscovered in a variety of different situations and I've got a list of things there. If we look at process calculus, which is probably a very rich area with multitudes of different calculus and multitudes of different people, we see that one of the things that's certainly central these days is name generation, union generation. That started really primarily in applied calculus, but any processed calculus worth its salt has pretty much got to have name generation, at least the ability to generate fresh names. Now, the world is rather fragmented, much more fragmented than perhaps appears on this picture, and that has several consequences. One is that the relationship between different models is unclear. There's a lot of rediscovery going on. In particular, the causal models are being rediscovered now in analysis of security protocols. And then I think a lot of time is spent on optimising particular calculates, making them look good, reducing the number of rules, working with reduction rules to get the number of rules even less and so on, losing compositionality sometimes in order to do that, and it's in itself an obscure of the connections there are between these calculates.

1:27:30 Now another fact, another feature, I think, is that it's often, if you like, simulation driven, and what I mean by that, I mean that people often look for something out there in the world and they try and model it, and it's going to be a big thing, it can be a kind of domain, it can be a domain that you recognise that computation actually takes place within certain domains, maybe it goes by firewalls and so on, so you're led to a fairly big idea like the Ambien Calculus, Or it can be fairly small ideas like, well, I mean small in quotes, ideas like a particular protocol and trying to model that and tweaking your process calculus and equivalence to be able to reason about that particular protocol. But what I'd like to do is somehow wrap all of this, what would be nice is if we could wrap up this rather fragmented world into a uniform world. We had a kind of domain theory which could do things like we somehow incorporated models like event structure and so on, could somehow represent causal independence between events, could at the same time cope with name generation, and of course, as part and parcel of being a domain theory, also cope with higher order processes. And it would be nice too if we had a good operational reading of this domain theory, so we have an operational semantics associated perhaps with some meta-language that came out of the mathematical structure. So if we look, say, at traditional domain theoretic approaches to contrariancy based on power domains, power domains are going to come back again in this fiction, but as they're traditionally used, say, as domains of resumptions. One tends to model computation paths by non-deterministically choosing the next action. So if you do this, you're going to fall short of the detailed structure of independence, for example, and events that might exist in these paths. So what this suggests...

1:30:00 Of course, it's a rather loose suggestion, it's not a watertight assignment. What this suggests is that perhaps we should try to base our domain theory, our model of processes, directly on computation paths, and so that we can have a whole structure in the computation paths, and then we can put some motion and state on top of it. Of course, this is not a new idea. Way back, in trying to give the semantics of CSP, Tony Hall came up with using trace sets, sets of sequences of actions involving processes. But let's try to use that idea, ignoring for the moment objections around the branching behaviour of processes. So, some kind of notion of computation path, general in what I understand of computation paths or computation path shapes. And where the order between them can represent something like extension of one computation path. So for example, we could have computation paths which were strings, or non-empty strings over some alphabet L, and the order could be that of extension. Once we've got our notion of computation path, then we... We want to have a notion of a non-deterministic process with paths of that type, or we can say more briefly, we want to have a notion of a non-deterministic process of time, p, where p is the computation path, a characteristic function from those computation paths, so something that gives us zero if the computation path is not present in the process, and one if it is. But we want it to be the case that if we have a computation path in a process, then a sub-computation path should also be in the process.

1:32:30 And so our characteristic function should reasonably be a monotonic function of P off from the converse order until the optimistic processes are going to be promoted. We can just take given such a problem and that will be down with both. And we can assemble all of these non-deterministic processes together. We can just say down with both cells it's a computation task and they have an ordering on them, an ordering given by inclusion. And so you get a, if you like, a domain of non-deterministic processes of type P associated with all of these characteristic functions. They are thinking of it as consisting of downward closed sets ordered by inclusion. It's obvious that they have a union, and so that can be used to represent the non-deterministic sum of processes. In particular, the empty sum would give us the dead process, the empty set, which wouldn't have any capabilities at all. And more mathematically, we can see this guy, this guy here, as the free joint completion of the path P. And if we go to, if we take the instantiate P to just be the non-empty strings, then we recover four trace sets, this model that's been around since the obvious objections to this one, but let's just brush those aside for the moment. Let's think about maps between these non-deterministic processes. Based on the fact that these domains of processes are free-join conditions, it would be made to map the matrix test.

1:35:00 And finally, to look at what I call linear maps, which are the joint preserving functions between the domains. So we'll take the linear map from P to Q, where P and Q are these partial orders of path shapes, to be a joint preserving function from P to Q. And of course, that just corresponds to a monotonic function from P to the domain Q. Or alternatively, it corresponds to a kind of relation, a kind of proximal relation, I suppose, And these guys really would have got the collection. Then they form a domain. A domain over a gadget written by this. You know, I'm sure many of you know this category. I mean, it's rich in type structure. You have a tensor product with respect to which you have a function space given in these ways. In this linear category, it preserves all joints, and in particular it preserves the empty joints, so it takes the dead process to the dead process. So if we're interested in using these operations in this category of process languages, we're pretty much stuck. Because that's generally not the case, that the dead process is catastrophic when we set them in as an argument of an operation. From this category, we'll go broader with a more tolerant version of math, and we'll go to, of course, in this context, we'll be able to move to the category in which we keep the same objects with partial orders of path shapes, so we're still thinking of these representing types of non-deterministic processes by specifying more path shapes for their computations and the like, and now we move to continuous functions between the domains.

1:37:30 There's a way of understanding these in terms of linear maps, because as we all know, continuous functions from domain of P to domain of Q, they're determined by how they act on the finite elements. So these guys correspond to linear maps going from band P to Q, but band P is just the partial order of finite elements of the domain of P. Now, back in 1993, Matthew Hennessy used this category of continuous to give a denotational semantics to a higher order CCS, in the sense that it was CCS but where you were allowed to pass processes, not just values. And of course, he relied on the fact that this category is not too close. All these terms are given by a construction which would just lay the two path orders side by side in a function space, again as a path order, which can be obtained in this way. However, what Matthew Dilley did was pay very much attention to the relation between the continuous category and the linear category. And if we pay a little bit of attention, we see that we get a very fairly useful, very useful, general language for process accounting coming out of value junction. So let's use a language which we call, Lucas Louvain suggested we call Hopper.

1:40:00 We can have recursive types, old technology there, and at all types we have non-deterministic sums including a nil process, the empty sum, and we can have recursive definitions. But there's a new thing that we have too, which is something I call prefix sum. In other words, a process that produces a computation class. And that's going to be associated with two operations, one a prefix, first with the action alpha and then with u as t, and then a prefix match operation, which roughly has the property that what it does is it takes the process u of type as prefix sum, looks to see if it has the capability of doing an alpha action, Whatever it does matches the resumption that it gets after they're doing an alpha action to x and then passes that to t. And then, of course, there may be more than one or no successful matches, and then it will take the sum of all of those matches, all of those successful matches. So that's the syntax, but let me explain why this operation comes out as the assumption. So what we do is, while we're defining this prefix sum here, to be the ordinary sum of these types, just a disjoint union of these partial orders, but where we bound them first. And then from the induction we can spot that we have a natural bijection between linear maps from here to here, linear maps from the prefix sum,

1:42:30 These are all examples of continuous maps on the components, on the frequency. If we work out what that's really telling us, it's telling us that we have this prefix sum operation. It's not quite a coproduct, but it's very nearly a coproduct. It's a coproduct in where we have the mediating morphism here is actually within, Also, from the uncertainty in Q to the prefix sum and look at where the identity goes to, that will provide us with a couple of maps going from the components into the prefix sum. And these will just be the prefix operations. Concretely, what they'll do is they'll take an element of the domain of p beta and give you the set. All things in banky beta that that x dominates, and that would be of course an element of this domain here. So this suggests that we put a construction like this in our language, but I'm not going to do that because you can boil it down to a more simple construction which you obtain by making a particular choice for the f betas. Given by the denotation of a term with a resumption variable in it, and where we take every other component, every other f alpha, where alpha is not equal to beta, we just take it to be the trivial map, which is going always to the empty process, to the empty element of the domain key. Then we'll take this guy here to mean, to just denote, the same as the composition of this mediating map that we get for this particular choice.

1:45:00 So the application of this mediating map to the denotation. Because of where we built this up, we see that because of this triangle commuting when beta, and so on, with the resumption put in for x. And in the other cases, where we made a trivial choice for the f-alpha, we again, because of the commutative triangle, will know that if we try and match something that can do an alpha not equal to beta, against beta, based on the beta pattern. And then, because this mediating map was linear, it has to be linear because we notice that sums in this position pull outside. They distribute through the matching. So we get these little algebraic problems. Of course, when I write this, I really mean the denotation of the thing on the left equals the denotation of the thing on the right. Is a linear category a subcategory? Yes, it's a subcategory, with the bang thing being there. So, well, let's give semantics to traditional person's counting. We don't have a name generation.

1:47:30 You see, we can give a, we can express CCS directly in this language popular. We can take the prefix sum, we can just define the type of CCS to be p, where p equals the prefix sum at this time, where the atomic actions are those of CCS, tau and a's and complements. And then, there's no problem with most of the operations, they're just very direct translations, but for parallel composition we can make use of prefix match. So the S parallel T, what do we do? Well, we look and see what capability S has, and if S has a capability, like alpha, do an alpha reaction, and then go to the resumption X, then the parallel composition has that same capability, and go to the parallel composition of X with what's with this right hand side T. And similarly, if T had a capability, the parallel composition would share that same capability. So this would correspond to just once one or the other side proceeding asynchronously, independent of the other side. But we can also synchronize, and we can do that by looking to see whether or not S and T have got complementary capabilities. And if they have, they can synchronize through use of tau action and resume as the parallel composition of the resumptions of the two components. So, in this way, there are really, there are four expressions really written here, but I've only written the two of them by symmetry. In this way, we can express parallel composition in CCS, parallel composition of CCS and Hofmann. And without very much extra work, we can express all of the CCS. Of course, there's a little bit of sugaring going on in what I've told you. Really, we'd have to write, we'd have to write a type like this, and our parallel composition would be given by recursive definition in the language itself. Simple observation, something that's like a co-product of where the mediating map is linear, we can derive Riemann's expansion law from the prefix sum laws. So if we have the S and T given in terms of sums, non-deterministic sums, prefixed processes like this, what will happen is when we plug those in into the definition,

1:50:00 These definitions here, because of the rules over there, will filter out just the appropriate components in order to give us something that is really just Milner's expansion law. So we derive Milner's expansion law from the previous sum laws. In this semantics, which is a trace semantics, we've got many more identifications as well. In this way, and it will involve outputting, so we're now thinking of a higher order CCS, so we're now allowed to accept, accept processes, send processes, and then resume with other processes, with concretions given by just products, we have pairs of processes. And then just in the same way, we can define a parallel composition recursively. Now, of course, it's more complicated because processes can go to concretions or abstractions and so on. So we're involved with a much more complicated, we're involved with simultaneously defining parallel composition, not between processes and processes, but also between abstractions and concretions and so on. But it's still the same idea that we saw for CCS. You just write the Parallel Composition in this kind of way. This is the component associated with S doing its thing on its own and the Parallel Composition then able to just do that action. This is where S and T do complementary actions, so you get a synchronization in which a process is passed to the S side, from the T side.

1:52:30 It's much more cheaply to go to the extent of looking at the category of all continuous functions between these domains. That's because by the nature of things, often maps in distributing computation have an affine linear character. It's a finite configuration, it's a finite element of the domain of P. So it consists of several possibly known computation paths. And you can think of that, if you like, as a kind of compound computation path associated with lots of copies, with several copies of processes. Now, in distributed computation, it's generally easy to discard or ignore other processes. But it's often hard to copy. Because you have no control over the complete sprawling distributed system. So many operations of distributive computation have the property that they depend on their argument in the sense that they depend on at most one copy of their argument. They may ignore their argument, but if they call it, they generally only use it once. Us often being concerned with operations or maps which have the following property, that a computation path of the process arising from the operation applied to an input process has resulted from at most one computation path of the input process. There may have been no computation path at all, but at most one. If we take that idea seriously, we're led to small continuous maps.

1:55:00 In a way, it doesn't really matter so much, but they happen to be non-empty joint-reserving functions from here to here, but they really correspond to linear maps going from P-lift, and here I just mean take the partial order P and stick an empty path, bottom, underneath it. What is P-hat? P-hat is the domain. So I'm using P-hat to correspond to the domain of down-closed subsets of P. So we're looking at math which... So now we're looking at mathematics. So this is really a subset of math, where we're looking at either singleton copies or no copies at all. And now, I'm not going to do it, but one can, from this, start developing an affine poplar. A language like the one you see, but with certain lineality constraints scattered around. I'm not going to go into detail, but it's based on types which are A tensor and a function space with respect to that tensor, a prefix sum, which is now a modifimate in this way, and then you get a language which is an a-flat and an a-flat linear or linear language now of course with sums, recursion, prefix and prefix match. Provided you respect the linearity constraints necessary for this language, you can imitate the kinds of things I showed you could do for Hoppe. And this is one of the things that Mickey Newbolt will talk about, and it's the thing that's addressed in this little bit of paper that Mickey will talk about as well. Okay. Well, there are lots of those. What about branching-sensitive equivalencies, like biostimulation?

1:57:30 What about independence models, like event structures? What about name generation? If we're going to cope with these things, we need to move to a more informative semantics. If we're going to see these kinds of things arising in our denotational semantics, we're going to have to move to a more informative model. But we do that by using essentially the same idea that you just see. We make a kind of sideways step. The slogan is, don't use to, in your characteristic functions use sit. Partial order of computation paths which might for example be non-empty strings and then we now take a non-deterministic process of types p to now be a functor going from p of now into set rather than into two so it's a kind of generalized characteristic function instead of saying yes or no to whether a path is in there it gives you the set of computational paths of that shape and then now assemble these processes together But this time, we're not going to get a partial order domain, we're going to get a category, we're going to get a category of pre-sheets, functions going with these characteristic functions. In particular, if we think of this, the path shapes p as being the non-empty strings, then we see that the category we get, the category of pre-sheets, is isomorphic to the category of synchronization. And even the natural transformations between the maps and features, they correspond to a kind of simulation map. When it comes to, of course, the paths can be more complicated than just strings, and in particular they might be based on concepts.

2:00:00 And they're the suitable choice for a category of concepts, time-out concepts. We can get, appreciate that it will be such that it fully and faithfully embeds event structures. So we have event structures coming out as certain kinds of generalized structures. And more than that, by moving to this more detailed model, Which, as you can see, because it captures things like synchronization trees and event structures, it respects branches of it. All of that, we have that each type is associated with a kind of bisimulation which comes from open maps. I'm not going to give you a definition of that, but there is a general way of getting the notion of open map bisimulation associated with each type. So now we just replay what I did before. More informative semantics is useful. The first thing we can observe is if we replay the definition of linear map, our domains now are replaced by free sheet categories, our free joint condition is replaced by a free cononic condition. So mathematically the natural maps are the cononic preserving functions between the free sheet categories. And these, as before, these correspond to special kinds of functions going from p to free sheets over q. And these correspond again to special kinds of relations, but generalised in a generalised sense, namely pro-factors, where we now go from p cross qr. Instead of going to 2, we go to set. And you can show one of the things that kind of told us, or made us feel we were on the right track, was way back when Luko was working on this, we suddenly realised that the maps we had here were preserving open maps by simulation. In terms of modeling process calculus, the maps here are too restrictive. We don't want the dead process always taking place in the dead process.

2:02:30 So we loosen up on the kinds of maps, and we loosen up first to H5 maps. And these are going to correspond to functions from P-Lib, linear maps from P-Lib to Q-Lib. And then, it's an incidental thing, but useful, that these types are pre-sheaves of free, not just the free co-limit condition of P, they're the free connected co-limit condition of P-LIFT. For that reason, we get a lapse in these Mayfine maps, given in this way, preserve subjective, special kinds of maps, but enough to guarantee that we preserve by simulation. By simulation is built around the bounds of subjective or epimorphic. And just as the domain form of this A-fine category gave a semantics, a sort of semantics to an A-fine grid, now we have congruent results, but if you look carefully at this more informative pre-sheath semantics, there are decomposition results about pre-sheaths that guide you towards an operational semantics. And in particular, if you look at pre-sheaths over P-lift, They decompose into a sum of rooted pre-sheeps, where there's a single impromptu key idea in getting and moving towards an operational semantics.

2:05:00 So, Michael Lugo and I, a paper in Litware, discusses an operational semantics for this sum that comes out of the pre-sheep semantics. It only goes up to first form. And the reason we couldn't go further is that we have some difficulties with tensor. The reason why it's tricky is roughly the following, or more or less the following, that for a process of tensor type, a choice of action in one component of the tensor generally affects the choice of action in the other component, a kind of atomic entanglement. And this means that you can't, whereas when you're used to working with products where you can project yourself out of trouble, when you have a tensor you can't, and this has meant that at least we couldn't see how to get our operational semantics to work also for higher types. But what we did do was try to understand, try to read the feature semantics as operationally as we could. And we noticed that there was a lot of structure in the elements of the pre-shoots, in the elements of the sets we were creating. And in particular, they seemed to have the structure of configurations of an event structure. And that really was the case, at least the first of them, in that one can give an event structure to mathematics of the whole of A-fine popular, this A-fine version of this kind of orthopressor's definition. Which, of course, at high attack is going to, like a stable domain theory, is going to start diverging from the stop domain theory that I'm basing this on here. But for the first order, it's going to tell you that the elements of the pre-sheets are finite configurations. And moreover, it exposes the tensor operation, which was a bit of a mystery to us. There's nothing more than a parallel composition of event structures, a very simple parallel composition just got by taking two event structures and putting them together. I think there's a lot going on in this, all the exploiting here. And part of the reason for that is that we're using it implicitly. Prakash Nagarvan and Thomas Sullivan and I were using it implicitly many years ago when we were giving semantics to non-deterministic data.

2:07:30 And perhaps the fact that close connection with event structures is no coincidence, because many semantics, or non-deterministic, use causal structure of instance, similar in character to event structures, and look to some kind of continuous functions between these pre-sheet categories, and if we look at... All the continuance will be filtered color-representing functions between the P-sheet categories, they correspond to functions going from band P to linear maps, from band P to Q, where band P is the finite color-representation of P, and then one can go ahead, just as before, use this category, now with domain categories, with the categories of domains. And again, what we do in the Concur paper this year is base an operational semantics on that pre-sheet semantics, again relying on a decomposition result. But there is a problem here though. The open map by simulation is the one canonical by simulation we have here. But if you look at the maps in continuous they don't necessarily preserve open maps. However, there are several alternative exponentials that do. And some of these are discussed in an admittedly rather sketchy way in the... This time we can give an operational semantics for the whole language because we don't have... because we banish tensors, we don't have tensors.

2:10:00 It fits in the linear scheme while we're in the narrative so directly. I'd better say a word or two about name generation, which is, to some extent, orthogonal to what I've done here. I've found ground with a bit more recent work, but there has been some work on name generation in domains. Of course, there's the work of Ian Stark and there's the work of Marcelo Lourdes. But if we look at the kinds of models we've presented here, which are based on either to or set, Then, way back in 1996, inspired by Ian Stark's work, Matthew Hennessy gave a trace model of the time calculus, but it was a trace in terms of a function category now, going from these domains with the continuous maps that you've seen, going to that from a category which consists of finite name sets, finite sets of names with injections. The idea being that in this way one could represent the fact that names are dynamic degenerates and he gave up a fully abstract model with respect to an operational semantics where he was interested in observation just of the trace time, what kind of sequences of executions you could get but I think more important than that is that I believe but this needs to be pinned down better The denotational semantics suggests a meta-language which somehow subsumes the existing process calculus, and is based on new name abstractions of the kind that Ian Stark was the first to stress, and a kind of dynamic form of the prefix sum that you see. I'm going to do a recursion of non-deterministic sums, and then of course all the lambda calculus features. Now, what I've done together with a student of mine from Paris, Francesco Zacca Mardelli, is give an operational semantics to this idea.

2:12:30 But what we don't know is that this is really secure in the sense that we have the existence of these. So we've tried that, but some of the operational analysis has been got by reading from the denotational model based on features. However, there's some looseness in that, and what we don't know is whether or not, for example, all the function spaces that we need really exist. We'll lose ends and so on here, or go into all of them, but we'll need that. It's very gratifying that event structures somehow arise naturally from trying to understand the operational character of the features. And that there's an event structure of semantics. But I'm afraid it's also disappointing, because one can show that the event structures are of such an impoverished nature, one can show that every event causes and depends on at most, immediately causes and depends on at most one event. Because of that, one can show that one's knowledge, one is never going to be able to give within that particular semantics, and knowledge relieving. Not only is there maybe canonical event structure semantics for CCS. So, there's room in the category, the A5 category, to play around with variations of how to do it, but I don't think anybody's impressed with that. Okay, and now it's late in the day, but what I'll say is that, okay, there are several promising leads. And I think, now, I think I believe that it's possible to get a domain theory which supports higher order name generation, independence of actions, and kind of an operational stance, in terms of equivalences and so on. But it's still some way off. In the Fawcett version, you were solving some domain versions. Was it worked out in the categorical?

2:15:00 Yes, in some of the work that Marcelo and Lupe Catali did in VIX-97. In fact, they did most of that work together. So they generalized the recursive domain constructions together. Though you can, of course, work very concretely, too, because you have to define these path orders recursively, and that's not so hard. You just do that often by exactly definition. This is a completely crazy question. When you went from two to set, set seems awfully large to me. What about taking finite sets? Does it make any sense when we're talking about mathematics? Yeah, I mean, yes, a lot of... you could certainly do that. I mean, could you just restrict what you could do? Well, that would work. Yeah, but I don't think it would get you many gains. It may just get in the way. I have a question. I've got my Algebraic hat on, so set some lines, just the cool of it, so you jump there and sort of soup, I'm just showing you what the Algebra is, just soups, because you just, only jumps in choice, that's too little, you want more, you haven't really said what you want, you just give yourself a lot of stuff, but it isn't quite everything you want, but... You could ask me what's beyond algebraically. Do you do algebra for cats, or do you do something for one cat? I don't know what kind of operations you mean. You mean, of course, it's more than just seeing the sun, but also making an identification. Yeah, yeah. That's right. And that's essentially, it's essential to this idea, because it's that identification that's giving you the question. What it means, you know, I don't know. I mean, I don't know.

2:17:30 It's as if you take the models and that's nice, but what they do can be better. Yes, yes. Is that related to the question of what identities you get when you do the semantics or the mathematics? You alluded to the fact that someone earlier guesses that... For the domain, for the functional models, that's right. When you go to the better one, you work with the identities associated with the biceps. And then, in many cases, you just get the biceps the same as biceps in relation to the biceps. So there you just get bisimulation. But of course when you start with the open mathematical simulation from higher order processes, it's odd, it's odd. It's a little bit more than you might expect. You might think that processes should be bisimilar or higher order, even though on common inputs they get bisimilar answers, but there's more, there's an extra little clause that comes in. Which is meant that understanding by simulation is not only meaningful. To read the standard and communicate from the organizers of the workshop. Because Lars and I would like to thank all the speakers of the workshop. I would like to thank Linus Kropp for so conveniently planning these surveys worth it in the same year as Plouffe and Kouple and for providing a course of inspiring questions, suggestions and comments during the workshop and as ever before.

2:20:00 Thank you for your attention. This is great. Tell me more about that tomorrow morning. You probably want to do a bit of networking, don't you? It's already going to be very productive. Just talking to, as far as organizing meetings, because I just want to speed up. They're both very... Yes, you can... It's actually safe, we're definitely... Very good, very good. I see you're very... I'll spend a lot more time with you. No, no, no, that's absolutely perfect. No, no, I think it's perfect. I don't think they need anything flashy. I just wanted to run it past you because I didn't want to choose anything that you might have. Subsequently, feel uncomfortable with philosophical ramifications and practical theory or conceptual ramifications and practical conclusions. So, I'm going to leave Chicago. No, we certainly won't call it that. We certainly won't call it that. And I won't call it Hollywood back in the day because I was just teasing. No, thanks. I was thinking that that's an awful lot of rediscovering the wheel. Not saying it's been wrong, but an awful lot of rediscovering the wheel. So it's a natural thing to do, but here we have this theory that it's a bit crazy, but he was sort of candid about it, and he did that, so it's a little funny, but he didn't want to do it, and he didn't match very well, and he didn't do that much of a job.

2:22:30 I intend to take a rather long lecture on mathematics, but I have to do a separate one, so then I'll see you at the end of the day. Thank you. It always has a lot more content and a vague evidence of mathematics. So I'm going to take a short break now. Thanks for getting me to the church on time. The question is how little of the folklore that was around in the 70s got written down and how much people are having to discover. Communally, 60s and 70s, but we communally didn't do a good job. If I think of, you know, things people sort of say, this happens and they discuss it and it happens and I think that... Everybody used to know X or Y. Well, most of this stuff, you see, everybody in the 60s, everybody knew this. This was the basic method. But I think the only place it's written down is, correct me if I'm wrong, McLean and Murdoch in 1992. There's something there, yes, there's a lot of it there, yes, that's right. Yep, yep, there's an awful lot of it there. But I don't think there's any place where you can find it actually written down. No, I mean, at least enough to impress upon you the fact that this is the basic. This is the way of doing it. Yeah, exactly. Which category theory works. Yeah. Anyway, that's all. I guess we'll do this. All right, I'll just go. I'll see you. See you. I guess we're just too busy cramming that stuff. We wanted to talk about the calendar. In fact, a few minutes ago. Yeah. Okay, right.

2:25:00 Yeah. Good. I'll mention you at 1 o'clock. Thank you. Well, I'm a little bit of a man of speed, I'm pretty nice, but that's all right, that's all right, that's all right, that's all right.