Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Verification of Concurrent Programs on Weak Memory Models Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Unification for \(\lambda \)-calculi Without Propagation Rules

Author : Flávio L. C. de Moura

Published in: Theoretical Aspects of Computing – ICTAC 2016

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present a unification procedure for calculi with explicit substitutions (ES) without propagation rules. The novelty of this work is that the unification procedure was developed for the calculi with ES that belong to the paradigm known as “act at a distance”, i.e. explicit substitutions are not propagated to the level of variables, as usual. The unification procedure is proved correct and complete, and enjoy a simple form of substitution, called grafting, instead of the standard capture avoiding variable substitution.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Towards MC/DC Coverage of Properties Specification Patterns
next chapter Soundly Proving B Method Formulæ Using Typed Sequent Calculus
Footnotes
1
We write the type information only in the initial terms of the examples for readability.
 
Literature
1.
2.
Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: Tiwari [36], pp. 6–21
3.
Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, 1–3 September 2014, pp. 363–376. ACM (2014)
4.
Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 659–670. ACM (2014)
5.
6.
7.
Accattoli, B., Kesner, D.: Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods Comput. Sci. 8(1), 1–44 (2012)MathSciNetCrossRefMATH
8.
Accattoli, B., Dal Lago, U.: On the invariance of the unitary cost model for head reduction. In: Tiwari [36], pp. 22–37
9.
Ayala-Rincón, M., Kamareddine, F.: Unification via the \(\lambda s_e\)-style of explicit substitution. Logical J. IGPL 9(4), 489–523 (2001)CrossRefMATH
10.
Ayala-Rincón, M., Kamareddine, F.: On applying the \(\lambda s_e\)-style of unification for simply-typed higher order unification in the pure lambda calculus. Matemática Contemporânea 24, 1–22 (2003)MATH
11.
de Moura, F.L.C., Kesner, D., Ayala-Rincón, M.: Metaconfluence of calculi with explicit substitutions at a distance. In: Raman, V., Suresh, S.P. (eds.) 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), vol. 29, pp. 391–402. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2014)
12.
de Moura, F.L.C.: Higher-order unification via explicit substitutions at a distance. In: LSFA 2014 (2014). Accepted for short presentation
13.
de Moura, F.L.C., Ayala-Rincón, M., Kamareddine, F.: Higher-order unification: a structural relation between Huet’s method and the one based on explicit substitutions. J. Appl. Logic 6(1), 72–108 (2008)CrossRefMATH
14.
de Moura, F.L.C., Kamareddine, F., Ayala-Rincón, M.: Second-order matching via explicit substitutions. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 433–448. Springer, Heidelberg (2005). doi:10.​1007/​978-3-540-32275-7_​29 CrossRef
15.
16.
17.
Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1009–1062. MIT press and Elsevier (2001). Chap. 16
18.
Dowek, G., Hardin, T., Kirchner, C.: Higher order unification via explicit substitutions. Inf. Comput. 157(1–2), 183–235 (2000)MathSciNetCrossRefMATH
19.
Briaud, D., Lescanne, P., Rouyer-Degli, J.: \(\lambda \upsilon \), a calculus of explicit substitutions which preserves strong normalization. JFP 6(5), 699–722 (1996)MathSciNetMATH
20.
21.
22.
23.
24.
25.
Huet, G.: Résolution d’équations dans les langages d’ordre 1,2,..,\(\omega \). Ph.D. thesis, University Paris-7 (1976)
26.
Kamareddine, F., Ríos, A.: Extending a \(\lambda \)-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. J. Func. Program. 7, 395–420 (1997)MathSciNetCrossRefMATH
27.
Kesner, D.: A theory of explicit substitutions with safe and full composition. Logical Methods Comput. Sci. 5(31), 1–29 (2009)MathSciNetMATH
28.
29.
Loader, R.: Higher order \(\beta \) matching is undecidable. Logic J. Interest Group Pure Appl. Logics 11(1), 51–68 (2003)MathSciNetMATH
30.
Mellies, P.-A.: Typed \(\lambda \)-calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 328–334. Springer, Heidelberg (1995). doi:10.​1007/​BFb0014062 CrossRef
31.
Milner, R.: Local bigraphs and confluence: two conjectures: (extended abstract). ENTCS 175(3), 65–73 (2007)MathSciNetMATH
32.
33.
34.
Snyder, W., Gallier, J.H.: Higher-order unification revisited: complete sets of transformations. J. Symb. Comput. 8(1/2), 101–140 (1989)MathSciNetCrossRefMATH
35.
Stirling, C.: A game-theoretic approach to deciding higher-order matching. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 348–359. Springer, Heidelberg (2006). doi:10.​1007/​11787006_​30 CrossRef
36.
Tiwari, A. (ed.) 23rd International Conference on Rewriting Techniques and Applications (RTA 2012). LIPIcs, Nagoya, Japan, 28 May 2012 – 2 June 2012, vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)
Metadata
Title
Unification for -calculi Without Propagation Rules
Author
Flávio L. C. de Moura
Copyright Year
2016
Book
Theoretical Aspects of Computing – ICTAC 2016

Print ISBN: 978-3-319-46749-8

Electronic ISBN: 978-3-319-46750-4

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-46750-4_11

Premium Partner

    Image Credits