RS-2 Tagging, Encoding, and Jones Optimality

Authors

  • Olivier Danvy
  • Pablo E. Martínez López

DOI:

https://doi.org/10.7146/brics.v10i2.21773

Abstract

A partial evaluator is said to be Jones-optimal if the result of specializing a self-interpreter with respect to a source program is textually identical to the source program, modulo renaming. Jones optimality has already been obtained if the self-interpreter is untyped. If the self-interpreter is typed, however, residual programs are cluttered with type tags. To obtain the original source program, these tags must be removed.

A number of sophisticated solutions have already been proposed. We observe, however, that with a simple representation shift, ordinary partial evaluation is already Jones-optimal, modulo an encoding. The representation shift amounts to reading the type tags as constructors for higher-order abstract syntax. We substantiate our observation by considering a typed self-interpreter whose input syntax is higher-order. Specializing this interpreter with respect to a source program yields a residual program that is textually identical to the source program, modulo renaming.

Downloads

Published

2003-01-06

How to Cite

Danvy, O., & López, P. E. M. (2003). RS-2 Tagging, Encoding, and Jones Optimality. BRICS Report Series, 10(2). https://doi.org/10.7146/brics.v10i2.21773