Deciding Context Unification (with Regular Constraints) View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2019-07-10

AUTHORS

Artur Jeż

ABSTRACT

Given a ranked alphabet, context are terms with a single occurrence of a special symbol \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\bullet }$$\end{document} (outside of the alphabet), which represents a missing subterm. One can naturally build equations over contexts: the context variables are treated as symbols of arity one and a substitution S assigns to each such a variable a context S(X). A substitution S is extended to terms with context variables in a natural way: S(X(t)) is a context S(X) in which the unique occurrence of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\bullet }$$\end{document} is replaced with S(t). For historical reasons, the satisfiability of context equations is usually referred to as context unification.Context unification generalizes word equations and first-order term unification (which are decidable) and is subsumed by second order unification (which is undecidable) and its decidability status remained open for almost two decades. In this paper I will sketch a PSPACE algorithm for this problem. The idea is to apply simple compression rules (replacing pairs of neighbouring function symbols) to the solution of the context equation; to this end we appropriately modify the equation (without the knowledge of the actual solution) so that compressing the solution can be simulated by compressing parts of the equation. When the compression operations are appropriately chosen, then the size of the instance is polynomial during the whole algorithm, thus giving a PSPACE-upper bound. The best known lower bounds are as for word equations, i.e. NP. The method can be extended to the scenario in which tree-regular constraints for the variables are present, in which case the problem is EXPTIME-complete. More... »

PAGES

18-40

Book

TITLE

Developments in Language Theory

ISBN

978-3-030-24885-7
978-3-030-24886-4

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-24886-4_2

DOI

http://dx.doi.org/10.1007/978-3-030-24886-4_2

DIMENSIONS

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


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": "University of Wroc\u0142aw, Wroc\u0142aw, Poland", 
          "id": "http://www.grid.ac/institutes/grid.8505.8", 
          "name": [
            "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": "2019-07-10", 
    "datePublishedReg": "2019-07-10", 
    "description": "Given a ranked alphabet, context are terms with a single occurrence of a special symbol \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$${\\bullet }$$\\end{document} (outside of the alphabet), which represents a missing subterm. One can naturally build equations over contexts: the context variables are treated as symbols of arity one and a substitution S assigns to each such a variable a context S(X). A substitution S is extended to terms with context variables in a natural way: S(X(t)) is a context S(X) in which the unique occurrence of \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$${\\bullet }$$\\end{document} is replaced with S(t). For historical reasons, the satisfiability of context equations is usually referred to as context unification.Context unification generalizes word equations and first-order term unification (which are decidable) and is subsumed by second order unification (which is undecidable) and its decidability status remained open for almost two decades. In this paper I will sketch a PSPACE algorithm for this problem. The idea is to apply simple compression rules (replacing pairs of neighbouring function symbols) to the solution of the context equation; to this end we appropriately modify the equation (without the knowledge of the actual solution) so that compressing the solution can be simulated by compressing parts of the equation. When the compression operations are appropriately chosen, then the size of the instance is polynomial during the whole algorithm, thus giving a PSPACE-upper bound. The best known lower bounds are as for word equations, i.e. NP. The method can be extended to the scenario in which tree-regular constraints for the variables are present, in which case the problem is EXPTIME-complete.", 
    "editor": [
      {
        "familyName": "Hofman", 
        "givenName": "Piotrek", 
        "type": "Person"
      }, 
      {
        "familyName": "Skrzypczak", 
        "givenName": "Micha\u0142", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-24886-4_2", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-030-24885-7", 
        "978-3-030-24886-4"
      ], 
      "name": "Developments in Language Theory", 
      "type": "Book"
    }, 
    "keywords": [
      "historical reasons", 
      "unification", 
      "paper I", 
      "context", 
      "symbols", 
      "special symbols", 
      "unique occurrence", 
      "decades", 
      "idea", 
      "way", 
      "end", 
      "alphabet", 
      "single occurrence", 
      "reasons", 
      "rules", 
      "part", 
      "terms", 
      "one", 
      "instances", 
      "status", 
      "problem", 
      "occurrence", 
      "context variables", 
      "assigns", 
      "cases", 
      "operation", 
      "scenarios", 
      "constraints", 
      "natural way", 
      "context equations", 
      "context unification", 
      "bounds", 
      "method", 
      "variables", 
      "second-order unification", 
      "solution", 
      "size", 
      "equations", 
      "arity one", 
      "word equations", 
      "first-order term unification", 
      "term unification", 
      "order unification", 
      "algorithm", 
      "simple compression rules", 
      "compression rules", 
      "compression operation", 
      "whole algorithm", 
      "lower bounds", 
      "subterms", 
      "substitution S", 
      "satisfiability", 
      "decidability status", 
      "tree-regular constraints"
    ], 
    "name": "Deciding Context Unification (with Regular Constraints)", 
    "pagination": "18-40", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1119756454"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-24886-4_2"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-24886-4_2", 
      "https://app.dimensions.ai/details/publication/pub.1119756454"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:49", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_369.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-24886-4_2"
  }
]
 

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-030-24886-4_2'

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-030-24886-4_2'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-24886-4_2'

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-030-24886-4_2'


 

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

119 TRIPLES      23 PREDICATES      79 URIs      72 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-24886-4_2 schema:about anzsrc-for:01
2 anzsrc-for:0101
3 schema:author N7fb6ca260d2d4fbea71fe2932088c8fd
4 schema:datePublished 2019-07-10
5 schema:datePublishedReg 2019-07-10
6 schema:description Given a ranked alphabet, context are terms with a single occurrence of a special symbol \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\bullet }$$\end{document} (outside of the alphabet), which represents a missing subterm. One can naturally build equations over contexts: the context variables are treated as symbols of arity one and a substitution S assigns to each such a variable a context S(X). A substitution S is extended to terms with context variables in a natural way: S(X(t)) is a context S(X) in which the unique occurrence of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\bullet }$$\end{document} is replaced with S(t). For historical reasons, the satisfiability of context equations is usually referred to as context unification.Context unification generalizes word equations and first-order term unification (which are decidable) and is subsumed by second order unification (which is undecidable) and its decidability status remained open for almost two decades. In this paper I will sketch a PSPACE algorithm for this problem. The idea is to apply simple compression rules (replacing pairs of neighbouring function symbols) to the solution of the context equation; to this end we appropriately modify the equation (without the knowledge of the actual solution) so that compressing the solution can be simulated by compressing parts of the equation. When the compression operations are appropriately chosen, then the size of the instance is polynomial during the whole algorithm, thus giving a PSPACE-upper bound. The best known lower bounds are as for word equations, i.e. NP. The method can be extended to the scenario in which tree-regular constraints for the variables are present, in which case the problem is EXPTIME-complete.
7 schema:editor N7067b59a3bd14c3a856e07a92c05132a
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N7d538e293738471e87da012b92ede643
12 schema:keywords algorithm
13 alphabet
14 arity one
15 assigns
16 bounds
17 cases
18 compression operation
19 compression rules
20 constraints
21 context
22 context equations
23 context unification
24 context variables
25 decades
26 decidability status
27 end
28 equations
29 first-order term unification
30 historical reasons
31 idea
32 instances
33 lower bounds
34 method
35 natural way
36 occurrence
37 one
38 operation
39 order unification
40 paper I
41 part
42 problem
43 reasons
44 rules
45 satisfiability
46 scenarios
47 second-order unification
48 simple compression rules
49 single occurrence
50 size
51 solution
52 special symbols
53 status
54 substitution S
55 subterms
56 symbols
57 term unification
58 terms
59 tree-regular constraints
60 unification
61 unique occurrence
62 variables
63 way
64 whole algorithm
65 word equations
66 schema:name Deciding Context Unification (with Regular Constraints)
67 schema:pagination 18-40
68 schema:productId N239d3166ec444291b2b4d951aa050106
69 Nd97a83260a1a4639a39f491b2f3bd92e
70 schema:publisher N1301fc48c4c945ad9fb3425f3f0e94df
71 schema:sameAs https://app.dimensions.ai/details/publication/pub.1119756454
72 https://doi.org/10.1007/978-3-030-24886-4_2
73 schema:sdDatePublished 2022-05-10T10:49
74 schema:sdLicense https://scigraph.springernature.com/explorer/license/
75 schema:sdPublisher N146bf67260804889b8304f25557be4dd
76 schema:url https://doi.org/10.1007/978-3-030-24886-4_2
77 sgo:license sg:explorer/license/
78 sgo:sdDataset chapters
79 rdf:type schema:Chapter
80 N1301fc48c4c945ad9fb3425f3f0e94df schema:name Springer Nature
81 rdf:type schema:Organisation
82 N146bf67260804889b8304f25557be4dd schema:name Springer Nature - SN SciGraph project
83 rdf:type schema:Organization
84 N239d3166ec444291b2b4d951aa050106 schema:name doi
85 schema:value 10.1007/978-3-030-24886-4_2
86 rdf:type schema:PropertyValue
87 N7067b59a3bd14c3a856e07a92c05132a rdf:first N7451af4b79df4508b342c52bf8e88f0c
88 rdf:rest Naa40b48fb0e940f6bd0a382ecc232639
89 N7451af4b79df4508b342c52bf8e88f0c schema:familyName Hofman
90 schema:givenName Piotrek
91 rdf:type schema:Person
92 N7a170ad2d3b44da68b4d94e9c5ccc744 schema:familyName Skrzypczak
93 schema:givenName Michał
94 rdf:type schema:Person
95 N7d538e293738471e87da012b92ede643 schema:isbn 978-3-030-24885-7
96 978-3-030-24886-4
97 schema:name Developments in Language Theory
98 rdf:type schema:Book
99 N7fb6ca260d2d4fbea71fe2932088c8fd rdf:first sg:person.015252371751.76
100 rdf:rest rdf:nil
101 Naa40b48fb0e940f6bd0a382ecc232639 rdf:first N7a170ad2d3b44da68b4d94e9c5ccc744
102 rdf:rest rdf:nil
103 Nd97a83260a1a4639a39f491b2f3bd92e schema:name dimensions_id
104 schema:value pub.1119756454
105 rdf:type schema:PropertyValue
106 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
107 schema:name Mathematical Sciences
108 rdf:type schema:DefinedTerm
109 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
110 schema:name Pure Mathematics
111 rdf:type schema:DefinedTerm
112 sg:person.015252371751.76 schema:affiliation grid-institutes:grid.8505.8
113 schema:familyName Jeż
114 schema:givenName Artur
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015252371751.76
116 rdf:type schema:Person
117 grid-institutes:grid.8505.8 schema:alternateName University of Wrocław, Wrocław, Poland
118 schema:name University of Wrocław, Wrocław, Poland
119 rdf:type schema:Organization
 




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


...