

\twoslide{Synthesis of the negation of \texttt{linear}}{1/3}
 \bit
\item 
An
expression is {\bf not} linear if there is some function which
either does \emph{not} use its argument or uses it \emph{more than once}.
\item An application is not linear if either the first element
or the second is not linear: no new problems.
\beq
  \neg linapp & : & \neg linear(app\ E_1\ E_2)\\
  & & \qquad \If \neg linear(E_1)\Or \neg linear(E_2).
\eneq
\item A lambda expression is not linear  if it is
not linear in its first argument or
if  its body is not linear:  how to negate a hypothetical and parametric goal?
\enit
\mends

\twoslide{Synthesis of the negation of \texttt{linear}}{2/3}
\bit
\item We mimic a
failure derivation  to provide a  derivation from the
negative definition;  it needs to mirror failure {\bf from} assumptions.
\item Assumption complementation more complicate than static clause
  complementation: not all information is available at
  compile-time.
\item Restriction to parametric assumptions allows to complement
  \emph{around} the parameter, delaying dynamic
  instantiations as constraints .
\item  We synchronize clause, assumption and goal
complementation  (\emph{augmentation}).
\enit
\mends

\twoslide{Synthesis of the negation of \texttt{linear}}{3/3}

  \beq
linxlm& : &linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \top_{linx}\Imp linx (\lx E\ x\ y)).
\eneq
\bit
\item Compute $y\oftp exp\vd\mnota(\top_{linx})=linx(\lx y)$.
\item Augment the clause \texttt{linxlm} with $ y\oftp exp\vd\mnota(\top_{linx}$: 
\beq
\ald(linxlm)& : &linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \fbox{$\neg linx(\lx y)$}\Imp linx (\lx E\ x\ y)).
\eneq 
\item  Negate: \beq
\neg \ald(linxlm)& : &\neg linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ 
y)).  
\eneq 
\enit
\mends
