Executable Firstorder Queries in the Logic of Information Flows
Formal Metadata
Title 
Executable Firstorder Queries in the Logic of Information Flows

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 
2020

Language 
English

Content Metadata
Subject Area  
Abstract 
The logic of information flows ( LIF) has recently been proposed as a general framework in the field of knowledge representation . In this fra mework, tasks of a procedural nature c an st ill be modele d in a decl arativ e, log icbased fa shion. In this paper, we foc us on the task of query proc essing under limited access patterns, a wellstudi ed p roblem in the database literatur e. We show that L IF is wel lsuited for modeling this task. Toward this goal, we introduce a variant of LIF called "forward" LIF, in a firstorder setting . We define FLIF^io, a syntactical fragment of forward LIF, and show that it corresponds exactly to the "executable" fragment of firstorder logic defined by Nash and Ludäscher. The definition of FLIF^io involves a classification of the free variables of an expression into "input" and "output" variables. Our result hinges on inertia and determinacy laws for forward LIF expressions, which are interesting in their own right. These laws are formulated in terms of the input and output variables.

Related Material
00:00
Dependent and independent variables
Multiplication sign
Correspondence (mathematics)
Source code
Database
Limit (category theory)
Formal language
Logic
Profil (magazine)
Password
Logic
Query language
Pattern language
Information
00:22
Source code
Password
Information
00:34
Classical physics
Tuple
Equaliser (mathematics)
Source code
Password
Set (mathematics)
Methodenbank
Parameter (computer programming)
Computer programming
Formal language
Exponential function
Profil (magazine)
Finitary relation
Information
Endliche Modelltheorie
output
Position operator
Source code
Dependent and independent variables
Matching (graph theory)
Gradient
Attribute grammar
Type theory
Logic
Password
output
Procedural programming
Row (database)
Algebraic function
01:35
Classical physics
Group action
Graph (mathematics)
Relational database
Database
Semantics (computer science)
Declarative programming
Formal language
Different (Kate Ryan album)
Algebraic closure
Query language
Navigation
Procedural programming
Social class
Email
Computer program
Group action
Limit (category theory)
Algebra
Algebraic closure
Interpreter (computing)
Pattern language
Procedural programming
Regular expression
Resultant
02:41
Graph (mathematics)
Graph (mathematics)
Prisoner's dilemma
Workstation <Musikinstrument>
Set (mathematics)
Database
Semantics (computer science)
Binary file
Group action
Limit (category theory)
Wave packet
Wave packet
Arithmetic mean
Personal digital assistant
Algebraic closure
Query language
Finitary relation
Bus (computing)
Interpreter (computing)
Navigation
Pattern language
Bus (computing)
Series (mathematics)
Regular expression
03:20
Graph (mathematics)
Relational database
Prisoner's dilemma
Selectivity (electronic)
Regular expression
Instance (computer science)
Regular expression
Freezing
Form (programming)
Exception handling
03:53
Logical constant
Quantum state
Keyboard shortcut
Bit
Binary file
System call
Variable (mathematics)
Wave packet
Atomic number
Finitary relation
Bus (computing)
Regular expression
output
Regular expression
04:44
Physical law
Database
Binary file
Limit (category theory)
Cartesian coordinate system
Semantics (computer science)
Power (physics)
Formal language
Logic
Finitary relation
Energy level
Pattern language
Endliche Modelltheorie
output
Freeware
05:26
Standard deviation
Group action
Momentum
Ferry Corsten
Equaliser (mathematics)
1 (number)
Set (mathematics)
Function (mathematics)
Variable (mathematics)
Dedekind cut
Wellformed formula
Nichtlineares Gleichungssystem
output
Form (programming)
Key (cryptography)
File format
Bit
Semantics (computer science)
Variable (mathematics)
Grass (card game)
Limit (category theory)
Equivalence relation
Category of being
Bargaining problem
Wellformed formula
Order (biology)
output
Resultant
07:06
Momentum
Key (cryptography)
1 (number)
Translation (relic)
Bit
Function (mathematics)
Binary file
Mereology
Demoscene
Variable (mathematics)
Impulse response
Medical imaging
Performance appraisal
Discrepancy theory
Symmetry (physics)
Different (Kate Ryan album)
Function (mathematics)
Finitary relation
Regular expression
Office suite
output
Regular expression
Form (programming)
09:03
Group action
Momentum
Ferry Corsten
Modal logic
Multiplication sign
1 (number)
Translation (relic)
Valuation (algebra)
Function (mathematics)
Mereology
Equivalence relation
Theory
Wellformed formula
Queue (abstract data type)
Condition number
Form (programming)
Variable (mathematics)
Existence
Wellformed formula
Order (biology)
Statement (computer science)
Theorem
output
Regular expression
Family
Resultant
Arc (geometry)
10:50
Keyboard shortcut
Presentation of a group
Existential quantification
Graph (mathematics)
Ferry Corsten
Translation (relic)
Online help
Database
Limit (category theory)
Grass (card game)
Mereology
Formal language
Power (physics)
Wellformed formula
Query language
Personal digital assistant
Theorem
Pattern language
Regular expression
12:13
Graph (mathematics)
Query language
Planning
Data structure
Regular expression
Mereology
Data structure
00:00
greetings everyone my name is a diamond and you'd be presenting the people exist you to lose restore the crease in the logic of information flows this is really twenty quid what bogot's dimitris innings the uterus canyon been done because i consider it a source and do it for you give your user name along with that's where it and in the serb. the response back with the corresponding profile access with his database it to be restricted to the livers for example a new good on you that providing a bag of the username and password is not possible in the literature this time hundred mission source is said to have limited access patterns rest she did with access methods you provide.
00:40
they use for some actual use and then the source response back with all the top as the match they give indeed is what does set of that should use so intuitively you can think of the situation sources as models that the interest and utter and possibly multiple out that's for me this means that each nation is not only associated with. even at its the but also with an impact at its the and we will distinguish between the different positions by the fall and mitigation simply call and he used to priests between the input arguments in their first of the arguments where you can think of the ex's to be the includes and the wise to be the out its record our introduction example. so we have here a username fall by a password for grades semicolon in the profile classic equalling this type of information source is not either why none of the procedure algebra programs to our coal plants or i live in the climate of logic in english and such as executable f o.
01:41
and our question will be is there and different approach or is there a different way to think about the to these was limited access patterns and our answer would be yes do is in the group was what we call if you live which is short for forward live it's an aim which that has balls declarative and procedural features. and you can think of if lift to be a foreman isn't that falls under the class of navigation and expose like graft winning which is so will begin but short of you on the vision and explore like graphically languages and expression emailing which is in some doubt which is an edgy even or a composition of two expressions or.
02:21
where the cleaning or detest of closure of an expression also the classical settler patients like union intersection and difference if the expressions results in an expression and given the country's the the interpretation of the knicks depression is given by the mission semantics so for example the interpretation of the age label towel.
02:42
you will be the set of all praise of know it's such a that there is an edge of between them even tell for example the expression bus composition was minus train issue of then he waited on new was the to prison stations it would mean set of series of the station's explain why such a that's the question why is reachable from exploiting to pursue.
03:02
first but it's not really to and from x. by other it train and from the graph is a clear that we can only have one and five in the interpretation of he now since in our case the data amazes limit access patterns is used as a graph some natural questions are against like what will be the notes of the raf and what would be the edges.
03:22
for the first question the nose will be the other we shuns a in the second question the edges will be the possible access is given by our instance so what our to flip syntax jenner form of expression is quite similar to the navigational graph quickly likely in which its and the only.
03:42
freeze is the lack of the transfer of gluten operated in the possible exceptions for terry prisons the atomic expressions which are the edge labels the first suppression is the simple solution after where are here is the relation need for the other to expressions we have a selection in assignment expressions.
04:02
when we can check or say they have been able to another remember a constant concentrates chemo is their relations be and see each of them is a bind the nation with one in the stands for basanti for a train as a first example considered expression me access the call in my composition t y semicolon z.
04:23
the expression takes accident into it and retrieves the possibilities for y. and z. such that you can go from next to the through why you can each wine from x. ray a bus and you can go from why does he by train and for another example take the expression be extremely call and wine composition me why semicolon z. composition. and easy's in call an ex all of this intersection was x. equals x. the whole execration takes x. y. and z. is in bits and the czechs whether he can go from next to the way too much as to why and that you can go back rooms he to exploit a tween after introducing the syntax of the flip the question now and the.
05:03
is that it's a person enough to solve the problem in hand in particular how does it compare to executive level and other plants and to answer this question will ensure that every minute of if live has the since oppressive power as executive level and for that it would begin with a brief introduction and as you to the death of the executive is the law.
05:24
because formalism that's proposed by national dish or to know that we use over databases limited access patterns basically to send tactic treatment of free so the logic was natural semantics and a lady is to determine with their first model for men is executed or not and but executive really mean whether it respects the axis powers.
05:44
actions moreover this executive is he checked his done rid of to a set of variables the that intuitive you can think of as the input variables and here are some examples are considered a formula to exist to why are extremely call them why here x. is the only in it given of a four x. that it was a check.
06:04
six if there is every year for why such that are extremely common why holes histories form is said to be executed now consider the former next equal john in conjunction with our exwife's in the commons the interest on junk is executed for any said the since the v.a. for the x. is already given by the equation. for the second going junk and no and its x. two x. acute of the but since we really have the winding for the exit from the phrase can jump in the hall format is and you want you to however the next not a key covenants limit is not why executive the which means that hear the order of the conjunctions matters to and or. a bit to secure the first can jump for several years for the x. and y. should be provided has this limit his ex wife executive one but not why executive. in order to show equivalence result we need to classify the values of our if we fix oppressions into in bits and outputs and our the finish and for the impetus and outputs is in fact that but to make sure that they represent some semantic properties and intuitively the in the variables are the ones needed from the beginning of the park in the grass.
07:16
after each a result and out of the most are the was are allowed to change throughout the past so for their initial atom are extremely called and why clearly the impetus are the x.'s and outlets are the ones so you want composition eat to include very most are the interests of the want. together with the interests of the two that are not out parts of the more outlets for the composition geese are the union of the outposts of the subjects oppression. the same outfits are defined for the union a patient when the impulse are the union of the in its and the symmetry difference of the other parts of the warning eat to the intersection and difference between us and outputs are defined in a similar way moreover the definitions when they bits and now has one the rest of the expressions its kind of office. it's unclear from our definitions that every image can be both an increase in an hour but what does that mean consider the following example we have a boy and the nation inc with one in the art that is the envy of the in putting commented we want if we used the expression inc xm he called an ex this means given they really have to.
08:27
sex incremental been one and save it also in x. so the veil of the x. is all written by this if they for expression on the other hand this form is not satisfied by executive and ethical so this was complicated translation from if lift to ease the key to the f.o. hints of the solution will be. the working with what we call if you if i know which is that if a fragment of does joined include and arctic's oppressions our fairest translation serious is defaulting if we have a unique users from defy we can construct and if we fail expression he where the interests of each of the scene rails.
09:07
in the and there is still the free their use of fire among the arc of variables of the and not as you did this is only an included with this is a necessity since we were only with i was doing expressions the last condition says that far in any other almost equivalent and buy equipment into he mean that we get the same that they wish. is in the result starting from the same brother we should find on the inputs considered the following four in a r x's recall and x. y. in conjunction with n.y. semicolon see the whole formula is x. in the queue to be inexcusable f o conjunction is more of the composition if live since the order.
09:48
of the condoms matters moreover in the phrase conjuncture the exit provided for the into it must be the same x. in the final valuation this means that the phrase conjuncture has a part of the chicken side it so we need to find that they use for the why and at the same time we need to select only the vaguest for the x. that match the impetus. say you to do this is checked if we fail we need to use explicitly s. election statement since the very real use in the output are joined from the very ones used in the impetus for that to have an extra very busy you finally the transition shows that our expression is archaic semicolon you why. i followed by a check that takes in you have the same three years after that we access the immolation was white and z. this theory or shows that if we find no is at least as expressive as executive will ever know for the other translation which is from if i go to execute a f. who we have us. stronger result if we haven't if left by the expression he we can construct a former find certain that this form is the executive will be given the in its of the moreover we have that eat and quiet equivalent consider the following expression are extremely call and why you compose to annex.
11:09
the semicolon the u..
11:11
the impact of this expression is the x. thus we need an ex exit you to the end of four men from the translation expression interest to treat is why you buy in the interim are pretty given x. then it would cease to retrieve as ed you binding from them for the given x. which. they override the previous binding for you and this means that we need to ignore the phrase to be you provided today you we can do this with the help of the existential quantification in the end over four million be the existed they you for you so much that are x. the semicolon why you is true. all of this is can jump to two m. x. semicolon z u. as a summary of this part this means that if we fail and executive it ever will have to see him express his power to to conclude their presentation the doing databases in our case is a graph allows using navigation and grass with the languages to modern queries over the to these is limited access patterns.
12:19
and last but not least we show in our people without every if we failed suppression has a simple plan and by simply mean that it's a structure is quite similar to the structure of if you for your expressions moreover as a part of this simplicity dominating the plan does not need at to mutiny me and all to do. these are taken to the natural julian's to thank you so much were listening.