From 4353f331b5ab4af157f576f54b1cc79dd08abb12 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 23 Apr 2025 15:59:22 +0100
Subject: Current state of affairs.

---
 sec/reducer.ltx | 35 +++++++++++++++++++++++++++++------
 1 file changed, 29 insertions(+), 6 deletions(-)

(limited to 'sec/reducer.ltx')

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}
 }
 
-- 
cgit v1.2.3