Type-based homeomorphic embedding for online termination

Elvira Albert, John Patrick Gallagher, Miguel Gómez-Zamalloa, Germán Puebla

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

Online termination techniques dynamically guarantee termination of computations by supervising them in such a way that computations whose termination can no longer be guaranteed are stopped. Homeomorphic Embedding (HEm) has proven to be very useful for online termination provided that the computations supervised are performed over a finite signature, i.e., the number of constants and function symbols involved is finite. However, there are many situations, for example numeric computations, which involve an infinite signature and thus HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination. However, the existing techniques either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We propose Type-based Homeomorphic Embedding (TbHEm) as an extension of the standard, untyped, HEm. By taking static information about the behavior of the computation into account, expressed as types, TbHEm allows obtaining more precise results than those of the previous extensions to HEm for the case of infinite signatures. We show that the existing extensions to HEm which are currently used in state-of-the-art specialization tools can be reconstructed as instances of TbHEm. We illustrate the applicability of our proposal in a realistic case study: partial evaluation of an interpreter. We argue that the results obtained provide empirical evidence of the interest of our proposal.
Original languageEnglish
JournalInformation Processing Letters
Volume109
Issue number15
Pages (from-to)879-886
Number of pages8
ISSN0020-0190
DOIs
Publication statusPublished - 2009

Keywords

  • Analysis of algorithms
  • Partial evaluation
  • Program transformation
  • Homeomorphic embedding
  • Termination
  • Formal methods

Cite this

Albert, Elvira ; Gallagher, John Patrick ; Gómez-Zamalloa, Miguel ; Puebla, Germán. / Type-based homeomorphic embedding for online termination. In: Information Processing Letters. 2009 ; Vol. 109, No. 15. pp. 879-886.
@article{60b13db0567e11de981a000ea68e967b,
title = "Type-based homeomorphic embedding for online termination",
abstract = "Online termination techniques dynamically guarantee termination of computations by supervising them in such a way that computations whose termination can no longer be guaranteed are stopped. Homeomorphic Embedding (HEm) has proven to be very useful for online termination provided that the computations supervised are performed over a finite signature, i.e., the number of constants and function symbols involved is finite. However, there are many situations, for example numeric computations, which involve an infinite signature and thus HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination. However, the existing techniques either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We propose Type-based Homeomorphic Embedding (TbHEm) as an extension of the standard, untyped, HEm. By taking static information about the behavior of the computation into account, expressed as types, TbHEm allows obtaining more precise results than those of the previous extensions to HEm for the case of infinite signatures. We show that the existing extensions to HEm which are currently used in state-of-the-art specialization tools can be reconstructed as instances of TbHEm. We illustrate the applicability of our proposal in a realistic case study: partial evaluation of an interpreter. We argue that the results obtained provide empirical evidence of the interest of our proposal.",
keywords = "Analysis of algorithms, Partial evaluation, Program transformation, Homeomorphic embedding, Termination, Formal methods",
author = "Elvira Albert and Gallagher, {John Patrick} and Miguel G{\'o}mez-Zamalloa and Germ{\'a}n Puebla",
year = "2009",
doi = "10.1016/j.ipl.2009.04.016",
language = "English",
volume = "109",
pages = "879--886",
journal = "Information Processing Letters",
issn = "0020-0190",
publisher = "Elsevier BV",
number = "15",

}

Type-based homeomorphic embedding for online termination. / Albert, Elvira; Gallagher, John Patrick; Gómez-Zamalloa, Miguel; Puebla, Germán.

In: Information Processing Letters, Vol. 109, No. 15, 2009, p. 879-886.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Type-based homeomorphic embedding for online termination

AU - Albert, Elvira

AU - Gallagher, John Patrick

AU - Gómez-Zamalloa, Miguel

AU - Puebla, Germán

PY - 2009

Y1 - 2009

N2 - Online termination techniques dynamically guarantee termination of computations by supervising them in such a way that computations whose termination can no longer be guaranteed are stopped. Homeomorphic Embedding (HEm) has proven to be very useful for online termination provided that the computations supervised are performed over a finite signature, i.e., the number of constants and function symbols involved is finite. However, there are many situations, for example numeric computations, which involve an infinite signature and thus HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination. However, the existing techniques either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We propose Type-based Homeomorphic Embedding (TbHEm) as an extension of the standard, untyped, HEm. By taking static information about the behavior of the computation into account, expressed as types, TbHEm allows obtaining more precise results than those of the previous extensions to HEm for the case of infinite signatures. We show that the existing extensions to HEm which are currently used in state-of-the-art specialization tools can be reconstructed as instances of TbHEm. We illustrate the applicability of our proposal in a realistic case study: partial evaluation of an interpreter. We argue that the results obtained provide empirical evidence of the interest of our proposal.

AB - Online termination techniques dynamically guarantee termination of computations by supervising them in such a way that computations whose termination can no longer be guaranteed are stopped. Homeomorphic Embedding (HEm) has proven to be very useful for online termination provided that the computations supervised are performed over a finite signature, i.e., the number of constants and function symbols involved is finite. However, there are many situations, for example numeric computations, which involve an infinite signature and thus HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination. However, the existing techniques either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We propose Type-based Homeomorphic Embedding (TbHEm) as an extension of the standard, untyped, HEm. By taking static information about the behavior of the computation into account, expressed as types, TbHEm allows obtaining more precise results than those of the previous extensions to HEm for the case of infinite signatures. We show that the existing extensions to HEm which are currently used in state-of-the-art specialization tools can be reconstructed as instances of TbHEm. We illustrate the applicability of our proposal in a realistic case study: partial evaluation of an interpreter. We argue that the results obtained provide empirical evidence of the interest of our proposal.

KW - Analysis of algorithms

KW - Partial evaluation

KW - Program transformation

KW - Homeomorphic embedding

KW - Termination

KW - Formal methods

U2 - 10.1016/j.ipl.2009.04.016

DO - 10.1016/j.ipl.2009.04.016

M3 - Journal article

VL - 109

SP - 879

EP - 886

JO - Information Processing Letters

JF - Information Processing Letters

SN - 0020-0190

IS - 15

ER -