Okay, so let me first recall some of the things we saw yesterday. So the first result I presented yesterday was that the small model property in for for two variable fragment of first of the logic. In fact, in our construction, we started from an arbitrary model of a formula phi and constructed a new model, whose domain was a subset of the domain of the original model. The one types of elements were retained from the original model and the only only some two types have been exchanged. It's modified. So in fact, this construction guarantees also some some additional properties that the set of one types realized in both structures unidentical. All the types which are realized in the original structure are also realized in this new small model and each non-royal type recall that the type is royal if it is realized in a structure exactly once. So each non-royal type from from the original structure is realized in this new structure at least twice. So this was the first the first property we obtained yesterday. Another simple result about two variable logic, which will be useful today. It's a very simple thing that if we have an arbitrary model of a formula phi, then we and we take an arbitrary non-royal one type realized in this model, then we can add additional copy of this one type to the model. So this is the second result from yesterday and result. Very simple observation in fact. And then we considered two variable guarded fragment with equivalence relations in guards. Let me recall the normal form of the formulas which we are interested in. So we may say that there exists an element satisfying something. We may impose restrictions on connections between pairs of connected elements. So we may say that for all x, y, if they are connected either by an equivalence relation, which is which equivalence relations are denoted by E i or by a relation which is not required to be equivalence. Such relations are denoted by R i or similarly. So for connected elements we may impose some additional restrictions on connections between them. And there are formulas which would say that some elements satisfying some atomic properties require the so-called witnesses. Yes, for all x, if x satisfies some atomic formula, then there exists y connected to this x either by E i or equivalence relation or non-equivalence relation. And this connection should satisfy some properties, yes? In my today's talk, yesterday we considered the general satisfiability problem for two variable guarded fragment of equivalence guards. Today we will consider the finite satisfiability problem. And to simplify the presentation, I will not consider the these two types of contracts. It has those contracts which may require witnesses connected not necessarily equivalently, yes, to an element. So in fact what we can say, we can only say about require witnesses inside equivalence classes. This simplification is not crucial. It is very easy to add these two types of contracts. It will be just left as an exercise. One another thing is notation I sometimes use by phi phi with superscript ek. I denote the fragment of this formula which is related to, which imposes something on something in equivalence classes of the relation ek, yes? So it contains all the formulas which have ek as guards plus those universal formulas guarded by non-equivalence relations because they also may restrict, they also may have influence on the shape of E 1 class, yes, because in this E i class, sorry, E k class, because in this E k class, of course, we may have another binary connections. One important restriction on our language is that we allow these equivalence relations only as guards, yes? So this is why we call this variant with equivalence guards. So E i relations cannot appear in these formulas psi. But in the formulas psi, we may have additional realizations of, additional, we may use those non-equivalence symbols. Another thing we observed yesterday is that in fact there is a close relation between models for formulas for two variable logic and equivalence classes in models for formulas of two variable guarded fragment of equivalence guards, yes? In a single equivalence class in a model of GF 2 plus E g formula, we may we may do everything we do in the first of the logic, yes? For example, if you have a, in first of the logic with two variables, if we have a two variable formula, not necessarily guarded, then, and if we translate it to the guarded fragment by using a dummy equivalence guard, say E 1, yes, E 1 is a symbol which which is not a member of the signature of this formula. And simply we add this, we add guards to this quantifiers here, then we obtain formula whose equivalence classes have to be models of this formula. So this, there is a close relationship between these two things. And what we do yesterday, for general satisfiability, we started from an arbitrary model of GF 2 plus E g formula, and unraveled it into a three-like way providing, starting from some element and then providing classes for this element in such a way that any pair of elements is connected in this three-like model at most by one equivalence relation. This is the place where we use this restriction on, on the usage of equivalence symbols, yes, they can be, they can appear only in guards. So we can do such things. We can unravel the unravel the model, then we can, we can make the classes exponentially bounded and we can make this model regular. Yes, so and this, this, this implies that there is a simple, a simple decision procedure for, for this problem working in non-deterministic exponential time. Okay, so today I, I will talk about the finite satisfiability problem. As you see, starting from an arbitrary model, even finite, we usually, we usually end in, in, in an infinite model. Yes, so such, such approach is not very promising here. And instead of three unravelings, we will, we will describe the properties of models by using systems of equivalence, systems of linear equations. Let, let me first show you that there are some differences in, in this satisfiability and finite satisfiability problems. For example, in the case of satisfiability, general satisfiability, we obtained a property that every satisfiable formula has a model with exponentially bounded classes. Yes. So, so this property cannot be obtained in the case of finite models. A very simple example here will construct a formula delta n of land polynomial in n, such that it's every model will, will contain a full binary tree of depth to the n. And then we say, we will say that all leaves of the, of the, of these three are members of the same class. The number of leaves will be double exponential. So, so it will imply that there exists a double exponential class. Okay, so, so the models will look like this. We'll have an element, we say that there exists an element satisfying unary predicate, unary relation root. And for each, and, and, and we would think that each of the elements encodes one binary number from, from the set 0 up to 2 to the n minus 1. And such, such numbers can be encoded, encoded in an usual way using n unary predicates. And I explained yesterday that we can count up to 2 to the n. We can say that a pair of elements encodes numbers which differ by 1. So we may say that for every element from an even level of the tree, there are two elements on the next level connected to, to this element by ret relation, e1 relation. One of them is in L, one in not in L to, to have, to, to ensure that there are really two, two such elements. And from odd levels, we require two elements connected by blue relation, relation e2. And we want to enforce that models really are really complete binary trees. Yes, so we have to ensure that there is no such situation that two elements from the same level say this grey element and this grey element use the same element on the next level as, as, as the witnesses, for example, this one. And to do this, we say that elements from say even level, like even level, this is 0, 1, 2. So for example, from the second level that there are not two elements on this level which are connected by ret relation. Yes, such reusing of a witness would, would cause that because of transitivity of the ret relation that the two elements, the grey elements would become related by this ret relation. So we simply say that if there are two elements related by ret relation, e1, and they belong to an even level. To check if a level is even or odd, we just look at least significant bit, then they are really the same element. Yes, they cannot be distinct. So this ensures that we have really a complete binary tree. And then we, we have to say that all, all leaves of this tree are related by, by, by this blue relation here. We cannot say directly, yes, for all elements if x, x, y, if x is a leaf and y is a leaf, then connect them by blue relation because this formula would not be guarded. Yes, but we can for example say that each, each leaf is connected by a blue relation to a root. We have 2 to the, 2 to the, 2 to the n leaves. Unfortunately, we cannot enforce in, in the guarded fragment there is exactly one root, yes, because it is, it is impossible. We always take, always in the guarded fragment can take another copy of the same model and this is, this is a model. So the situation in, in models may be like this, that we have several roots, each of them with a complete, with its complete binary tree. And some of the leaves connect to the first root, some of the leaves connect to the second root. But of course we always have, have a ratio one root per 2 to the 2 to the n leaves. So at least one of the classes must be of size at least that the exponential. Of course if we, if we allow for infinite models then we can, then we can, and then we can always construct classes exponentially bounded. Since we simply, instead of taking this root we can construct a new one and go on. But in finite models we can enforce doubly exponentially bounded classes. So what, in the, in the remaining part of the talk I will use a notion of accounting type. And accounting type, the purpose of accounting type is to count the number of realizations of one type in equivalence classes. So formally accounting type is a function from the set of one types over the signature of, of a formula phi, of the formula phi we consider. And this function returns natural numbers. And we usually, we think in, we think about this in this way that if we have a class C and say EI class C, equivalence class C in, in a model A, then its counting time simply says for, for a given one type its counting time says how many times this type is realized in this class. How many elements of this one type we have in this class. We will say that accounting type is admissible for EI classes with respect to this, to this formula phi. If there exists an EI class C of realizing exactly this counting type which satisfies this part of the formula related to EI. So in other words accounting type is admissible for, for EI classes. If we can build EI classes which from local point of view are allowed to appear in models of, of phi. And the admissibility of accounting type is a simple property. We can simply, for, for a given counting type we simply guess the structure and perform model checking. So this is an, it is not, not hard to check if, if accounting type is admissible. So to explain my approach I will first show you a very simple, very simple idea. So in, in a simplified case. So the simplified case is that we assume that we have a bounded number of admissible counting types. This may not be true in general is because in these counting types we do not know a bound on, on, on the values which are values of this function. Yes, so potentially we may have infinitely many admissible counting types. But let us assume that there is only some bounded number of them. For example, we may assume that we are interested in satisfiability in models with exponentially bounded classes. Then, then the number of counting types will be bounded doubly exponentially. Yes, if we have exponentially many possible exponentially many elements then the values of this function are all values of, of the functions which are counting types are also exponentially bounded. So that there may, there may be at most doubly exponentially many such classes. And so, and we construct, we construct a system of equations for each counting type which is admissible for EI class. We introduce a variable, an unknown. So we have unknowns for EI, E1 classes, unknowns for E2 classes, for, for types of E1 classes, for types of E2 classes and so on. And what we say by our equations, we only say an obvious thing which, which has to be satisfied in every model. That each one, for each one type, T, and each equivalence relation EI, EJ, there is, this type is realized exactly the same number of times in E1 classes and in E2 classes. This is an obvious thing because every element is a member of an E1 class, is a member of E2 class, EI, EI, EJ in general. So this is the obvious, obvious thing which should be satisfied in the model. And we claim that this is, this condition is, that this is if and only if. So we, we claim that phi has a model if and only if the constructed system of equations has a non-negative integer solution. Okay, let me show you an example. Assume that we have one possible, we have two, two equivalence relations. E1, red and E2 blue. And there are three possible admissible counting types for E1 classes. One with yellow and, and one yellow and one green. One type blue and red. One just a singleton class with green relation. And admissible, and there is only one admissible type for blue classes with red, blue, two yellow and two green elements. So what our system of equations says, it simply says that from the point of view of red one types, the number of realizations of x in the model should be equal to the number of realizations of b. Because these are the only, only types which, in which red element appear. Similar equation is obtained from the, if we write an equation from the point of view of blue one type. From the point of view of yellow one type, we see that every realization of x requires two realizations of a. Yes, because we have two, two yellow types in, in this x type of class. And from the point of view of green elements, of green elements, every realization of x requires two classes with green elements, so it may be a or c. So this is why we say two x is equal to a, a plus c. And obviously, if there is a model using this admissible counting types, then this model has to satisfy, then this system of equation has a solution. In the opposite direction, consider an arbitrary solution. For example, we may say, we may take the solution with one realization of x, two realizations of a is equal to two, b is equal to one and c is equal to zero. This is a solution to the system. And now let us see that we can construct a model with exactly this, with exactly such types of classes, but not with exactly this number of realizations of these classes. Sometimes, for example, this solution suggests exactly one realization of this, this blue class, blue type of, this type of blue class. However, there are some red classes with two elements. In, in, in our language, we may enforce that, we may have formulas which enforce that every pair of classes, blue class and the red class, have at most one element in common. In fact, we obtained this property in our construction yesterday, but this property can be, can be enforced. For example, we may say that every pair of elements which is connected by blue relation is also connected by an auxiliary symbol b, which is not required to be equivalent. And similarly, every pair of elements which is connected by red relation satisfies, is not connected by b, yes? Then we cannot intersect two classes in more than one element, yes? But then because, because then this, this pair of elements should be connected by b and not connected by b simultaneous. So in this case, it may happen that we, we won't be able to construct a model with just one equivalence class of this type, yes? Because this class requires two, may require two, two different classes of type x. But what can we do? What, what, what we are sure after when we have the, the solution of this system? We may con, let us define the notion of the base set for this solution, the base set of elements. The base set of elements contains as many elements of particular one types as is suggested by the solution. So the solution suggests that there will be one class of type x. So in the base set and no, no other blue classes, yes? So in the suggested set of one types is one red, one blue, two yellow and two green, yes? Similarly, we may, we may do it from the point of view of red classes. The suggested solution is a is equal to two, b is equal to one, c is equal to zero. So we will have two green elements because a is equal to two yellow elements, four, no, sorry. No, two green, two yellow, one red, one, one blue, yes? Because b is equal to one. Of course, the base sets computed using solutions for blue classes and red classes have to be equal, yes? Because we constructed our system in such a way. And what we know about this base set, the solution of the system guarantees that this base set can be divided into proper, into admissible, E1 classes and into admissible E2 classes independently, yes? So what we do, we simply take some number of copies, it's six copies in this case. We have six elements in this set, so we take six copies and we arrange them into, in a grid in this case. In such a way that every column of this grid and every horizontal line in this grid, every row in this grid is a copy of this base set. Such an arrangement can be easily obtained just by starting from the first column and putting this base set in an arbitrary order and then just shifting the picture one row down, yes? And now we can divide columns into blue classes and rows into one classes, exactly as suggested by this solution, yes? So after this construction, every element has two admissible classes constructed, yes? Blue and red, so everything is okay. Remember that for simplicity I removed those formulas which require non-equivalent witnesses. This approach, of course, can be easily generalized if we have more than two equivalence relations than we simply construct multidimensional grids in this way. Okay, so this is the idea and the problem is that we do not know a bound on the number of counting times. This may be infinite, so in particular we would have infinitely many variables, yes? So it would be a problem. Instead of this, we will use some approximations of these counting types. And before I define this approximation, let me first just formalize one lemma which we will use. So we say that a counting type safely extends another counting type. If it preserves the number of one types which are realized, zero on one types in this realization, which are suggested by this type, yes? So if theta of t is equal to zero or one, then theta prime is also equal to zero or one. If theta of t is greater than one, then theta prime of t is simply greater or equal to theta of t. Of course, this definition has a close connection to the notion of these royal types in models of F2 formulas, yes? Simply that if we have a class of type theta, then we can safely extend it to a class of type theta prime, which still from a local point of view is proper class for the given formula. And this recall lemma 10 is this lemma about adding single realizations of non-royal types to F2 classes. And this is just a simple application of this lemma, yes? If we have a class, C is just a model which is an equivalence class of EI. It satisfies this fragment of the formula related to EI. Then if we take a counting type, theta prime which extends the counting type of C, then we can construct a model of this formula for EI which has exactly time theta prime. By adding the required elements as many times as required. So this is one thing. And another thing is the notion of M counting type. So instead of using exact counting type, we will use some approximations. We will count up to some M. M counting type, M is a parameter, is a function of the type from the set of one types to the set 01 up to M. And the interpretation is that if theta of t is equal to M, then it means that in a class there is at least M elements of type t. M minus 1, M minus 2, 1 and 0 means exactly M means at least. Now lemma 4 is this small model construction for FL2 formula. And using this construction, we may prove that there exists M exponentially bounded in the length of the formula. Such that if we have a class admissible for EI classes, a class satisfying phi of phi with superscript EI, and its M counting type is theta, then there exists a class C prime which has exact time equal to this theta. So if there is M realizations, at least M realizations, then in this new structure there will be exactly M realizations. And this is the same construction as in this lemma 4. Okay, so these are two auxiliary lemmas. And now how we construct the system of inequalities. So we introduce variables this time for M counting types, which are admissible for EI. So again we check if there is a class with exact counting type. We give an exact counting type like this with at most M realizations of every one type. What is the number of these M counting types? It is doubly exponential in the size of the formula phi as we observe later because we consider this situation. What will be our procedure? We will guess the set of one types which will be realized in the model of the given formula phi and write some inequalities. There will be two kinds of inequalities. The first kind of inequalities are just inequalities which ensure that elements of these quest one types will appear in the model. And the second kind of inequalities will say something about royal types. So now let us redefine this notion royal. We say that one type T is royal for EI classes with respect to the formula phi, of course. If every counting type admissible for EI has at most one realization of this type. So such a royal type, a type is royal for EI classes which if a type is royal for EI classes say, then we probably won't be able to add additional realizations of this type to the given class. And what kind of equations we write if T is royal for EI classes, then for every other equivalence relation we write inequality which say that T is realized in suggested by M counting types for EI classes at most as many times as for EJ classes. Okay, this may be unclear, I suppose so let us look at an example. Assume again, assume that we have two admissible M counting types. So this means that in our model we allow for such classes and this classes may be further extended by, this class may be extended by yellow elements, this may be extended by green elements. This one in fact also can be extended by yellow elements but green elements and yellow elements because we know a pattern which allows to connect to yellow element inside a class. And we have three admissible M counting types for red classes and what we say in our system of equations. So from the point of view of red element, red element is royal for both blue classes and red classes. In each class it appears at least at most once. So what we say we want to guarantee that the number of realizations of, oh, the definition from the previous slide implies that we should construct two inequalities which will produce such an equality. If we realize such a type then we have to realize type A. So X plus Y should be equal to A. From the point of view of blue elements, yellow elements of course, yellow elements are royal only for E2 classes. Oh sorry, for red classes it should be E1. For red classes because in each such red class there is at most one realization of yellow element. For blue classes, yellow is not royal because we have a class admissible type of class with two yellow elements. So this is the second kind of inequalities. The first kind of inequalities are those inequalities which say that our three one types, assume that we guess that there will be these three one types in the model and we ensure that they will be in a model. So we say that X plus Y is greater or equal to one. X plus Y is greater or equal to one and X plus Y is greater or equal to one. This ensures that in blue classes we will have red, yellow and green and the same we do for red classes. An example solution is one, X is equal to one, Y is equal to one, A is equal to two, B is four and C is zero. Now how to construct a model? Again we will define the base set for this solution. But this time the base set will be defined in a slightly more complicated way, namely how many elements of red type will have in the base set. We look how many types, times these elements, these red elements are suggested by our solution in blue classes, so twice. And how many in red classes? No, also twice in this case. So to the base set we take maximum from these two numbers, in this case two. But for yellow classes in blue classes yellow elements are suggested three times and in red classes they are suggested one, two and four, six times. So to the base set we take six yellow elements. So in our case the base set is like this. This is a single line, it's just a base set. So a base set contains two red elements, six yellow elements and five green elements. Again five is the number suggested by blue classes here and red classes suggest four green elements. So we take five copies. And what we know, what is guaranteed by this solution? The solution guarantees the system was created in such a way that the base set may be divided, not divided. In the base set we may distinguish one copy of class of type X and one copy of type Y. We have enough elements of appropriate colors for these. Here is E1 class and here is, sorry, this blue class and here is another blue class, a blue class of type X, class of type Y. And similarly for E2 classes we have enough elements to have two classes of type A and four classes of type B. They are presented here. This is because in our base set we always took this greater value of elements from those suggested by E1 classes or E2 classes. Of course we may have some elements left. We have three elements. If we divide the base set into E1 classes we have three yellow elements left. If we divide into E2 classes we have one green element left. Left means without its own class. But using our lemma we can simply add these elements to a class which contains yellow elements. Because we are sure that those remaining elements have types which are not royal. For royal types we always have equality. All of them will be taken to, or royal elements are taken to these classes suggested by the solution. The elements which remain must have non-royal types. If they have no royal types then they can be adjoined to classes containing realizations of these types. Using our lemma. We ensure that there will be such classes by this inequalities. Similarly the green element, this green element may be adjoined for example to this class. To connect these two green elements we will use this pattern from admissible class of type C which is not realized in our model at all. But we have a pattern of connections. This is one implication. If our system of equations has a solution then we can reconstruct the model. In the opposite direction we use this lemma which says that for every class it can be approximated by a class realizing exactly its M counting type. If we have a formula and its model then we take a solution to the system of equations. The number of realizations, if x is a type is a M counting type of a class. So we check how many times this counting type is realized in the model. This M counting type is realized in the model. How many times, how many classes have exactly this number of realizations of one type counted up to M. So for example a class with one red, two yellow, three green and for example four green elements is counted as a class of M counting type X. Maybe I will skip the detailed argumentation but this lemma about approximations allows us to prove that the system of equations is correct. So let us now think about bounds on the size of models we can obtain this way and the computational complexity of the problem. So this lemma is taken from the paper by Kalvaneze but in fact it is built on the classical results on the system of equations by Papadimitriou. So let us assume that we have a system of linear inequalities or equations with N unknowns, M inequalities or inequalities and N unknowns and coefficients are absolute value of coefficients is bounded by A. Then this system has a non-negative integer solution. Of course we are interested in non-negative integer solutions because these are numbers of realizations of classes so it has to be natural numbers. So the system has such a solution then it also has a solution in which values are bounded by such a number. It is not hard to see that in our case this number is doubly exponential because M the number of inequalities depends on number of one types. We construct two inequalities for each one type. We have doubly exponential number of unknowns because unknowns are M types of classes and M counting types of classes and coefficients are exponential because in each such M counting type we have at most exponentially many realizations of each atomic type. So in fact we have doubly exponentially bounded solution. So doubly exponentially bounded number of types of classes but in each class we initially put on the exponential number of elements. So the total number of elements will be doubly exponential and this theorem. Our construction from the beginning of this talk when we constructed a model of double exponential size was essentially optimal. Every finite satisfiable formula will have a model bounded doubly exponential which follows from this construction. But we want to obtain non-deterministic exponential bound on the complexity of the satisfiability problem. And this theorem suggests a simple procedure just guess a model double exponential size and check that it is a model. But this procedure is doubly exponential non-deterministic time. How to obtain singly exponential time? Observe that our equations are of very simple form. They are just c1, x1, plus c2, plus c3, x3 and so on, greater or equal to a number b which in our case is either 0 or 1. All of our inequalities can be rewritten to such a form. So it is not hard to see that instead of solving such a system of equations over integers we can solve it over real numbers. At this moment we are not interested in constructing the structure for formula phi but only checking if this model exists. So we only want to solve the system of equations. We guess the set of one types which will be realized and this is exponentially bounded information. And then construct a system of equations and try to solve it. But instead of solving it over integers let's solve it over real numbers. Of course if there is a solution over real numbers then we can multiply this solution by the product of denominators in the solution for all variables and we obtain integer numbers then. And those numbers obviously will satisfy these inequalities because they are of very simple form, greater or equal or something. If we multiply this side by some positive number of course then the relation will be still retained. So we may solve the system over real numbers instead of integer numbers and we can use a simple fact from linear algebra because what is the shape of our system of equations? Exponentially many inequalities and doubly exponentially many variables. Instead of such a system of inequalities we can construct a system of equalities which we have a solution. So let us think about equalities and in our algebra we know that the rank of these metrics is at most 2 to the n. So we can move all the variables, we can find a maximum non-zero minor, we can move all the variables not belonging to its minor to the right side of the system and substitute them for zero and we will still have a solution in which only those variables will be non-zero. So the theorem, the observation is that if we have such a system of equations over real numbers then we can always find a solution in which only exponentially many unknowns has non-zero values. Yes and all the others are zeros. This can be done for real numbers not for integers because we require that this system is over, to do this thing we want this system to be over a field, not just over the ring. So what is our algorithm now? We guess which types, which variables will be non-zero in our solution. So we guess the set of one types and we guess the set of those n counting types which will correspond to non-zero variables. And now we have only, and we construct the system but using only those variables. So we have a system with 2 to the n equations and 2 to the n variables. We solve it over real so we can do it in deterministic time, deterministic polynomial time, so we finally get, oh it is not important that this is deterministic because we have a non-deterministic algorithm because we guess something. So finally we guess exponential number of information, construct the system of equation and solve it all of this in exponential time. Okay, so I have a comment here that this technique of describing models by system of equations or inequalities is very often used. It has been used in many, many, many examples. I just mentioned two things which are related to our talk because they consider two variable logics in fact, yes. The first two papers are about description logics with number constraints, yes. Description logics with number constraints, the second one just two variable logic with counting quantifiers or one variable logic with counting quantifiers. So for example one variable logic with counting quantifiers, it has quantifiers of the form for all x. There exists at least mx such that or there exists at most mx such that, yes. So in this case these systems of equalities are even more natural I think. It was used by Ian Pratt, this approach was used by Ian Pratt Hartmann to produce an easy proof of a simple proof of the two variable fragment with counting, not of decidability but of next time upper complexity bounds. The previous proof also by Ian Pratt Hartmann was much more complicated and the previous results implied only decidability without precise complexity bounds. Okay, in this description logics are also based on two variable logics and these numerical restrictions correspond to counting quantifiers. Okay, so maybe I have two more things to show, maybe I will start from the third one. I will just state the second one, yes. So the statement of this next theorem is that the satisfiability problem for two variable logic or even to the guarded fragment with equivalence relations which can be used outside guards. In our construction we use the fact that equivalence relations are only in guards. So if we allow them outside guards then we can show undecidability using three equivalence relations. So this is one thing and to show that we are very close to the border between decidable and unsidable we can also show that two variable logic with two equivalence relations is decidable. So three equivalence relations are undecidable and two are decidable and I am not going to show you details of the theorem but I would like to show you some crucial differences in this situation and in our situation two variable guarded fragment with equivalence guards. So what are the differences? This problem is much harder, yes. What are the differences? The first thing is that of course we may enforce non-empty intersections of E1 and E2 classes. Because we may simply say that for example there exists an element, for every x satisfying p there exists an element y connected to this x by E1 and connected by E2. There are no restrictions on the pattern of, there are no guards in fact. So this is the first thing. Another thing we may say that some types of classes, regardless of this notion of type, some types of classes are realized exactly once in our model. For example we may say that every element satisfying r are contained in one E1 class. When we build our models we cannot take a copy of these classes because this is forbidden. We could also always do it in the guarded fragment. Here we won't be able to do it. Of course a simpler way of doing is just saying that there is exactly one element satisfying p in the whole model, yes. Which can be done without equivalence relations. Then both of its classes will be unique in some sense. It appears that we may even, if we consider a general satisfiability problem we may even enforce infinite classes this time. Remember that in the case of two variable guarded fragment with equivalence guards we had, we could always build models with exponentially bounded classes in the general satisfiability case. It is also much harder to deal with free witnesses, with those witnesses which lie not in the equivalence class of a given element. So there are some complications. In fact we can enforce triply exponentially models of triply exponential size this time using this fact that we may have some non-trivial intersection of classes. This is the same picture we saw previously. This time we consider those bullets to be not just individual elements but intersections containing 2 to the n elements each. And having such an intersection we may encode in such an intersection a number from the set 0 up to 2 to the 2 to the n. Because simply we have 2 to the n elements and we may use an additional binary symbol which works as 0, 1. And we have a binary representation of a number from the set 0 up to 2 to the 2 to the n. And having in f of 2 we can say that 2 intersections connected by say blue relation encode values which differ by 1. This is not obvious but not difficult just a complicated pattern of quantifiers. Some are using variables and it can be done. So we may enforce full binary trees of doubly exponential depth. And then we may again, as previously we may say that all leaves are in one blue class for example. This time we do not even need to use this route. We may simply say that if element is a leaf we can be checked somehow. If a pair of elements in both elements from this pair are leaves then they are connected by blue relation. So we may have models of triply exponential size and classes of triply exponential size. What is the idea of the proof? So the first thing is natural. We do not want to deal with these intersections so instead we will treat them as individual elements. But to do this we have to prove that every formula which is satisfiable is satisfiable in a model with small intersections. And it can be done. So now such small intersections so we have exponential bounded intersections so there is doubly exponential number of isomorphism types of possible intersections. And we will treat them as elements. But now we have two to the n possible types of elements. And we proceed similarly as in the case of two parable guarded fragments with equivalent guards. Of course there is a lot of details. Some of them are quite interesting, some of them are quite annoying but finally the procedure is to quest some information of doubly exponential size and construct a system of linear inequalities. But this time the system is larger. It has, this is one thing that is larger, of course, it has two to the two to the n variables and two to the two to the two to the n, sorry, and doubly exponentially many equations or inequalities and triply exponentially many variables. So the situation is similar as previously but the problem is that we do not have this nice form of inequalities. So of course we may solve this system in triply exponential type, triply exponential non deterministic time, obtaining three next time upper bound on the complexity but we want to obtain two next time, one exponential lower. And the difference in comparison with this guarded fragment is that we will require equations of the form x plus y plus z is not greater than one. These are, they are because we may say that, they appear because we may say that some types of class appear exactly once in the model. So we simply say types of types of classes are elements. So we may have something like this. So maybe sometimes we have that x is equal exactly once, maybe sometimes we have that x plus y plus z is not greater than one. And this trick with taking real solution and multiplying it by denominators will not work because it will not preserve, not necessarily preserve this kind of inequalities. But it appears, so we have to solve the system of equation over integers this time. And it appears that there is a similar theorem, not that simple like this one, but Eisenbrant and Spawning could show that if such a system of equation has, such a system of equation with not too many equations, but many variables has a solution that it has a solution which only polynomially many with respect to the number of equations, polynomially many variables is non-zero. So exactly what we want. But this is also not very difficult theorem, but not that obvious as in the case of real numbers. So we proceed analogously. We guess which variables will be non-zero and construct the system of equations ignoring those unnecessary variables. So we will have doubly exponentially many variables. And we have to solve this system over integers, but the problem of solving system over integers is in NP, so everything is okay. We finally finish in doubly exponential, non-deterministic time. A lower bound can be also shown, it was shown by Ian Fath Hartmann using a similar trick to the one, this trick with counting, to construct a grid of 2 to the n, of doubly exponential size. So the problem is two next time complete. Okay, so I have some more time, so I will go back to this undecidability theorem. Okay, so now I will try to explain why two variable guarded fragment becomes undecidable if we allow equivalence relations outside guards. So I will use a reduction from domino systems. A domino system is just a tuple consisting of set of domino tiles and some restrictions on horizontal and vertical connection, and the problem is to tile a grid of n times n, preserving those constraints. So we simply say these constraints say which pairs of domino types may be horizontal neighbors, which types of domino types may be vertical neighbors.


And away from Africa now, Australians will not be compelled to take COVID-19 jabs, according to Prime Minister Scott Morrison. He has also ruled out the use of rapid antigen testing as the country's national cabinet met for the 50th time since its formation. Morrison believes the most reasonable thing to do is to know who has tested positive. But when you're in the suppression phase, that is phase A of this virus, what is very important is that we need to know who's tested positive. And if you're doing voluntary rapid antigen testing at home and things of that nature, then the state health authorities won't know. And so it's important that we can know and then do contact testing and tracing to ensure that we can follow that through in the suppression phase. While you're in the suppression phase, knowing who has it, knowing who they've been in with and being able to follow that up and isolating close contacts and all of that, is a very important part of the public health response to the outbreak. So rapid antigen testing has a very important role to play. There's no doubt about that.


What's up everyone? It's your girl Kenzie here from Layton Sports Cards and I'm ripping some personals as always here for on our Sunday Day time for Justin s. All right, Justin We've got a 2022 tops chrome McDonald's all-american basketball hobby a 2022 tops gold label baseball hobby a 2022 pro-set metal football hobby and a 2022 panini mosaic choice. All right fun mixer here We're gonna start with the choice box Choices have been hot Let's see And then though the washer which apparently is the washer and dryer are not in the home warranty for some reason don't don't understand that The washer stopped draining all the way But Ro was able to fix that thankfully Like we had he had to go up under the thing and like drain whatever water was there. Oh my gosh It's stunk so bad it probably hadn't have been washed the entire time that the people before us lived there Brian de la Cruz silver rookie because it was like standing water, you know, that's stunk Frankie Montas Our choice exclusive Kyle Hendricks for the cups not numbered nice Lou Bob on the black and gold two of eight Y'all these choice boxes have been insane for us today. What is that the third black and gold? I believe Fourth or fifth number to eight at least That's crazy mosaic rookies of Lars new bar and a Gavin sheets Yeah, Joshua, it was it had not been drained and probably the entire time they had it before It was gross rookie Otto Glenn Otto for the Rangers Rangers Glenn Otto and then we have for the rays red Vidal Bruhan Red and then like the filter that like where the water comes out of the drain had not been cleaned and Really a long time either We're gonna go with the gold label baseball this go around One framed Otto again. I'm not opening any of this yet. So good luck here Justin See a golden nugget I've never pulled one. I saw was it forced or Matt pulled out of a wander. Yeah Golden nugget. I believe that one's a frame here. We go here first. All right. How's a Siri rookie? Got each routes Roanzee contraris rookie Nolan Ryan and Corey seeker Nice There's words of the classes. I like the design. They definitely upgraded it from Last year's or the year prior Jarenda ran rookie Red Sox Gavin sheets Ken Murphy, Jr. Acunia, Jr. and a Matt Manning Tigers Oh, it's Matt. Yeah, that was sick Ruhon rookie Frank Thomas they hurt each hero on the class to CJ Abrams rookie class one and Mike Schmidt Walker Bueller Joe Ryan rookie Class to read Demers rookie. That is a class three rookie We've got Acunia on the blue to 150 nice color match their breaks Yeah, Greg. I was looking for them. They're they're in like the Yeah, Edward Cabrera class one, they were hard to see out of the previous years It was like the background of the car. Yeah, Raffy Devers. We have Edward Cabrera rookie Green Nolan Aeronado Joe Ryan rookie and Ted Williams All right, last back before we get into the Both frame Ortiz Malina Nolan Ryan Class three there Alec Thomas and a cabrion Hayes All right, old frame time. Good luck. You're Justin Yeah, it's Roberto Clemente pull from the back here Yachty Malina and your gold frame auto is gonna be rookie of Curtis Terry for the twins Curtis Terry Twins rookie auto Let's see we're gonna do Procent metal up next These boxes have been pretty hot for so you're I ripped a few of these on drip last Monday and pulled the Kenny take it we pulled Sam how like five like Willis to five I'm a crazy run on this part of the box there All right. Good luck on this one. We've got black mojo pier strong junior that one is three out of five three of five Got action ink of Tyler Algier Falcons six to twenty five zebra of Hassan Haskins zebra scope five of five all these have been numbered oh Two out of fives and one out of twenty five so far Geez, then we have action ink of Malik Cunningham 23 of 40. I Like the action it's cool photos on that Green wave Brian Robinson Jr. four of 25 And nice one here printing plate One of one Kenneth Walker the third there you go Justin on the cayenne One of one printing plate Nice see how I sit there solid box All right tops chrome McDonald's all-American and it's my first look at this Two autos a box here Here we go. I fly your future stars of where? Living stuff. It's Luton. They've got Jordan Walsh Remembered on that one.  It's one of the kids you're looking for Nice one there. Oh, it's white Julian Phillips Bar grease Ben Spluton future stars of Maya Nash of Ashlyn Jackson that one is 40 of 99 from the West Ashlyn Jackson growing down It's soon a Brady Walker Jackson For one more auto refractor of Johnson and Nick Smith Jr. Yeah, Greg. It's it's it's cool for sure Poopers of Kiki rice that's sick like that insert Turner Clark God a Dean Bona his Patterson refractor Miller and Mitchell Future stars Derek lively the second. We've got Aqua wave of Reagan beers 50 of 199 Beer Dick we've got grace Vance Luton refractor. Nice. That's one of the Females you're looking for Vance Luton Derek lively the second Jackson and beers here is refractor of Mark Mitchell Future teammates it's a cool Couple packs left here Kiki rice refractor auto is going to be a chance gray chance gray Johnson Last pack here for you Justin Haley Ernest Uda refractor Najee and Whitmore Alrighty Justin that will do it for your four box. Congrats on all those. It's thanks as always for helping in every Sunday I always appreciate your support. We'll get these right out to you


10 Sentences That Can Change Your Life Sometimes it only takes one sentence to change your life and change how you think and encourage you to look at the big picture to stay positive and get the best out of life. This is because the message or messages in a sentence like that can change one's perspective about life and help you understand certain things better. In this video, I'll share with you 10 Sentences That Can Change Your Life. This I believe will help you become a successful person. If you're new here, consider subscribing so that you won't miss other interesting videos like this. 1. If you love what you do, you'll never work a day in your life.  No. Follow your passion. When you follow your passion, you'll be able to enjoy your life to the fullest and also ensure that you are putting your time and energy into something that is valuable and important to you. Doing this will make you feel satisfied because you'll be doing what you love. Work will begin to feel like play and you'll still get paid to do it. Isn't that amazing? 2. We don't see things as they are. We see them as we are. You see, there's a way things are and there's another way we perceive them to be, which in some cases is different from what the situation truly looks like. And Niasneen has a point here. You see, there's a way things are and there's another way we perceive them to be, which in some cases is different from what the situation truly looks like. So, sometimes, when you think that there's no way to see things other than the way you see them, rather than trying to validate your perception, which even may be a misperception, take time to listen to the other people's perception so that you can question yours and find out the actual state of things. 3. Anyone who has never made a mistake has never tried anything new. Mistakes are a part of the learning process. When you make mistakes, you know better what works and what doesn't so that you don't repeat the same mistakes in the future. When Thomas Edison, the man who invented the electric light bulb, tried to invent the model for the bulb, he failed several times, one thousand times to be precise. Do you know what his response was when he asked how he managed to keep up despite the many failed attempts? Edison responded saying, I have not failed, I have just found ten thousand ways that wouldn't work. Making mistakes doesn't make you a failure, it only makes you a learner. So, don't be scared to make mistakes, instead, challenge yourself to take up new challenges. Learn from your mistakes and make great moves. 4. Remember that failure is an event, not a person. When you feel bad about yourself or because you feel that something, try to remind yourself that failure isn't a person. It is only a circumstance or situation that happens to people. So, you are not a failure, you only feel because you are in the learning process. A phase where failure is allowed as long as you learn from your mistakes, not beat yourself up over your mistake. 5. Comfort is the enemy of achievement. When you notice that you have gotten too comfortable with a situation, a position or a place, maybe you aren't doing enough anymore and it might be time to live and opt out for something different and better. It takes some time to think about what you want your life to look like, set goals or re-strategize in some cases so that you can achieve your goals. And when you notice your goals are no longer challenging, it just might be time to set new ones. When you step out of your comfort zone, you are able to achieve much more. 6. How we spend our days is, of course, how we spend our lives. A lifetime consists of a collection of individual days, so it's best to make the most of each one. So, maybe it's time to stop viewing your life as the future when it is the present. Remember, your future is only a reflection of your present choices and decisions. 7. The future belongs to those who believe in the beauty of their dreams. Only dreamers can bring change to the world and inspire others to do so when the airplane, electricity, cars, ships, computers, telephones and the likes were invented, nothing like these existed before they were made. However, their inventors believed in their dreams and they could picture how valuable these items will be to mankind. Guess what? These inventions are not only valuable but have also served to create other valuables as well. So, if you believe in your dream, you are well on your way to change in the world. 8. If you accept your limitations, you go beyond them. Once you know your limitations, you can easily excel beyond your imaginations because knowing your limitation helps you to discover your strengths and power. With this, you can transform yourself and have the courage to face your fears. 9. Everyone you meet is afraid of something, loves something and has lost something. This is a reminder that we are all alike. The rest of the world, no matter how successful they look or not, are just like you. They are afraid of something, they love something and have also lost something just like you. So, just as you'd like to be treated, respect people's boundaries and show some empathy for their struggles. 10. Climbed mountains, not so the world can see you but so you can see the world. When certain goals for success understand that you are not doing it for people to see. Instead, you want to become a better human being for people to recognize so that you can add value to them. Take time to learn new things, discover more and explore more, travel the world if you have to do so, that your mind can be exposed and you'll learn more. Now that we are done, we hope these words have given you enough inspiration to become a better person. Thank you so much for watching our videos. If you like this channel, we're happy to announce to you that our team has launched three other interesting channels. One of our new channels is called Hunt TV, where we publish inspirational videos to inspire and encourage you as you go through the harsh journey of life. Our second channel is called Fame TV, where we share with you the interesting and inspiring stories and biographies of the successful people who have achieved greatness with their lives. Our third channel is called Money TV, which is a channel designed to use more dramatic video clips to teach you about money. Look at the description box to join our three new channels. We love you.


Hi, everybody. So as they said, my name is Drew Knox. I'm a PM on the storage team. I work on a few other projects, but storage is really what I'm here to talk about today.  So please laugh at all of my jokes. Otherwise, we'll be cripplingly embarrassing just throughout. So again, please thank you for that. So before I get started, I want to do a show of hands. I'm the talk right after lunch. So you guys are all probably in food commas, not really paying attention, catching up on email. So a little calisthenics to get you guys going. First, how many of you are still capable of raising your hands? You didn't eat too much. You can, yeah. All right, good. A few people lost, but that's OK. All right, now onto the real question. How many of you have used client-side storage in a meaningful way, not just playing around with Service Worker in a demo app, in one of your sites? All right, now keep your hand up if you viewed that primarily as a critical performance optimization, not offline. All right, it's about right. So when we look at these kind of numbers through Chrome usage metrics, we see that about 2.5% of page traffic uses things like index DB or cache storage. So my goal today is to convince all of you. So hopefully, you'll all have your hands up next time around at CDS, that client storage is the most important performance optimization you can make for load time in all browsers. And most importantly, because we all know that caching and all this is important, I want to convince you that it's available today and that it's kind of low hanging fruit for you to pick up everywhere for all of your users. So why is this important? We've heard this number repeated a lot, which is that you lose half of your users if your site takes more than three seconds to load. I won't belabor the point, but it's pretty scary, right? It's kind of a horror movie. But when you think about it, it's actually a lot worse than that, because on the average 2G network, it takes three seconds just to get the first byte. So we're kind of already hosed, right? We're fighting an uphill battle. And what's worse, 320 milliseconds is how long it takes to load one megabyte off the network. This is really hard. The deck is kind of stacked against us. So we need some tools to help us not just improve our loading performance, but avoid the need to hit the network at all. All right. So we know it's important. We know we've got to do something, but I don't just want to preach a horror movie. I want to give you guys some actionable steps. So in my talk today, I want to walk through how you should reason about spending your time on client storage, where the biggest wins the least amount of work for 80% of the value, some technologies that you can use, along with some libraries that'll make it easier, more ergonomic, how much storage space you have available. And then if you guys are all really good and you laugh at all my jokes, and my grandma is really proud of me at the end, I'll give you guys a view of some of the future things we're looking at that are kind of exciting. Now, before I move on, I was told I should explain the first line, because nobody thought that how you spend your time, that these emojis were conveying that. My girlfriend said it made no sense, but she's also an iOS developer. So what does she know? All right. How are you going to invest your time? Web developers are pulled a thousand different directions. Lots of us are full-stack engineers. Unfortunately, we're working in a place where Flexbox is still one of our most powerful layout primitives. We don't really have infinite resources to do infinite things. So before I get started, I want you, for the purposes of this talk, to think about storage as cash, not offline support. Offline support is really important, and it's something that's been touched on a lot. I just want to focus on cash as a performance optimization here today. All right. As a cash, you kind of have this spectrum of investment that you can make. Browser cash, all the way on the left, is sort of the default. It's relying on the browser to get things right for you, hoping that your responses are cashed and that they aren't cleared before the next time the user visits. And on the other end, you're building a spaceship. This is service worker, cash storage. You're optimizing everything to the nines.  This is sort of what you've been hearing from a lot of folks. So looking at the first one, browser cash, doing nothing, it does have some real benefits, right? You speed up repeat visits for your users, and that's not insignificant. But unfortunately, it only works for network responses. It's unpredictable. You don't know when it's gonna be cleared out. And it's got pretty coarse granularity, right? It's the level at which you served up files. So this is not great. It's kinda sad. Optimized browser cash is probably what a lot of you are doing today, and it's a really good step. This allows you to not only get repeat visits sped up, but you can actually get some proactive page load improvements using things like link rel equals import, or any number of things to try and load things before they come in. But it still only works for network responses. So these are a lot of the optimizations you see people, you've seen people suggesting sort of off-handed as they've been giving talks. It's still unpredictable, because again, you're relying on where the browser is storing things. And there's not much granularity here either, because it's still on the level of network resources that you've served up. Still not great. Content caching is where the first big step function can come in, in terms of improving performance. You get proactive page load improvements like before, but now you can work for all response types. So this is, when I say content caching, I mean things like saving image blobs in cache storage if it's available, or in index DB, and then serving your image tags with a blob URL, all kinds of things like that. You have some predictability, right, because the things that you're storing in cache storage, or in index DB, you have control over. But you're still using network responses for some other things, so it only gets a yellow here. It's not perfect. You have content granularity, and this is really important. Granularity is something where you wanna be able to change something and not have to re-download your whole bundle. So the more you can break things up and have your cache invalidate for only small pieces, the better. So again, you get granularity for content, but not for your network requests, so it only gets a yellow. This is still pretty valuable though. It gets a smiley face from me. Full cache control, the spaceship. This is a lot of work. I'm gonna be honest with you guys. I've never effectively done it, and I work on this team, and I should theoretically be able to say I've done a thousand of these. So it's great when you can nail it, and you've seen a lot of really big production apps that have, but with this comes a lot of work. You get proactive page load improvements, like before. You get all response types, again, that's great. It's fully predictable, because now you're pulling in even the network responses into a cache that you control, and that's really valuable. You can guarantee your user a certain performance level. You also have content granularity for your network requests and your content that you're serving. And as a major bonus, you get offline support, which people have talked about a lot. So I would be crying tears of joy if everyone started building their apps like this today, but I understand that that's pretty hard.  This is kind of the sweet spot, right? If you can serve all of your content from IndexedDB or CacheStorage or something like that now, you really have access to storing all of your content, even if you're not building that spaceship with ServiceWorker. So you can get full performance levels for your site, not just the app shell or something like that. All right, I've talked a lot about how this is, maybe not too hard, it's kind of low hanging fruit. It's really important, but let me put my money where my mouth is and dig into some code. So first of all, as I put this together, I really fretted about whether or not I should put my thens on a new line or attached. I was afraid I would get flamed one way or the other. I went with their own line, but please don't hurt me. That's my best go. So here I'm using a Redux app. It could work with any framework, right? You could use your own view binding library. I just create my store, get it set up. Here's the magic part. I'm using an IndexedDB wrapper library to store my state essentially whenever there's a change. This is done asynchronously, so it's not gonna block the main thread. And then later, when I'm re-inflating my state, instead of hitting the network or pulling from Firebase or something like that, I grab it and fire a database-loaded event, which will reinstate my state without having to hit the network. So this kind of pattern, as you can see, was only three to five lines of code, and it can avoid an entire network hop for your whole app, right? You have your entire app state all saved local disk really, really easily. So this is a pattern that I think works really well with Redux-style apps, but it really can work for anything. Maybe it's a little more work if you don't have a single object you're trying to save. If you wanted to tweet this, here's a good slide with all the syntax highlighting. In general, there are a few best practices. I hinted at them, but just to make them clear, when you're managing your cache on the user's device, you wanna make sure you're doing client-side chunking. This means you might pull in an initial bundle and then kick off requests for smaller, more granular pieces so that you can revalidate only small chunks as things change. This pattern is a little more complex, but can really save you network bandwidth. You also wanna preload pages the user might be about to visit. So if you imagine you're on some news site, you might wanna load all of the articles that are shown above the fold or something like that. You also wanna save commonly repeated components. So if you have a hero image, a logo, anything like that, just save as many of them as you can. Get rid of as many network hops as you can. What should you be using to do this, though? You guys might be aware that the web is not really one for having a single answer to a problem. There's lots of different ways to do things, but thankfully, it's pretty simple in terms of what you wanna use on the browser. So if your data is URL-addressable, you should use the cache storage where it's available. It's really simple. It's kinda just like a key value pair. Works really great with service worker. So it's your no-nonsense easy, easy solution. If you've got structured data or if you have a lot of users who don't have access to cache storage, Index TV is where you wanna go. These two combined, they're asynchronous. They're modern. They're getting lots of attention from browser makers. This is sort of your bread and butter. This is where you wanna be doing all your work. Now, in terms of availability of cache storage, I have here, can I use usage-weighted slides? It's available in a lot of places already. So I know some of you are thinking, oh, I don't wanna deal with having to do progressive enhancement or fall back to Index DB, but you can hit a lot of your users with cache storage today and it's only gonna improve in the future. So I have here just a few libraries that we think on the Chrome team are great for helping to improve your interactions with Index DB. They all give promise support. Some of them give database sync. Some of them even try to recreate SQL syntax, but these are all great libraries in terms of ergonomics, but also they've thought a lot about making themselves minified so they don't impact loading performance. So that is a really big win. For cache storage, it's a newer API. There's not quite as much available. We heard from Jeff about ServiceWorker Toolbox, ServiceWorker Precache. Webpack has the offline plugin, but otherwise there aren't quite as many things that are available now for use. All right. If I had to guess, I would say this was probably the area you guys were most skeptical when I started the talk. You are making websites, right? We aren't using device resources. This is the whole point of the web. It's ephemeral. It doesn't stick things around. I'm sure that's been changing as we've been talking about ServiceWorkers and kind of convincing you guys of offline, but it's still a real question. How much space do you get and how reliable is it? So at first I started looking at empirical ways that I could do this, right? Small demo apps to try to fill the cache, fill the storage partition and see what would happen, but then I realized why don't I just email all the different storage teams and the different browsers and ask them how much space is available. And it turns out that worked way faster. So the browser quota limits today are, they kind of fall into two camps. So we have percentage base. Chrome gives you 6% of free disk space per origin.  It's 10% shared across ETLD plus one. So this is like play.google.com and movies.google.com would share storage. Safari gives you at least 10% of free disk space. An edge is, well, it's a little bit more complicated, but thankfully it's still fairly reasonable, right? Like edge is largely a desktop browser. It's got, so you can rely on being in one of the higher tiers. So you don't have to worry about all four of these all the time. And based on usage statistics and sort of looking into our own telemetry, we found that a simple number, simple rule of thumb is that you have 50 megabytes available on all devices and all browsers today. So this will get higher as you're working on higher end phones, but you can think of this as your minimum budget that you can use to try and improve performance on your site. If you remember my slide before or a ways back, if it takes 320 milliseconds to load a megabyte across the wire and you've got 50 megabytes available to you, that's 16 seconds of load time that you can save averaged across all your users' visits. That's pretty huge, right? 16 seconds could take that 19 second loading app down to three if you were able to condense all of those network hops into something that you could cache. If I could, I would take this off and I'd do a mic drop because I think that's probably one of the most exciting things to me about client side storage. But with great power comes great responsibility, right? We're now using resources on the user's device and this is kind of reinventing what we think is the contract we make with users. So first and foremost, you need to make sure you're measuring and thinking about your app's overall storage footprint. So this is something like figuring out your eviction strategy to make sure you don't just balloon up to 6% after three visits. But the whole point was we wanted to be using the user's device, so we can't just keep arbitrarily lowering our storage footprint, right? That would get us back to where we are today. So the second number that comes in is your read to write ratio, and this is something that Chrome Storage Team thinks about globally as well, which is where we try to make changes to our eviction policies that reduce the storage footprint without lowering this ratio. That means we're trying to clear out data that's never going to be read again. Now, sometimes you'll clear something and maybe it was going to be read in three months, right? And sometimes that's right, but sometimes you actually do want your cache to stick around for three months. So another metric that you can look at is when you store something, check to see if you had cached the resource before. And if you had, look at the time difference between the two, and that'll give you a sense of how long of a horizon was this sitting there for kind of useless on the user's device. So these are the three numbers that Chrome looks at, and Chrome really cares about. And I think it's a really useful way to think about storage, but I would love to hear from other people if they have other metrics that they think are important to track. It's a really interesting space. Your eviction strategy is not the only thing at play though. The other browsers have eviction strategies of their own, or at least some of them do. So for Chrome and Firefox, we evict your storage, or any storage on the device. When Chrome or the disk is full, we evict the most least recently used, most least recently used, that's not great. The least recently used domain from the list. Now it's important to note, this is very rare. Chrome clears a domain storage less than 0.1% of the time. So for the most part, when you store something it sticks around, but it is something to keep in mind. Safari and Edge, however, don't clear index DB. So you can treat that as persistent. Now on Mozilla, or on Firefox and on Chrome, there is something to try and help you work around the eviction policies when it's important. It's called persistent storage. It shipped in Chrome 55, and it's in development with Firefox. So the way this works is you essentially request the persistent storage permission, and then Chrome will exempt you from automatic clearing. Well also, when the user clears browsing data, pop up a prompt for any persistent storage sites that says you're also gonna clear these, is that okay? So this is trying to help make sure that if you've entered a contract with your user that something should be available offline, you can guarantee that. Now unfortunately, when you do user surveys and you ask them about storage, it becomes pretty clear that it's not something they either want or are able to effectively reason about upfront. If you ask a user, hey I'd like to store 100 megabytes of your data, is that okay? They'll either freak out and say no, or they just won't really understand the question. But they are very good at reasoning about your storage is full, which site would you like to clear? So because of this, we try to avoid showing a permission prompt when you request durable storage or persistent storage. Instead, we have a heuristic, which we use to either automatically grant or deny. And the heuristic is essentially, if you're treated like an app, you'll get app like storage persistence. And that means if you've been added to home screen, if you have push notifications, if you've been bookmarked, or if we've seen if Chrome has tracked that the user has engaged with you, with your site a lot. So if any of those hold, you'll get the permission, otherwise it'll be denied. We recommend that you hold off on showing offline UI until you've received that permission so that you know it'll be around. Certainly not a requirement, but it's a little bit of a best practice. And then use the quota estimate API to make sure that you aren't ballooning your storage, or you want to make sure if you have a regression where you get some kind of storage leak, you can clear it up, because now you can't rely on the browser to protect you anymore. You have to kind of take your life into your own hands. That's sort of the end of my practical area of the talk. You guys laughed at a few of my jokes, so I like you. I feel like we've grown close over this time. I want to give you a look into what we're thinking for the future, because I think it's important. I think it's gonna change the way we think about storage and apps and offline and all of these things. So first and most importantly, we want to give you guys more space. We're kind of channeling our inner Elon Musk. You get more people with more space all the time. This is kind of a new paradigm. On Chrome, we're thinking about how can we start giving PWAs, or web apps in general, access to as much device storage as native apps get. And we want to do this because we think, as PWAs become more common, the divide between apps and PWAs and all these things are gonna become less clear. And so we want to give developers all the tools that they need to make great experiences. Some of you might be cringing or freaking out. It is a little bit of a divide. You could go to a website and it could take all of your storage. So this is something we're thinking about very carefully. And again, those three metrics I talked about before, we're tracking those very closely and we're gonna be ratcheting this up slowly to make sure that bad ecosystem changes aren't coming into play. So this is something, though, to be looking for storage increasing over time. We're also thinking about some new functionality and it kind of falls into two stages. We have one set of things that are in development. They're actually pretty far along.  So if you have a kind of UI that uses something like that, it's really effective for making it quite simple. Async cookies are gonna be a big win. They'll also be available in service worker. So that's pretty awesome. Both of these are Wikig or YCG specs that have some degree of implementation. So they're coming soon, they're sooner rather than later. Then we have a couple areas of exploration that we're looking at. So I mentioned a lot of libraries that will give you promise support for IndexedDB. We know it's great. We know it's the way that people wanna work with async code moving forward or at least a large subset of people wanna work with it that way. But it turns out layering on IndexedDB promises to transactions is kind of thorny. It turns out to hit all the edge cases it's hard. So this is an area that in terms of baking into the platform we're still thinking about and figuring out. The last one is kind of exciting and it's personally very, very cool to me. We're calling it writable files but it's the idea that we wanna start giving web apps the ability to get reusable handles to files on the user's device. So I'm sure a lot of you have gone to some website where they ask you to upload a file or they offer to download a file and you downloaded it as a zip or every time you made an edit you had to re-download the file. You had to re-upload the file. It's not a great user flow. So instead what we wanna do is create a way for apps to get a handle to a file such that they can just track changes to it like a normal app would. Again, this is an area of exploration. We're figuring out how to get the privacy and security models right but it is a spec that's available on the Wikig and we would love to get people commenting there telling us what use cases they might have for it, what concerns or mitigations they have planned. It's all on GitHub. We would love to get collaboration from everyone. All right. I hope that I've made an okay, hopefully great case for the idea that caching with client-side storage is a huge win that you have available to you today. It's not the easiest or the first thing you'll jump at. Performance optimization is kind of in a lot of ways, at least for me, when I'm developing a secondary impulse to making it look right or adding a cool new feature but it can be a huge win and it can really translate to increased bottom lines. So it's very important. And I hope that I've convinced you guys that there's stuff that you can do via link rel preload, loading blob URLs for images, storing things in index DB that work across all browsers and that you can do today and that it's not too much work to get it working. A few concrete takeaways is that storage isn't just about offline. Think about it as a performance optimization just as much, if not more. Offline is amazing but until your page is loading quickly, there's not gonna be anything available offline anyways. 50 megabytes is available to you on all browsers, on all devices. And this is gonna go up as time goes on and it will go up when you have users who are using higher end devices but this is sort of your bare minimum budget you have for improving performance. Index DBs for structured data, cache storage where it's available is for URL addressable data. And that's it. Thank you guys, I really appreciate you taking the time.


The question is the problem unfortunately is that this is in general not the case, in general v upper bar will not be equal to v lower bar ok. So, if so as I was saying that if these two end up being equal then it would be that each player's projection about the worst case actually in short comes true right. So, we can formalize that by through this concept. So, suppose let i star j star be a player 1, player 2 such that a i star j star ok. So, you look at a i star j star with this is what is this quantity here, this quantity is the payoff that the players would get when they each play i star and j star ok. Let i star j star be a strategy such that a i star j star is less than equal to a i j star and also greater than equal to a i star j for all i and j ok. So, which what does this mean? That means that i star j star is such that when the if you look at it from the point of view of the row player here ok. So, there are two inequalities that i star j star satisfies, i star j star as this property that if you look at it from the point of view of the row player then assuming the column player is playing j star the row player responds with i star right is the best thing for him to do is to play i star and likewise assuming the row player plays i star it is the best thing for the column player to do is to respond with j star is clear. So, if you have these two such a if i star j star or if a pair of strategies is like this that satisfies this then i star j star are called a saddle point ok. So, this pair is called a saddle point. Now, I have used the notation i star j star for security strategies I am also using it again for saddle point and the reason for that is see if the if the security strategies together ended up forming a saddle point then you would have that then this then they would actually suffice to solve the game because effectively it would mean that each player when playing his security strategy the other guy responds also with the security strategy right because the response to i star is j star then the response to j star is i star ok. Now, how now this so if you could find such a pair i star j star that satisfies this is called a saddle point if you could find such a pair then this would actually end up solving our problem alright. So, we will actually let us actually prove that. So, theorem is this let A so, suppose let A be a matrix game such that V upper bar is equal to V lower bar then one then A has a saddle point ok and B second the saddle point comprises of security strategy. You can write out another part of this that if any pair of security strategies is a saddle point alright. So, so let us let us go about proving this. So, we already know that there always exist security strategies. Now, what we are going to show is that if V upper bar is equal to V lower bar and you put together that pair of security strategies they automatically form a saddle point ok. So, that is that will then show that A has a saddle point and secondly it will also show 3 which is that any pair of security strategies is a saddle point is this clear ok. So, that is what we are going to show ok. So, now remember we have we already know that V upper bar is always equal to V lower bar sorry what am I writing we know that V upper bar is greater than equal to V lower bar ok. So, which means that we know that max over j A i star j is greater than equal to min over i A i j star for security strategies i star and j star. But now what have we been given we have been given that these two are in fact equal ok. We always know that these are this is a greater than equal to but we have been given given V upper bar equals V lower bar that these are equal ok that is what we have been given. So, which means what therefore we have max over j A i star j is equal to the min over i A i j star ok. So, these are remember i star and j star are security strategies. Now what I need to show is basically that this actually i star j star in fact saw form a saddle point ok. So, how do I show that well remember min over i of this is always less than equal to A i j star and max over j of this is greater than equal to A i star j ok. So, now if I put and so this is true for all i comma this is true for all i comma j which means what now if I put i equal to i star and j equal to j equal to j star what would I get I would get A i would get equality throughout I would get A i star j star is equal to V upper bar A is equal to V lower bar A is equal to A i star j star alright. Now what this in particular means now remember what was V upper bar A V upper bar A itself was equal to the min over i max over j of A i j alright. So, in other words this was always always less than equal to max over j in lower bar A is max over j min over i A i j. So, therefore, this was always greater than equal to min over i for all j ok. But now what we what we showed was actually the these are each equal to A i star j star both of these are equal to A i star j star. So, therefore, now putting putting this is this is true for all i and for all j. So, I can write this for all i for in fact for i star and j star. So, what would I get I would get therefore, A i star j star putting these two together gives me. So, this is the minimum over i of A i j star. So, therefore, this is less than equal to A i j star for all i and also greater than equal to A i star j for all j. So, actually I do not need this to be less than equal to the point I actually need just this impact to be out here all I need is that this is impact the max over j A i star j and this is min over i of A i j star is this clear. So, I just showed that we upper bar we lower bar are both equal to A i star j star and because they are themselves equal to max over j A i star j and min over i A i j star that then gives me this input which means that which means that i star j star is a saddle point. So, what does what has this shown this is shown that both this as well as this. So, it is shown that A has a saddle point that is also shown that you take any pair of security strategies they will necessarily be they will they necessarily form a saddle point. You actually get one more thing for free here which I have which I have not specified, but that it tells you that actually when there is a saddle point right is V upper bar and V lower bar are in fact, functions of just the matrix and not the saddle and does not matter what the saddle point is whichever saddle point you choose if there is a saddle point whichever saddle point you choose the V the value is always going to be V upper bar and V lower bar is clear. So, so V upper bar and V lower bar were defined for from security strategies and therefore, they were functions of just a the saddle point was just defined abstractly as a bunch of inequalities. So, there is no guarantee that the value of that saddle point could be is has to be the same for every saddle point, but we are getting that for free whenever there is a saddle point, it will always be equal to it will always be equal to these this particular value. So, alright, so let us actually show the second part 2 here, which is that that a saddle point comprises of security strategies. Alright, so now what is the definition of a saddle point saddle point is that is the point I star J star such that I star J star if I star J star is a saddle point, then this must hold and what we will show is we will show that I star J star are security strategies. So, how do I argue this from this inequality I want to argue that I star J star are security strategies, which means I want to argue that I star is the one that minimizes the worst case damage for the row player and J star is the one that minimizes the worst case damage for the column player. So, how do I argue that we could try by contradiction, there is a simpler argument here. So, if you actually look at just this part, right, so this is the in fact the the interesting thing about zero sum game. See, if you look at these in isolation, any of these in isolation, look at this inequality in isolation or this inequality in isolation, this is only saying that I star is is the best reply to J star and this is saying that J star is the best reply to I star. It does not actually say that these two are, we are not really using the fact that these two hold simultaneously. This is just saying that each player is responding with his best reply, but that they end up giving the same value is not actually being used here. So, if you want to get back the security concept, right, then you have to use that you have to you cannot use it is not enough to use any of these in isolation. You have to use the entire chain of inequalities, which means that you have to use that this left extreme is actually less than equal to the right extreme. Now, what does that mean? That means that A I star J is less than equal to A I J star, okay? A I star J is less than equal to A I J star. So, but then what is A I J star that is in turn less than equal to A that is in turn less than equal to the max over J A I J, right? The right hand side is now, okay, I should maybe I will make it easier. I will first do this. So, this is the left hand side is a function of J. The right hand side does not have J. It has only J star. So, I can say well, therefore, max over J of A I star J is less than equal to A I J star, but A I J star is itself less than equal to max over J of A I J. And so, therefore, you get that max over J of A I star J is less than equal to max over J of A I J, which means that I star is a security strategy. So, this one here, I can observe that in this from this inequality on the first inequality here, left hand side is now not a function of I and the right hand side is a function of I. So, I can do a min over I over there, min over I J star and the left hand side will be, will still remain I star J, but then that is in turn greater than equal to min over I A I J. Now, combining these two tells me that J star is a security strategy. In other words, there is really, once the V upper bar and V lower bar are equal, there is no difference between saddle points and security strategies. Conversely, if a saddle point exists, then automatically you will get for free that the V upper bar and V lower bar are equal, because every the saddle point has to comprise of security strategy. So, if there is a saddle point, you will, they comprises of security strategies and you will get that, yeah, this saddle point value is actually equal to V upper bar and V lower bar.