Okay, so it's five minutes past two. I think we start the afternoon session. Welcome back, everyone. So the first talk will be from Kasha Vigil, which will be titled in the search of a bijection between Tanomo-3 and the composable planar lambda terms and beta-01 trees. And this one is actually quite a nice talk because it's started from a bijection from last year's CLA. So we're really curious to hear more about it. So Kasha, please go ahead. Thank you, Mikhail. I hope you all see my slides and hear me well. So this talk is covered by Guanru and I will explain soon how he came into play, how he started doing in this lambda business as well. So last year, no, I'm at the talk and this talk was covered with Jason Reed. And after his talk, I wanted to see what it all was about and to recall some details. And at some point, one thing struck me, namely this conjecture. So I forgot about everything that I saw so far, about everything that I learned. I just focused on this very conjecture which was exactly in this form as what we saw recently. It was the slide by none. And the conjecture says that beta normal free in the composable planar terms accounted by the OEIS sequence A00257. So while I was, since I was a postdoc in Vienna at that time, I thought this must be easy for me in this Vienna environment. So this Vienna atmosphere should work pretty well and inspiring. And I kind of quickly find some recursive definition and so on use symbolic methods and then standard methods of analytic combinatorics. But it turned out that I failed. And then I thought, okay, I cannot do it like this. I should read something more. So I went to the OEIS webpage with this entry 257. And what I liked about it is where those descriptions about maps. So it turned out that the sequence enumerates some particular kind of maps. And since I was an office mate of one rule and he was just finishing his PhD, he's just in maps. So I thought, okay, we can work together. Why not? And he is an expert in maps. I know something about Lambda terms so we can join the forces and somehow solve this problem. So okay, I have to admit we didn't solve it. We have some ideas how to attack it. We have some partial results. I won't prove the conjecture, but I hope we are in a good way. And this can be also discussed during the open problem session. And if you have any ideas, it would be nice if you could give us a hand. And here is a mind-bub showing some combinatorial objects that are enumerated by this sequencing question. What you can see here in the middle, there exists an explicit formula for the number of those particular maps or beta 01 trees, about which I will speak soon. And as we hope, beta normal free in the composable planar Lambda terms. And the formula is not really complicated. But what's interesting is that when some researchers were studying rooted by cubic maps, they didn't find a nice recursive description of the sequence that enumerates for the numbers that enumerates these objects. And this formula was not derived directly. The other objects that are interesting that are in bijection with these rooted by cubic maps are beta 01 trees. And I will speak a lot about them because we really concentrate mostly on those. But the other objects which are also very nice are new intervals in tamaril lattices and Wengie's degree trees. I'm happy Wengie's here because I read his paper where he shows the bijection between his degree trees and new intervals in tamaril lattices. And I like the ideas there. Maybe he can also help us somehow with how to deal with this beta 01 trees business. Okay, and because this is the first talk where Lambda terms appear, probably I should just very quickly mention what they are for those of you who have never heard about them. So Lambda terms are building blocks of Lambda calculus which is the model of computation. But we can forget about computations about Lambda calculus because we will look at Lambda terms as at some particular unary binary trees. But in general, we have a countable set of variables and we built new trees in such a way that every variable is a term, every application of two terms is a term and every abstraction is a term. Abstraction is this thing that we have here and we write Lambda variable and the term that exists. So if I write Lambda, some variable X and the term, this is also a Lambda term. And here is an example of a quite big Lambda term the longest I could fit here in the screen. And of course, we cannot see much out of it, but what is important is that we don't care about the names of the variables here, all the variables that appear here are bound. So it means that every variable has been introduced by some Lambda like here. And what we really care about is which variable is bound to which Lambda. So here I write down this Lambda term just using colors. I don't need variables. So if we see the blue dot like here, it means that this is a variable that is bound to this blue Lambda and so on. But of course, this notation is also not very nice to deal with. So what we can do, we can use another representation and we will represent Lambda terms as trees. So now every unary operation, this is this abstraction is replaced by a unary note like this and everything else goes below. And if we have a binary note here in the street, it means that it means that we have an application and this application doesn't have a sign here. It means that we have two terms that are applied one to another. So this is one big term and this is another big term. But we don't really need to focus on this because we can get rid of the names of the variables. And for example, your scholars, but the nicer way is to use arrows or connections or those edges even without these arrow endings. So it means that the variable that is represented by the sleeve is introduced by the unary note or Lambda in abstraction that is exactly here. So we have this structure which is a tree with some pointers added and it's much nicer to look at this structure at least that's my opinion. But as you might have noticed in my title, there were many objectives describing some very special Lambda terms and this terms indeed have many properties which makes the whole picture much easier. So the first thing is that we consider on the linear terms. The linear terms are such that every unary note has exactly one binding to one leaf. And there are no unary notes that have no bindings. And of course every leaf this follows from the definition of Lambda terms is bound on exactly by one Lambda. So this term that we have here to the right anywhere but it's easier to look at this tree. So this term is of course not linear because there are many Lambdas that do not bind anything. And the other reason is that there are some Lambdas like this one that bind too many Lambdas. We like for example this Lambda, this unary note because it has just one binding. And because now linear terms have a very nice tree representation namely by unary binary trees in which the number of binary vertices is just by one smaller than the number of leaves and the number of unary notes. We can measure the size of a term as the number of applications only. Okay, so I will write that now the size of a term is three K plus two. I mean all the vertices in the tree representing the term has three K plus two and notes where K is the number of applications of binary notes. So this will be our size of a term. And now what we will do, we will fix the order on leaves and we fix the order from right to left. And now we join every leaf with the first Lambda on the path that leads from this vertex to the nearest Lambda that hasn't been taken yet. And the resulting structure will correspond to a planar Lambda term. This is because these Lambda terms as viewed as these graphs or maps for some reasons are really planar. So I will show the example because otherwise it's difficult to understand anything. So here we have this skeleton. Here we have a unary binary tree that corresponds to some probably many linear Lambda terms and what we do as I said, we fix the order on leaves. So there are four leaves here and we take the rightmost one and we find for it the first free unary note that lies on the path to the root. So this is the corresponding unary note. And then we search for the first three Lambda for this one. So we have this, then we have this, and then we find this. And as you see, having this operation, we of course have a planar, we obtain a planar graph. So I don't want to get into those details about maps and so on, but that's how we are going to look at those trees. We always encircle the tree from the right side and make those edges longer and longer so to encompass the already created structure. So here is nicer picture showing what I wanted to explain. And for those who prefer to think more in a more Lambda calculus way, here is what it means to be a planar term when we have a linear term. Then the variables that appear, like the occurrences of variables are exactly in the order that they were introduced. I mean, the first, it's not exactly maybe what I should say, but it's again linking to the nearest Lambda. Okay, and the size of this tree or this term is free because there are exactly three binary notes. So this is one, two, and here is the third one. Okay, there are more. I think we're the closest to the Lambda because in this example, Lambda x, y, x, x, x. Oh, you wrote something. I'm sorry, you asked soon. Can you repeat it because I hear it really badly. Maybe it's a good idea if I put the questions because you cannot easily hear me. Oh, yeah, I hear you, but you wrote something. I guess this is not very important, but at least this is a kind of a question. One can, oh, okay. The convention of parenthesizing. We parenthesize Lambda terms as usual. So whenever we have an application, I'm sorry, I stopped writing, it is like this and P, let's say, then we parenthesize to the left, but whenever we have an abstraction, should I write like this, Lambda x, y, z, it's, oh, I'm sorry. Okay, so this denotes something like this, Lambda x, Lambda y, Lambda z, and then the closing parenthesis. Does it understand, does it answer your question? And here is, it was to Jason, and that's for CRDA. I know the terms of closes, applications with ones. Yeah, yeah, so that's why I said that it's not, yeah, I said that I made a mistake. It's not the closes, but it's not the second closes. It's the, oh no, I'm sorry. So CRDA, I don't understand it actually. I'm sorry. Maybe we can discuss it later. I think that this figure here can clear things up. So we find the first three, Lambda. Do they agree or not? I would like to know it. We're at the same level. Okay, I don't see any comments, so I will go on. How can I formulate? Let's skip this question for now. Okay, I wanted to make it as short as possible because anyway, I have too many things to present. Okay, so we can discuss it later. Sorry. Okay, so there are two more things that I have to explain. The first one is being better normal. So a Lambda term is better normal if it doesn't contain any, oh, I'm sorry. It shouldn't be written like this. It should be like this. Lambda XM applied to N, I mean, in the terms of trees, it means that left leaf is never unary. So we never have a situation like this. So we never have a subterm of this shape. So this node, this left node is never a unary node. Okay, and now the last definition is about free in the composableness, in the composability. Namely, in the case of those terms that we have here, we always joined unary nodes with leaves. And as we see, these nodes are not very informative, so we can just skip them. And when we skip them, we want the resulting map or graph to be internally free connected. And that means that if we remove any two edges, but the two incident to the root ones, then the map or the graph has to remain connected. So I think I will again show a figure. It's much easier to understand what's going on. So of course it will look like this. So we obtain a graph that looks like that. Then after this operation, we remove the leaves. And this resulting graph has to be free connected, but there is this adverb internally free connected. And it means that removing these two edges does not count. So removing any over pair of edges cannot lead to disconnecting this graph. So I have an example of a term that violates this condition. So let us look at this picture. First, we join the leaves with unary nodes, then we forget about the leaves. We obtain a graph that looks like that. And for example, if we choose these two edges, then the whole structure becomes disconnected. Okay, I hope these notions are not well-defined. So these are the objects we are interested in. These are lambda terms, which are planar, which are beta normal and also free in the composable. So the corresponding unary binary trees have some particular properties. So the first one is whenever we have a term of size, at least three, then it starts with at least three unary nodes. The second property tells us that if we look at the term and forget about those unary nodes, then the left subtree is always triggered, namely it's always a single leaf. Otherwise the free in the composability condition would be violated. And the third condition, which is probably the most difficult one to describe, is such that whenever we look at a subterm, which is proper, so it's not the whole tree, and it's rooted at the highest lambda, or unary nodes, on the path of lambdas. So in this case, there would be free. Free trees like that. Then the number of unary nodes in the right subtree, so we look only at the right subtree, plus the lambdas on the path has to be smaller when the number of leaves in the right subtree. And I will show the examples so that you could understand what I have just said. So let's look at this simple subtree. It's rooted at the unary node. And now we count all the unary nodes that appear in the right subtree, and we add all unary nodes that are on the path here. So it makes one, of course. And then we look at the right subtree and count all the leaves that are in this subtree, and in this subtree have three leaves. And we see that indeed three is greater than one. So when we look at another example, here we have one unary node and we have two leaves in the right subtree. And again, this condition is satisfied. And for the big one, we count the right leaves. That's easy, that's six. But as for the unary nodes, we count all the unary nodes that are in the right subtree, and we add these top ones. So that's why we obtain three here. And of course, six is greater than three. So this condition is satisfied in this case. And I'm not sure, but probably these three conditions, that's what we conjecture, these three conditions should be enough to describe lambda terms that satisfy all these properties that we're interested in. Okay, and now when we have these trees, we can only look now at unary binary trees because we know which unary node is connected to which leaves so we can forget about the pointers. And now we do some preprocessing on these trees. So the first operation that we do is skipping all unary nodes that are above because this number is determined by the difference between the number of all leaves here and the number of all unary nodes. We just have to add all the missing unary nodes here. So we can skip this upper part. Oh, I'm sorry. I mean, notice this device takes time. Okay, so that's one thing. And the other thing is this strange operation of sending gifts and they don't want to give a formal definition. I will show an example of what we do. So we look at the rightmost path of unary nodes, but we care only about unary nodes ordered via this tree. So it means that we also look at this unary node here. If there's the right unary node for us. And now when we do that, we look at all left sub trees. So these left sub trees are now in those and circled by this nice curves. And what we do next is we shift all of them one level up. We have to remember that this tree here is trivial. This is only a leaf. So we never need to shift anything from here. So all of those bubbles moved one level up. So after this operation, we obtain a tree that looks like that. And no wonder this leaf here remains alone this tree here becomes simply a leaf. And this will be an important part in our bijection. So this sending gift part means that we have some linear order on some sub trees and we just move them one level up. Okay, so when we perform this preprocessing, we obtain some unary binary tree. And now we can decompose it into maximal binary parts with some unary paths. So we can see now that every tree can be represented by some binary trees with some placeholders marked and then the number of unary nodes and so on and so on. So this is the composition will be interested in. Here I just gave a definition of what it means to for a plane and routed them up to be bi-cubic because I started with bi-cubic maps. It's not important for us. So I'll just say that these maps are bi-partite and cubic but it was difficult for us to deal with maps. And we decided to deal with overstructured structures namely beta-01 trees because they are numerated by the same sequence. And beta-01 trees are trees that are routed, they are plane and they are of any r-e-t. But what is important is that every leaf is labeled with zero. Every parent is labeled by one of the labels from zero up to the sum of the labels of its children plus one. And another note that has a determined label is the root namely the root is equal to the label of the root is equal to the sum of its children's labels plus one. Okay, so this is what I have already mentioned. So now let's play a little bit with beta-01 trees. Here are some examples of beta-01 trees. So let me recall every leaf is labeled with zero. Then when we go up, we can, for example, here we can choose from either zero or one. In this case, here we can choose either zero or one because we add the labels in for children and make it greater by one. And for example, a more interesting case which is more interesting. For example, I know I made a lot of jumps here. So this one, this is one plus two and we can increase it by one if we want but it could be free for example. So these are examples of beta-01 trees and the conjecture states that these trees are in the bijection with our lambda terms. So our goal is to know how to decompose beta-01 trees so that it corresponds nicely to the decomposition of lambda terms. So for this reason, we define the so called beta-01 bricks or bricks for brevity. And this will be beta-01 trees which have just one leaf. So they have no binary nodes with its root removed. We know that in beta-01 trees, the label of the root is determined. So we don't need it here because it doesn't give us any new information. So these are all possible bricks. And as you can see, or guess, the bricks are enumerated by Catalan numbers. And it did, we can show it easily and we will use this fact, we'll use this proof. So the first thing we do, we label regular binary trees and we label them in such a way but every internal node gets a label which corresponds to the number of right edges or right leaning edges on the path from the root to the node that is being labeled. So this is the recursive definition of how we label them. And of course, we start with zero because there are no right edges leading to this node. And on this leftmost path, we'll only have zeros. But if we go a little bit down, the label of those nodes will increase. And here I can draw an example, sorry. Okay, so we start with the root, it will be zero. And now we proceed recursively and we remember that for this tree, we don't change anything. And for this right tree, we'll have to add one to every label. So this one becomes zero and we proceed recursively. So this is zero again. This will, in this part, we have to increase by one. So this is one and this is one. And similarly, here we have to increase the labels by one. Then we don't need to go to the left. There are no internal nodes on the left. So we go once more to the right. So it's two and here it's two again. Okay, so it's not maybe not nicely drawn but this is how we label binary trees. And now how do we translate bricks to trees? So whenever we have a brick, we find the highest zero. There is always at least one zero in a brick. And then we bend it and translate it recursively this time decreasing the labels in this right tree. So let's say we have such a brick. So what happens if we want to translate it to a tree? We look at this highest zero and we bend it. So this will go down. So we have zero. And for this part, I maybe shouldn't say, I should maybe say right. And this is left. So we bend this left one. Where do we bend it? We bend it where the highest zero is. So it's this zero. So to the right, we have nothing. And to the left, we have this tree. So it makes zero, one and two. I can also give, oh, I have already given a label here. It's zero, zero, zero, one and two. And to the right, we have one one and one one gives us one and one. So this is how we translate bricks to trees. We can of course remove the labels that matter whether we have a label tree or not. And in a very similar way, we translate trees to bricks. So I'm not going into the details. It's straightforward how we do it. So this is an example. I will skip it. And as I said, our ultimate goal is to know how to decompose.  Yeah, I know, I know. So we want to know how to decompose those beta zero, one trees and how to decompose encode lambda terms. The important thing is that in our candidate for a bijection, the number of those maximal binary trees, those maximal parts in lambda terms corresponds to the number of leaves in beta zero, one trees and it makes everything much easier. So we have some trivial cases. I would steal five minutes because I started five minutes later. Okay, so the trivial case is when we have an empty tree and this will correspond to this trivial linear term, the smallest one. And if we have an over-trivial case, namely the beta zero, one tree is just a single node. Then we have an over, the next smallest lambda term, which is this one. And we see that we can just skip this and skip this and skipping those head unary nodes. And then we translate what is left. So for this binary node here, it's just zero and it corresponds to zero. Now, if we have a nice situation, namely there are, the easiest cases when we have just one leaf in beta zero, one trees, then that the composition is straightforward, namely we just create a brick out of a beta zero, one tree. So we forget about this top node then we translate it to a binary tree and then we add this missing left single node and add an appropriate number of unary nodes. So this is the first building block that we have. So lambda trees with no lambda terms, with no unary nodes in this part, are just generated by Catalan numbers. Okay, so if we have such a binary tree, we just skip this one, we translate it to a binary tree and we get a lambda term that looks like that. Then if we have no jumps, it means, okay, I will skip what it means being a jump, I can explain later. If we have a nice situation, then the composition is also nice. So we always take the right most edge, but it's possible to be taken. And in this case, we take these six edges and then we just write what we obtained from this decomposition and we add those classes here to denote how many steps we have to go up to start a new edge. So here we had to go one level up, here we go to levels up, double and so on. And if we have those, we translate those parts into binary trees and then we combine them in a very easy way, it will be always be the right cleaning thing. The problem appears when we have jumped. And this is a, I've forgotten that we have this gift. So at the very end, we have to give this gift down. Okay, so the main part in our research at jumps and the jumps are those nodes that are not roots, but they are greater by at least two than the right most child. So in this case, those jumps are shown how they look like. So here we see that two is greater by at least two than zero, three is greater than one, much greater and four is much greater than two. And two is much greater than zero. So in the third case, we have two jumps. And I have no time to discuss the jumps, but we have distinguished three kinds of jumps, the green, red and blue, and they dictate somehow the decomposition of trees. But it's, I knew that I would need more part because for every jump, we have some special translation which translates us one brick into an over and tell us then how to make the combination and how to cut out those things. So I have some examples so the slides will be available. Maybe you can go through them. I think it's more illustrative to look at those examples than just listening to me. But anyway, in this very example, you can see that now we don't take the cool thing out. This time we just take a net which consists of these two vertices. So it's much more involved than before. Okay, I know I have to stop. So I will stop at this point. So thank you very much, Kasia. Thank you very much. Very colorful talk. So we are quite in time, but maybe we have time for a very quick question. We can postpone all the discussion, I guess into the example section or on the open problem session because there I guess you can maybe then explain in detail what kind of problems you have there. But could I just ask a question, Kasia? So could you say again, I mean, what exactly is missing from the projection? Okay, so I didn't present everything that I had here, but we have these three kinds of jumps and we know what to do when we have just a single kind of jumps in a tree. Just one particular kind of jumps, but we get lost if there are many different kinds of jumps. So those they are interliving. So the character of a jump is determined by these paths on which they lie. So if we have a path like that, it dictates the character of a jump. And then we know how to do it. Could you just back up? So you're building a function from beta 01 trees to three... To those lambda terms. Yeah. To those lambda terms? Okay. Or the other way around. Or the other way around. Yeah, yeah. Based on the composition of the lambda terms. What's the idea? Go ahead. So, okay, so maybe I will quickly throw an example. Oh, here I have some space. So don't bother about what we have here. If we have a case of a term like this, then in this right tree, we have two kinds of... Okay, I mentioned jumps. So the first operation that we perform is sending this thing here. Okay. And when we send it here, then we have unary nodes in both sub trees, in the right and the left. And it corresponds to some kind of a jump in beta 01 trees. And then when there are many situations like that, at some point we get lost about how to proceed recursively for this. So we have some building blocks. We know, for example, how to deal with this case. We've some more involved ones, but there is a level where we are lost. We don't know what happens if there is a subterm that corresponds to a red jump inside the subterm that corresponds to a blue jump and so on. If there are too many levels of those, we don't know how to translate those. Okay. And just so the beta 01 trees were known to be in bijection with bi-cubic planar nodes. Yes, yeah. Exactly. And any, what about anything else in that diagram you showed? Oh, I have tried to work for a while with the tree trees by 1G, but then one of our had a new idea about those beta 01 trees and we finally stank again doing these things. Stank again. Yeah, I knew that 35 minutes wouldn't be enough for this. So I would be really happy I could discuss it with anybody interested. So, Alex has just created some couple of more channels on the Discord server to continue discussing the different talks so we can go ahead and discuss for all of the talks afterwards in Discord. Okay, so I will stop sharing because it's time. It's a perfect thank you, Kasia. And well, we're supposed to start right.