\documentclass[landscape]{slides}
\usepackage{latexsym}
% \usepackage{amssymb}
%\usepackage{cdsty}
%\usepackage{prooftree}
\usepackage{amsfonts}
\newcommand{\myslidetitle}[2]{
 \begin{tabbing} {\large #1} \` #2 \end{tabbing}
 \vspace{.1cm} \par          \hrule
 }
\newcommand{\ctr}[1]{\begin{array}[c]{c}#1\end{array}}
\newcommand{\rep}[1]{\ulcorner #1\urcorner}

 \usepackage{fslide-com}

\newcommand{\UImp}{\GImp{u}}
%\newcommand{\ZImp}{\stackrel{\mbox{\tiny  $0$}}{\Imp}}
%\newcommand{\GImp}[1]{\stackrel{\mbox{\tiny  ${#1}$}}{\Imp}}
%\newcommand{\RImp}{\stackrel{\mbox{\tiny  1}}{\Imp}}
\newcommand{\god}{\Gamma; \Omega;\Delta}
\newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}
\newcommand{\etaexp}{\stackrel{\bar\eta}{\longrightarrow}}
\newcommand{\lxua}{\lambda x^{u}\!:\!  A.\, }
\newcommand{\D}{\Delta}
\newcommand{\mmnot}{\mnot}
%\newcommand{\lf}{\l f\! . \, }
%\newcommand{\gdo}{(\GG,\Delta);\Omega;\cdot}
%\newcommand{\ctx}{\GG^{+};\cdot;\cdot}
\renewcommand{\O}{\Omega}
\newcommand{\cM}{{\cal M}}
\newcommand{\yield}{\Rightarrow}
\newcommand{\da}{\downarrow}
\newcommand{\bua}{\Uparrow}
\newcommand{\buda}{\Uparrow\!\downarrow}


\renewcommand{\NF}{\emph{NF\ }}
%\input fpsfonts.def

%
% Normal Width (61)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Extra Width (70)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Small (73)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Small, Extra Width (85)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Height:
%   Normal: 17 or 18 lines?
%   Small: ??

\pagestyle{plain}
\sloppy
\raggedright
\renewcommand{\arraystretch}{1.5}

\begin{document}

 \begin{slide}{}
  \begin{center}
  {\bf The Transformational Approach to Negation\\
 in a Logical Framework} 
\\[1em]
  Alberto Momigliano\\
Carnegie Mellon University\\[1em]
  \end{center}

  \vspace{1em}
  \begin{itemize} \itemsep 0pt
   \item Logical Frameworks
   \item   Negation in a Logical Framework
   \item Modified Closed World Assumption
   \item Term Complement
   \item Future Work
  \end{itemize}
  \vfill
 \end{slide}


%% 1
 \begin{slide}{}
  \slidetitle{Deductive Systems}
 \begin{itemize} \itemsep 0pt
 \item \textbf{Deductive System:} Calculus of axioms and inference
   rules which define derivable judgments. Used in the presentation of
   logics and aspects of programming languages:
 \begin{itemize}
   \item Type systems.
   \item Operational semantics. 
   \item Compilation.
   \item Algorithms (e.g. type inference, unification, theorem proving).
  \end{itemize}
\enit
\mends
 \begin{slide}{}
  \slidetitle{Logical Frameworks}
\bit
 \item \textbf{Logical Framework:} Meta-language for the
   specification, implementation and verification of (the meta-theory 
   of) deductive systems. Applications as a teaching and research tool include:
  \begin{itemize}
   \item Reasoning {\bf within} a specified system (operational
     semantics of Mini-ML).
   \item Implementation of algorithms (evaluation, type inference).
   \item Reasoning {\bf about\/} a deductive system (proof of type
     preservation).
  \end{itemize}
\end{itemize}
  \vfill
 \end{slide}

%%2
\begin{slide}{}
 \slidetitle{Systems}

\bit
\item \textbf{Formalism:} hereditary Harrop formulae (HHF),
  dependently typed $\l$-calculi, labeled deductive systems, inductive definitions, rewrite
  logics.
%\item \textbf{Languages:} functional (ML, rewriting), relational
%  ($\l$Prolog, Elf).
\item \textbf{Environments:} interactive theorem proving vs.\ \lp and
  proof-checkers. 
\item \textbf{Implementations:} Isabelle, $\l$Prolog, Elf,   Maude,
  Pi\dots
%\item \textbf{General Systems:} HOL, Coq, Lego\dots
\item \textbf{Applications:} Mobile Code Security (Proof-Carrying Code) and
 Certifying Compilation (Necula),
  Protocol Security Verification (Paulson)\dots
\enit
%\end{small}
\end{slide}

%% 3
\begin{slide}
\slidetitle{Logical Framework's Design}
\bit
\item Logical frameworks are \textbf{weak} by design to facilitate:
\bit
\item Informal proofs of adequacy of representation.
\item Effective checking of the validity of
derivations.
\item Proof-search and unification.
\item Efficient implementations.
\enit
\item \textbf{Extending} a logical framework: balance benefits against
  complications in its  meta-theory.
\item Extensions: subtyping,  modularity, equational
  reasoning, linearity\dots What about having negation?
\enit\mends
%\newcommand{\Bimp}{\leftrightarrow}


%% 4
\twoslide{Our Contribution: Adding Negation}{1/2}

In specifications, \emph{negation} is often used.
\bit
\item In Prolog,  obtain  $odd(n) \mbox{  from  } \neg even(n)$.
\item Two elements are \textbf{different}, an element is
  \textbf{not} a   member of a list.
\item Type inference: an expression is \textbf{not} well-typed.
\item Functional program analysis: a function is \textbf{not} linear.
\item Operational semantics: an expression is \textbf{not}  a value.
\item Algorithmic subtyping: a sort is \textbf{not} a subsort (of another).
\enit
\mends

%% 5
\twoslide{Our Contribution: Adding Negation}{2/2}
\bit
\item Lf's with logic programming interpretation have no negation operator.
\item Need to explicitly program the negative code (tedious and error-prone).
\item Need to \textbf{prove} that this code implements the
  negation of the intended predicate.
\item \textbf{Our result:} automation of  this synthesis of negative 
information.
\item \textbf{Benefits:} a sound negation operator allows us to implement
  topics  too unwieldy to deal with otherwise.
\enit
\mends


%% 6
\twoslide{Negation-as-Failure: Horn case}{1/3}
\bit

\item 
\NF is the usual answer in logical programming: 
\begin{center}$\cP$ infers $\neg A$
if  $A$ finitely fails from $\cP$\end{center}
\item Not declarative, but easy to implement.
\item Possibly unsound and generally incomplete: semantics?
\item \textbf{Closed World Assumption:}   Horn Logic $\sim$ inductive
  definitions:  everything
which is not provable from a program is assumed to be false.
\item Allowing negation in clauses spoils their inductive nature.

\enit
\mends

%% 10
\twoslide{Negation-as-Failure: Lf's case}{2/3}
\bit
\item Even in a well-behaved fragment, \NF in the meta-language makes
  adequacy theorems too complicated (provability and
  unprovability).

\item Lf's 
 not  inductive definitions, because of  embedded implication and universal quantifiers:
\beq
Q\If (D\Imp G)\\
Q\If \PI{x}{A} G
\eneq
\item \textbf{Open World  Assumption:}  programs and signature are
  open-ended.
\item \NF and embedded implication is particularly problematic (Gabbay
  [1985]): failure of cut-elimination.
\enit\mends
\twoslide{Between CWA and OWA}{}
\bit
\item Intrinsic tension between CWA and OWA.
\item 
Both assumptions represent  too extreme poles.
\item
Is there is a middle ground where
  negation is meaningful?
\item We need to identify a class of ``possible worlds'' which are stable under
extensions of the program and signature.
\enit
\mends
\twoslide{ Related Work}{}
\bit
\item  Strict distinction between CWA and OWA predicates;
  \NF for the former,   minimal negation  for the latter (Harland [1991]).
\item A modal approach to account \textbf{arbitrary extensions} of the program as possible
  worlds (Olivetti \& Giordano [1998] for N-Prolog, Bonner [1994]    
 for Hypothetical Datalog).
\item Embrace partiality of  inductive definitions and use \emph{definitional
    reflection} to obtain   closure  (Schroeder-Heister [1994],
  McDowell\& Miller [1997]).
\item Unsatisfactory: need to negate OWA predicates, while not
  extending the language; PID's technically inadequate for Lf's.
\enit
\mends
%% 8
\twoslide{Transforming Negation}{1/3}
\bit
\item Our approach is   \textbf{transformational} 
(Sato \& Tamaki [1984] Barbuti et al. [1990] for Horn
logic and  to CLP's [1994]):

%\begin{tabbing}
\qquad Given a clause $Q\If G, \neg p, G'$\\
\qquad a definition of $p$\\
\qquad \textbf{synthesize} a positive definition
of $non\_p$, such that\vsk
%\end{tabbing}
%\begin{center}
\qquad\qquad\qquad\qquad $\nvd  p \mbox{  iff  }  \vd non\_p$\vsk
%$\end{center}
%\begin{tabbing}
\qquad Replace $non\_p$ in  $p$: $Q\If G, non\_p, G'$
%\end{tabbing}
\item Technically:
\bit
\item Bring the  program  in negation normal form.
\item Need an algorithm to complement terms (Lassez [1987]) to negate atoms.
\enit
%\item Give an operational interpretation to \emph{local} variables.
\enit 
\mends

%% 9 
\twoslide{Transforming Negation: Benefits}{2/3}
\bit
\item Compile-rime source-to-source transformation.
\item No need to extend the language;
  negative information are `positivized'. 
\item No new  semantics problems, no floundering, no
  incompleteness.
\item  Proof terms provide evidence for negative information.
\item Adequacy theorem(s) unalterated. 
 \enit \mends

  \twoslide{Transforming Negation: Problems}{3/3} \bit
\item Unfortunately, elimination of negation does not scale
  immediately to a logical framework as HHF:
\begin{itemize}
\item Same friction  between \textbf{Closed} and \textbf{Open} World
  Assumption.
 \item Negation normal forms are incompatible with the (constructive)
   operational   semantics associated to HHF.
\item HHF terms language based on the simply-typed $\l$-calculus,
which is  \textbf{not} closed under term  complement.
\end{itemize}
\enit
\mends


%% 11
\twoslide{Our Solution: Modified CWA}{1/2}
\bit
\item \textbf{Modified CWA:} restrict to programs whose dynamic
  assumptions extend the current database in a \textbf{regular} way,
  so that static and dynamic clauses never \textbf{overlap}.
\item Observation: in Lf's embedded implications 
%(and \ho abstract  syntax) 
represent \textbf{scoping constructs}, such as abstractions,
  quantifiers and rules with hypothetical premises.
\item Implications paired with intensional universal quantifier to
  express the parametricity of the assumption.
\item The eigenvariable condition ensures no overlap. %with static program
\item A program is \textbf{deniable} if every
  assumption is parametric.

\enit
\mends
%% 12
\twoslide{Modified CWA}{2/2}
\bit
\item Example: checking whether a $\l$-term is \texttt{closed}:
\[\begin{array}{l}
\PI{E}{exp}closed(lam\ E) \If \PI {x } {exp}\ closed( x) 
\Imp closed(E\ x).\\
\PI{ E_{1}}{exp}\PI{E_{2}}{exp} closed (app\ E_{1} \ E_{2}) \If 
closed( E_1) \And closed( E_{2}).
\end{array}\]
%\item Simple way to ensure no overlap between dynamic and static
%  clauses.
\item Not allowed: encoding of implication introduction in natural deduction:
\[\begin{array}{l}
 nd(A\ imp\ B)\If (nd(A) \Imp nd(B)).
\end{array}\]
\item If implication is not parametric, need to explicitly manage assumptions
 as lists (see McDowell\&  Miller [1997]).
\item Our restriction has shown to be both elegant and pragmatically
  adequate (and conservative \wrt Horn logic).
\enit
\mends
%% 13
\begin{slide}
\slidetitle{Negation Normal Forms}
\bit
\item Operational semantics of embedded implication is intuitionistic.
\item No negation normal forms available in intuitionistic logic.
\item Strong negation normal form (Nelson [1949]) incompatible with
  semantic of failure:
\beq
\neg (D\Imp G) & = & D\Imp \neg G
\eneq
\item Valid for \textbf{deniable} programs.
\enit
\mends
\begin{slide}
\myslidetitle{Term Complement}{1/2}
\bit
\item $\l x\ldot x$ is an instance of $\lambda x\ldot E\ x$ 
% matches any term
%of appropriate type; 
\item $\l x\ldot y$ in an instance of $\lambda x\ldot E$,
where $E$ does not \textbf{depend} on $x$. 
% matches only closed
\item The complement of $\lambda x\ldot E$ is the set of all terms 
 that \textbf{does} depend on $x$.
\item The simply typed $\l$-calculus theory is not strong enough to
  directly represent the complement of partially applied patterns.
\item We need to have a notion of \textbf{strictness} in the language to
  express variable occurrence constraints.
\enit
\mends
% 13
\begin{slide}
\myslidetitle{Term Complement}{2/2}
\bit
 
\item We \textbf{internalize} strictness as a type system, 
generalizing the language of simple types to include: 
\bit
\item \textbf{strict functions} of type $A \RImp B$, 
  guaranteed to depend on their argument
\item \textbf{invariant functions} of type $A \ZImp B$,
  guaranteed \textbf{not} to depend on their argument
\item the uncommitted function space $A \UImp B$.
 \enit
\item We embed the simply-typed calculus.
\item In this system we can perform \textbf{any} boolean operation on finite sets of patterns (unification as intersection).
 \enit \mends


%% 14
\begin{slide}{}
 \slidetitle{Conclusions}
 \bit
\item Negation is useful in Lf's, but it is difficult to allow.
\item We have approached  the problem of negation by source-to-source 
\textbf{transformation}.
\item We have found a middle ground between CWA and OWA. 
\item We have isolated a significant fragment of HHF, where program
  negation is possible.
\item We have formulated a strict $\l$-calculus, which gives an
  independent contribution to the understanding of sub-structural
  calculi.


\enit\mends
%% 15
  \begin{slide}{}
  \slidetitle{Future work}
  \bit
\item Lift some of the current restrictions (no local variables),
related to question of extensionality in Lf's.

\item Extend to  dependently typed $\l$-calculi.


\item Implement this pre-compiler to languages as $\lambda$Prolog,
  Elf, and possibly to general purpose systems such as Isabelle.
\item Investigate the transformational approach to  negation in
  substrucural calculi and languages (Lolli, Forum, Linear LF).
 \enit
 \mends
\end{document}


