Type-based homeomorphic embedding for online termination
| Autor: | Miguel Gómez-Zamalloa, Elvira Albert, John P. Gallagher, Germán Puebla |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
Computation
Program transformation 0102 computer and information sciences 02 engineering and technology Function (mathematics) Formal methods 01 natural sciences Signature (logic) Partial evaluation Computer Science Applications Theoretical Computer Science 010201 computation theory & mathematics Signal Processing 0202 electrical engineering electronic engineering information engineering Embedding 020201 artificial intelligence & image processing Algorithm Information Systems Mathematics Analysis of algorithms |
| Zdroj: | Information Processing Letters. 109:879-886 |
| ISSN: | 0020-0190 |
| DOI: | 10.1016/j.ipl.2009.04.016 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect