Equivalence Between HOFL Denotational and Operational Semantics

Abstract

In this chapter we address the correspondence between the operational semantics of HOFL from Chapter 7 and its denotational semantics from Chapter 9. The situation is not as straightforward as for IMP. A first discrepancy between the two semantics is that the operational one evaluates only closed (and typable) terms, while the denotational one can handle terms with variables, thanks to environments. Apart from this minor issue, the key fact is that the canonical forms arising from the operational semantics for terms of type τ are more concrete than the mathematical elements of the corresponding domain (V _τ )_⊥. Thus, it is inevitable that terms with different canonical forms can be assigned the same denotation. However, we show that terms with the same canonical form are always assigned the same denotation. Only for terms of type int do we have a full agreement between the two semantics. On the positive side, a term converges operationally if and only if it converges denotationally. We conclude the chapter by discussing the equivalences over terms induced by the two semantics and by presenting an alternative denotational semantics, called unlifted, which is simpler but less expressive than the one studied in Chapter 9.

Honest disagreement is often a good sign of progress. (Mahatma Gandhi)