twice). This is discussed in more detail in
\in{section}[sec:normalization:duplicatework].
- \subsubsection{Literals}
+ \subsubsection[sec:normalization:literals]{Literals}
There are a limited number of literals available in Haskell and Core.
\refdef{enumerated types} When using (enumerating) algebraic
data-types, a literal is just a reference to the corresponding data
{\lam{\forall A, B, C \exists D (A ->> B ∧ A ->> C => B ->> D ∧ C ->> D)}}
Here, \lam{A ->> B} means \lam{A} \emph{reduces to} \lam{B}. In
- other words, there is a set of transformations that can be applied
- to transform \lam{A} to \lam{B}. \lam{=>} is used to mean
- \emph{implies}.
+ other words, there is a set of transformations that can transform
+ \lam{A} to \lam{B}. \lam{=>} is used to mean \emph{implies}.
For a transformation system holding the Church-Rosser property, it
is easy to show that it is in fact deterministic. Showing that this