Model theory of XPath on data trees. Part II: Binary bisimulation and definability

We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over possibly infinite data trees. We introduce a suitable notion of saturation with respect to node expressions, and show that over saturated data trees, the already studied notion of (una...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Figueira, Santiago Daniel
Publicado: 2017
Materias:
Binary trees
Bins
Fault tolerance
Forestry
Characterization theorems
Equality tests
Expressive power
First-order formulas
Free variable
Indistinguishability
Path expressions
Separation theorem
Trees (mathematics)
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08905401_v255_n_p195_Abriola
http://hdl.handle.net/20.500.12110/paper_08905401_v255_n_p195_Abriola
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_08905401_v255_n_p195_Abriola
record_format dspace
spelling paper:paper_08905401_v255_n_p195_Abriola2023-06-08T15:47:07Z Model theory of XPath on data trees. Part II: Binary bisimulation and definability Figueira, Santiago Daniel Binary trees Bins Fault tolerance Forestry Characterization theorems Equality tests Expressive power First-order formulas Free variable Indistinguishability Path expressions Separation theorem Trees (mathematics) We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over possibly infinite data trees. We introduce a suitable notion of saturation with respect to node expressions, and show that over saturated data trees, the already studied notion of (unary) bisimulation coincides with the idea of ‘indistinguishability by means of node expressions’. We also prove definability and separation theorems for classes of pointed data trees. We introduce new notions of binary bisimulations, which relate two pairs of nodes of data trees. We show that over finitely branching data trees, these notions correspond to the idea of ‘indistinguishability by means of path expressions’. We prove a characterization theorem, which describes when a first-order formula with two free variables is expressible in the downward fragment. We show definability and separation theorems, for classes of two-pointed data trees and in the context of path expressions. © 2017 Elsevier Inc. Fil:Figueira, S. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2017 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08905401_v255_n_p195_Abriola http://hdl.handle.net/20.500.12110/paper_08905401_v255_n_p195_Abriola
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Binary trees
Bins
Fault tolerance
Forestry
Characterization theorems
Equality tests
Expressive power
First-order formulas
Free variable
Indistinguishability
Path expressions
Separation theorem
Trees (mathematics)
spellingShingle Binary trees
Bins
Fault tolerance
Forestry
Characterization theorems
Equality tests
Expressive power
First-order formulas
Free variable
Indistinguishability
Path expressions
Separation theorem
Trees (mathematics)
Figueira, Santiago Daniel
Model theory of XPath on data trees. Part II: Binary bisimulation and definability
topic_facet Binary trees
Bins
Fault tolerance
Forestry
Characterization theorems
Equality tests
Expressive power
First-order formulas
Free variable
Indistinguishability
Path expressions
Separation theorem
Trees (mathematics)
description We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over possibly infinite data trees. We introduce a suitable notion of saturation with respect to node expressions, and show that over saturated data trees, the already studied notion of (unary) bisimulation coincides with the idea of ‘indistinguishability by means of node expressions’. We also prove definability and separation theorems for classes of pointed data trees. We introduce new notions of binary bisimulations, which relate two pairs of nodes of data trees. We show that over finitely branching data trees, these notions correspond to the idea of ‘indistinguishability by means of path expressions’. We prove a characterization theorem, which describes when a first-order formula with two free variables is expressible in the downward fragment. We show definability and separation theorems, for classes of two-pointed data trees and in the context of path expressions. © 2017 Elsevier Inc.
author Figueira, Santiago Daniel
author_facet Figueira, Santiago Daniel
author_sort Figueira, Santiago Daniel
title Model theory of XPath on data trees. Part II: Binary bisimulation and definability
title_short Model theory of XPath on data trees. Part II: Binary bisimulation and definability
title_full Model theory of XPath on data trees. Part II: Binary bisimulation and definability
title_fullStr Model theory of XPath on data trees. Part II: Binary bisimulation and definability
title_full_unstemmed Model theory of XPath on data trees. Part II: Binary bisimulation and definability
title_sort model theory of xpath on data trees. part ii: binary bisimulation and definability
publishDate 2017
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08905401_v255_n_p195_Abriola
http://hdl.handle.net/20.500.12110/paper_08905401_v255_n_p195_Abriola
work_keys_str_mv AT figueirasantiagodaniel modeltheoryofxpathondatatreespartiibinarybisimulationanddefinability
_version_ 1768542510844477440

Ejemplares similares