diff options
| -rw-r--r-- | sec/reducer.ltx | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx index 77b5ce7..2079e49 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -127,13 +127,16 @@ structural induction. \subsection{Encoding Algorithm}% \label{subsec:encoding} -In \cref{M-sec:encoding} we described a process to embed \lang{} +In \cref{M-sec:encoding} we described an algorithm to embed \lang{} within System~T. We have written this algorithm in \lang{} itself, -simultaneously mechanising the conversion and proving it is -terminating. Our input is type-annotated \lang{} terms, and we output -unannotated System~T terms as in \cref{lst:term-ty}. Each phase is -accompanied by its own inductive types representing types and -type-annotated terms. +simultaneously mechanising the conversion and indirectly proving it is +terminating. Our input is a type-annotated \lang{} term, and we output +an unannotated System~T term as in \cref{lst:term-ty}. Each phase is +accompanied by its own inductive types representing the phases' types +and terms. To compute the encoding, any term formers that are not in +System~T must be annotated with their types. For simplicity, our +finite sums and products are over unlabelled lists of types instead of +finite sets. Folds in \lang{} are destructive---the inductive components used to generate the induction hypothesis are unnamed. This has some |