Title:   Reflections on Reflections
Authors: Gilles Barthe, John Hatcliff, Morten Heine Soerensen
Source:  PLILP'97

In the functional programming literature, compiling is often expressed
as a translation between source and target program calculi.  In recent
work, Sabry and Wadler proposed the notion of a "reflection" as
"the appropriate relation between the source and target calculi".  A
reflection elegantly describes the situation where there is a kernel
of the source language that is isomorphic to the target language.
However, we believe that the reflection criteria is so strong that it
often excludes the usual situation in compiling where one is compiling
from a higher-level to a lower-level language.

We give a detailed analysis of several translations commonly used in
compiling that fail to be reflections.  Our broad conclusion is that
there is not necessarily a single relation between source and target
calculi that is most appropriate.  Rather, there are several
relations weaker than reflections that characterize many rigorously
justified translations appearing the the literature.  We give a framework
for describing these alternative relations.