nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs

verfasst von : Henning Christiansen, Maja H. Kirkeby

Erschienen in: Functional and Constraint Logic Programming

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating CHR programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated as is needed for confluence proofs, thus extending our previous theoretical results towards a practical implementation.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Synthesizing Set Functions

Nächstes Kapitel Reference Type Logic Variables in Constraint-Logic Object-Oriented Programming

A similar property has been studied by [8] in term rewriting under the name of “local termination”.

We may introduce more types in the following whenever we need them.

Abdennadher, S.: Operational semantics and confluence of constraint propagation rules. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 252–266. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0017444CrossRef

Abdennadher, S., Frühwirth, T., Meuss, H.: On confluence of Constraint Handling Rules. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 1–15. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61551-2_62CrossRef

Abdennadher, S., Frühwirth, T.W., Meuss, H.: Confluence and semantics of constraint simplification rules. Constraints 4(2), 133–165 (1999)MathSciNetCrossRef

Christiansen, H., Kirkeby, M.H.: Confluence modulo equivalence in constraint handling rules. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 41–58. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17822-6_3CrossRef

Christiansen, H., Kirkeby, M.H.: On proving confluence modulo equivalence for constraint handling rules. Formal Aspects Comput. 29(1), 57–95 (2017)MathSciNetCrossRef

Christiansen, H., Kirkeby, M.H.: Confluence of CHR revisited: invariants and modulo equivalence. In: LOPSTR 2018, vol. 11408. LNCS, pp. 83–99. Springer, Heidelberg (2019)

Duck, G.J., Stuckey, P.J., Sulzmann, M.: Observable confluence for constraint handling rules. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 224–239. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74610-2_16CrossRef

Endrullis, J., de Vrijer, R.C., Waldmann, J.: Local termination: theory and practice. Logical Methods Comput. Sci. 6(3), 1–37 (2010)MathSciNetCrossRef

Frühwirth, T.W.: User-defined constraint handling. In: ICLP, pp. 837–838. MIT Press (1993)

10.

Frühwirth, T.W.: Theory and practice of constraint handling rules. J. Logic Program. 37(1–3), 95–138 (1998)MathSciNetCrossRef

11.

Frühwirth, T.: Proving termination of constraint solver programs. In: Apt, K.R., Monfroy, E., Kakas, A.C., Rossi, F. (eds.) WC 1999. LNCS (LNAI), vol. 1865, pp. 298–317. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44654-0_15CrossRef

12.

Frühwirth, T.W.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009)CrossRef

13.

Gall, D., Frühwirth, T.: Confluence modulo equivalence with invariants in constraint handling rules. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 116–131. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_8CrossRef

14.

Holzbaur, C., Frühwirth, T.W.: A PROLOG constraint handling rules compiler and runtime system. Appl. Artif. Intell. 14(4), 369–388 (2000)CrossRef

15.

Huet, G.P.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)MathSciNetCrossRef

16.

Langbein, J., Raiser, F., Frühwirth, T.W.: A state equivalence and confluence checker for CHRs. In: Proceedings International Workshop on Constraint Handling Rules, Report CW 588, pp. 1–8. Katholieke Universiteit Leuven, Belgium (2010)

17.

Newman, M.: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43(2), 223–243 (1942)MathSciNetCrossRef

18.

Pilozzi, P., De Schreye, D.: Automating termination proofs for CHR. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 504–508. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02846-5_43CrossRef

19.

Pilozzi, P., De Schreye, D.: Improved termination analysis of CHR using self-sustainability analysis. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 189–204. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32211-2_13CrossRef

20.

Schrijvers, T., Demoen, B.: The K.U. Leuven CHR system: implementation and application. In: Workshop on Constraint Handling Rules: Selected Contributions, pp. 1–5. Ulmer Informatik-Berichte, Nr. 2004–01 (2004)

Titel: Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs
verfasst von: Henning Christiansen
Maja H. Kirkeby
Verlag: Springer International Publishing
Buch: Functional and Constraint Logic Programming
Print ISBN: 978-3-030-16201-6

Electronic ISBN: 978-3-030-16202-3

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-16202-3_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"