organization.tex

Organizational approach #4--emphasis on applications

Each chapter has 6 sections:

a. discuss the program we wish to derive for equations, purify from Prolog, or translate from Scheme
b. give background on theorem proving, half-adders, type inference
c. examine and discuss the obstacles that make this awkward or impossible, given the techniques we've see so far [alternatively, obstacles could be addressed as they come up]
d. perform the derivation/purification/translation, discussing the obstacles and techniques in detail as we encounter them
e. show off the resulting relation with lots of interesting example programs
f. provide the implementation(s) of related language constructs

A catalog of the techniques could then be presented as Appendix A.

Basic idea of this organizational approach: can't discuss obstacles and techniques without looking at a specific application.

Techniques section?

\chapter{}
\section{Application}
binary arithmetic system
\section{Background}
computer architecture: half adders, full adders, etc
\section{Obstacles}
divergence
\section{Derivation/Purfication/Translation}
\section{Examples}
\section{Implementing Related Language Constructs}
vanilla miniKanren, without constraints (or pehaps this implementation was given even before the first application)

\chapter{}
\section{Application}
type Inferencer
\section{Background}
type inference for extended lambda calculus 
\section{Obstacles}
\section{Derivation/Purfication/Translation}
\section{Examples}
type inference, type checking, type inhabitation
\section{Implementing Related Language Constructs}
nominal logic/alphaKanren

\chapter{}
\section{Application}
theorem prover
\section{Background}
\section{Obstacles}
\section{Derivation/Purfication/Translation}
\section{Examples}
\section{Implementing Related Language Constructs}

\chapter{}
\section{Application}
interpreter and/or PLT-style reduction system
\section{Background}
\section{Obstacles}
\section{Derivation/Purfication/Translation}
\section{Examples}
\section{Implementing Related Language Constructs}
tabling (assuming the tabling actually stops divergence the way I think it does)

\chapter{}
\section{Application}
\section{Background}
\section{Obstacles}
\section{Derivation/Purfication/Translation}
\section{Examples}
\section{Implementing Related Language Constructs}

\chapter{}
\section{Application}
\section{Background}
\section{Obstacles}
\section{Derivation/Purfication/Translation}
\section{Examples}
\section{Implementing Related Language Constructs}

\chapter{}
\section{Application}
\section{Background}
\section{Obstacles}
\section{Derivation/Purfication/Translation}
\section{Examples}
\section{Implementing Related Language Constructs}