Enumeration on Trees with Tractable Combined Complexity and Efficient Updates
Video in TIB AVPortal:
Enumeration on Trees with Tractable Combined Complexity and Efficient Updates
Formal Metadata
Title 
Enumeration on Trees with Tractable Combined Complexity and Efficient Updates

Title of Series  
Author 

License 
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. 
Identifiers 

Publisher 

Release Date 
2019

Language 
English

Content Metadata
Subject Area  
Abstract 
We give an algorithm to enumerate the results on trees of monadic secondorder (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 circuitbased enumeration algorithms based on deterministic tree automata, and is also inspired by our earlier result on words and nondeterministic sequential extended variableset 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 firstorder variables, we can enumerate the results with linear preprocessing and constantdelay 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.

00:00
Inheritance (objectoriented programming)
Wage labour
Link (knot theory)
Algorithm
Multiplication sign
Quantification
Price index
Theory
P (complexity)
Data management
Goodness of fit
Performance appraisal
Network topology
Wellformed formula
Query language
Logic
Monad (category theory)
Vertex (graph theory)
output
Inheritance (objectoriented programming)
Kolmogorov complexity
Cellular automaton
Magnetooptical drive
Set (mathematics)
Enumerated type
Subject indexing
Numeral (linguistics)
Wellformed formula
Intrusion detection system
Alphabet (computer science)
Logic
Network topology
Order (biology)
Phase transition
Resultant
01:25
Rekursiv aufzählbare Menge
Algorithm
Kolmogorov complexity
Multiplication sign
Subject indexing
Pattern language
Damping
Aerodynamics
Data structure
Enumerated type
output
Mereology
01:54
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
Normalform game
Logarithm
Kolmogorov complexity
Binary code
Moment (mathematics)
Keyboard shortcut
Constructor (objectoriented 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
08:28
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
Wellformed 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
Wellformed 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)
14:37
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
00:04
so what's the problem we have given the
00:07
dataentry you as a note says labor all
00:10
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
01:26
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
01:45
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
01:57
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 usercreated 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 bottomup 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
07:06
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
08:29
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 Macbased 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 backends 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 preprocessing 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
14:36
have looked for a lower bound which is
14:38
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 nonspecial 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