Enumeration on Trees with Tractable Combined Complexity and Efficient Updates

Video thumbnail (Frame 0) Video thumbnail (Frame 2128) Video thumbnail (Frame 2585) Video thumbnail (Frame 10599) Video thumbnail (Frame 12705) Video thumbnail (Frame 21860) Video thumbnail (Frame 24433)
Video in TIB AV-Portal: Enumeration on Trees with Tractable Combined Complexity and Efficient Updates

Formal Metadata

Enumeration on Trees with Tractable Combined Complexity and Efficient Updates
Title of Series
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Release Date

Content Metadata

Subject Area
We give an algorithm to enumerate the results on trees of monadic second-order (MSO) queries represented by nondeterministic tree automata. After linear time preprocessing (in the input tree), we can enumerate answers with linear delay (in each answer). We allow updates on the tree to take place at any time, and we can then restart the enumeration after logarithmic time in the tree. Further, all our combined complexities are polynomial in the automaton. Our result follows our previous circuit-based enumeration algorithms based on deterministic tree automata, and is also inspired by our earlier result on words and nondeterministic sequential extended variable-set automata in the context of document spanners. We extend these results and combine them with a recent tree balancing scheme by Niewerth, so that our enumeration structure supports updates to the underlying tree in logarithmic time (with leaf insertions, leaf deletions, and node relabelings). Our result implies that, for MSO queries with free first-order variables, we can enumerate the results with linear preprocessing and constant-delay and update the underlying tree in logarithmic time, which improves on several known results for words and trees. Building on lower bounds from data structure research, we also show unconditionally that up to a doubly logarithmic factor the update time of our algorithm is optimal. Thus, unlike other settings, there can be no algorithm with constant update time.
Inheritance (object-oriented programming) Wage labour Link (knot theory) Algorithm Multiplication sign Quantification Price index Theory P (complexity) Data management Goodness of fit Performance appraisal Network topology Well-formed formula Query language Logic Monad (category theory) Vertex (graph theory) output Inheritance (object-oriented programming) Kolmogorov complexity Cellular automaton Magneto-optical drive Set (mathematics) Enumerated type Subject indexing Numeral (linguistics) Well-formed formula Intrusion detection system Alphabet (computer science) Logic Network topology Order (biology) Phase transition Resultant
Rekursiv aufzählbare Menge Algorithm Kolmogorov complexity Multiplication sign Subject indexing Pattern language Damping Aerodynamics Data structure Enumerated type output Mereology
Logical constant Complex (psychology) Presentation of a group Greatest element Digital electronics Code State of matter Correspondence (mathematics) Multiplication sign Source code Combinational logic Mereology Automaton Semantics (computer science) Neuroinformatik Database normalization Preprocessor Rekursiv aufzählbare Menge Mathematics Semiconductor memory Phase transition Network socket Forest Query language Negative number Pattern language Cuboid Aerodynamics Logic gate Partial derivative Physical system Normal-form game Logarithm Kolmogorov complexity Binary code Moment (mathematics) Keyboard shortcut Constructor (object-oriented programming) Automaton Variable (mathematics) Element (mathematics) Binary tree Preprocessor Linearization Compilation album output Normal (geometry) Right angle Freeware Task (computing) Set (mathematics) Motion capture Family of sets Theory Depiction Product (business) Performance appraisal Network topology Helmholtz decomposition Term (mathematics) String (computer science) Subject indexing Energy level Data structure Codierung <Programmierung> Compilation album Linear map Task (computing) Physical law Set (mathematics) Semantics (computer science) Digital electronics Performance appraisal Personal digital assistant Logic Network topology Partial derivative
Context awareness Presentation of a group Boolean algebra Euler angles Multiplication sign Combinational logic Neuroinformatik Front and back ends Preprocessor Rekursiv aufzählbare Menge Forest Videoconferencing Convex set Vertex (graph theory) Algebra Multiplication Physical system Electronic mailing list Sound effect Automaton Term (mathematics) Demoscene Abstract syntax tree Forest Arithmetic mean Well-formed formula Preprocessor Theorem output Normal (geometry) Right angle Resultant Asynchronous Transfer Mode Polynomial Twin prime Freeware Untere Schranke Real number Exponentiation Rule of inference Root Network topology Well-formed formula Term (mathematics) Operator (mathematics) Representation (politics) Baumautomat Form (programming) Context awareness Cellular automaton Physical law Exponentiation State of matter Enumerated type Cartesian coordinate system Uniform boundedness principle Algebra Personal digital assistant Network topology Rewriting Matrix (mathematics)
Theory of relativity Untere Schranke Multiplication sign Physical law Enumerated type Theory Rekursiv aufzählbare Menge Network topology Query language Network topology Query language Reduction of order Theorem Vertex (graph theory) Data structure output Resultant Reading (process) Reduction of order Physical system
so what's the problem we have given the
data-entry you as a note says labor all
for the sake of support have just call us and we have to use in monadic 2nd order logic so they can ask as I know it has a certain kind over the notice a parent or some other knowledge and the have quantification of UN notes and sets of nodes and the results of Salesforce's theories I just all possible assignments of notes to the the value of of the formula such that the formula becomes true over the given tree and of course you might have exponentially many answers so all we had link and numeration so they have a 1st step very f and indexing phase of you know it's another 1 that's not Leticia so the the produce some next in a document which allows us then to good use on cells 1 after the other I think no thank you at 1 after the other in constant delays all the time between as is just a linear in the
size of a gay any resides and then you can produce 1 after months after the other as there are already many known resides we can all from several different terrorism so that he can do these enumeration this constant today there yeah but
this is now the updates at this time we just we have to recompute scenic structure from scratch if you change any part of the 3 then the improvements on
the next factor such that we cannot dates in poorly logarithmic ordered Resnick time but the coast of the disease that update time was that the delay got fully is made our memories make finally there was some there that we could get constant delaying and not there is need update but only for text soulful Strings not for trees and finally known in this that I presenter resides really can get constant delay and updates logarithmic in the size of the so I was talking about data complexity of course if I have them as all clearees salmon evaluation is on elementary in the size of 6 theory at least if he does not equal the most 3 reside actually much simpler than that and therefore the use bottom up yet for most case of support binary ultimate how to represent a lot theories so be compiled this screws and automaton and actually have some reasonable complexity in the size of salt from what so given an outcome uttermost of mandatory or Edwards and works by knowledge compilation the computer set circulate in decomposable negation normal form from a given automaton endocrine free and this set C accrued encodes all on task that the have a father of theory and answer the given treat so how does a very active semantics of the circuits as follows each gate of a circuit captures a set of sets so in the bottom you have no it's like cease code variable nodes which is like these it's 1 invites really says out take very big should be bond to node 1 and varied right should be bond to notes read so the semantics of such a notice just as set containing a singer I have just notes which say our can be part of an accepting runoffs automaton but actually does not produce any all put because I just some parts it it belongs to a part of a tree which does not belong to the reside but OK it's still it's true I can have nodes a or dates which say that Gaza's does not belong to any valid runoffs automaton this gate source it does not constant belong to any answer and I have combinations like this product where I combined every on some on the left side to every ounce on the right side if I have 2 inputs to produce new begun science and I have union which just takes a union of 2 sets of answers to user because of answers so union is used to combine several different runs also automaton and times is used to combined to Pasha runs to a began around which yeah corresponds to beyond this the all variables and then we can enumerate as a set of some presided for some date and actually it's not that we can do this enumeration constant in it so how does this compilation work on a very high level at taking a lottery the CompuAdd and user-created and actually for every node of all its new input tree we get a subsequent a box they are the have you have you have 1 books for every node of the tree in each of these books is the have Monday which catch captures all Pasha runs of salt come on that end in some states useful for each state of automaton in each box deception gate very kept show partial runs and so this is the bottom-up construction which gives us the socket and then we can use this set a circuit and the enumeration after some additional preprocessing so starting from the circus we need some normalization which just prunes all parts of suspected the way that are not necessarily needed for onset such that you get a smaller selected and the do not based time into parts of the circuit that that do not contribute to an answer that we want to output and on this normalized circuit used you need something next structure to have some shortcuts Diffie do not always need to walk up all Alsace circuit to find the next and so on and on this in next moment I circuitry can finally do or enumeration this constant in in OK so this explains how the
enumeration Lax but this does not explain how I can do updates and still so updates in logarithmic time and then continue enumeration this constant delay the constructions of what impact if I change some node in the tree I can do that date in the ad linear in the depths of the tree just by recomputing sources the secrets a change so starting in 1 box of the 3 they also circuit and then go up all the way to the top and computes part of system OK that's fine but the tree might have a big debt and then still have slightly update time and as we want to avoid and the other thing is all of which I talked up to now is about binary trees the construction it can be generalized to ring trees but out be we need to do a few more tricks Sponring trees and all I want to do 2 things at the same time limits the depths of my construction for lovers size and going to honoring tree is such that I can really work this like HTML documents which of course and ring the solution that we chose laws to depict trees by forest logic what terms so these
spores what terms as an eye of it's basically 2 operations the first one is concatenation it puts trees next to each other so we are now talking about not about trees but about forests and a 1st as an ordered list of trees and I can concatenate forest to get the got for a system which what this more OK it's a 2nd operation is context applications a context as a forest where there is exactly 1 whole year Mac-based there and context application means takes the operand to the right and connected into this the whole which is operand also left and then I get that if I put it forest into given context and Ruud gets a forest Of course I can do context application on the right side there's also a context and that resides in context because the studio hole inside my reside back-ends duplex some sink into and using ceased operations and the size of I can actually we present trees by means also algebra so if I want to represent a tree on the left I can for example stop is put to being notes next to each other so this is what a concatenation operation dust then I can say I take the blue knowledge which has a whole and true lack the result of the formula which I just created into the blue whole this video from your tree was of root and tubing notes the law so all this is a subtree of the given trees obvious through need to add something more on like you can put a rule Nault right also of what the null created and at the end take my knowledge a holed below and plaque everything into the sport there what they keep computed peaceful but of course there are many ways to represent the same to me this does not look very nice and because it's still of great that's we want to have something well balanced but I can edit 1 I tentatively status from real notes next to each other almost which has all be known I can't at my root of it so I have the a right to know knowledge now is tool below and 1 of these modes to as hole the left of the 2 nodes and after lots I can plug into the whole that to written notes distributed of the presentation of the very same and this representation of forest algebra from last been known the to actually represent all input trees to get to yet logarithmic that's so it can be shown that for every input trees there's a formula which has the VA's make debts and even 1 if you do local updates now that we can maintain this logarithmic that's in this form nascent of the formula correspond to the nodes of a given tree it so that the inner nodes are convex application and concatenation and at the bottom of of cease to the syntax trees in the size of our representation I have some notes of solution yeah so to maintain members make that I can use rewritings anxiety run so this is just associative the lawns eye browse that effect plucked 1 next to 2 and then at this we next to it than I can also clock through next was read and Z then at a 1 in front of it so 1 twins we can be arbitrarily the forest OK this vertex because as underlying operation is associated with the same works if I have context application and 1 2 and 3 are context and of course I can also do some more complex quotation and the person who know this can already see that this is modest exactly as an aviator trees what the use your for rebelling scene but this only Exodus' operations which I involved in such tations the same operation if I have them each a light yeah 1st to work DEC's application and then on top tools some concatenation science in reviving needs to look differently and not all combinations of operations can actually be rewritten in a nice rainy so in this case is that if 1 has a whole cells this forest or context represented by 1 then it's the same effect Lax really into it and then act at a true to the right and I can instead attitude to the right of 1 and then Lax read into the whole which is still in the formula represented by 1 and we have a similar rewriting this is a whole is contained in 2 weeks and 1 can show that these operations of these rewritings I enough to always maintain the worst make debts so this gives all main Surinam that you can do on enumeration of is all formulas in time that this pre-processing is linear in the size of the tree and polynomial in the size of the automaton the delay is constant in the tree it only depends on the size of the results on the arity of or clearing and again putting all Newton's automaton and updates are actually logarithmic in the size of simply this expo norms known exponent ominous only obvious which are and there's the exponent of the way in markets which application which happens to be here because we need to do some there leachability computations on the Cypriot and this exponents floor is actually the because we have to leave right so religion ultimate with to an automaton that vexed over the seige apart from us what so is the main resides in 1 as a pub bound we
have looked for a lower bound which is
almost kind so there is this does existential marked and suspect theories form data structures you read there's a question is just we have had to really was some mark notes insufficiency I a lot to ask that some old and he has a market into insist or caves updates that I load are just not on market note and he knows it's a Q retirements update time are somehow related so there are some law bones on the relational sees 2 times and he can do when reduction to an emotion updates sold give you have enumeration of theories but we can assimilate is within the risk by making if a makes a query is has you mark and I can marks along the especially then in the Wedtech theory which passed he said a special North is a marked insist so there's only 1 special note at all and therefore it's it's some reside this knowledge has to be has to have a marked and system and after lots of what I mark years non-special again to be ready for the next 3 read and this gives me the relation between the delay an update time is that we cannot be better and this is not an over OK and so if you don't want to sacrifice or what constant delays than the update and cannot be better than lot and overlock and you have not an updated so and the success of the tree so there is only a small audience so here have a lot of results again and thank you for your attention