From 3bf65269f795b34a34d3b835bd3b64be0964f4c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 10 Sep 2020 01:20:21 +0100 Subject: [PATCH] Rewording --- thesis.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/thesis.tex b/thesis.tex index df170b3..36bc391 100644 --- a/thesis.tex +++ b/thesis.tex @@ -3288,7 +3288,7 @@ If $M \reducesto N$ then $\pcps{M} \reducesto^+ \areducesto^* \pcps{N}$. \paragraph{Plotkin's colon translation} -The defacto standard method for proving the correctness of a CPS +The traditional method for proving the correctness of a CPS translation is by way of a simulation result. Simulation states that every reduction sequence in a given source program is mimicked by its CPS transformation. @@ -3300,10 +3300,10 @@ arise in the source program. \citet{Plotkin75} uses the so-called \emph{colon translation} to overcome static administrative reductions. % -Informally, it is defined such that given a source term $M$ and a -continuation $k$, the term $M : k$ is the result of performing all -static administrative reductions on $\cps{M}\,k$, that is -$\cps{M}\,k \reducesto^\ast M : k$. +Informally, it is defined such that given some source term $M$ and +some continuation $k$, then the term $M : k$ is the result of +performing all static administrative reductions on $\cps{M}\,k$, that +is to say $\cps{M}\,k \areducesto^* M : k$. % Thus this translation makes it possible to bypass administrative reductions and instead focus on the reductions inherited from the