The Equivalence of Reduction and Translation Semantics of Java Simple Closures

FGCJ is a minimal core calculus that extends Featherweight Generic Java, FGJ, with lambda expressions for Java Simple Closures. It has been introduced to study, in a reduction semantics framework, properties of Java Simple Closures, including type safety and abstraction property. F is a source-to-source, translation rule system from Java 1.5 extended with lambda expressions, back to ordinary Java 1.5. It has been introduced to study, in a translation semantics framework, the design and the implementation features of lambda expressions, including simple closures, this transparency, non local variables and relations with anonymous class objects. In this paper we prove that the reduction semantics and the translation semantics commute in FGACJ. Where FGACJ is a minimal core calculus that extends FGCJ, by adding Java interfaces and anonymous class objects and that allows a restricted definition of translation semantics F.