% $Id: reflection_manual.tex,v 1.2 2008/01/25 13:30:19 logik Exp $
\documentclass[a4paper]{amsart}

\newenvironment{code}{\noindent\tt\small\\}{}

\usepackage{xspace}

\input{minlog.mac}

\newcommand*{\prfl}   {\texttt{(prepare-reflection)}\xspace}
\newcommand*{\rfl}    {\texttt{(reflection)}\xspace}
\newcommand*{\rscm}   {\texttt{reflection.scm}\xspace}
\newcommand*{\sr}     {semi-ring\xspace}
\newcommand {\out} [1]{\textrm{\textit{#1}}}
\newcommand*{\Z}      {\ensuremath{\mathbb{Z}}\xspace}

\title{Manual for Reflection}
\author{Klaus Thiel}

\begin{document}

\maketitle

\begin{abstract} Reflection is a simplification procedure for
quantifier free formulae over a \sr with $0$ and $1$ and
decidable equality. Given the goal $G$ reflection produces a new
formula $G'$ and a proof of $G'\to G$ which is then applied to
$G$ thus one is left with the new goal $G'$ which should be
easier to prove.
\end{abstract}

\tableofcontents


\section{Introduction}
\label{sec:introduction}

Let us consider the proof of $\forall
x,y,z\in\Z(x+y+z=z+y+x)$. In order to show this statement by hand
from the \sr-axioms one needs six steps:

\begin{code}
  (sg "int1+int2+int3=int3+int2+int1")\\
  (strip)\\
  (simp "IntPlusCom")\\
  (simp-with "IntPlusComm" (pt "int1") (pt "int2"))\\
  (simp "IntPlusAssoc")\\
  \out{; ?\_5: T}\\
  (use "Truth-Axiom")\\
  \out{; Proof finished.}\\
\end{code}

The amount of steps increases quickly if one deals with more
complex goals. The proof search is not always able to find
a proof:

\begin{code}
  (sg "int1+int2+int3=int3+int2+int1")\\
  (search) \quad \out{; no proof found}\\
  (strip)  \\
  (prop) \quad \out{; Not provable ...}\\
\end{code}

With the reflection procedure one needs only three steps whatever
the goal might be --- provided it is provable from the \sr axioms.

\begin{code}
  (sg "int1+int2+int3=int3+int2+int1") \\
  (strip) \\
  (reflection "int")\\
  \out{; ?\_3: int1+int2+int3=int1+int2+int3}\\
  (use "Truth-Axiom")\\
  \out{; Proof finished.}
\end{code}



\section{How To Use It}
\label{sec:howtouseit}


\rfl is defined in the file \rscm. This file depends on
\texttt{nat.scm}, \texttt{list.scm} and
\texttt{reflection\_thms.scm}.

\rfl can only be applied to a quantifier free goal over some
\sr. But before doing so, we need to prepare the reflection
procedure for which we use the function

\begin{verbatim}
(prepare-reflection
    Ring
    Null Unum
    RingAdd RingTimes
    RingAddAssoc RingAddNeutral RingAddComm
    RingTimesAssoc RingTimesNeutral RingTimesComm
    Distr)
\end{verbatim}

This will generate the proofs and theorems used for the
simplification and its proof. The twelve expected arguments have
to be strings with the following meaning:

\begin{tabular}{@{ \tt}l@{\quad\rm name of }l}
  Ring             & \sr\\
  Null             & neutral element for \texttt{RingAdd}\\
  Unum             & neutral element for \texttt{RingTimes}\\
  RingAdd          & addition\\
  RingTimes        & multiplication\\
  \multicolumn{2}{l}
  {\texttt{RingAddAssoc, RingAddNeutral, RingAddComm}}\\
  \multicolumn{2}{l}
  {\texttt{RingTimesAssoc, RingTimesNeutral, RingTimesComm, Distr}}\\
  & theorem or global assumption\\[1ex]
\end{tabular}

In order to invoke the reflection procedure one uses the command
\verb+(reflection Ring)+ where \verb+Ring+ is a string naming the
\sr to which reflection is applied to.


\subsection*{Example}
\label{ssec:example}

\begin{verbatim}
  (exload "ordinals/reflection.scm")
  (libload "numbers.scm")
  
  (aga "IntPlusAssoc"    (pf "all i,j,j2.i+(j+j2) = (i+j)+j2"))
  (aga "IntPlusNeutral"  (pf "all i.IntZero+i = i"))
  (aga "IntPlusComm"     (pf "all i,j.i+j = j+i"))
  (aga "IntTimesAssoc"   (pf "all i,j,j2.i*(j*j2) = (i*j)*j2"))
  (aga "IntTimesNeutral" (pf "all i. (IntPos One)*i = i"))
  (aga "IntTimesComm"    (pf "all i,j.i*j = j*i"))
  (aga "IntDistr"        (pf "all i,j,j2.i*(j+j2) = (i*j)+(i*j2)"))
  
  (prepare-reflection "int" "IntZero" "IntPos One"
                      "IntPlus"  "IntTimes" 
                      "IntPlusAssoc"  "IntPlusNeutral"  "IntPlusComm"
                      "IntTimesAssoc" "IntTimesNeutral" "IntTimesComm"
                      "IntDistr")

  (sg "i+2+j+2+i*j2+j+j = i*(1+j2)+j*2+4+j")
  (strip)
  (reflection "int")
\end{verbatim}

\out{; ?\_3: 4+i+3*j+i*j2=4+i+3*j+i*j2}

\verb+(use-with "Truth-Axiom")+

\out{; Proof finished}


\section{How Does It Work ?}
\label{sec:howdoesitwork}

Let us assume that we have a goal $G$ over a \sr $R$. The
reflection method simplifies the goal to $G'$,  builds a proof of
$G'\to G$ and applies that proof to $G$ thus we are left with the
new goal $G'$.


\subsection*{Which Goals Can Reflection Be Applied To ?}
\label{ssec:whichgoals}

The goal must be an atomic formula consisting of a binary boolean
valued function applied to two arguments. The general pattern is
$f(t_1,t_2)$ where $f$ is of type $R=>R=>boole$ and $t_1$ and
$t_2$ are terms of type of $R$. Moreover $R$ must be discrete,
e.g. a finitary algebra with boolean valued equality $=$.



\subsection*{How Does Reflection Simplify The Goal ?}
\label{ssec:howsimplify}

The simplification from $G$ to $G'$ is not done within $R$ but on
the meta-level. That is why this method is called
reflection. \prfl introduces an expression algebra named
``ringexpr'', where ring is replaced by the \sr's name. The
algebra has the following constructors:
\begin{center}
\begin{code}
  \begin{tabular}{l@{:}l}
    ringVar   & nat=>ringexpr\\
    ringConst & ring=>ringexpr\\
    ringAdd   & ringexpr=>ringexpr=>ringexpr\\
    ringMult  & ringexpr=>ringexpr=>ringexpr\\
  \end{tabular}
\end{code}
\end{center}

If one applies \rfl to some goal $f(t_1,t_2)$, then the terms
$t_1$ and $t_2$ are reflected into that algebra. The mapping of
\sr-terms into the expression algebra is done by the functions
\texttt{(term-to-linarith-expr-and-env )} and
\texttt{(terms-to-list-term )}.  For example if $t_1$ is a
variable (term in var-form), then it will be assigned the
expression \texttt{ringVar Zero}.

In order to reobtain the corresponding \sr-term from an
expression, one needs to know which number has been assigned to
which variable. Therefore while reflecting $t_1$ and $t_2$ into
the expression algebra a list of \sr-variables called
``environment'' is produced. The $i$\raisebox{1ex}{\tiny th}
variable in the environment has been assigned the expression
\texttt{ringVar i} where $i$ is a numeric term of the algebra
\texttt{nat}.


Syntacticly different terms will be assigned to two different
expressions which are semantically different in the expression
algebra, For example in the case of the \sr \verb+int+:\\

\begin{tabular}{ll}
  Goal & \tt IntPos 2+IntPos 2 = IntPos 2*IntPos 2\\
  lhs  & \tt intAdd(intConst 2)(intConst 2)\\
  rhs  & \tt intMult(intConst 2)(intConst 2)\\
  env  & \tt (Nil int)\\
  \\
  \\
  Goal & \tt i+2+j+2+i*j2+j+j=i*(1+j2)+j*2+4+j\\
\\
  lhs  & \begin{minipage}{1.0\linewidth}\tt
\begin{verbatim}
intAdd
(intAdd
 (intAdd
  (intAdd(intAdd(intAdd(intVar Zero)(intConst 2))(intVar(Succ Zero)))
   (intConst 2))
  (intMult(intVar Zero)(intVar(Succ(Succ Zero)))))
 (intVar(Succ Zero)))
(intVar(Succ Zero))
\end{verbatim}
\end{minipage}\\
\\
  rhs  & \begin{minipage}{1.0\linewidth}\tt
\begin{verbatim}
intAdd
(intAdd
 (intAdd(intMult(intVar Zero)(intAdd(intConst 1)(intVar(Succ(Succ Zero)))))
  (intMult(intVar(Succ Zero))(intConst 2)))
 (intConst 4))
(intVar(Succ Zero))
\end{verbatim}
\end{minipage}\\
\\
  env  & \tt i::j::j2:\\
\end{tabular}

% \begin{code}
% (define two+two "IntPos 2+IntPos 2")\\
% (define two*two "IntPos 2*IntPos 2")\\
% (pp(car\\  \rightline{
% (term-to-linarith-expr-and-env (pt two+two) "int" "IntPlus" "IntTimes")))}\\
% \out{; intAdd(intConst 2)(intConst 2)}\\
% (pp(car\\ \rightline{
% (term-to-linarith-expr-and-env (pt two*two) "int" "IntPlus" "IntTimes")))}\\
% \out{; intMult(intConst 2)(intConst 2)}\\
% \end{code}



\subsection*{What Reflection Cannot Do}
\label{sec:cannot}

\rfl is not a complete decision procedure. It cannot be one
because it is applied to quantifier free formulae with free
variables in the full language of Arithmetic, i.e. including
addition and multiplication. For example \rfl is not able to
solve Fermat's Last Theorem, not even the instance $n=3$. The goal
$k*k*k+m*m*m \neq n*n*n$ is not changed by \rfl does not
normalise to \verb+false+.



% \section{Further Work}
% \label{sec:furtherwork}



\end{document}



%%% Local Variables: 
%%% mode: latex-math
%%% TeX-master: t
%%% End: 
