Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2018

AUTHORS

Thom Frühwirth

ABSTRACT

We present a straightforward source-to-source transformation that introduces justifications for user-defined constraints into the CHR programming language. Then a scheme of two rules suffices to allow for logical retraction (deletion, removal) of constraints during computation. Without the need to recompute from scratch, these rules remove not only the constraint but also undo all consequences of the rule applications that involved the constraint. We prove a confluence result concerning the rule scheme and show its correctness. When algorithms are written in CHR, constraints represent both data and operations. CHR is already incremental by nature, i.e. constraints can be added at runtime. Logical retraction adds decrementality. Hence any algorithm written in CHR with justifications will become fully dynamic. Operations can be undone and data can be removed at any point in the computation without compromising the correctness of the result. We present two classical examples of dynamic algorithms, written in our prototype implementation of CHR with justifications that is available online: maintaining the minimum of a changing set of numbers and shortest paths in a graph whose edges change. More... »

PAGES

147-163

References to SciGraph publications

  • 2015. Constraint Handling Rules - What Else? in RULE TECHNOLOGIES: FOUNDATIONS, TOOLS, AND APPLICATIONS
  • 1999-05. Confluence and Semantics of Constraint Simplification Rules in CONSTRAINTS
  • 2008. A Flexible Search Framework for CHR in CONSTRAINT HANDLING RULES
  • 2001. Adaptive Constraint Handling with CHR in Java in PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING — CP 2001
  • 2005-06-10. Operational semantics and confluence of constraint propagation rules in PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING-CP97
  • Book

    TITLE

    Logic-Based Program Synthesis and Transformation

    ISBN

    978-3-319-94459-3
    978-3-319-94460-9

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-319-94460-9_9

    DOI

    http://dx.doi.org/10.1007/978-3-319-94460-9_9

    DIMENSIONS

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


    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/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "University of Ulm", 
              "id": "https://www.grid.ac/institutes/grid.6582.9", 
              "name": [
                "Ulm University"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Fr\u00fchwirth", 
            "givenName": "Thom", 
            "id": "sg:person.013750414271.15", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013750414271.15"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-3-319-21542-6_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010556081", 
              "https://doi.org/10.1007/978-3-319-21542-6_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0017444", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010989701", 
              "https://doi.org/10.1007/bfb0017444"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0017444", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010989701", 
              "https://doi.org/10.1007/bfb0017444"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/s1574-6526(06)80025-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1011953429"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1023/a:1009842826135", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1017229802", 
              "https://doi.org/10.1023/a:1009842826135"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/871895.871903", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034281470"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-92243-8_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039051456", 
              "https://doi.org/10.1007/978-3-540-92243-8_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-92243-8_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039051456", 
              "https://doi.org/10.1007/978-3-540-92243-8_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1080/088395100117052", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1048214470"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-45578-7_18", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051810129", 
              "https://doi.org/10.1007/3-540-45578-7_18"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s1471068405002383", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1054006325"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s1471068405002383", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1054006325"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s1471068405002383", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1054006325"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s1471068412000208", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1054088935"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/cbo9780511609886", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1098740870"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2018", 
        "datePublishedReg": "2018-01-01", 
        "description": "We present a straightforward source-to-source transformation that introduces justifications for user-defined constraints into the CHR programming language. Then a scheme of two rules suffices to allow for logical retraction (deletion, removal) of constraints during computation. Without the need to recompute from scratch, these rules remove not only the constraint but also undo all consequences of the rule applications that involved the constraint. We prove a confluence result concerning the rule scheme and show its correctness. When algorithms are written in CHR, constraints represent both data and operations. CHR is already incremental by nature, i.e. constraints can be added at runtime. Logical retraction adds decrementality. Hence any algorithm written in CHR with justifications will become fully dynamic. Operations can be undone and data can be removed at any point in the computation without compromising the correctness of the result. We present two classical examples of dynamic algorithms, written in our prototype implementation of CHR with justifications that is available online: maintaining the minimum of a changing set of numbers and shortest paths in a graph whose edges change.", 
        "editor": [
          {
            "familyName": "Fioravanti", 
            "givenName": "Fabio", 
            "type": "Person"
          }, 
          {
            "familyName": "Gallagher", 
            "givenName": "John P.", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-319-94460-9_9", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-319-94459-3", 
            "978-3-319-94460-9"
          ], 
          "name": "Logic-Based Program Synthesis and Transformation", 
          "type": "Book"
        }, 
        "name": "Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms", 
        "pagination": "147-163", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-319-94460-9_9"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "0f0227080e27a97d93d076976e353f47a88602a655b206cfc35c738fad5eb42e"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1105427502"
            ]
          }
        ], 
        "publisher": {
          "location": "Cham", 
          "name": "Springer International Publishing", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-319-94460-9_9", 
          "https://app.dimensions.ai/details/publication/pub.1105427502"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-15T22:38", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000001_0000000264/records_8693_00000604.jsonl", 
        "type": "Chapter", 
        "url": "http://link.springer.com/10.1007/978-3-319-94460-9_9"
      }
    ]
     

    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-319-94460-9_9'

    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-319-94460-9_9'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-94460-9_9'

    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-319-94460-9_9'


     

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

    108 TRIPLES      23 PREDICATES      38 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-319-94460-9_9 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Nd7a12f8942da4a43a193178b098a28c3
    4 schema:citation sg:pub.10.1007/3-540-45578-7_18
    5 sg:pub.10.1007/978-3-319-21542-6_2
    6 sg:pub.10.1007/978-3-540-92243-8_2
    7 sg:pub.10.1007/bfb0017444
    8 sg:pub.10.1023/a:1009842826135
    9 https://doi.org/10.1016/s1574-6526(06)80025-8
    10 https://doi.org/10.1017/cbo9780511609886
    11 https://doi.org/10.1017/s1471068405002383
    12 https://doi.org/10.1017/s1471068412000208
    13 https://doi.org/10.1080/088395100117052
    14 https://doi.org/10.1145/871895.871903
    15 schema:datePublished 2018
    16 schema:datePublishedReg 2018-01-01
    17 schema:description We present a straightforward source-to-source transformation that introduces justifications for user-defined constraints into the CHR programming language. Then a scheme of two rules suffices to allow for logical retraction (deletion, removal) of constraints during computation. Without the need to recompute from scratch, these rules remove not only the constraint but also undo all consequences of the rule applications that involved the constraint. We prove a confluence result concerning the rule scheme and show its correctness. When algorithms are written in CHR, constraints represent both data and operations. CHR is already incremental by nature, i.e. constraints can be added at runtime. Logical retraction adds decrementality. Hence any algorithm written in CHR with justifications will become fully dynamic. Operations can be undone and data can be removed at any point in the computation without compromising the correctness of the result. We present two classical examples of dynamic algorithms, written in our prototype implementation of CHR with justifications that is available online: maintaining the minimum of a changing set of numbers and shortest paths in a graph whose edges change.
    18 schema:editor N0f14f1ef7c92426eaa582801f11a32e9
    19 schema:genre chapter
    20 schema:inLanguage en
    21 schema:isAccessibleForFree false
    22 schema:isPartOf Nb896ad512fe142c5b7e6b460dac22fb7
    23 schema:name Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms
    24 schema:pagination 147-163
    25 schema:productId N3e972ae2c1054b43988cb29c5679b174
    26 N65c7137931a0442498095318113292bb
    27 Ne281a0c24dfd48ff94cf777de10efd91
    28 schema:publisher Nd00615975ec14b9984e1b670e81a383e
    29 schema:sameAs https://app.dimensions.ai/details/publication/pub.1105427502
    30 https://doi.org/10.1007/978-3-319-94460-9_9
    31 schema:sdDatePublished 2019-04-15T22:38
    32 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    33 schema:sdPublisher N318777680eab409f8211ccac91dced30
    34 schema:url http://link.springer.com/10.1007/978-3-319-94460-9_9
    35 sgo:license sg:explorer/license/
    36 sgo:sdDataset chapters
    37 rdf:type schema:Chapter
    38 N0f14f1ef7c92426eaa582801f11a32e9 rdf:first Na4ed6bead8c54ae19b58b9d5f99dcee9
    39 rdf:rest N4b8c05a8e5414fc8859754a287cb2fce
    40 N318777680eab409f8211ccac91dced30 schema:name Springer Nature - SN SciGraph project
    41 rdf:type schema:Organization
    42 N3e972ae2c1054b43988cb29c5679b174 schema:name readcube_id
    43 schema:value 0f0227080e27a97d93d076976e353f47a88602a655b206cfc35c738fad5eb42e
    44 rdf:type schema:PropertyValue
    45 N4b8c05a8e5414fc8859754a287cb2fce rdf:first N7cd9338e38914f4e90cb9bbd862d919d
    46 rdf:rest rdf:nil
    47 N65c7137931a0442498095318113292bb schema:name dimensions_id
    48 schema:value pub.1105427502
    49 rdf:type schema:PropertyValue
    50 N7cd9338e38914f4e90cb9bbd862d919d schema:familyName Gallagher
    51 schema:givenName John P.
    52 rdf:type schema:Person
    53 Na4ed6bead8c54ae19b58b9d5f99dcee9 schema:familyName Fioravanti
    54 schema:givenName Fabio
    55 rdf:type schema:Person
    56 Nb896ad512fe142c5b7e6b460dac22fb7 schema:isbn 978-3-319-94459-3
    57 978-3-319-94460-9
    58 schema:name Logic-Based Program Synthesis and Transformation
    59 rdf:type schema:Book
    60 Nd00615975ec14b9984e1b670e81a383e schema:location Cham
    61 schema:name Springer International Publishing
    62 rdf:type schema:Organisation
    63 Nd7a12f8942da4a43a193178b098a28c3 rdf:first sg:person.013750414271.15
    64 rdf:rest rdf:nil
    65 Ne281a0c24dfd48ff94cf777de10efd91 schema:name doi
    66 schema:value 10.1007/978-3-319-94460-9_9
    67 rdf:type schema:PropertyValue
    68 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    69 schema:name Information and Computing Sciences
    70 rdf:type schema:DefinedTerm
    71 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    72 schema:name Computation Theory and Mathematics
    73 rdf:type schema:DefinedTerm
    74 sg:person.013750414271.15 schema:affiliation https://www.grid.ac/institutes/grid.6582.9
    75 schema:familyName Frühwirth
    76 schema:givenName Thom
    77 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013750414271.15
    78 rdf:type schema:Person
    79 sg:pub.10.1007/3-540-45578-7_18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051810129
    80 https://doi.org/10.1007/3-540-45578-7_18
    81 rdf:type schema:CreativeWork
    82 sg:pub.10.1007/978-3-319-21542-6_2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010556081
    83 https://doi.org/10.1007/978-3-319-21542-6_2
    84 rdf:type schema:CreativeWork
    85 sg:pub.10.1007/978-3-540-92243-8_2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1039051456
    86 https://doi.org/10.1007/978-3-540-92243-8_2
    87 rdf:type schema:CreativeWork
    88 sg:pub.10.1007/bfb0017444 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010989701
    89 https://doi.org/10.1007/bfb0017444
    90 rdf:type schema:CreativeWork
    91 sg:pub.10.1023/a:1009842826135 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017229802
    92 https://doi.org/10.1023/a:1009842826135
    93 rdf:type schema:CreativeWork
    94 https://doi.org/10.1016/s1574-6526(06)80025-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011953429
    95 rdf:type schema:CreativeWork
    96 https://doi.org/10.1017/cbo9780511609886 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098740870
    97 rdf:type schema:CreativeWork
    98 https://doi.org/10.1017/s1471068405002383 schema:sameAs https://app.dimensions.ai/details/publication/pub.1054006325
    99 rdf:type schema:CreativeWork
    100 https://doi.org/10.1017/s1471068412000208 schema:sameAs https://app.dimensions.ai/details/publication/pub.1054088935
    101 rdf:type schema:CreativeWork
    102 https://doi.org/10.1080/088395100117052 schema:sameAs https://app.dimensions.ai/details/publication/pub.1048214470
    103 rdf:type schema:CreativeWork
    104 https://doi.org/10.1145/871895.871903 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034281470
    105 rdf:type schema:CreativeWork
    106 https://www.grid.ac/institutes/grid.6582.9 schema:alternateName University of Ulm
    107 schema:name Ulm University
    108 rdf:type schema:Organization
     




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


    ...