Context Unification is in PSPACE View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2014

AUTHORS

Artur Jeż

ABSTRACT

Contexts are terms with one ‘hole’, i.e. a place in which we can substitute an argument. In context unification we are given an equation over terms with variables representing contexts and ask about the satisfiability of this equation. Context unification at the same time is subsumed by a second-order unification, which is undecidable, and subsumes satisfiability of word equations, which is in PSPACE. We show that context unification is in PSPACE, so as word equations. For both problems NP is still the best known lower-bound.This result is obtained by an extension of the recompression technique, recently developed by the author and used in particular to obtain a new PSPACE algorithm for satisfiability of word equations, to context unification. The recompression is based on applying simple compression rules (replacing pairs of neighbouring function symbols), which are (conceptually) applied on the solution of the context equation and modifying the equation in a way so that such compression steps can be performed directly on the equation, without the knowledge of the actual solution. More... »

PAGES

244-255

Book

TITLE

Automata, Languages, and Programming

ISBN

978-3-662-43950-0
978-3-662-43951-7

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-43951-7_21

DOI

http://dx.doi.org/10.1007/978-3-662-43951-7_21

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1045044342


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/01", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Mathematical Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0101", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Pure Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Institute of Computer Science, University of Wroc\u0142aw, Wroc\u0142aw, Poland", 
          "id": "http://www.grid.ac/institutes/grid.8505.8", 
          "name": [
            "Max Planck Institute f\u00fcr Informatik, Saarbr\u00fccken, Germany", 
            "Institute of Computer Science, University of Wroc\u0142aw, Wroc\u0142aw, Poland"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Je\u017c", 
        "givenName": "Artur", 
        "id": "sg:person.015252371751.76", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015252371751.76"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2014", 
    "datePublishedReg": "2014-01-01", 
    "description": "Contexts are terms with one \u2018hole\u2019, i.e. a place in which we can substitute an argument. In context unification we are given an equation over terms with variables representing contexts and ask about the satisfiability of this equation. Context unification at the same time is subsumed by a second-order unification, which is undecidable, and subsumes satisfiability of word equations, which is in PSPACE. We show that context unification is in PSPACE, so as word equations. For both problems NP is still the best known lower-bound.This result is obtained by an extension of the recompression technique, recently developed by the author and used in particular to obtain a new PSPACE algorithm for satisfiability of word equations, to context unification. The recompression is based on applying simple compression rules (replacing pairs of neighbouring function symbols), which are (conceptually) applied on the solution of the context equation and modifying the equation in a way so that such compression steps can be performed directly on the equation, without the knowledge of the actual solution.", 
    "editor": [
      {
        "familyName": "Esparza", 
        "givenName": "Javier", 
        "type": "Person"
      }, 
      {
        "familyName": "Fraigniaud", 
        "givenName": "Pierre", 
        "type": "Person"
      }, 
      {
        "familyName": "Husfeldt", 
        "givenName": "Thore", 
        "type": "Person"
      }, 
      {
        "familyName": "Koutsoupias", 
        "givenName": "Elias", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-43951-7_21", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-662-43950-0", 
        "978-3-662-43951-7"
      ], 
      "name": "Automata, Languages, and Programming", 
      "type": "Book"
    }, 
    "keywords": [
      "word equations", 
      "simple compression rules", 
      "context unification", 
      "PSPACE algorithm", 
      "context equations", 
      "actual solution", 
      "equations", 
      "recompression technique", 
      "second-order unification", 
      "problem NP", 
      "compression rules", 
      "PSPACE", 
      "unification", 
      "satisfiability", 
      "solution", 
      "compression step", 
      "algorithm", 
      "terms", 
      "extension", 
      "holes", 
      "NPs", 
      "variables", 
      "same time", 
      "rules", 
      "technique", 
      "argument", 
      "step", 
      "results", 
      "way", 
      "time", 
      "context", 
      "authors", 
      "recompression", 
      "place", 
      "knowledge"
    ], 
    "name": "Context Unification is in PSPACE", 
    "pagination": "244-255", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1045044342"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-43951-7_21"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-43951-7_21", 
      "https://app.dimensions.ai/details/publication/pub.1045044342"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:42", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/chapter/chapter_174.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-662-43951-7_21"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-43951-7_21'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-43951-7_21'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-43951-7_21'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-43951-7_21'


 

This table displays all metadata directly associated to this object as RDF triples.

111 TRIPLES      23 PREDICATES      61 URIs      54 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-43951-7_21 schema:about anzsrc-for:01
2 anzsrc-for:0101
3 schema:author N28a9044373a14b50952be8c09c51cb2d
4 schema:datePublished 2014
5 schema:datePublishedReg 2014-01-01
6 schema:description Contexts are terms with one ‘hole’, i.e. a place in which we can substitute an argument. In context unification we are given an equation over terms with variables representing contexts and ask about the satisfiability of this equation. Context unification at the same time is subsumed by a second-order unification, which is undecidable, and subsumes satisfiability of word equations, which is in PSPACE. We show that context unification is in PSPACE, so as word equations. For both problems NP is still the best known lower-bound.This result is obtained by an extension of the recompression technique, recently developed by the author and used in particular to obtain a new PSPACE algorithm for satisfiability of word equations, to context unification. The recompression is based on applying simple compression rules (replacing pairs of neighbouring function symbols), which are (conceptually) applied on the solution of the context equation and modifying the equation in a way so that such compression steps can be performed directly on the equation, without the knowledge of the actual solution.
7 schema:editor N4afb3af595f641a99ecb9138058a1be5
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N750d13d90a7642ca8da88128d0642f38
12 schema:keywords NPs
13 PSPACE
14 PSPACE algorithm
15 actual solution
16 algorithm
17 argument
18 authors
19 compression rules
20 compression step
21 context
22 context equations
23 context unification
24 equations
25 extension
26 holes
27 knowledge
28 place
29 problem NP
30 recompression
31 recompression technique
32 results
33 rules
34 same time
35 satisfiability
36 second-order unification
37 simple compression rules
38 solution
39 step
40 technique
41 terms
42 time
43 unification
44 variables
45 way
46 word equations
47 schema:name Context Unification is in PSPACE
48 schema:pagination 244-255
49 schema:productId N3fe88cea73eb47ec8c9bd645d85f9db7
50 Nf0638c38cd024af0b00333ec9dd24449
51 schema:publisher N95e49ea73d4e4bb98d86110be5744a5b
52 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045044342
53 https://doi.org/10.1007/978-3-662-43951-7_21
54 schema:sdDatePublished 2022-05-20T07:42
55 schema:sdLicense https://scigraph.springernature.com/explorer/license/
56 schema:sdPublisher Ncd5026dde69d470ab25ef7e04322da73
57 schema:url https://doi.org/10.1007/978-3-662-43951-7_21
58 sgo:license sg:explorer/license/
59 sgo:sdDataset chapters
60 rdf:type schema:Chapter
61 N03da17b9f6cb4a558d74c5cc61d2ff9d rdf:first N50cccf1f7a864b228f889022d2e4c364
62 rdf:rest rdf:nil
63 N1c60114feb544489b0a5d9c281ac8f65 rdf:first N66a8ce98a81b4c549d7ff55f065c15cc
64 rdf:rest Nebcb62a074df4750803f08a60df0106b
65 N28a9044373a14b50952be8c09c51cb2d rdf:first sg:person.015252371751.76
66 rdf:rest rdf:nil
67 N3fe88cea73eb47ec8c9bd645d85f9db7 schema:name dimensions_id
68 schema:value pub.1045044342
69 rdf:type schema:PropertyValue
70 N4afb3af595f641a99ecb9138058a1be5 rdf:first N71f322c431404b988e5daa6cac7ea2b3
71 rdf:rest N1c60114feb544489b0a5d9c281ac8f65
72 N50cccf1f7a864b228f889022d2e4c364 schema:familyName Koutsoupias
73 schema:givenName Elias
74 rdf:type schema:Person
75 N66a8ce98a81b4c549d7ff55f065c15cc schema:familyName Fraigniaud
76 schema:givenName Pierre
77 rdf:type schema:Person
78 N71f322c431404b988e5daa6cac7ea2b3 schema:familyName Esparza
79 schema:givenName Javier
80 rdf:type schema:Person
81 N750d13d90a7642ca8da88128d0642f38 schema:isbn 978-3-662-43950-0
82 978-3-662-43951-7
83 schema:name Automata, Languages, and Programming
84 rdf:type schema:Book
85 N7a02c0a1a8a7429489ff85391c9f27aa schema:familyName Husfeldt
86 schema:givenName Thore
87 rdf:type schema:Person
88 N95e49ea73d4e4bb98d86110be5744a5b schema:name Springer Nature
89 rdf:type schema:Organisation
90 Ncd5026dde69d470ab25ef7e04322da73 schema:name Springer Nature - SN SciGraph project
91 rdf:type schema:Organization
92 Nebcb62a074df4750803f08a60df0106b rdf:first N7a02c0a1a8a7429489ff85391c9f27aa
93 rdf:rest N03da17b9f6cb4a558d74c5cc61d2ff9d
94 Nf0638c38cd024af0b00333ec9dd24449 schema:name doi
95 schema:value 10.1007/978-3-662-43951-7_21
96 rdf:type schema:PropertyValue
97 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
98 schema:name Mathematical Sciences
99 rdf:type schema:DefinedTerm
100 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
101 schema:name Pure Mathematics
102 rdf:type schema:DefinedTerm
103 sg:person.015252371751.76 schema:affiliation grid-institutes:grid.8505.8
104 schema:familyName Jeż
105 schema:givenName Artur
106 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015252371751.76
107 rdf:type schema:Person
108 grid-institutes:grid.8505.8 schema:alternateName Institute of Computer Science, University of Wrocław, Wrocław, Poland
109 schema:name Institute of Computer Science, University of Wrocław, Wrocław, Poland
110 Max Planck Institute für Informatik, Saarbrücken, Germany
111 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...