Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Nominal Unification of Higher Order Expressions with Recursive Let

verfasst von : Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine their complexity.

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 Coinductive Soundness of Corecursive Type Class Resolution
Nächstes Kapitel Automata Theory Approach to Predicate Intuitionistic Logic
Literatur
1.
Aoto, T., Kikuchi, K.: A rule-based procedure for equivariant nominal unification. In: Informal Proceedings HOR, p. 5 (2016)
2.
Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: POPL 1995, pp. 233–246. ACM Press, San Francisco (1995)
3.
Ariola, Z.M., Klop, J.W.: Cyclic lambda graph rewriting. In: Proceedings of IEEE LICS, pp. 416–425. IEEE Press (1994)
4.
Ayala-Rincón, M., de Carvalho-Segundo, W., Fernández, M., Nantes-Sobrinho, D.: A formalisation of nominal alpha-equivalence with A and AC function symbols. In: Proceedings of LSFA 2016, pp. 78–93 (2016)
5.
Ayala-Rincón, M., Fernández, M., Nantes-Sobrinho, D.: Nominal narrowing. In: Pientka, B., Kesner, D. (eds.) Proceedings of First FSCD, pp. 11:1–11:17. LIPIcs (2016)
6.
Ayala-Rincón, M., Fernández, M., Rocha-Oliveira, A.C.: Completeness in PVS of a nominal unification algorithm. ENTCS 323(3), 57–74 (2016)MathSciNet
7.
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–532. Elsevier, MIT Press, New York, Cambridge (2001)CrossRef
8.
9.
10.
Cheney, J.: Nominal Logic Programming. Ph.D. thesis, Cornell University, Ithaca (2004)
11.
12.
Cheney, J.: Relating higher-order pattern unification and nominal unification. In: Proceedings of 19th International Workshop on Unification (UNIF 2005), pp. 104–119 (2005)
13.
Cheney, J.: Toward a general theory of names: binding and scope. In: MERLIN 2005, pp. 33–40. ACM (2005)
14.
15.
Furst, M.L., Hopcroft, J.E., Luks, E.M.: Polynomial-time algorithms for permutation groups. In: 21st FoCS, pp. 36–41. IEEE Computer Society (1980)
16.
Garey, M.R., Johnson, D.S., Tarjan, R.E.: The planar Hamiltonian circuit problem is NP-complete. SIAM J. Comput. 5(4), 704–714 (1976)MathSciNetCrossRefMATH
17.
18.
Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27–57 (1975)CrossRefMATH
19.
20.
21.
Levy, J., Villaret, M.: An efficient nominal unification algorithm. In: Lynch, C. (ed.) Proceedings of 21st RTA, LIPIcs, vol. 6, pp. 209–226. Schloss Dagstuhl (2010)
22.
23.
Luks, E.M.: Permutation groups and polynomial-time computation. In: Finkelstein, L., Kantor, W.M. (eds.) Groups And Computation, Proceedings of a DIMACS Workshop (DIMACS), vol. 11, pp. 139–176. DIMACS/AMS (1991)
24.
Marlow, S. (ed.): Haskell 2010 - Language Report (2010)
25.
Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)CrossRefMATH
26.
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497–536 (1991)MathSciNetCrossRefMATH
27.
Moran, A., Sands, D., Carlsson, M.: Erratic fudgets: a semantic theory for an embedded coordination language. In: Ciancarini, P., Wolf, A.L. (eds.) COORDINATION 1999. LNCS, vol. 1594, pp. 85–102. Springer, Heidelberg (1999). doi:10.​1007/​3-540-48919-3_​8 CrossRef
28.
29.
Schmidt-SchauSS, M., Rau, C., Sabel, D.: Algorithms for extended alpha-equivalence and complexity. In: van Raamsdonk, F. (ed.) 24th RTA 2013. LIPIcs, vol. 21, pp. 255–270. Schloss Dagstuhl (2013)
30.
31.
Schmidt-Schauß, M., Schütz, M., Sabel, D.: Safety of Nöcker’s strictness analysis. J. Funct. Program. 18(04), 503–551 (2008)CrossRefMATH
32.
33.
Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive logic programming. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 330–345. Springer, Heidelberg (2006). doi:10.​1007/​11799573_​25 CrossRef
34.
Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in nominal Isabelle. Log. Methods Comput. Sci. 8(2:14), 1–35 (2012). www.​lmcs-online.​org
35.
36.
Metadaten
Titel
Nominal Unification of Higher Order Expressions with Recursive Let
verfasst von
Manfred Schmidt-Schauß
Temur Kutsia
Jordi Levy
Mateu Villaret
Copyright-Jahr
2017
Buch
Logic-Based Program Synthesis and Transformation

Print ISBN: 978-3-319-63138-7

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

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-63139-4_19