Complexity & Computation (Session 10)

But nevertheless, I will try to do them. Also this session is kind of like a, it's supposed to be, you know, the last session of the computation, but it is not really because we are, you know, just like too many stops are still kind of left unanswered. So we are working on Petrinets and just some basic introduction on linear logic. And that kind of puts us in the direction for unpacking all of this stuff with regard to computation, with regard to language, which would be the third and final

session. So we are having how many sessions? We have still four more sessions, I think. Yes. Which means two additional sessions that, two sessions in addition to our pre-planned schedule. Because we didn't manage to cover all of the topics. Sylvie happened. But Reza, I emailed you. REZA KADZALOVYSKI- Yes. I sent you an email. Or I actually, oh, you left last time at the end.

I thought you were there. I said that. I apologize. I completely had a really fucked up internet that week. So I couldn't really do Hangout. would be great if you can give me any date. I'm free for the coming week, and I'm home usually. So any time that works for you is fine for me. MALE SPEAKER 1 MALE SPEAKER 1 I'll send a follow up with a couple options. A superb, superb essay, by the way. Excellent. MALE SPEAKER 1 And I was also wondering if there was an assignment for the second module. ALEK SINGHERBURGENGARANI Yes, yes. But a couple of people asked, I'm going to put on the classroom page this week,

it has something to do with Petri Nets and linear logic. It's more of a problem solving, given rather than typical philosophical ruminations on a topic. I thought it was better to just, because these are kind of like technical stuff, and it's very easy to be impressionistic about these kinds of topics, like this or concurrency multi-agent systems and stuff. So I thought the best course is to choose some, like a concrete, at least theoretical problem or mathematical problem, and then give it as a kind of a problem so the students can either solve it or talk about it.

I will put it on the classroom page. Was that the exercise also? No, the exercise I will give it at the end of this session, yes. At this session. How are you doing, by the way? Better this week. Okay, good. No party, no hangout. Yeah, exactly. You are not living in New York, are you? No, I am. I'm still in New York. I'm in Brooklyn now, but yes. Oh, you are in Brooklyn. Okay, so it's very easy to kind of get involved in massive amount of partying and going out. One of the downsides of living in New York is that you never get the stuff done precisely because you always have to go somewhere, some art stupid show, hang out with friends.

Yeah, it's... It gets in the way, yes. I love the city itself, but as a place, I despise it. I absolutely think that, you know, as a city, as an architectural edifice, it's absolutely one of the best wonders. But really, like, kind of, it has this atmosphere of constant tension, obscenity. It's really kind of, like, downside of it. Better to retire to Connecticut Yeah In the middle of nowhere Connecticut is not bad I mean at least in the spring and summer it's beautiful But it is basically just backwater It's just a Puritan New England

You know, sheds hold But it's okay I suppose It's actually Yeah, I know You told me. All right, shall we? Okay. Any questions? Let's start from previous session. We talked about, what was it? We talked about multi-agent systems a little bit about games and the kind of behaviors that makes multi-gen systems very appealing as, you know, kind of a conceptual object of the study in theoretical computer science.

And, you know, of course it has applications for program design, network design, designing algorithms, so on and so forth. Then we talked about different scenarios that usually arise in multi-agent systems. We had at the end of the last session also we had some commentaries on why is that, you know, this computational pattern of interaction is kind of significant, not only in complexity sciences, but also a reinterpretation and revisitation of main theoretical ideas that

really signify the advent of modern sciences. For example, in biology, Darwinian theory of evolution, once we have an interactive computational model, many classical or traditional ideas, for example, in Darwinian theory of life, become more sophisticated. can be revised. We talked a little bit about sex and the interactive computational interpretation of sex in Darwinian evolution of life. And we made this contrast that from a Darwinian

point of view, for example, sex has no import for procreation. That's just like a very antiquated, biblical almost account of what sex is. We talked about it in terms of calibration of in terms of fitness landscapes, asexual behaviors in a species, but also in terms of its contribution to altering landscape that results in further complexification and down the line aspeciation.

that's really the function of sex and how interactive paradigm of computation can allow us to better interpret this rule of, for example, natural selection, for example, through the vector of sex and reproduction in terms of recombination of alleles, so on and so forth. Anyway, today I'm going to talk about, if you remember, we kind of mapped out the landscape that we are going to explore. And that would be interactive theory of computation

with topics like game semantics, semantics of information, processing and concurrent system, interactive logic, and that would give us kind of good philosophical, conceptual, and scientific resources for to tackle problems like construction of human level AI, a study of languages, whether it's natural language or formal languages, artificial languages, a study of complex systems, social computation, or social mind. And the prerequisite for exploring this landscape, this tripatriate landscape, comprising of

a study of multi-agent problems like epistemic modeling, game theoretical scenarios, communication between agents in different scenarios, which we briefly explored last session. Then the other one is concurrent problems, study of concurrent problems, and that's the theory of processes, scheduling, the introduction of concepts of resources that we did in computer science, which we are going to look at this session under the rubric of petrinets, because petrinets are really the canonical objects of a study in concurrent dynamics, like the

most famous, most well-known, and most well-defined way of thinking about concurrency. And then the third landscape, which is the most important one, are the study of logical problems. And that basically resulted in the unification of the study of multi-gen systems, concurrency problems, and some of the pre-neal logical investigations inside logics and mathematics, like proof theory, semantics, or analysis of sequence. And I'm going to, after working out an introduction on Petri Nets, I'm going to introduce the

elementary aspects of linear logic, because linear logic gives us a good grasp of what at a stake in the correspondence between logics and computation, and how logics can, once understood at the deepest level, no longer as simply a tool for verification, can unify in fact these three landscapes, the classical problems of logics, problems of multi-agent systems and problems of concurrency. Linear logic is a really good tool for this and it

is really the tool that theoretical computer science extensively uses and further develops to reach this goal, this unification goal. So questions, discussions, anything before we move forward? Anything? Nothing?

Okay, so first thing, Petri Nets, and that's, as I said, is going to be a brief exploration of problems in concurrency. Petrinets are graphical and mathematical modeling tools applicable to many systems. There are, in fact, if you're familiar with engineering, system engineering,

For any kind of engineering discipline, one of the first things that you are taught at school is Petri Nets. They are extremely powerful, extremely significant for you to visually grasp the flow of dynamics, flow of information, the flow of resources, the flow of events in, for example, production chain, in design of, for example, an engine, how, for example, a pump works, how a logical

circuits and electrical circuits needs to be modeled accurately so it doesn't for example enter any problem. So PET-3 nets are really some basic engineering tool. They are promising tools for describing and studying information processing systems broadly understood. are characterized as being concurrent, asynchronous, distributed, parallel, non-deterministic, and or stochastic. As a graphical tool, Petri Nets can be used as a visual communication aid similar to flow

charts, block diagrams, and networks. In addition, tokens are used in these nets to simulate the dynamic and concurrent activities of systems, or broadly speaking, resources. As a mathematical tool, it is possible to set up state equations, algebraic equations, and other mathematical models governing the behavior of the system. Historically, as I mentioned, the concept of Petri Nets has its origin in Karl-Adam Petri's dissertation submitted in 1962. Although they were first really invented by him when he was 13, I think in 1939.

He invented PET-3 nets to study chemical reactions. Since 1960s, huge amounts of papers have been published on PET-3 nets, different applications on PET-3Nets, different modification on PET-3Nets. And they slowly, during the 80s, mid-80s, in computer science, they started to pay attention to PET-3Nets. And PET-3Nets also became a very powerful, very interesting object of studying in computer science.

Design and analysis of PetriNets is based on a strict and definite mathematical theory. Software tools developed have made PetriNets represent powerful mechanisms for modeling and analysis of particular applications. The theory of Petri-nets provide a well-defined theoretical mechanism for modeling of the discrete event systems and analysis of their characteristics. Petri-nets have been successfully used for learning behavior of various problems arising in scientific engineering and industrial domains, especially in relation to computer science problems arising in concurrent systems like asynchronous actions, scheduling, resource

control, etc. The only rule, so I'm going to start to give kind of a very brief introduction of how a PetriNet works and what are the rules governing a PetriNet. And I will at some point talk about the reason why we are so interested in petrinets and why we should be. And its significance for computer science, especially when we understand the significance

of how a PetriNet represents the transition of the states and the flow of resources then becomes extremely important in terms of how it can be unified with a logical account of resources, basically, and this is one of the ongoing research to model, in fact, logics, for example, SQL and calculus, or linear logic, interpretation of SQL and calculus, on Petri nets.

Because as I said, Petri nets are extremely powerful tools for software design, application design for a study of concrete problems in computation. They have, in fact, applied basically imports. You can use them to design software. And it's really important that if they represent certain concrete problems, but also precisely because of their mathematical algebraic properties. And they can, in fact, be used to model

kind of substructural logics, resource-sensitive forms of logics. And that's basically what the main research is in contemporary theoretical computer science. So the only rule one has to learn about PetriNet theory, the rule of transition, enabling, and firing. Although this rule appears very simple, its implication in PetriNet theory is very deep and complex. And it wasn't really obvious when PetriNet were introduced in the 60s. when it became an object of interest for computer science, computer scientists and mathematicians

started to see that behind this extremely very simple rule and simple structure in Petrinets, there is an underlying complexity, computational complexity. And the way that PetriNet represents it is extremely interesting. So let me share the screen with you because we are going to have some diagrams and formulas. Hello. OK, one second.

OK, then Dropbox. Okay. Okay.

Can you see the screen? Yes. Yep. Good. OK, so very briefly, as I said, Petri nets are just like flow charts. So they're composed of these basic elements. The basic elements of a Petri net are circles, markings represented by solid dots, or you can replace them with numbers if your solid dots are

Many arches or arrows and solid blocks. Circles are representing places. The markings or dots represents resources or tokens. arches or arrows represents the orientation of your transitions, the dynamics between states. And the solid blocks, rectangular blocks, are representing transitions.

So as I said, the only rule that you need to learn about a PetriNet is the rule of transition enabling and firing. Although this rule appears very simple, its implication in PetriNet theory is very deep and complex. A PetriNet is a particular kind of directed graph, together with an initial state called the initial marking M0. The underlying graph N of PetriNet is a directed, weighted, bi-patriot graph consisting of two kinds of nodes, called places and transitions, where arcs are either from a place to a transition or from a transition to a place.

So your arrows, your arcs, can be either connecting a place transition or transition to a place. In graphical representation, places are drawn as circles, transition as bars or boxes or solid rectangles. Arcs are labeled with their weights, positive integers. Where a k-weighted arc can be interpreted as a set of k-parallel arcs. And these you We can think about this as k parallel arcs, as k parallel processes.

Labels for unity weight are usually omitted. A marking, a state, assigns to each place a non-negative integer. If a marking assigns to place p, a non-negative integer k, we say that p is marked with k tokens. going to show you the diagram so you will see what I'm talking about. Pictorially, we place K black dots, or tokens, in place P in the circles. But you can, as I said, you can simply omit the markings and just write the number. And especially, people usually and they do that when the number of dots are many.

A marking is denoted by M, an M vector, where M is the total number of places. The Pth component of M, denoted by MP, is the number of token in place P. The number of your resources at any place, any states in your, for example, system or process or whatever. In modeling, using the concept of conditions and events, places represents conditions and transitions represents events. A transition, an event, has a certain number of input and output places representing the

preconditions and post-conditions of the event, respectively. The presence of a token or resource in a place is interpreted as holding the truth of the condition associated with the place. In another interpretation, K-tokens are put in place to indicate that K-data items or resources are available. Some typical interpretations of transitions and their input places and output places are shown in the following table. So input places, transitions, output places, preconditions, events, postconditions, input

data, computation step, output data. These are each row, each triad on a row represents a different interpretation of basically your circles, your arrows, and your circles, again with markings or not markings after an arrow. You can, depending on the context, you can interpret the basic elementary Petri net

according to these trials. Pre-conditions, event, post-conditions, input data, computation, output data, input signal, signal processor, output signal, resource needed, task for job, resources released, conditions, clause in logic, conclusions, buffers, processor buffers. So as you see, precisely because of the elementary and fundamental way of how a patronet represents estates and resources and transitions, you can interpret a patronet in any kind of dynamic.

And in fact, that becomes a kind of a unified tool for logic, computation, engineering, judgment, so on and so forth, programming. And here, the formal definition of PetriNet. A PetriNet is a five-two-pole PN. P places, circles, T transitions, A, W, M, zero, where P comprising of P1, P2, PN is a finite set of places, T, T1, T2, T3, TN is a finite set

of transitions, A being a subset of P multiplied T, union T multiplied P, the set of arcs of flow relations, W is a weight function, and basically something that's usually doesn't being studied in the elementary accounts of Petri Nets. I will talk about this later, but for now we don't really get into the weight function. M0, as I said, it's really the marking,

It's the initial marking that basically can be understood as tokens that are being processed once are admitted or put in a place. And place, as I said, can be understood as a condition, as a buffer, as you can see it as a premise, for example, in a logical formula. A premise can be understood in a logical formula as your initial marking.

And then also one thing that is important to think about PET-3NEDS always, as I said, that triadic interpretation of PET-3NEDS, whenever we are talking about markings, transitions, places, try to think about it kind of analogously between, for example, a logical formula or a piece of judgment comprising of premises and implication or entailment and then a hypothesis.

of it as a logical judgment in comparison to, for example, a state transition or a function required to translate an input to an output given a certain amount of resources. And this This becomes a key as we move forward, and especially we look at linear logic. This kind of interpretation, going back and forth between logic and computation and mathematics and processes becomes a key.

And really, as I said, Petrinets gives you a better way of not only, in an applied sense, tackling concrete problems, but also really at a theoretical level, see these isomorphism, these fundamental correspondences between logics, computation, mathematics, engineering problems. A Petri-net structure with the PTAW places time.

Floor relations and weight functions without any special marking is denoted by N. A petrinet with the initial marking is denoted by P-N, P-T-A-W, initial marking. The behavior of many systems can be described in terms of system states and their changes. In order to simulate the dynamic behavior of a system, a state or a marking of petrinet is changed according to the following transition, also called a firing rule. A transition T is said to be enabled if each input place P of T, T is transition, not time.

If each input place P of T is marked with at least WPT tokens. Where WPT is the weight of the arc from P to T, an enabled transition may or may not fire depending on whether or not the event actually takes place. A better way of understanding this in your graphs is that you have the same amount of marking and basically the solid dots and the same amount of arrows in a diagram. Then your diagram fires, your process initiates. A firing of an enabled

transition T removes WPT tokens from each input place P of T. So every time that you have a firing in your diagram, a resource is consumed and adds WPT tokens to each output place P of T. So it removes it from the marking or the solid circle, solid dot, from its previous place and adds it to the next very intuitively. A resource is being consumed and then put on the output box. Exactly like a logical formula, when you are making a judgment, your premise

is consumed and adds, if your net, if your logical net is in fact enabled, your resource, the premises consumed and add to the hypothesis, to the conclusion. A transition without any input place is called a source transition, and one without any output place is called a sync transition. Note that the source transition is unconditionally enabled, and that the firing of a sync transition consumes token but does not produce any.

A pair of a place P and a transition T is called a self-loop if P is both an input and output place of T. A petrinet is said to be pure if it has no self-loops. A petrinet is said to be ordinary if all of its R weights are 1s. Here we have a very basic Petri net, which is kind of faithful to its original purpose, illustrating, representing a chemical reaction. As you see, this two example represents a transition firing

group. In A, we have the marking before firing the enabled transition T. In B, the second diagram, we have the marking after T transition, where T is disabled because the firing has taken place. A chemical reaction has happened. Your resources have been consumed and put on the output box or the output place. The above transition rule is illustrating

the chemical reaction 2H2 plus O2 gives us 2H2. Two tokens in each input place in diagram A show that two units of 2H and 2O are available. And the transition T is enabled. After firing T, the marking will change to the one shown in diagram B, the second one, where the transition T is no longer enabled.

For the above rule of transition enabling, it is assumed that each place can accommodate an unlimited number of tokens or resources or markets. Such a PetriNet is referred to as an infinite capacity net. For modeling many physical systems, it is natural to consider an upper limit to the number of tokens that each place can hold. Simply put, when we are dealing with physical systems, but also when we are dealing, for example, with a judgment, a logical formula, our resources are constrained, are bound.

We don't have many premises. You can't add or copy premises or formulas or resources freely. And as I said, one of the most important things in PetriNet is this idea of resource sensitivity that allows us to accurately represent resource sensitivity and the transition of your resources instantiation of a process, whether it's computational, logical, or physical. Such a PetriNet, as I said, referred to an unconstrained, basically a resource-free PetriNet

is called an infinite capacity. And the resource constraint one is called a finite capacity net. For finite capacity net, n, m0, each place p has an associated capacity, kp, the maximum number of tokens that P can hold at any time. For finite capacity nets, for a transition T to be enabled, there is an additional condition that the number of tokens in each output place P of T cannot exceed its capacity Kp after firing T.

This rule with the capacity constraint is called the strict transition rule, whereas the rule without the capacity constraint It's called the weak transition rule. Given a finite capacity net, nm0, it is possible to apply either the strict transition rule to the given net, nm0, with initial marking, nm0, or equivalently the weak transition rule to a transformed net, n prime, m prime 0. The net obtained from nm0, n initial marking, by the following complementary place transformation where it is assumed that n is pure. Step one, add a complementary place p prime for each place p where the initial marking

A p prime is given by m prime 0p equals kp minus m0p, simply a complement. At step two, between each transition t and some complementary places p prime, draw new new arcs, T, P prime, or P prime T, where W T prime equals to W P T, and W prime T equals to W P T. I will show this in diagram. So that the sum of tokens in place P and its complementary place P prime equals its capacity K P for each place P, before and after firing

the transition T. A Petri net can be represented by listing its components as well. Consider a simple Petri net illustrated in the following figure. In this figure, the transition T1 has one input place, P1, and two output places, P2, and P2, P3, and P4. And, P4, and P2, and Same petrinet can be represented by explicitly describing its components. P, P1, P2, P3, P4. T, transition 1, transition 2.

I, P1, T1, P2, T2, P3, T3. O, T1, P2, T1, P3, T1, P4. It should be noticed that components I and O can be defined in terms of transition as well as places. A PetriNet is an object that is characterized by its estates. Each estate is defined by the number of tokens in places. As we saw in the production of 2H2O diagram. A token can move from place to another place if certain conditions are satisfied.

The basic rules which regulates the work of a PetriNet are as follows. Enabling transition. A transition is said to be enabled transition if each input place has at least one token. For all input places, the number tokens in a place of enabled transition must be equal to or greater than the weight of arc connecting named places with transitions. As I said, the market and the arcs at least being equal and then your diagram fires. It's enabled. The transition T1 of PetriNet in the following figure

is an enabled transition. Two markings, two arcs. So it's basically an enabled transition. And it can produce an output marking. Disabled transition. You see, here we have one marking and two arcs or two arrows. We say that a transition is disabled transition if there exists an input place with a number of tokens less than the weight of corresponding arc. For instance, T1 in the following figure is a disabled transition.

As you see, your marking is one and your corresponding arcs are two. Firing action. An enabled transition can fire or occur or instantiate. When transition fires, its input places elude some of their tokens, resources being consumed. For all input places, the number of tokens removed from the source place equals to the weight of the arc from source place to the transition.

Then output places receive tokens. For output places, the number of tokens placed in output places equals to the weight of arc from the transition to the output arc. This is illustrated in the next papers. So as you see, consumed but also the marking, the number of marking corresponds to the number of your, the weight of arc from transition to the output place. Here, from the transition to the output place, from T1 to P2. You have also one arc that represents

your transition that represents the mapping between T1 and P2. And you have one marking in place, P2. So they are both one. And that needs to correspond to the number of the marking and the number of arc. And here again, you have a slightly more, with two markings and two arcs, two places, and the same thing.

Each estate of a PetriNet is described by allocation of tokens in its places. Consider the PetriNet in the figure below. Again, each estate of a PetriNet is described by allocation of tokens in its places. This PetriNet is enabled in the initial state, which is described by marking M0. M0, 1, 0, 1, 0, 0, 0. Occurrence of T1, transition 1, changes the state of PetriNet from M0, 1, 0, 1, 0, 0,

the representation of your markings to M1, 0, 1, 1, 0, 0, which is the next figure. Finally, firing of T2 transition to changes the state of Petrinand to M2, marking 2, which can be represented as 00110. This is shown again in the following figure.

Sorry, I read that part twice. I was sorry, sorry. Because I'm reading off of the iPad and trying to scroll this at the same time. Sorry, finally, firing of T3 sets the PetriNet to M4 00101. Then PetriNet becomes disabled. Basically all of your resources have been consumed. A state of M1 of the PetriNet is said to be reachable from M0 if there exists a sequence

of occurrences of the transitions changing a state of the PetriNet from M0 to M1. This reachability is one of the main concepts of PetriNet. I will talk about it and it has certain properties. But really the basic understanding of the reachability principle in PetriNet is that your diagram is in a firing condition, each estate can be reached from the previous estate using or consuming the resources. So basically there is a firing condition between your state transitions. A state M1 is directly reachable,

as you see in this diagram. Is there any question? Can you hear me, guys? Or because of the . Yeah, you can hear me. Or I can hear you. I'm going to now. Yes. Yeah. Yes. OK, OK. Sorry. A state M1, as you see in this diagram, is directly reachable from M0 if there exists a single occurrence at a state M0 zero setting the PetriNet to M1.

Multiple transitions again in PetriNet, in certain state of PetriNet, if this is the case then each of these transitions may occur. The winner among transitions is usually chosen according to users preference or decision or needs of application being considered. This is another property of Petri Nets, that they allow decisions, the choice of which transition and which resources need to be undertaken or need to be fired. Such transitions are concurrently enabled transition.

You can think of this very intuitively in... Are you guys familiar with semaphore? Like the... Not the... I mean, I will talk a little bit about the computational concept, but really the semaphore in railways. especially you have it's kind of like a pole with with a sign that's you know with markings usually red and white and then when goes up and down depending up

how the arm is raised it opens the railway in for example different directions that also for in railways so you can intuitively think of this Petri nets in the concurrently enabled transition as representing the function of a semaphore in railway. Simply it allows you to choose. But the introduction of some constrained Petri nets put a strict rules on, for example, which process or which resources can be consumed and which firings need to be enabled.

It's very kind of like a, because obviously when you are dealing with a concurrent system, not always it's the system that chooses which process needs to be undertaken. It's sometimes the environment that chooses this, with a kind of a non-deterministic manner. And in that case, PetriNet can represent again this choice imposed by the environment, which exactly, which, how many resources need to be allocated to which place and which transition

needs to be fired. So this is the concurrent one, but also there is also a parallel representation, a parallel PetriNet. A parallel PetriNet is one that your transition may fire or may occur at the same time or in parallel, as well as one another, after one another. So basically there is no constraint as to which of your resources are going to be consumed and which of the transitions are going to be acquired. And this is one of the kind of the subtleties behind Petri Nets, that parallelism in Petri

nets is in fact a special case of the general concurrency. Synchronous concurrency is a special case again of asynchronous concurrency in pet free nets. And this is in fact one of the main things that we will look into when we are talking talking about concurrent games and concurrent systems. Synchronicity, a special case of asynchronicity and parallelism, a special case of concurrency.

If multiple transitions are concurrently enabled and can fire at the same time, the occurrence of these transitions can be described as a step. For instance, the occurrence of transitions in the previous figure could be represented as steps S1, T1, T2, and S2, T1, T3, the diagram. It should be noticed that the transition in S1, T1, T2 cannot occur in reverse order, Since occurrence of T2 blocks T1 or changes its status from enable to disable, meaning

that S3 equals T2, T1 is not a step. A transition may even occur concurrently to itself. If so, a step contains multiple copies of the transitions. In this example, S3, T1, T1, T1 indicates that transition T1 occurs three times in a row. In general, each step is a multi-set over the set of all transitions. A multi-set is usually denoted by sums where each element has a coefficient telling how many times it appears. For instance, in a step S4, 2T1, T2, 2T3, which is enabled in M0 initial marking, transitions

T1, T2, and T3, respectively, occur 2, 1, and 2 times in the order. This step set the Petri net to a state 1022. In general, a place or a condition can receive multiple tokens or multiple resources. If the number of tokens in a place is large enough, numerical values are assigned rather than dots. For example, a PetriNet in the next figure is characterized by the initial state 47, 7, 13, 42.

values are used to indicate the number of token resources in places rather than placing 47 dots in P1, et cetera. So these are the basic rules of a PetriNet, just the elementary rules. And depending on how PetriNets are represented, because PetriNets don't have a concept of time, depending on how if you put time constraint on Petri Nets, the rules are slightly changed, addition of some rules and constraints. But also there are different kinds

of interpretation of Petri Nets. But nevertheless, the basic rules and the basic behavior of Petri Net was the one that I just gave. So now a few rudimentary examples. Example of a bending machine. The machine dispenses two kinds of snack bars, 20 cents and 15 cents. Only two types of coin can be used, 10-cent coins and 5-cent coins. The machine does not return any change. The graphical representation of our PetriNet is like this.

We can alternatively make it with more, basically, represent. That was just like, kind of a very spelled out, and this is the graphical representation of a PetriNet or our vending machine. Now we can imagine three scenarios for this vending machine. Scenario one, deposit five cents, deposit five cents, deposit five cents. So you are giving three tokens. Oh, sorry, deposit five cents. Take 20 cents at Snackbar. You are depositing four tokens and you get a 20-cent Snackbar.

get an initial, you get, you, you, so how should it be represented? It should be represented as four markings, four arcs, and your output place is one marking, one arc. Or you can Alternatively, go with putting four dots, in fact, in the vending machine with one. Actually, it should be four arcs and four markings for your initials.

Scenario two, deposit $0.10, deposit $0.05, take $0.15 at Snackbar. Scenario three, deposit $0.05, deposit $0.10, deposit $0.05, take $0.20 at Snackbar. And we can have these in PetriNet and these different kinds of scenarios. Now, the reason that PetriNets are so appealing for computer science because they capture two concepts that are key. One is that they are sequential.

They represent a sequence of events and actions. And two, they can capture concurrency or concurrent executions. But in both cases, the way that they represent sequentiality and concurrency is resource sensitive, meaning that you have the constraint of resources and your transitions, both your sequentiality and your concurrency can only be modeled on the basis of how many resources

you have and how your resources are consumed throughout the process. So even though Petri Nets are simply graphical tools for representing sequentially and concurrency, The real import of PetriNet, as I said, is the idea of resource management. And in PetriNet, resources are always invariant. They are conserved. You need to take into account how your resources are consumed, what your initial resources

are, so on and so forth. But you always have the conservation of resources. Each resource in your state transitions need to be accounted for. Where it is, when it is consumed, where it is consumed, etc. The net structure of Petri nets, again, is an important property which makes it, again, appealing for modeling computation, modeling logical formulas, so on and so forth.

They can represent non-deterministic events like conflict choice or decision, a choice of either E1 or E3. Simply again, for example, in a multi-agent setting, you can think of this, that Petri Nets for this reason can adequately capture those complex behaviors that we saw arising in games where the opponent makes the choice or where you have obstructing moves from opponents

blocking you access to a certain state transition, to a certain branch of moves in your games. Also they can capture the idea of synchronization, and that's why they are widely used in a scheduling, modeling scheduling problems in engineering and computation. Scheduling, you can think of this as, for example, an engineering problem dealing with, for example,

at you want to, for example, design an electrical circuit. And this electrical circuit shouldn't go into race condition. What is race condition? Race condition is, very briefly, it's kind of like a glitch in any kind of system using resources. For example, in old times, electrical circuits,

you have two inputs. And if there is a delay in your state transitions, in your electrical circuit, the outputs can conflict. You can think of this, for example, that we have a logical circuit representing P and not P. So, if there is a delay, if there is no correct scheduling, there is a possibility that an

output condition arise where because of the delay in the processing of the signal, P and not be, become true at the same time. It simply leads to a contradiction, to a fault, to a glitch, and the system halts, crashes. This is a race condition. So petrinets try to control this condition. Not only they try to, when modeling and scheduling and synchronization, and synchronization, they not only solve the race condition problem, but also they are

supposed to model resource management so that your system doesn't enter into resource starvation. And what is resource establishment? Resource establishment's basic example was our ATM machine. Old times ATM machines, I take money from my account. My friend take money at the same time from another ATM from my account.

And if there is no synchronization within these two ATM machines, my accounts can go to negative. So this synchronization eliminates two things, race condition and resource starvation. And how many of you are, actually I asked this, the concept of semaphore, the intuitive idea of railway as also a counterpart in computation in programming. Again, it's called

semifores. Semifores are just these, in the most trivial way, there are these integers. They cannot be manipulated. They are type of data constraints. They can be incremented or decremented. And they are useful when they are decremented. They are signaling, they are representing weight.

For example, a semaphore in programming can be used to represent a buffer. they are decremented when at least when okay so actually kind of an intuitive example for you to understand some for think of this as you have a laptop five

laptops and you have a bunch of students who want to use these laptops. So in order for us to avoid any kind of race condition and fairness so every student can at some point access a laptop, we can introduce the concept of semaphore. And semaphore, in our example, serve two functions either representing a weight or a signal for a student's wait until another student uses the laptop if the integers are positive

non-zero, it signals a student can use an available laptop. But if the integers are zero, the number of laptops are zero availability, then the students need to wait in order for a laptop to become available so they can use it. So in this example of a semaphore, when it is on zero, it is a weight semaphore. And when it is a positive integer, namely our availability of resources, is a signaling function. Simply as students can come and

use an available laptop. So this is the concept of semaphore in programming, really capture this idea of resource management, fairness, and race condition in Petri Nets. And there are, in fact, good ways of how Petri Nets can represent semaphores in computation. So, back to Petri Nets. Properties of Petri Nets are two, behavioral properties and structural properties.

Behavioral properties hold given an initial marking. properties independence of initial markings relies on the topology of the net structure behavioral properties are reachability boundedness liveness reversibility coverability etc and this is a reachability diagram a reachability M2 is reachable from M1 and M4 is reachable from M0 in the above diagram. In the vending machine example, all markings are reachable from every marking. M0, T1, M1, T3, M2, T5 and it goes on.

Then the boundedness. A PetriNet is said to be k bounded or simply bounded if the number of tokens in each place does not exceed a finite number of k for any marking reachable from M0. Again, in our vending machine example, the PetriNet for vending machine is one bounded. Liveness. A PetriNet with initial marking M0 is live if, no matter what marking has been reached from M0, it is possible to ultimately fire any transition by progressing through some ferding firing sequence. A live PetriNet guarantees deadlock-free operation, no matter what firing sequence is chosen.

The vending machine is live. A transition is dead if it can never be fired in any firing sequence. Further, we have, in addition to behavioral properties, we have, as I said, structural properties of bed-free nets. Structurally live, there exists a live initial marking for n, controllability. Any marking is reachable for any other marking. A structural boundedness, bounded for any finite initial marking, conservativeness. Total number of tokens in the net is a constant. Simply put, you need to account for all of your resources, where they go.

The classical problem that captures many properties and many key concepts of Petri-Nets is a problem by Edsgard Dijkstra, known as Dining Philosopher's Puzzle. Simply is this thought experiment. There is a dining room containing a circular table with five chairs.

At each chair is a plate, and between each plate is a single chopstick or fork. In the middle of the table is a bowl of spaghetti. Near the room are five philosophers who spend most of their time thinking, but who occasionally get hungry and need to eat so they can think some more. Now in order to eat, a philosopher must sit at the table, pick up the two chopstick or forks to the left and right of a plate. Then serve and eat the spaghetti on the plate. The layout of our tables when we have four philosophers is like this. Each philosopher

can be represented by the following cryptocode. Process PI, while true, do, think, pick up chopstick I, chopstick I, one, mod five, eat, put down chopstick I, chopstick I, one, mod five. A philosopher may think indifferently. Every philosopher who eats will eventually finish. Philosophers may pick up and put down their chopstick in either order or non-deterministically. But these are atomic actions. And of course, two philosophers cannot use a single chopstick at the same time. Now, the problem with, I mean, this is intuitively,

we can think it's actually solvable. But it has been shown that, in fact, the philosophy problems does not have a canonical solution. You can devise a Petri net for it and show that you can have different scenarios where it can be solved, the dining philosophy problems, but only at the cost of excluding other scenarios. For example, you can solve the resources starvation in your dining philosophers, so no philosophers die of hunger and at the same time can think, but then you enter race condition. Or you can eliminate race condition,

but then again you have resource starvation. Dijkstra, in fact, solved this problem using a hierarchy of resources, kind of a complex setting. But then again, that solution has been shown that it's completely impractical when it actually involves many resources and many schedules. It basically leads to really complicated scheduling problems. You can go and check. There's a massive amount of essays and different solutions, different way of, for example, people

right programs for solving the dining philosophy problems. You can look at it online. It's actually quite very interesting, precisely because the dining philosophy problems captures all the complications, nearly all the complications that arise from resource management. It simply highlights the rule of resources in computation and respectively scheduling, concurrency, problems of race, condition, resource starvation, choice, so on and so forth.

So what I would like as kind of an exercise is, I'm going to give you two exercises. You can select one of the two. One, make a petrinette for a dining philosopher problem. You can, in order to make it less complex, you can just limit your number of philosophers to three. Make a petri-net for a dining philosopher, and in any kind of scenario that you have in

mind, either in order to eliminate race condition or to eliminate resources starvation or simply to model the basic Petri net of a dining philosopher table. So in order to do that, you need to be capable of, one, make a Petri net for each philosopher. Then you need to, in a correct way plug these petri-nets for each individual philosophers together. So your petri-net in a multi-setting, in a multi-agent setting, in a concurrent processing setting, can be

enabled and simply fired. So either you can do this, make a petri-net of a dining philosopher, Or you can do exactly like the first session. Get a solution from online because as I said there are so many solutions given for dining philosophy problems. get a solution and then analyze it to see whether this solution holds for resource estimation criteria or race condition criteria or scheduling criteria and when or where basically it starts

to malfunction, doesn't hold anymore. Because as I said, the reason behind this, suggesting this dining philosophy problem as a kind of a puzzle of thought experiment, precisely because it captures some of the main concepts of concurrency, the problematics of concurrency, why is concurrency, is kind of a thorny subject precisely because of this, as I said, the idea of management of resource is not really as straightforward. Depending on how the moves are being made in your interaction game, in your multi-agent

setting, different complications can arise. Any questions before we move forward? Sorry, so there are two aspects to it? So the first one is the statement.

Oh, no, no. I said this is one of our assignments, but it has two aspects. I will give the second assignment that you can select between the two. But if you go for this one, two things. You can either get one of the solutions you can find online and try to analyze it to see whether it leads to resource estimation or it leads to race condition. Or just try to make a PetriNet, according to one solution or another, make a PetriNet for a dining closet problem. For that, as I said, first you need to come up with a petriness for one individual philosopher and then plot these in the right combination, in the right state transition firing condition

together. Okay. Actually, it's really interesting that the majority of the learning philosophy problems, when you study concurrency in computer science, this is one of those things that teachers always give their students to work on. And usually, as students, the first things that they do to write a program for dining philosophers is using semaphores.

But semaphores are good for race condition. They nevertheless lead to resource starvation. But you can, I will actually put some of the links, some of the good solutions. Well Dijkstra's own solution is the strongest one, it's just impractical. It leads to complications when the amount of philosophers and the amount of scheduling increases. And Dijkstra also is the person who came up with the concept of semiforhs in computer science also. I didn't know Dijkstra was responsible for semaphores. That's a cool detail. It's an

interesting thinker. Some of course are really these kinds of interesting programming objects. Because they're really trivial. Just as I said, there are integers that they can be, you can manipulate them. There are not zeros and ones that you can simply manipulate. You can decrease them or increase them. They can be decremented or incremented. As I said, incrementation and decrementation, signaling and wait. When it is zero, it's a wait one. It's a wait semaphore.

You don't have resources available, so you have to wait. It's a good way of how to model a buffer with a semaphore. When you have availability of resources, positive integers, then they can be decremented. It signals for a buffer to be available, or your laptops in our example to be available for students so they can use it. This is a very trivial kind of concept of sum of words. It can become more complex. But one of the interesting thing about sum of words is that they tell you how many resources are available, but not which resources are available.

That is an interesting thing, and that's one of the reasons that simply using semiforce to model dining philosophy problem will lead to resources salvation, precisely because of this absence of which resources are available, which forks are available. However, and Dijkstra again works on this, you can create different classes of semaphores, adding more constraints on your semaphores, that can represent, that can show which resources are available. But that again becomes an impractical issue.

there are a number of philosophers, the number of scheduling increase. Questions? Comments? Diaries? I mean the other way I would relate Dykstra to complexity is the usual way that you would run into him in computer science is actually from a software engineering perspective and the introduction of structured programming constructs, which are basically hierarchical

mechanisms and managing complexity in a way, right? Yes. So he has this famous short note called, go to considered harmful, right? And this is where he's saying don't use go to, where you can go to arbitrary parts of the code, rely on control structures, if then, and sort of functional decomposition and so on. And that is meaningful and good advice because it's containing the amount of complexity that you need to deal with as a programmer. It's isolating these modules, these separate pieces in

the closing hierarchy and therefore making it more navigable. Yes, absolutely. Yes, yes. That's, in fact, a solution-designing problem is really this hierarchization, because of this, that gives you this navigational controllability over your resources. But the thing is that, again, as the number of scheduling problems arise, precisely because your elements increase, it becomes harder to navigate these hierarchies. It becomes theoretically sound, but practically infeasible. Yeah, it's interesting. I have to go through a solution again. It's been years. So thank you.

Also, one thing that's just very trivial commentary. In that crypto code that I made for the dining philosophy problem, there was mod mod. Any of, I'm sure you guys, some of you guys are familiar with the mod operator. Would be fantastic for those of us who do not know what mod is, just give a brief explanation of what a mod operator is in computer science. Oh, like the mod operator? Yes. Like modular, basically. module or operator, yeah.

Go on. I'm trying to think of the technical definition. Either Sean or you. Someone else jumped in at your. It's a equivalence relation, actually. It makes things that might not seem equal equal. So if you can imagine, like, I guess it's typically used in the remainder. Like you think about five divided by two, that's gonna have one remainder. But if you think about your incrementing a sequence, you're gonna create these cycles, and with the remainder, it's gonna return to zero under some kind of modulus. So you're creating a class of numbers that are therefore equivalent. And this sort of principle extends into all sorts of interesting areas, like quotient spaces. In which you create like loops, by extending into distance, or having some distance,

but also kind of stay in constraints. It's actually kind of cool. Yes, yes. OK, so very briefly, modular operator is simply the computer take on Gauss modular arithmetic. As Sean says, it's an equivalence relation. It's very, very basic rudimentary sense. You can think of as the quotient and remainder in your division. For example, 4 mod 2 equals 0. You can think of this as a clock has four time divisions, 0, 1, 2, 3. And then so mod would be the circles around your clock that go from 0, 1, to 1, 2, 3,

And then makes enough circles so it comes back on zero. Cycles, enough cycles. So that's your mod. Four mod two zero. It's the number of cycles that you make around this clock. So obviously you see the importance of why using mod in dining philosophy problems. You are essentially working with a clock, a mod space, with philosophers around the round table so you can have a mod of philosophers and forks.

So, that was PetriNet and concurrency with some very briefly talking about some of the problems that PetriNet represents in the study of concurrent problems. The complications that might arise in concurrency and scheduling, synchronization, complications in synchronization and scheduling, like race condition, resources, starvation, so on and so forth.

Now we move to the basic part, the most important part of that triadic landscape of interactive paradigm of computation. That's the landscape of studying logical problems. why logic is important and significant, and why once it's reinterpreted, it can unify all of these aspects in multi-agent system and concurrency problems, and in some of the main classical concerns of logic.

And this all leads to kind of interactive pattern of computation as being discussed in theoretical computer science. So before moving to this logical problem, I would like to just talk a little bit about when and where this emphasis on logic and computation comes from, at least the way that contemporary computer science puts the emphasis on.

We can think of, you know, okay, let's, you remember in the diagram that I charted out our landscape of interactive pattern of computation, when it came to studying logical problems, I talked about the holy trinity of computation. that allows for us to envision a holy trinity of computation. Very kind of as a kind of fun thing is that we can think of this doctrine of Trinitarianism,

of Trinity, exactly like Christian Trinitarianism in computation, where you have one God that is manifest in three persons, the Father, the Son, and the Holy Spirit. We together form the Holy Trinity. We can have an equivalent of this in computation, where we have a doctrine of computational trinity that holds that computation manifests itself in three forms proofs of propositions programs of a type and mappings between structures these three aspects give rise to three sects of

worship, basically. Logic, which gives primacy to proofs and propositions. Languages, which give primacy to programs and types. Categories, which gives primacy to mappings and structures. Now, the central dogma or doctrine of computational trinity holds that logic, languages, and categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment. Each aspect provides insight that comprise the experience of computation in our lives in the broadest possible sense.

The Holy Trinity of computation entails that any concept arising in one aspect, in logic, in mathematics and in computation, in programs, in proofs, and in structures, should have meaning from the perspective of the other two, exactly like the Holy Trinity. If you arrive at one insight or discovery that has importance for logic, language, and categories, then you may feel sure that you have elucidated or you have made a discovery an essential concept of computation, you have made an enduring, basically scientific discovery that can correlate, can bridge these gaps

between mathematics, logics, and computation. So in this sense, advances in understanding of computation arise from insight gain in many ways. Any data is useful and relevant in this respect. but their essential truth does not depend on their popularity. Logic tells us what propositions exist, what sorts of thoughts we wish to express, and what constitutes a proof, how we can communicate our thoughts to others in the simplest way. Languages, in the sense of programming at least, so artificial languages, computational languages, tells us what type exists, i.e. what computational phenomena we wish to express,

and what constitutes a program, how we can give rise to that phenomena. in the sense of category theory, tells us what structures exist, what mathematical models we have to work with, and what constitutes a mapping between them, how they relate to one another. In this sense, all three have ontological force. They codify what is, not how to describe what is already given to us. In this sense, they are foundational. If we suppose that they are merely descriptive, we would be left with the question of where these previously given concepts arise, leading us back again to foundations.

Of particular interest here is that a type system is not under this conception an arbitrary collection of conditions imposed on a previous given notion of program, whether written with horizontal lines or not. It is rather a way to say what programs are in the first place, and what they mean as proofs and as mappings. So the holy trinity of computation in fact gives you a fundamental account of what a program is and what computation really is at deepest level. This correspondence between mathematics, logics, and computation, between

proofs, and programs is also called in widely known as the so-called Curry-Howard-Lambeck isomorphism or correspondence. So it's isomorphism in a very trivial sense. It's not the kind of isomorphism that you have that kind of straight isomorphism, rules of isomorphism, but simply shows fundamental correspondence between objects of mathematics, objects of logics, and objects of computation.

The people who were behind it were Curry, Howard, and Lambeck. Reha Award, they worked on the correspondence between logic and computation, between proofs and programs. Lambeck, Joachim Lambeck worked on category theory and the correspondence between structures and computation and logic. Lambic especially is an obscure figure, just for you to make

a note of it. He's kind of like, if you're familiar with category theory and William Louvert, he's kind of like Louvert. He made some revolutionary insights in the field of algebraic topology and modeling and giving an algebraic definition of languages, whether natural language or formal languages. And through this kind of investigation, he saw these correspondences between basically structures, proofs, and computation, programs, simply. So I'm going to outline the basic correspondence

between logic, language, and categories by examining their structural properties. I'm not going to go into any details for now, because it just will be too much. This is precisely because this Corrie-Houart-Lambeck correspondence, the so-called Holy Trinity of computation, It's very intuitively, it can be grasped, but technically it's extremely difficult when you get into the level of technical details. I will try to throughout the course of the next sessions, I'll try to bring out different aspects of this fundamental correspondence to the forum as we move forward. So first thing to know is that the fundamental notion of logic

is that of entailment. And if you remember in the last session, we said that entailment was usually notated by a double arrow in the classical logic sign of implication. Gerhard Gensen modified this into a sequence interpretation of entailment. The arrow became a turnstile. So let me share the screen again.

Okay, can you see the screen? Yeah. So as I said, the fundamental notion in logic is that of entailment or implication. Written P1, P2, Pn entails P. What really entailment is, is that Brauer for the first time when he laid out the foundation of intuitionistic logic, came up with a famous dictum that entailment

is really a construction. A proof is always a construction. A construction is the ultimate object of mathematics for excellence or logic. When we think of construction in this sense or derivability, entailment as construction, proof as construction, then we can also think of this construction as a program, in fact, a program needed for us to construct P from P1, P2, P3, Pn, or derive P conclusion from its premises.

So in the formula for entailment, it expresses derivability of p from p1 and pn. This means that p is derivable from the rules of logic, given the pi as axioms or premises. In contrast to admissibility, more details about this admissibility hopefully in the next session. This form of entailment does not express implication. In particular, an entailment is never vacuously true. Entailment enjoys at least two crucial structural properties, making it a preorder.

P entails P, P entails Q, Q entails R, then P entails R. This is, you see, if I said that sequence, this is written in the sequence, sequence calculus format. Gerhard Gensen's responsible for it. As I said, the sequence format, all the sequence are taking the form of gamma turnstile delta. Gamma entails delta. And your proposition, your chain of deduction is written line by line, as you see. Each line is a conditional tautology, a conditional tautology.

In addition, we often have the following additional structural properties. Now these structural properties, I will talk about this shortly, more in details, are really the rules that capture the main properties, the main behaviors of classical logic. These These are called the structural rules. And what are they? One weakening, two, one contraction, two weakening, three exchange.

idempotency of entailment, monotonicity of entailment, and exchange. In the first one, we have P1, Pn entails Q. And P1, Pn, Pn plus 1 entails Q. So we have added an additional premise P n plus 1 to our formula and still what we have derived, we have yielded Q. So our conclusion hasn't been changed by the addition of a new premise

to R sequence. This is the first structural rule of classical logic. The second structural rule of classical logic, we have P1, Pi, Pi plus 1, Pn entails Q. Then the next line, We have P1, Pi plus 1, Pi, Pn, Pn entails Q. If you notice, simply the order of i and i plus 1 in the next slide has changed.

Nevertheless the conclusion is still the same. This is the rule of exchange. The order in most contexts does not matter. Simply, if we put pi plus 1 before pi, we still get the same conclusion. The third one, we have P1, PI, PI, PN entails Q. The next line, P1, PI, PN entails Q. Or

you can reverse it in fact. You can in the first line have P1, PI, PN entails Q and in the second line you can have P1, PI, PI again, PN entails Q. What does that mean? It means entails Q. What does that mean? It means that addition of new premises does not change the conclusion. So the first one was the expansion, sorry, not the addition of new premises, copying or reducing the number of copies of your premises does not change the conclusion.

So in the first one we had the addition of new premise does not change the conclusion and the addition of new premise was P and plus one. On the third structural rule, we have you can freely copy or subtract a number of copies of your premises and still you can get the same conclusion. So these are the three structural rules of classical logic. Briefly, these state that extra axioms do not affect deduction.

The order of axioms does not matter. Duplication of axioms or copying axioms does not matter. Now the thing is that these are, as I said, these are the properties, the structural properties or structural rules of classical logic. When in a logical system, one, two, or all of these structural rules are abolished and suspended, we get substructural rules. Substructural rules, accordically, is a logical system in which one or all of the structural rules of classical logic are suspended.

logic that we are going to discuss is considered to be a sub-structural logic because at least two of the main structural rules of classical logic are being suspended. You can no longer freely add new premises. You can no longer freely copy or subtract the number of your or axioms or premises. And I will talk about intuitive examples to see why these structural rules give classical logic too much power, too much power that actually makes classical logic extremely weak

in terms of how it can model computational complexities, how it can model semantics of of information processing, so on and so forth. And if you have already noticed, substructural logic then are fully resource sensitive form of logic, precisely because your premises, the number of your premises, the kind of your premises do matter. You can no longer freely add to them or copy them.

In languages, we have the fundamental concept of a typing judgment. What is a type exactly in type theory as invented by Peter Martin-Loeuf? Sorry, Peter Martin-Loeuf. I'm confused. A type, for now, for our purpose, you can think of a type as a set, even though type is not a set. In languages, we have the fundamental concept of a typing judgment.

X1, A1, and ellipses Xn, An entails M of type A, stating that M is an expression of type A involving variables Xi of type Ai. A typing judgment must satisfy the following basic structural properties. X of type A entails X of type A. So, remember we talked about this a little bit in the last sessions that the majority of classical examples in our multi-agent setting, dialogues, interactions

and stuff involved typing systems. You have the same type of players that can interact precisely because of this typing criteria. I'm not going to talk about this right now, but typing, typing you can think of this again as a constraint, as a fruitful constraint. But if you relax the typing constraint, you can get an untyped logical system. An untyped logical system, the intractive phenomena, the logical behavior, the computational

behaviors are extremely complicated in those. It's like a wild forest with so many surprised moves, behaviors, logical connectives, multiplicatives, et cetera. An example of untyped system is Jean-Yves Girard's ludics that I will talk in the third module. So we have, again, as I said, basic structural properties of a typing judgment is that X type A must entail X type A. Y type B entails N type C and X type

A entails M type B. Then your X type A must entail MY and type C. You may think of the variables as names for libraries, in which case the first states that we may use any library we wish, and the second states closure under linking with mxn being the result of linking x in n to the library m. In categories, we have the fundamental concept of mapping, as we talked about in kind of

introduction to categories theory in one of our previous sessions, morphisms. F, being a morphism between X and Y, maps X to Y between two structures, between two objects, x and y. The most elementary structures perhaps are sets and mappings are functions. Morphisms, if you remember, are functions. They are degeneralization, category theoretical generalization of the concept of function in mathematics. But it is more common to consider, that X and Y are topological spaces and F then in this sense is a continuous

function between them and this is in fact the way morphisms are being interpreted in algebraic topology mapping satisfy analogous structural properties identity map X maps X to X facing X onto itself and being the morphism of X to X and G being morphism to X actually sorry this is this is not correct this should be F the morphism of X to Y and G the morphism of Y to Z then

the composition of the two functions or two morphisms, G and F, is the morphism between the structure X and Z, one that maps the structure X to the structure Z. These express, respectively, existence of the identity map and the closure of maps under composition . They correspond to reflexivity and transitivity of entailment in logic, and to the library and linking rules of languages or programs in computation.

As with types, one may expect additional closure conditions corresponding to the extra reordering and duplication axioms by giving suitable meaning to multiple assumptions. I will not go into this here, but numerous standard sources treat these conditions in detail, and I will try to make a few excursions to these in the next sessions. Now what is captivating about computational trinity is that it is integrative and unifying. Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, and every mapping to a proof.

Imagine a world in which the code is the map, in which there is no separation between the reasoning and the execution, no difference between the language of mathematics and the language of computing. Trinitarianism is the central organizing principle of a theory of computation that integrates, unifies, and enriches the languages of logic, programming, and mathematics precisely through this different constructive interpretation of entailment. Being understood in terms of mapping, being understood in terms of a sequence and being

understood as what? A program. It provides a framework for discovery as well as analysis of computational phenomena at the base of any phenomenon, whether pertaining to quantum physics, geometry, or natural language. An innovation in one aspect must have implications for the other. If an idea does not make good sense logically, categorically, and typically in the computer science or understanding of type, then it cannot be manifestation of, you know, in our

Trinity example of computation. So this was, you know, giving you a kind of like a brief idea of why the study of logical problems in this, now in this revised landscape, in this Trinitarian landscape is important precisely because it brings to the foreground these fundamental correspondences between mathematics, computation, and logics, between structures,

between types and programs, between proofs. So in order for us to get into this fundamental correspondence, also known as Corey Howard Lambic correspondence or isomorphism, which is simply the reinterpretation and refinement of Broward's constructivism for grammar logic. We need to introduce linear logic. We need to kind of get familiarized with the basic elements of linear logic and how linear logic can really index in a very surprisingly simple but elegant and powerful way these

fundamental correspondences. moving forward, any questions, any thoughts, commentary? Nothing? Do you think no? Sorry, Adam, I couldn't... I just wanted to give you some feedback to make sure that you understood that people

are still listening. Okay, okay. Sure, thank you very much. Okay, let me get back to the screen sharing again then. Sorry, I'm very stuffy today. Excessive sniffing. Did I just close the... Okay, we don't need the screen sharing right now. I will share the screen when it's needed. So again, let's get back a step back and look into this whole idea of implication or more

precisely entailment, for now just implication, and logics and how the constructive interpretation of this is given and how this leads to the fundamental correspondence of Coriomar-Lambeck. What does an implication A double R O B mean? A implies B mean. According to classical logic, A double R O B, A implies B, is true if and only if either A is false or B is true or both. This is regarded as specifying the meaning of implication because generally classical logic finds the meaning of a statement in the conditions of it being true.

According to the constructive logic, as developed by Brouwer and Hayting, a proof of A implies B is a, in fact, a construction, converting any proof of A into a proof of B. This is regarded as specifying the meaning of implication. Implication is construction as such in the Brauerian framework, in the constructive framework. Because constructive logic finds the meaning of a statement in what is required to prove it, not in the condition of the premise being

true. So because when we say that the condition, something is true, then how do we think that How is that we know it's true? The construction becomes the fundamental thing, the fundamental object in the Brauerian hating framework. It's the construction that gives us the proof, that verifies something, that gives us something to be true. And when it is about construction, It's about how we get from A to B and how we can derive or alternatively how we can construct B from A. Obviously, you can already see this idea of construction as derivability

or as how to construct from an element, something more complex, requires addition, introduction of additional components to logic, resources, interaction as we will talk about, you know, a good account of how a logical process functions sequentially, you know, in the kind of small step way of the chain of deduction. So already we can see that this shift from the kind of

formal classical logic to the constructivist framework of Brauer and Haitin exposes us to a lot of the stuff that we were talking about, multi-agent systems, interactions, complications, resource sensitivity, so on and so forth. And linear logic, as we will talk about, really is the kind of refinement of the constructivist framework and refinement of classical logic in this sense. Two close relatives of Brouwer-Hating interpretation of implication, the constructivist interpretation of implication, are Kolmogorov's interpretation in terms of problems and the Kari-Howard interpretation

in terms of types. Kolmogorov regarded the statements as representing problems and interpreted A implies B as the problem of reducing B to A, that is, solving B given a solution of A. Cartier and Howard, on the other hand, pointed out a correspondence between logical systems and type theories, where propositions correspond to types which can be identified, as I said for now, as sets, even though types are not set. Don't tweet that types are sets. A implied B is the type

of a function from type A to type B. If we identify propositions with the type of its proofs and identify constructions with functions, then the Curry-Howard correspondence amounts through the Brouwer-hating interpretation. So, you know, the kind of a historical timeline of Kari Howard correspondence is more of a later development, and it can in fact be seen as a refinement, as a further development of the interpretation of implication, given

Then by Brouwer and Hayting, simply the constructive account, and Kolmogorov's interpretation of implication in terms of problem, reducing conclusion to premises, simply taking the conclusion as a problem that needs to be solved by its premises. The Curry-Howard correspondence, as I said, has been of interest hugely in theoretical computer science, especially in the past decade or so. Where one deals with data types and where A implies B could be the type of a procedure

with a formal variable of type A and value of type B. So, in this, again, in this Holy Trinity model of computation, we have two key concepts, construction and procedurality. And these are coming hand in hand always. Procedurality is the introduction of new constraints, hence indexing new phenomena, new behaviors, and construction is, you know, really captures the correspondences between morphisms, functions,

and proofs. The preceding comments about implications have analogues for other connectives. For example, the conjunction A, conjunction B is defined classically as being true whenever both A and B are true. However, it is defined constructively by saying that to prove A conjunction B, A and B, one One must give a proof of A and a proof of B. Proof itself is the ultimate object. This is the heart of Brouwer's dictum as the progenitor idea of the Cory Award correspondence. The

idea that all of mathematics, including the concept of a proof, is to be derived from the concept of a construction, a computation classified by a type. In intuitionistic mathematics, proofs are themselves first-class mathematical objects that inhabit types that may as well be identified with proposition that they prove. Proving a proposition is no different than constructing a program of a type. Like in a formula by implication. A, you have premises of certain type and the conclusion of the same type again.

So your proof is the computer program, the program, computational program that you, through which you can construct your conclusion of this type from the premise of the same type. In this sense, logic is a branch of mathematics, the branch concerned with those constructions that are proofs. Mathematics is itself a branch of computer science, since according to Brouwer's Dictum, all of mathematics is to be based on the concept of computation. But notice as well that there are many more constructions than those that correspond to proofs. Numbers, for example, are perhaps the most basic ones,

as would be any inductive or co-inductive types, or even more exotic objects such as Brouwer's own choice sequences. From this point of view, the judgment M belongs to A, stating that M is a construction of type A, is of fundamental importance, since it encompasses not only the formation of ordinary mathematical constructions, but also those that are distinctly intuitionistic, namely mathematical proofs constructively understood. So in Corey-Howard's framework proposition as types, the Browerian interpretation of A and B, A conjunction B, conjunction becomes a Cartesian product of types of A and B, type

of A and type of B. It becomes a Cartesian product of the two conjunctions. And this This is usually denoted in linear logic by a tensor sign. So now to linear logic. The first central idea of linear logic introduced in the mid-'80s by French musicians Jean-Yves Girard is to keep track of how often a hypothesis is used in deducing a conclusion equivalently via the Corey Howard correspondence, one keeps track of how often an input is used in computing

and output. Remember that proofs are now constructions. In construction you can think of this as type, functions of type, types of functions, or morphisms. So if linear logic is about how many times you use premises in order to construct a conclusion, you can also think of this as how many inputs you use in order to produce a certain output. And now that's the central idea of linear logic. You remember that the structural properties, especially two of structural properties of classical logic emphasize on the idea that you can duplicate

or you can add premises freely. But if you suspend those structural rules, then obviously you can have a fundamentally different logical systems capturing extremely interesting computational phenomena precisely by virtue of this Curry-Halward lambda correspondence, but also extremely interesting phenomena in category theory, namely mathematics, the relation between the structures, how you map one structure to another, precisely because you can no longer duplicate, copy, and add resources freely. You can no longer think that you have infinite amount of inputs to produce an output.

You can no longer have infinite amount of premises or you can freely manipulate premises to construct or to prove a conclusion. So, this idea that keeping track of how often a hypothesis is used to deduce a conclusion And again, by virtue of the Corey Howard correspondence, keeping track of how often an input is used

in computing and output, this and related concepts in linear logic can be thought in the context of ability to perform actions rather than knowledge of facts, because knowledge in a logical sense, is normally permanent and reusable, while abilities can be constrained in the sense that someone who can do A and can do B may not necessarily be able to do both. Although it is unclear in the context of classical set theory, for example, what it would mean for a function to use an argument a particular number of times, the notion is considerably more clear in algorithmic procedures and memory management, and especially in logic.

So linear logic is really this shift of logical system from interpretation of sequence, namely judgment in terms of knowledge in a logical sense, not the epistemic sense, in terms of knowledge to interpretation of proofs or constructions in terms of abilities. Abilities require for you to construct a proof, to construct a conclusion, to produce an output, to generate a certain structure. The formal development of linear logic is based on sequence calculus, which

as I said is denoted in the most basic form as gamma, turnstile symbol, delta. Gamma entails delta. In traditional logic, gamma implies delta or entails delta, where gamma and delta are lists of statements or formulas. Means that the conjunction of the statement in gamma, in your premises, entails the disjunction of the statements in delta or conclusions. So you can write the sequence of, decompose the sequence of gamma turnstile delta to, for example, A conjunction, A1 conjunction, A2 conjunction, A3 conjunction,

An, turnstile symbol, entailment. Then on the right side of your sequence, you can write B, your conclusion, B1, disjunction B2, disjunction B3, disjunction Bn. So this is how you can think of a sequence. The first step toward linear logic is to establish the rule of contraction, also known as idempotency of entailment, which states that one may derive the same consequences from many instances of a hypothesis as from just one.

That was, that we showed it as simply duplicating your premises. For example, you have p, let me share the screen so you can see this. The first step to our linear logic is to establish the rule of contraction, also known as idempotency of entailment, which is stated that one may derive the same consequences from many instances of hypothesis as from just one. Example Pxx implies Q can be derived from Pr implies Q. In the sequence format, the idempotency

of entailment or rule of contraction is as follows. Gamma A A, these are your premises, implies delta. You can have gamma A implies delta. In a nutshell, contraction formalizes the idea that hypothesis can be reused without restriction. One hypothesis A is good as two copies of it. The removal of the contraction rule results in a system called affine logic. In it, a sequence, gamma implies delta, carries the additional information that each hypothesis

is to be used at most once. So you are no longer free to reuse your premises in order to derive a conclusion. You can use them at most once. Resource constraint, as you see. Linear logic is obtained from affine logic by also further suspending the rule of weakening or monotonicity of entailment. What is the monotonicity of entailment or weakening? is that the hypothesis of any derived fact may be freely expanded with additional assumptions. P implies Q can be expanded as Px implies Q. Simply, you add an additional premise to

your sequence and still you have the same conclusion. You can think of this as syllogisms that can admit additional premises. For example, all bachelors are clumsy, or John is a bachelor, then John is clumsy. So you can add, for example, add some sort of absolutely irrelevant premise to your sequence. For example, all bachelors are clumsy, John is a bachelor, pigs are mammals, implies John is clumsy. You have an irrelevant premise to your sequence and you still get

the same consequence. This is one of the structural rules of classical logic. Now linear logic suspends this one as well. You can no longer add freely new premises to your sequence. Again, in sequence format, for weakening, we have this, as you see. Gamma implies delta. Gamma addition of new premise A still implies delta.

The weakening formalizes the idea that a hypothesis can be ignored. Addition of new premise can be ignored. In linear logic, gamma implies delta requires that each hypothesis in gamma, in your premise, premises is used exactly once. So the first one was in linear logic or affine logic. You have each premise is used at most once. This is in the second criteria of linear logic by suspension of the monotonicity of entailment is that each hypothesis in gamma, in your set up premises is used exactly once. There is also the non-community version of linear

logic which I don't talk about this. In which the third is structural rule, the rule of exchange is also suspended. Remember that the rule of exchange was that, for example, you swapped the order of a PI and PI plus one and so you were getting the same conclusion. So you have gamma 1, A, B, gamma 2 implies delta. You have gamma 1, B, A, gamma 2 implies delta. You have swapped the order of A and B, premises A and B, in your gamma, in your set of hypotheses, and you still get the same conclusion. Then gamma implies delta requires that the hypothesis be used in the order listed.

So the first two, the suspension of monotonicity of entailment, contraction and weakening, were resource sensitivity in a kind of a very strict sense of the amount of resources being used and how they are used. Now this is about the order of your resources. suspension of the third one in the non-community version of linear logic, wherein you suspend the exchange rule of classical logic. The order of resources matter. The order of premises matter. And hence, construction requires the order of how resources are being consumed.

Again, back to our kind of like a PetriNet, it is kind of very, corresponds neatly with PetriNets, the order of how resources, where resources are being consumed does matter. And again, think of this through that analogy, that comparison that I made, Petri Nets, how for example you could imagine and model a kind of state transition in your physical

system, how resources are being consumed, and how your formulas are being consumed in the construction of a conclusion, or how your program consumes inputs to produce a certain output. Now, Girard, as I said, introduced linear logic in mid-80s, but since then he Now, Girard, as I said, introduced linear logic in mid-'80s, but since then he has extensively revised the main concepts and even interpretation of linear logic. And so many logicians and computer scientists have made, again, refinements to linear logic,

giving rise to more robust logical systems that can index interactivity, semantics of information, processing, you know, asynchronicity, so on and so forth. As we move forward, I will start to talk about these refinements, additional refinements, and why is it that these additional refinements were made. The linear logic insistence that hypothesis be used just once raises a question about the meaning of conjunction. Should one use A and B constitute one or two uses of A conjunction B, A and B? Girard's answer is that there are two sources of conjunction for which he

introduced the notion A tensor B and A ampersand B. One use of A consistence of a use of A and a use of B. One use of A ampersand A and B consists of one use of A or one use of B, whichever the user wants. So in classical logic, you have this as having, if you remember, for A conjunction B to be true, you need to have A to be true and B to be true. You have the sense of both A and B. You have both resources. In linear logic, it's a refinement of this

adjective of this word or this concept both, having a both. In one sense you have, you know, very straightforward, both A and B and in another sense you have one use of A and one use of B. All you have, and that's denoted by A ampersand B, it's all you have is the the free choice between A and B. I will clarify this in concrete examples as we move forward. If you have noticed, already by laying out a logical system in terms of resources, we have a startup to adopt implicitly interactive concepts. Here the interaction between hypothesis

and its user. And especially in the case of A&B, we can see this very clearly. I have the choice of, for example, in classical logic, and this is Girard's famous example, I have one dollar. In classical logic, I can buy with this one dollar, one dollar is my premise, I can buy two conclusions, a pack of Marlboro and a pack of Camel. Of course this doesn't make sense in the resources, in the real world it doesn't make sense. You can't have it both ways. You know, leaving a logic where this idea of having, idea of both is refined, it becomes

two. The conjunction becomes two, tensor and ampersand. The tensor is resource sensitivity. You need to have two $1 bills in order to buy, for example, a camel and marlboro, each costing $1. The ampersand is the idea that you have one dollar, obviously you can't buy both. You can freely choose to spend your money toward either a pack of camel or a pack of

model. This is A&B. A tensor B is the idea of resource sensitivity. And A&B is the idea of free choice of resources. I can spend my resources freely toward this one or that. I don't have sufficient resources to buy both. All I can buy is either Camel or Marlboro, And I have the free choice.

These two conjunctions are governed by the rules of inference. Gamma entails A, gamma entails B, gamma entails A ampersand B. The next one, gamma entails A, delta entails B. Gamma and delta entails A tensor B. This rule would be equivalent in the presence of contraction weakening in classical logic. The interactive idea that I alluded to within a user requesting information, shopping packs of cigarettes, and or in our, we can also think of how you spend formulas

to construct premises to construct a conclusion, how you spend inputs to construct an output. So the interactive idea that I alluded to between a user requesting information on hypothesis is supply information or more generally query and reply. Leads to a second idea of linear logic, namely linear negation, the operation that interchanges questions and answers. An answer of type A, top sign, is a question of type A and vice versa. So linear negation is the best way to think of this is the interchange of rules in our

games, player, opponent, system environment, algorithm environment scenarios where I make one move and then you make another move. move, the opponent move, is a negation of my move. And that interchange of role going back and forth between the two is denoted through a linear negation, a orthogonal sign. And you can see behind this there is an intuition of dialectics. The ultimate sign of negation is the dialectics, is the conversation, is the interaction, the

interchange of rules. That is, a refinement or generalization of the concept of duality in mathematics. And there have been several attempts to model semantically this sort of interaction in linear logic framework by people like Abramsky, Andreas Blass, Jagadason, Japaridze and other people. I will talk about Blass, Abramsky, Gheorghe Japaridze's semantic, interactive semantics

of linear logic that allows us to kind of develop really a strong, powerful logical computational models for natural language, formal systems, complexity, theories, and so on. Especially Georgi Javaritza's program is extremely interesting precisely because he develops a computability logic in which he reconstructs Church's lambda definability, theory of computability, solely on the basis of resource management in linear logic, in game semantics. A program,

A function can be said to be computable if it accurately uses all the resources. It has a robust resource management. This is in a logical sense. And this is like the central idea behind Jafar Itzis' computability logic. reinterpretation of lambda definability and theory of computability based on resource management, resource sensitivity. Resource in a logical computational sense becomes the main object of computation in

this sense. becomes basically the building block, even more fundamental than the theory of effective calculability and theory of computability as laid out in the canonical sense of mathematical functions. Because functions themselves can be interpreted at a more fundamental level according to their resources, how many inputs they use in order to construct an output, generate an output. A linear negation is a refinement of generalization of De Morgane laws or mathematical duality in general.

What are De Morgane laws? The negation of a conjunction is a disjunction of negation. And the negation of a disjunction is the conjunction of the negation. Negative of and, or negative of, or and. And not A and B is the same as not A or not B. Not A or B is the same as not A and not B. Sorry, I completely forgot. Am I sharing the screen with you? Can you see the screen? Yeah, we can see it. Oh, okay.

Two essential ideas at the base of linear logic, accordingly, are resource consciousness and a linear negation. The former refers to keeping track of how often a hypothesis or an input or premise or axiom is used in deriving a conclusion or constructing an output. The latter is a duality, a linear negation, a duality, an interchange of role in a two-player setup. in a multiplayer such as a multi-agent system can be said not in terms of interchangeable but in terms of permutation and that's a different topic that we'll cover later on

the latter is duality which although related to classical true-false duality is sufficiently different to require my opinion interaction as an underlying intuition so and the reason that duality in mathematics can be understood as an interaction. How linear logic accurately represents this duality leads to really massive amounts of interactive models of computation, to just one interactive pattern of computation, but myriad of interactive models of computation

depending on how you interpret duality. For example, whether you are interpreting duality in the sense of interchange of role or permutation of roles, whether you interpret dualities in terms of choices, in terms of asynchronous, desynchronous, and so on and so forth, exactly like our multi-agent setups. The idea is that in order to deduce both conjuncts, sorry, some of the symbols are missing here, And the conjuncts are these two, A tensor B and A ampersand B. One was about, as I said,

a strict resource sensitivity, and the other one was a free choice of how to spend my resources. The idea that in order to reduce both conjuncts, one needs enough hypotheses to reduce both of A and B separately, while to deduce the user's choice of one conjunct version A ampersand B, one needs only enough hypothesis to deduce at the user's demand either one of the conjuncts. The two introduction rules for conjunction would be equivalent in the presence of weakening and contraction, but in linear logic they are genuinely different. The part of linear logic described so far is sufficient to suggest why it is difficult

to produce a natural semantics for the logic. The concept of resource consciousness was described in explicitly proof-oriented terms involving the number of uses of hypothesis. The concept of resource consciousness was described in explicitly proof-oriented terms involving the number of uses of hypothesis in introduction. It is not clear how one could introduce, however, resource consciousness into classical semantic notions." Although this has been done too recently by people like Abramsky.

What would it mean for a sentence, basically, he introduces resource consciousness, in fact, to classical logic. What would it mean for a sentence A to be semantic consequence of a list of sentences used exactly once each? Semantic consequences in the usual sense simply doesn't use hypothesis as proofs to. This difficulty is reflected in the fact that although linear logic has a well-developed proof theory, its semantic is still in experimental stage and the focus of a lot of interesting projects in computer science, especially regarding the underlying computational intuitions behind

the syntax-semantics interface, so-called hard problem of formal languages and natural languages, how you make a bridge between syntax and semantics, especially with regard to linear implication and linear dualities. The intuitive semantic situation improves somewhat if we apply the Corrie-Haward isomorphism and proposition as type paradigms. Here, as I said, the formulas of a logical system are interpreted not as truth value, but as types. Implication from A to B, A implies B, is interpreted as a set or type of function from A to B,

conjunction as Cartesian product and disjunction as disjoint union. In this schema, then the central issue is to keep track of how often a function uses each of its inputs in producing its outputs, how many times in a construction we use axioms, premises, or hypotheses to construct a conclusion. So intuitionistic linear logic is what we are going to introduce. But first it would be useful for you to understand some of these symbols at least in some sort

of vague connection with the symbols of classical logic. So in classical logic we have implication with arrow, in linear logic we have a lollipop symbol. Really, it reads A implies B. In linear logic, it reads A lolly B. Negation, you have negation sign A, whereas linear negation is A orthogonal or A top sign. And as I've said, it's about duality or interchange of roles, at least in a two-player framework.

Fusion in classical logic, then you have, in linear logic, you have tensor sign having both A and B. Conjunction, you have A conjunction B in classical logic, in linear logic, the conjunct then becomes A ampersand B, the free choice between A and B. The disjunction in classical logic becomes A multiplicative disjunction B. So, The first symbol that we need to learn and understand is linear implication. Linear implication reads a lollipop B, indicates that the resource A is consumed and the resource

B is produced as a result. This is the resource conscious counterpart of turnstile symbol entailment in our sequence calculus. What is this? Sorry for bad spelling. Hard in typing. From a constructive perspective, A lollipop B then means can we construct or derive B by using A exactly once? So, we have two things. the Brauer-hating interpretation of entailments plus resource sensitivity, the amount of premises or axiom or inputs we can use in order to generate an output.

If, and you remember, if we can only use an input or a resource exactly once. This happened when we, this new interpretation of entailment or implication resulted when And we suspended the rules of contraction and the rules of weakening, idempotency and veracity of entailment. For example, for a given function called eating, you have hungry lollipop food indicates that

the act of eating, simply understand it's a function or construction, has the effect of removing a state of being hungry and generating a new state of being food. Again, an input has been used, consumed, and produced a new state. You can think of this in terms of Petri net. A marking was consumed and produced and moved the marking to an output state. And in this implication, you need to account for your resource, how your resource is being spent. In a computational reading, the name eating refers to the action.

Remember that this whole idea of structural logic to substructural logic, classical logic to linear logic was also a shift of landscape from knowledge of facts, permanent reusability of our database, to abilities, abilities that are now all resource constrained. You need to take, you need to account for your resources. So in computational reading, the name eating refers to the action of eating and has the linear logic type hungry volume of food, which specifies the behavior of the action. See the type of the action, the behavior, the behavior of the action. Eating is your type of function in the type system theory,

computation, the Corey-Hawart-Lambert correspondence. This shows the notation we use for relating planning actions to their logical specification. We can omit the action's name when it is not of interest, when basically we are, we do not want to talk about their type. Now, as I said, as soon as we introduce the ideas of resource sensitivity, abilities, precisely because resources can be chosen either from the environment or from the system,

from the player or the opponent, verifier or falsifier, precisely because of this constraint on resources. In the broadest possible sense, you are already within an interactive framework. And this is the whole idea. in the most basic intuitionistic linear logic has intractive implications. So an intractive interpretation of linear implication is that the players play A interleaved with B, with players' role being reversed in A. The opponent must move in one or both components whenever it is his turn in at least one component.

But when it is the opponent's turn to move in both components, he must move in one of them. This sort of compound game is a natural way for the proponent to defend the claim, I could win B if I were showing how to win A. In effect, the players are playing B, but the proponent may, whenever he wishes, temporarily suspend the player of B to consult an expert oracle, a referee, about how to play A. The consultation consists of the proponent acting as the prop opponent in a play of A while the oracle, the referee, acting as proponent in that play. It shows him how to win A. This This description, in terms of oracles, kind of a computational interactive setup, is essentially

the same as the previous description of A, a Lollipop, linear implication B, except that in the latter, it is the opponent, not an oracle, that acts as a proponent in the play of A. That difference has no effect as far as winning strategies for the proponents are concerned. Now, linear implication has this internal form that can be, you can simply, exactly like a Duh-Morgan dualities, how you can transform Duh-Morgan rules to one another, logical formulas, interpret them according, decompose them, recompose them according to other logical connectives, you can rebuild linear implication with a multiplicative conjunction and linear

negation. A, multiplicative conjunction, linear negation B, in parentheses, linear negation. Now what is multiplicative conjunction? Multiplicated conjunction A tensor B indicates that both resources A and B are present. Example, a $1 bill tensor multiplicative conjunction. And $1 bill yields or implies or generates a hot drink. that using up to $2 can produce a hot drink. For example, the cost of generating three cultures in our civilization game example is a wine tile and a monastery, which I can

buy with 200th faith. When I have both the resources, a wine tile and 200th faith, then I can say one wine, 10th or 200th faith, lollipop, three cultures. So this is a multiplicative What is the semantics of its intractive import? A play of A, multiplicative conjunction B, consists of interleaved runs of the two constituents, A and B. Whenever it is the proponent's turn to move in one or both constituents, he must move there. When it is the opponent's turn to move in both constituents, he must choose choose one and move in it. In versions of game semantics where the criterion for winning

must be specified the opponent wins a play of A tensor B if and only if he finishes and wins at least one of the two sub games and otherwise the problem wins. The third symbol for the third sign. And the second conjunct in linear logic is additive conjunction. So you have additive signs and multiplicative signs in linear conjunction. Additive conjunction, multiplicative conjunction, additive disjunction, and multiplicative disjunction. Now additive this junction. Imagine when we say I have two $1 bills, it only means free choice. In

that case, we are dealing with additive conjunctions, symbolized by ampersand. A ampersand B means one's own choice between A and B, but not both. Like suppose I have generated enough culture in our civilization, now I have to spend my culture on buying a cultural policy. In this case, I have the choice between liberty and tradition, but not both. Secondly, it also implies that an action has been requested by the game, which here can be represented as the opponent. Not me. I am only free to perform one of the two actions that must be executed for the game to move forward. either spending the cultural resources on selecting the tradition tree or the liberty

tree, but not both. Either choice is mutually exclusive. The intuition here is that the formula A represents, for example, a server capable of providing to some user elements of type A. If A is of the form A1&A2, then before the server can provide an appropriate element, the user must specify which A, I, which type of A he wants an element from. Now, additive disjunction.

So additive conjunction was an ampersand and additive disjunction is a circle plus. A circle plus indicates that either resource A or B is present, but not both. A lottery ticket, a lollipop, win, additive disjunction, lose. Means that a lottery ticket can be used to make one win or lose, but one cannot choose the outcome. So you see the difference between additive disjunction and additive conjunction is that In the additive conjunction, you had the free choice, but in this one you do not have the

choice. In comparison with A&B, namely additive conjunction, in additive disjunction, the server may choose arbitrarily which AI to provide an element of. It's the game that in fact gives you, orders you which action you need to be performing. It decides, it's basically, it's the environment that decides completely and ultimately. Compound formulas, like for example, A ampersand B, additive disjunction C ampersand D, requires

a slightly longer interaction between server and user, verifier and falf-fire, player system opponent environment. The server must tell the user which side of Circle Plus or additive disjunction it intends to provide an element of so that the user can choose one side of the appropriate ampersand. You see, so the additive disjunction, the Circle Plus is no free choice. The ampersand is the free choice. So if in that R formula, it's the server that decides for you, for the user. Either go for A ampersand B or C ampersand D. Now when it

comes to the A ampersand B or C ampersand D, now it's the user who can choose between A and B. So you can see these formulas in this way. After which the server finally provides the required element, unless of course A, B, C, and D contain more additive connectives, in which case an even longer protocol or interaction or dialogue between server and user or player and opponent results. Thus, consideration of the additive connectives automatically leads to a semantics with at least some game-like aspects, interactive aspects.

Game A additive conjunction ampersand B is played by first letting the opponent choose one of A and B and then playing the chosen game. A additive disjunction, circle plus, is the same except that the initial choice of A or B is made by the problem. Multiplicated disjunction. So as I said, you don't have only additives connected, but you have multiplicative connectives in linear logics. It is denoted as A, invert ampersand B, reads A par B. Invert ampersand linear logic is

called par operator. A par B. Par is a doom organ dual of A ampersand B, named additive conjunction. Dually, in A par B, play continues with both games in parallel. If it is their turn in either game then it is their turn overall if it is our turn in both games then it is our turn overall if either game ends then play continues in the other game if both games and then the overall game ends if they have both won both games then they have one overall if we have won either game then we have one over one. Again, the internal form of A par B is parenthesis A linear negation,

tensor B linear negation, close parenthesis linear negation. So the difference between in disjunction and conjunction, in linear logic. In conjunction, they choose what game to play. In disjunction, we have control. Whoever has control must win at least one game to win overall. And this winning strategy, you can think of in terms of provability of formulas. That's the whole point in linear logic, in proof-theoretic account of linear linear logic or the construction of a certain output as your winning condition when you

are dealing with the concept of programs in computation. The other symbol in linear logic is bang or of course. is noted by exclamation mark a, of course a. What is of course a? You see, so far in linear logic we have complete resource sensitivity, precisely because we suspended the idempotency and monotonicity of entailment, the structural rules of classical logic. Now, of course a means that you have infinite amounts of resources of A. So, of course A indicates that one can

get an arbitrary number of copies of the resource A. Having, of course, T lollipop euro as a resource can be used to express the ability to sell T for a euro as many times as needed. A more refined interpretation of of course is that of course A means a form of A that can be used any number of times, including zero times rather than just once. Thus, the rule of contraction and weakening are admitted when the formula being contracted or introduced by weakening has the form of course A. So of course A, operator, of course operator in linear logic is for linear logic to again admit rules, structural rules of idempotency

and moturinacy of entailment, contraction and weakening when it is needed, when you basically require to have arbitrary amounts of resources. In the formulas as types interpretation, an object of type, of course, A, should be viewed as an object of type A stored in such a way that it can be repeatedly accessed by a computation. Sometimes in computation you find need to infinitely accept, without any restriction, something in order to construct something else. And that is denoted in the logic by a course operator. In the action interpretation, the ability of course A means the ability to do A repeatedly.

So when it is about abilities or actions in linear logical framework, it basically means that you can repeat an action as many times as you want. A logical approximation of course, you know, the internal logic of it is as follows. A is approximate to 1&A tensor 1&A tensor 1, 1 represents a singleton type, say a star. It is presented to allow non-use of A. So

this approximation means the type of sequences in which each term is either a star or an object of type A. Therefore, it can, like a stored element of type A, be accessed repeatedly. But there is no guarantee that each axis produces the same element. That's a really key issue. You see, in linear logic, I mean in classical logic, the whole idea of the structural rules of weakening and contraction, or the whole idea that you can, you know, duplicate as many copies of premises or axioms or formulas or inputs as you want always yielded the same

conclusion. That was the whole point. Now in linear logic, of course operator is, you you know, equivalent of this freeness of resource, as in classical logic. But the difference is that each time you, in fact, use this resource, even though you do not have any constraint on your resource, your conclusion would be different. Each time that you perform the same action, precisely because you can use it as many times as you want, this does not not mean that your conclusions will be left intact. So again, you see a refinement, which is more in line with how real constructions in computational,

mathematical, or even real concrete physical systems are. Different things that happen, different actions that are performed, doesn't mean that it leads to a monotonic result. In fact, resource freeness, in the sense that you can repeat an action or use a resource any arbitrary amount as you want, leads to non-monotonicity, If A represents having a dollar, then of course A could represent having an unlimited supply

of dollars rather than having one, arbitrary reusable dollar. It's another important thing to know about dollars, the of course operator. It's about unlimited supply of resources rather than reusable resource. Can you still see the screen? Yes? Yes.

The last one of our symbols is linear negation. It is denoted as a top sign or linear negation sign. A linear negation captures the idea of duality or interchange of roles, at least in a two-player setup. A linear negation is the game A with the roles of proponent and opponents reversed, going back and forth. This operation is very natural from the point of view of debates about the correctness of proposition. Because, you see, when you are thinking about proof or construction, you can, in fact, think it about a game. it. And that's how it should in fact be understood. You can think of as one player trying to prove

or construct a conclusion. The other one is trying to refute it. So linear negation is the dialectic between the two. It's really a function of negation, moves that are making against one another. And if approved cannot be constructed, meaning that the falsifier, the opponent, has the upper hands. It is considerably less so, linear negation is considerably less so from the point of view of clients and servers or from the point of view of abilities or actions. So these were the basic symbols and the basic concepts of linear logic.

There are still a lot left to talk about linear logic, but we kind of at least introduced a few of the motivations beyond the development of linear logic, how it can be used to unify mathematical, logical, and computational correspondence between proofs, types, and structures, the idea of resource sensitivity and abilities in linear logic as in contrast to classical logic. And with that, we can conclude today's session. Then next session I will go further in linear logic and start to get into how linear logic

can be developed in order to chart, map out interactive programs, come up with the different paradigms of writing, functional programming, understanding complexity, interaction, so on and so forth. Questions, answers, commentaries? No, I cannot hear you. You are still on mute. Yes. Hello. Yes, Tony.

Are we wrapped? Sorry, it's like, I thought Gregory was talking, yeah. I can't hear your mic. Can you hear Gregory? Okay. Yeah, I can't hear you. I think if you just refreshed the browser and came back in, it might fix it. So it's a good way to check it if you want to. Who's trying to speak? Yeah, correct me, right. Sorry, Reza. No, it's absolutely okay.

Juan, do you have any questions? Wrap it up or no? while we wait for a girl. Oh, here you. Hello, can you guys hear me now? Yes, we can hear you now. Ah, great, okay. So, sorry if this question is a little bit out of stick with where we are. Yeah, it's now, now the session is 3.30 a.m. for us. So, so it's getting harder, but it's all right. This is brutal torture. I know. linear logic in the middle of night.

I know. And then also being absent is his own kind of torture. Okay, so going back to concurrency, and maybe this is something you covered when you first started talking about it. I may not have been here. I'm still a bit confused between these three senses. Concurrency, synchronicity, and parallelism. Like they all are like they don't all denote the same thing. No. Parallelism can be understood as fully synchronic framework,

but also there is an additional criteria that makes it distinguish from just synchronicity. It's the idea that at the same time two processes are moving. And it's not either, I mean, basically you do not have any, you do not have a kind of constraint of either or. Right. Would it also be that like synchronicity carries with it like a timestamp? Yes. Oh, absolutely. Parallelism could be different timestamps. It doesn't make it rhyme. Yes, yes. But also you can have fully synchronic parallel systems.

But really, it's the whole idea of parallel system is about not timing issue, but it's the whole idea of two processes are moving at, you know, They're concurrently running. Both moving. Yeah, both moving, concurrently running. And you do not have constraints of either or. Now, this is synchronicity adds the constraints of time and parallelism. Concurrency, so parallelism is, as I said, is a special case of concurrency that can come against synchronic and asynchronic. Now you can have a concurrency of a synchronic concurrency,

where basically concurrency, the difference between concurrency and parallelism is that you have either or constraints. But also there are a synchronic concurrent systems where, you see parallelism always imply, imply, that there is a coordination going back and forth between your players, between your states of transition, between your processes. Hence they are parallel. Basically parallel precisely because There is an implicit interaction between going on,

between this process and that process, even though they are working at different timestamps. But concurrency, the way that is technically defined, means that you do not need to have this explicit interaction. You do not need for your players to explicitly interact. I can play on the other side of the continent. you can play on the other side of continent. We might not have any interaction whatsoever, explicit interaction with one another that constrains us to one another. But still, nevertheless, there is a logic of resource management precisely because we might be bound by the resources of our continent,

how we are using it. It's a good civilization game. We are like in the same, using the same tiles. I mean, basically there are distribution of tiles of resources. We might not have, our civilization might not have any explicit interaction for time being with one another. But there is this resources boundedness to our tiles shared in our continent. And, in fact, Abramsky shows, proves that parallel systems in either synchronic or asynchronic framework are, again, special cases of asynchronic concurrent, the most general form of dynamic

processes. Because even at the asynchronic concurrent systems in which players do their own things at different times and stamps, still there is a flow of information that might not exhibit an explicit interaction between players, like going back and forth within players, but nevertheless there is a flow of information. So a synchronic concurrent system is considered to be the most general case of dynamic processes, whereas parallel synchronic systems are considered to be the most special case.

I find this really interesting. Would you have a recommendation for a text or a particular thinker? Or should I just Google it? Yes. A good example of which I will talk about this paper especially is an essay by Samson Abramsky about game semantics where he talks about a copycat strategy. A copycat a strategy, if you are, I think you were absent in previous sessions, this idea that how to

beat one, two grand chess masters at the same time. So a copycat copies the move of one grand chess master against another, and no matter which one is winning, the copycat is always the winner. The copycat here is that you can understand these two chess masters as two basically concurrent processes, concurrent strategies, concurrent players who might not have any interaction. But the implicit figure, the shady figure of the copycat who moves, steals the move of one copied against another, can be understood as the flow of information within the concurrent games. So basically the copycat shows the flow of information,

conservation and transformation of information in the general case of asynchronous concurrent games, showing that even the asynchronous concurrent games have interactivity. Right. That's fascinating. I realize it's quite late, so I have a couple of administrative questions. How many more sessions do we have now? Where is the end of this module? I think this was, let's not talk about the end of this module, because this is not really the end of the module. But we think, we can imagine that today is the end of our module. But we have four, which basically we are going to talk about constructed landscape of interactive

theory of computation, talk about game semantics and stuff, and talk about the implications of this interactive theory of computation for AGI, National Intelligence, National Languages, et cetera. JOHN MUELLER, Yeah, I think I'm going to be. That's how you go, Tony. Thank you. I think technically this is the eighth session, but yeah. But what Reza's saying is it doesn't really mean that we're finished with the module. I think we are far beyond. It's actually not the eighth session. I think it's the tenth session, really. But nevertheless, we think there is our eighth session. Yeah, relative to the schedule, the intended schedule. Because I'm going to be in London for a few weeks.

So in that time, I'll be in a more civil state and not be doing linear computational logic in the middle of the night. Yeah. And last thing, Roza, did you get my email about? ROZA KUZANIUZIUKI- Yes. I still need to. Yes. Yes, absolutely. Yes. I read. Yes. Excellent. Thank you. ROZA KUZANIUZIUKI- All good. No worries. That's all from me for now, I think. ROZA KUZANIUZIUKI- OK, superb. And Juan, it would be great if you can send me some dates. Sorry, I didn't get to the dates that you were suggesting. So we can coordinate something in the coming week, whenever you are free. We can talk about your assignment.

It would be fantastic. And if you don't have any questions, We can conclude this session then. Tony, anything from you? Welcome. TONY CHANDALEEVYSKI- No, I think that's good for me. OK, superb. Bye, guys. Bye.