Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation

Homeomorphic Embedding (HEm) has proven to be very powerful for supervising termination of computations, provided that such computations are performed over a finite signature, i.e., the number of constants and function symbols involved is finite. However, there are situations, for example numeric computations, which involve an infinite (or too large) signature, in which HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination, but they 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 introduce Type-based Homeomorphic Embedding (TbHEm) as an extension of the standard, untyped HEm to deal with infinite signatures. In the paper, we show how TbHEm can be used to improve the accuracy of online partial evaluation. For this purpose, we propose an approach to constructing suitable types for pa...

• Type: Conference
• Year: 2007
• Where: LOPSTR
• Authors: Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, Germán Puebla
• Keywords: Homeomorphic Embedding, LOPSTR 2007, Online Partial Evaluation, Partial Evaluation