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:
Programming with “Big Code” Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Decision Algorithms for Checking Definability of Order-2 Finitary PCF

verfasst von : Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi

Erschienen in: Programming Languages and Systems

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We consider a definability problem for finitary PCF, which asks whether, given a function (as an element of a cpo), there exists a term of finitary PCF whose interpretation is the function. The definability problem for finitary PCF is known to be decidable for types of order at most 2. However, its complexity and practical algorithms have not been well studied. In this paper, we give two algorithms for checking definability: one based on Sieber’s sequentiality relation, which runs in quadruply exponential time for the size of the type of the given function, and the other based on a saturation method, which runs in triply exponential time for the size. With the recent advance of higher-order model checking, our result may be useful for implementing a tool for deciding observational equivalence between finitary PCF terms of types of order at most 3.

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 Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs
Nächstes Kapitel Uncovering JavaScript Performance Code Smells Relevant to Type Mutations
Fußnoten
1
We thank an anonymous reviewer for providing us the information of Stoughton’s work.
 
2
A function f between pointed cpos is continuous if f is monotonic and preserves the least upper bound of any directed subset. Note that, if f is a function between finite cpos, f is continuous if and only if f is monotonic.
 
3
A cartesian product of two cpos \(D_1=(S_1,\le _1)\) and \(D_2=(S_2,\le _2)\) is a cpo \((S_1\times S_2,\le _{D_1 \times D_2})\) where \((d_1,d_2)\le _{D_1 \times D_2}(d_1^{\prime },d_2^{\prime }) \mathop {\Longleftrightarrow }\limits ^{\mathrm {def}}d_1 \le _1 d_1^{\prime }\wedge d_2 \le _2 d_2^{\prime }\).
 
Literatur
1.
2.
Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998) CrossRef
3.
Amadio, R.M., Curien, P.L.: Domains and Lambda-Calculi. Cambridge University Press, Cambridge (1998)CrossRefMATH
4.
Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of CSL 2013. LIPIcs, vol. 23, pp. 129–148 (2013)
5.
Hopkins, D., Murawski, A.S., Ong, C.-H.L.: Hector: an equivalence checker for a higher-order fragment of ML. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 774–780. Springer, Heidelberg (2012) CrossRef
6.
Hopkins, D., Murawski, A.S., Ong, C.-H.L.: A fragment of ML decidable by visibly pushdown automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 149–161. Springer, Heidelberg (2011) CrossRef
7.
Hopkins, D., Ong, C.-H.L.: Homer: a higher-order observational equivalence model checkER. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 654–660. Springer, Heidelberg (2009) CrossRef
8.
9.
10.
Loader, R.: The undecidability of lambda-definability. In: The Church Festschrift. CSLI/University of Chicago Press (1994)
11.
12.
13.
Murawski, A.S.: On program equivalence in languages with ground-type references. In: Proceedings of LICS 2003, pp. 108–108. IEEE (2003)
14.
15.
Murawski, A.S., Walukiewicz, I.: Third-order Idealized Algol with iteration is decidable. Theor. Comput. Sci. 390(2–3), 214–229 (2008)CrossRefMathSciNetMATH
16.
Ong, C.-H.L.: Observational equivalence of 3rd-order Idealized Algol is decidable. In: Proceedings of LICS 2002, pp. 245–256. IEEE (2002)
17.
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81–90. IEEE (2006)
18.
19.
Plotkin, G.D.: Lambda-definability and logical relations. Technical report, SAI-RM-4, School of Artificial Intelligence, University of Edinburgh (1973)
20.
Plotkin, G.D.: Lambda-definability in the full type hierarchy. To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 363–373 (1980)
21.
Ramsay, S.J., Neatherway, R., Ong, C.-H.L.: An abstraction refinement approach to higher-order model checking. In: Proceedings of POPL 2014, pp. 61–72. ACM (2014)
22.
Reynolds, J.C.: The essence of Algol. In: O’Hearn, P.W., Tennent, R.D. (eds.) ALGOL-like Languages. Progress in Theoretical Computer Science, pp. 67–88. Springer, Heidelberg (1997) CrossRef
23.
Sieber, K.: Reasoning about sequential functions via logical relations. In: Applications of Categories in Computer Science. London Mathematical Society Lecture Note Series, vol. 177, pp. 258–269. Cambridge University Press (1992)
24.
Stoughton, A.: Mechanizing logical relations. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 359–377. Springer, Heidelberg (1994) CrossRef
25.
Winskel, G.: Formal Semantics of Programming Languages. The MIT Press, Cambridge (1993)MATH
Metadaten
Titel
Decision Algorithms for Checking Definability of Order-2 Finitary PCF
verfasst von
Sadaaki Kawata
Kazuyuki Asada
Naoki Kobayashi
Copyright-Jahr
2015
Buch
Programming Languages and Systems

Print ISBN: 978-3-319-26528-5

Electronic ISBN: 978-3-319-26529-2

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-26529-2_17