We introduce the Calculus of Delayed Reduction (CDR), that expresses that redexes can only be contracted when brought to the right position in a term, and will show that Call by Name or Value (CBN, CBV) reduction for the lambda calculus can be modelled through reduction in CDR, and that the CBN fragment of the lambdabar-mu-mutilde-calculus can model reduction in CDR. CDR is a Call by Push Value calculus (CBPV) in that it separates terms in computations and values, with their corresponding types. Some simulation results were already achieved by others for CBPV, but only up to equality for CBV; for CBN the results are rather weak.

In order to achieve a single-step reduction respecting mapping for the CBN lambda-calculus, we allow forcing only for variables, thunking only for computations that are not forced variables, and change the nature of term substitution, and abolish the U-reduction rule. We will show that, by changing the standard interpretation, we can achieve a reduction respecting mapping for the CBV lambda-calculus as well. Moreover, these changes make it possible to establish a strong relation between CDR and lambdabar-mu-mutilde, allowing to simulate CDR reduction in lambdabar-mu-mutilde, and preserving assignable types.