summaryrefslogtreecommitdiff
path: root/sec/reducer.ltx
diff options
context:
space:
mode:
Diffstat (limited to 'sec/reducer.ltx')
-rw-r--r--sec/reducer.ltx35
1 files changed, 29 insertions, 6 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 8cd19f0..d48e600 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -1,16 +1,39 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
-\section{Fuelled Self-Reducer for System T}%
+\section{Writing ARTiST Programs}%
\label{sec:reducer}
\TODO{
\begin{itemize}
- \item fuelled self-reducer
- \item high-level strategy
- \item example: case distinction
- \item qualitative comparison
- \item quantitative comparison (dLoC)
+ \item state I have written two non-trivial programs in ARTiST
+ \item briefly describe the fuelled reducer and encoder
+ \item describe the syntactic sugar I have added
+ \end{itemize}
+}
+
+\TODO{
+ \begin{itemize}
+ \item describe the operation of the fuelled reducer
+ \item explain why fuel is necessary for the reducer
+ \item show some example snippets
+ \end{itemize}
+}
+
+\TODO{
+ \begin{itemize}
+ \item describe the inputs to the embedding
+ \item describe the output of the embedding
+ \item show a ``non-destructive'' fold
+ \item justify use of destructive folds
+ \end{itemize}
+}
+
+\TODO{
+ \begin{itemize}
+ \item describe why encoded terms have lots of beta redices
+ \item describe potential benefit of composing two programs
+ \item explain the limitiations of the reducer (e.g. eta and bools)
\end{itemize}
}