\documentclass[landscape]{slides}
\usepackage{latexsym}
% \usepackage{amssymb}
%\usepackage{fpslides}
%\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{\exa}{\exists x\!:\!A.\,}
 \newcommand{\lin}{\mbox{ linear}}
\newcommand{\linx}{\mbox{ linear in }x }
\renewcommand{\lx}{\Lambda x \,.\, }
\renewcommand{\ly}{\Lambda y \,.\,}
\newcommand{\bca}{\[\begin{array}{c}}
\newcommand{\eca}{\end{array}\]}

\newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}


\newcommand{\D}{\Delta}
%\newcommand{\lf}{\l f\! . \, }
%\newcommand{\gdo}{(\GG,\Delta);\Omega;\cdot}
%\newcommand{\ctx}{\GG^{+};\cdot;\cdot}
\renewcommand{\O}{\Omega}




%\newcommand{\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 Elimination of Negation in a Logical Framework} \\[1em]
%   Alberto Momigliano\\
% Department of Math and Computer Science\\
% University of Leicester\\
% Leicester, UK\vsk\mbox{}
% \date{August, 25 2000}\vsk
%  \emph{CSL2000} \\[1cm]
% %   \textbf{Thesis Committee:} \\
% %   Frank Pfenning, Chair \\
% %   Dana Scott \\
% %   Dale Miller, Pennsylvania State University 
%   \end{center}

\title{The Transformational Approach to  Negation in a Logical Framework}
\author{Alberto Momigliano\\
 Department of Mathematics and Computer Science\\
 University of Leicester}
\date{\today}
\maketitle
%\vfill
%\end{slide}

\begin{slide}
\slidetitle{Outline}
  \begin{enumerate} \itemsep 0pt
  \item Complementing (Partial) Inductive Definitions
   \item Logical Frameworks
   \item  Adding Negation
     \item Negation-as-Failure vs.\ Transformation of Negation
%\item Elimination of Negation in a Logical Framework
 %       \ben
   \item Clause and Term Complement
%   \item Term Complement \enen
   \item Conclusions and Future Work
  \end{enumerate}
  \vfill
 \end{slide}

\newcommand{\cU}{{\cal U}}
\twoslide{The Issue (in set-theoretic terms)}{}
\bit
\item Take a \textbf{rule set} $\Phi$ ([Aczel' 77]), \ie a possibly
  infinite set of pairs $\la X,x\ra$ (notation: $x\If X$) on an universe $\cal U$, such
  that $x\in\cU, X\subseteq 2^{\cU}$.
\item Let $Id(\Phi)$ the set \emph{inductively defined} by $\Phi$
  (intersection of all $\Phi$-closed subset of $\cU$).
\item Consider its set-theoretic complement $\cU\setminus Id(\Phi)$:
\begin{quote}
\emph{Can it be expressed as an inductively defined set as well?}
\end{quote}
\item Construct a rule set $\Psi$ such that 
\beq Id(\Psi)&=& \cU\setminus
  Id(\Phi)\eneq \enit \mends

\twoslide{Example}{}
\bit
\item Take the type of  numerals and the following rule set
  (\emph{even} numbers):
\beq
\ianc{\emptyset}{zero}{}\qquad\ianc{\{zero\}}{suc(suc\
  zero)}{}\qquad\cdots\ianc{\{N\}}{suc(suc\ N)}{}\cdots
\eneq
\item Its complement (in that type) are the \emph{odd} numbers:
\beq
\ianc{\emptyset}{suc(zero)}{}\qquad\ianc{\{suc(zero)\}}{suc(suc(suc\
  zero))}{}\qquad\cdots\ianc{\{N\}}{suc(suc\ N)}{}\cdots
\eneq
\item The logical view: finitary version of a rule set are a
  conjunction of Horn clauses:
\beq
even(zero)\And
\PI{N}{nat} even(suc(suc(N))\If even(N)
\eneq
\enit
\mends
\twoslide{Complement of Id = Negation of LP} {}
\bit
\item Complementing an inductive definition is equivalent to
  \textbf{negate} a \emph{logic} program:
\beq
odd(suc(zero))\And
\PI{N}{nat} odd(suc(suc(N)))\If odd(N).
\eneq
\item More interestingly: \textbf{Partial} Inductive Definitions
  [Halln\"as'91]: $ x\If (C\Rightarrow X)$.
\item The \emph{definiens} $X$ may depend on some (possibly
  defined) \emph{condition} $C$.
\item In general, they do not yield monotone inductive operators.
\item Logically speaking, they correspond to \emph{higher-order} rules
  or \emph{hypothetical judgments}  (Martin-L\"of).
\enit\mends

\twoslide{PID's Example: Judgment `$e$ linear'}{}

\bca
%\phj{x\lin}{u}{ x \lin}{\linear\atm}\qquad
\ibnc{ \begin{array}{c}\vsk \lx e\linx\end{array}}{\begin{array}{c}
                        \ianc{}{x\lin}{u}\\
                         \vdots\\
                        e\lin\end{array}}
                         {\lx e\lin}{linlam^{x,u}}
\vsk
\ibnc{ e_1 \lin}{e_2\lin}{  (e_1\ e_2) \lin}{linapp}
\vsk\vsk
\ianc{}{  \lx x\linx}{ linxx}
\qquad
\ianc{ \lx e\linx}{ \lx \ly e\linx}{ linxlm^y}
\vsk 
\ianc{  \lx e_1\linx}{ \lx (e_1 \ e_2)\linx}{linxap_1 } 
\qquad
\ianc{  \lx e_2\linx}{ \lx (e_1 \ e_2)\linx}{ linxap_2} 
\eca

\mends
%\input{abc}
%\input{ex}

\renewcommand{\ly}{\lambda  y\,.\,} 
\renewcommand{\lx}{\lambda  x\,.\,} 
\newcommand{\sn}{\ol{s_n}}
% \begin{slide}{}
% \begin{center}
% \fbox{1. Logical frameworks:}
% \\[1em]
% A brief summary of their features and use.
% \end{center}
% \mends
 \begin{slide}{}
  \slidetitle{Deductive Systems}
 \begin{itemize} \itemsep 0pt
 \item Call a (partial) inductive definition a \textbf{Deductive
     System.}
 \item  Calculus of axioms and inference rules which define
   derivable judgments. Used in the presentation of logics and
   aspects of programming languages such as:
 \begin{itemize}
   \item Type systems.
   \item Operational semantics. 
   \item Abstract machines and 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 Implementation of algorithms (evaluation, type inference). 
  \item Reasoning {\bf within} a specified system (operational
     semantics of Mini-ML).
   \item Reasoning {\bf about\/} a deductive system (proof of type
     preservation).
  \end{itemize}
\enit
\mends
\begin{slide}{}
  \slidetitle{Brief History, I}
  \begin{itemize}
   \item Automath [de Bruijn'68]
   \item Theory of Judgments [Martin-L\"of'85]
   \item (Edinburgh) Logical Framework 
    [Harper, Honsell \& Plotkin'87] ,
    Elf [Pfenning'89,91]
   \item Hereditary Harrop Formulas,
    [Nadathur, Miller, \& Scedrov'87] [Paulson'87] \\
    $\lambda$Prolog [Nadathur \& Miller'88],
    Isabelle [Paulson'89]
\item We work in a fragment of HHF ($\lambda$Prolog), but our
  design decisions are influenced by LF (\emph{Twelf\/}).
  \end{itemize}
  \vfill
 \end{slide}
\begin{slide}{}
  \slidetitle{Brief History, II}
 \begin{itemize}
  \item Inductive definitions / FS0 [Feferman'87]
  \item Inductive type theory / ALF [Coquand, Magnusson, Nordstr\"om'91]
  \item Partial inductive definitions/Pi [Halln\"as'91] [Eriksson'93]
  \item Labeled deductive systems [Gabbay'89]
  \item Sub-structural frameworks [Schroeder-Heister'91] [Girard'93] [Miller'94]
  \item Equational frameworks [Mart\`{\i}-Oliet \& Meseguer'93] [C.~Kirchner,
H.~Kirchner \& Vittek'93]
 \end{itemize}
  \vfill
 \end{slide}

 \begin{slide}{}
  \slidetitle{Brief History, III}
 General systems for constructive mathematics have also been used
as logical frameworks.  For example:
  \begin{itemize}
   \item NQTHM (Boyer-Moore) [Shankar'86]
   \item Otter (Lusk-Overbeek) [Wos'88]
   \item Nuprl (Constable et al.)  [Basin \& Constable'91]
   \item Coq (Huet et al.) [Huet'93]
   \item LEGO [Pollack'93]
  \end{itemize}
  \vfill
 \end{slide}
%%2
% \begin{slide}{}
%  \slidetitle{Systems}

% \bit
% \item \textbf{Formalism:} hereditary Harrop formulae (HHF),
%   dependently typed $\l$-calculi, labelled 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}
\twoslide{Hereditarely Harrop Formulae}{}
\bit
\item A fragment of Church's theory of simple types:

\[ \begin{array}{rrcl}
 \mbox{\textit{Simple Types}} & A & \bnfas & a \bnfalt A_1 \Imp A_2 \\
 \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam x\oftp
A\ldot M \bnfalt M_1\ M_2 \\
\mbox{\textit{Atoms}}& Q & \bnfas & q\ \vM \bnfalt \neg q\ \vM \\
\mbox{\textit{Goals}}& G & \bnfas & Q \bnfalt \top\bnfalt \perp\bnfalt\\
%\vM \eqd \vN\bnfalt \vM \neqd \vN\bnfalt\\
& & & G_{1}\And G_{2}\bnfalt
G_{1}\Or G_{2}\bnfalt D\Imp G\bnfalt\PI{x}{A} G\bnfalt\exa G\\
\mbox{\textit{Clauses}}& D & \bnfas & \top\bnfalt\perp\bnfalt Q\bnfalt D \If
G\bnfalt D_{1}\And D_{2}\bnfalt D_{1}\Or D_{2}\bnfalt\PI{x}{A} D
\end{array}
\]
\item Can be given a \lp interpretation ($\l$Prolog) in terms of
  \emph{sequent-style uniform proofs}: every non-atomic derivation
  ends in a right introduction rule.
\enit\mends
%% 3
\begin{slide}{}
  \slidetitle{Framework Design Goals}
 \begin{itemize} \itemsep 0pt
  \item Simple and uniform, concise
  \item Close to (good) informal practice
  \item Efficiently implementable
  \item Support for search and meta-programming
  \item Decide validity of derivations
  \item Feasibility of proving correctness of representations
  \item Means for structuring large specifications
 \end{itemize}
  \vfill
 \end{slide}
\begin{slide}
\slidetitle{Logical Framework Extension}
\bit
\item \textbf{Extending} a logical framework: need tools to make
  specifications concise, but balance benefits against complications
  in its meta-theory.
\item Conservative extensions (of HHF and LF): ``pay as you go''. 
\bit
\item sub-typing [Pfenning 93],  modularity [Harper\&Pfenning 98], equational
  reasoning and constraints [Virga  99], linearity [Cervesato 95,
  Miller\&Hodas 94]
\item  What about having negation?
\enit
\enit\mends
%\newcommand{\Bimp}{\leftrightarrow}
% \begin{slide}{}
% \begin{center}
% \fbox{2. Adding Negation:}
% \\[1em]
% Why negation is a useful notion in specifications.
% \end{center}
% \mends
% %% 4
\twoslide{Negation in Specification: Examples}{1/2}
\bit
% \item 
% In specifications, \emph{negation} is often used:
\item Formal definition of a programming language in the style of
  natural semantics: Progress lemma (well-typed expressions cannot go
  wrong):
\begin{center}If  $e\hastype\tau$ and $e$ is
\textbf{not} a value, there exists  $e'$ such that
$e\mapsto e'$
\end{center}
\item Process algebra: \emph{safety} in an algorithm for mutual
  exclusion: for any transition, if the initial state is \emph{safe},
  so is the final one. 
 \bit
\item
A state is {\em safe} if (all) processes are
\textbf{not} in their critical section at the same time.
\enit
\enit
\mends
\twoslide{Negation in Specification: Examples}{2/2}
\bit
\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}  in normal form.
\item Algorithmic sub-typing: a sort is \textbf{not} a sub-sort (of another).
\item Prolog style predicates: two atoms are \textbf{different}, an element is
  \textbf{not} a   member of a list.
%\item Determinacy of rules application: a declarative
%  \texttt{if-then-else} statement. 
 \enit \mends

%% 5
\twoslide{Negation in Logical Frameworks}{}
\bit
\item Logical frameworks with logic programming interpretation have no (declarative)
  negation operator, to preserve goal-oriented proof search.
\item Need to explicitly program the negative code: for example,
  define \texttt{non-value(e)}.  Tedious and error-prone,
  non-monotonic \wrt specifications evolution.
\item Need to {prove} (informally) that this code implements the
  negation of the intended predicate.
\item \textbf{Our contribution:} automation of  this synthesis of negative 
information, proven correct once and for all.
% \item \textbf{Benefits:} a sound negation operator allows us to implement
%   topics  too unwieldy to deal with by direct coding.
\enit
\mends
% \begin{slide}{}
% \begin{center}
% \fbox{3.   Negation-as-Failure vs.\ Elimination of  Negation:}

% \bit
% \item Problems with \NF
% \item Elimination of  Negation in the Horn case
% \item Benefits of Elimination of  Negation
% \enit
% \end{center}
% \mends
%% 6
\twoslide{Negation-as-Failure: Horn case}{1/2}
\bit
\item \NF (Clark [1978]) is the usual answer in
  LP:
\begin{center}$\cP$ infers $\neg A$
  if $A$ finitely fails from $\cP$\end{center}
\item Not declarative, but easy to implement (no change to the \lp
  interpreter).
\item Possibly unsound and generally incomplete: semantics?
\item \textbf{Closed World Assumption:} Horn Logic $\sim$ inductive
  definitions: what is not provable is assumed to be false.
\item Allowing negation in clauses may spoil their (monotone)
  inductive nature.
\enit
\mends

%% 10
\twoslide{Negation-as-Failure: Logical Frameworks}{2/2}
\bit
\item Even in a well-behaved fragment, \NF in a logical framework
  makes the meta-theory much harder (provability and unprovability).
\item Logical frameworks such as HHF cannot in general be seen as
  \emph{total} inductive definitions, because they allow hypothetical
  and parametric judgments:
%embedded implication  and universal quantifiers in goals: 
\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 with hypothetical judgment 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.
% \item \emph{Regular World Assumption:} extensions are enforced to be regular.
% \enit
% \mends

%%%%%%%%% KEEP %%%%%%%%%%%%
% \twoslide{Related Work: \NF \& Logical Frameworks}{}
% \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 (PID) and use
%   \emph{definitional reflection} to obtain (some form of) closure
%   (Schroeder-Heister [1994]).
% \item Unsatisfactory (for our needs): need to negate OWA predicates,
%   while not extending the language; PID's technically inadequate for
%   logical frameworks.  \enit \mends
%% 8
\twoslide{Eliminating Negation}{1/4}
\bit
\item Our approach is \textbf{transformational} (Sato \& Tamaki [1984]
  Barbuti et al. [1990] for \fo Horn logic and CLP's): 
\bit
\item Given a clause $Q\If G\And \fbox{$\neg p(\tn)$}\And G'$
\item a (positive) definition of $p$
\item[$\yield$] \textbf{synthesize} a \textbf{positive} definition of $non\_p$,
  such that for all (closed) terms $\sn$:
\beq
\nvd  p(\sn) &\mbox{iff}&  \vd non\_p(\sn)
\eneq
\enit
\item By replacing $\neg p$ with $non\_p$, obtain the
  \textbf{negation-less} clause: $$Q\If G\And \fbox{$non\_p(\tn)$}\And G'$$
\enit \mends
\twoslide{Eliminating Negation: Benefits}{2/4}
\bit
\item Compile-time source-to-source transformation: no run-time overhead.
\item No need to extend the language; meta-theory unaltered, since
  negative information are `positivized'. 
\item No new  semantics problems, no
  incompleteness.
\item  Proof terms provide evidence for (positivized) negative information.
\item User level: adequacy theorems unaltered. 
 \enit \mends

\twoslide{Eliminating Negation: Techniques}{3/4}
\bit
\item Take the \emph{iff-completion} of a program.
\item Negate both sides and via  classical transformation bring
  the body to negation normal form.
% \[
% \begin{array}{l}
% \forall x\, . \, even(x) \Bimp x = 0 \Or \exists y \, . \, 
% x =s(s(y)) \And even(y)\leadsto\\
% \quad\forall x\, . \, \neg even(x) \Bimp x \neq 0 \And \forall y \, . \, x  
% \neq s(s(y)) \Or (\exists y\, . \,  x =s(s(y))  \And \neg even(y))
% \end{array}\]
\item Use an algorithm to complement \fo terms  to extract positive
  information from dis-equations. 
\item Example: the negation of \texttt{p(s(0))}
\ben

\item $p(x) \Bimp x = s(0)$
\item $\neg p(x) \Bimp x \not= s(0)$
\item $\neg p(x) \Bimp x=0\Or\exists y:x=s(s(y))$

\enen
\enit 
\mends

%\twoslide{Eliminating Negation}{1/3bis}
% \twoslide{A Simple Example: from \texttt{even} to \texttt{odd}}{1/2}
% \bit
% \item Even numbers: 



% \item The complement:
% \beq
% \lefteqn{\mnotd(even(0)\And
% \PI{Y}{nat}even(s(s(Y))) \If even(Y))=}\\
%  &&\mnotd(even(0))\Or \mnotd( \PI{Y}{nat}even(s(s(Y))) \If even(Y))
% \eneq

% \item Compute complement of  an atom by computing the complement of the term 
% ($\mnot(0)$):
% \beq
% \mnotd(even(0))=\BAnd_{M\in\mnot(0)}\neg even(M)= \PI{X}{nat}\neg even(s(X))
% \eneq
% \enit
% \mends
%  \twoslide{A Simple Example: from \texttt{even} to \texttt{odd}}{2/2}
% \bit
% \item Complement of a rule is the conjunction of the complement of the
%   head with the complement of the body
% \[\begin{array}{l}
%   \mnotd( \PI{Y}{nat}even(s(s(Y))) \If even(Y))=\\
%  \qquad\qquad \BAnd_{M\in\mnot(s(s(Y))}\neg even(M)\And\mbox{}\\
%  \qquad\qquad   \PI{Y}{nat}\neg even(s(s(Y))) \If \mnotg(even(Y))=\\
%   \neg even(0)\And\neg even(s(0))\And \PI{Y}{nat}\neg even(s(s(Y)))) \If
%   \neg (even(Y) )
% \end{array}\]
% \item Compile away  disjunctions inside the new  predicate definition via unification to  recover goal-oriented proof-search.
% $$\PI{X}{nat}\neg even(s(X))\Or(\neg even(0)\And\neg even(s(0)))\leadsto\neg even(s(0))$$
%   \enit \mends
%% 9 


  \twoslide{Eliminating Negation: Problems}{4/4} \bit
\item Unfortunately, elimination of negation does not scale
  immediately to a logical framework such as HHF:
\begin{itemize}
\item Intrinsic friction  between \textbf{Closed} and \textbf{Open} World
  Assumption.
\item Negation normal forms (and completion-based approaches) 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}
\item Solution: restrict to a fragment, \emph{complementable
    clauses}, where hypothetical judgments
  are not ``unbound''.
\enit
\mends
% \begin{slide}{}
% \begin{center}
% \fbox{4. Elimination of Negation in a Logical Framework:}
% \vsk
% Part (a) Clause Complement.
% \bit
% \item An Example
% \item The Regular World Assumption
% \item HHF Clause Complement
% \enit
% \end{center}\mends
\renewcommand{\lx}{\Lambda x\,.\,}
 \begin{slide}{}
\myslidetitle{Example: Encoding the (untyped) $\l$-calculus} {}
\bit
\item The language of expressions:
\beq
e & \bnfas & x \mid  (\lx e) \mid  e_1\  e_{2}
\eneq
\item The signature:
\beq
 exp& \hastype& \mbox{\textrm{type}}\\
 lam&\hastype &(exp\Imp exp)\Imp exp\\
 app& \hastype &exp \Imp exp\Imp exp
\eneq
\item
The representation function:
\beq
\rep{x} & = & x\hastype exp\\
\rep{\lx e} & = & lam\ (\lamb{x}{exp} \rep{e})\\
\rep{e_1\ e_2} & = & app\ \rep{e_1}\ \rep{e_2}
\eneq
% \item
% The encoding a $\beta$-redex  as a pattern using logic variables
%  $E_{exp\Imp exp}$ and $F_{exp}$:
% \beq
% \rep {(\lx e)\ f} & = & app\ (lam\  (\lamb{x}{exp} (E\ x))\ F)
% \eneq
\enit\mends 
\renewcommand{\lx}{ \lambda x\,.\,}
\begin{slide}{}
\myslidetitle{Example: (object-level) linear terms}{}
\bit
% \item
% Complement of the $\beta$-redex in the \textbf{empty} context:
%  $\lx e, (e_1 \ e_2) \ e_3$, that is
% \beq
% \lefteqn{\cdot\vd\mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)=}\\ 
% && \{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_3\}
%  \eneq

% \item
% Encoding a $\eta$-redex, where $x\not\in FV(e)$:
% \beq
% \rep{\lx (e\ x)} & = & lam(\lamb{x}{exp} (\fbox{$app\ E$}) \ x)
% \eneq

% \item Hence $e$ {\em does \textbf{not}} depend on $x$.  Intuitively
%   its complement should contain those application sub-terms where $E$
%   {\bf does} depend on $x$:
% $$lam(\lamb{x}{exp} (\fbox{$app\ F\# x$}) \ (H\ x))$$
\item  A lambda term is 
\emph{linear}  if every functional sub-term uses each of its
arguments exactly once:
\beq
linapp & : & linear(app\ E_1\ E_2)\\
& & \qquad\If  linear(E_1)\\
& & \qquad \If linear(E_2).\\
linlam& : & linear(lam( \lx E\ x))\\
& & \qquad\If  linx( \lx E\ x)\\
& & \qquad \If (\PI{x}{exp} linear(x)\Imp linear(E\ x)).\\
linxx& : & linx(\lx x).\\
linxap_1& : & linx(\lx app\ (E_1\ x) \ E_2)\\
& & \qquad\If  linx(\lx E_1\ x).\\
linxap_2& : & linx(\lx app\ E_1\ (E_2\ x))\\
& & \qquad\If  linx(\lx E_2\ x).\\
linxlm& : &linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} linx (\lx E\ x\ y)).
\eneq
\enit
\mends

%% 11
\twoslide{Complementable Clauses }{}
\bit
\item Observation: in logical frameworks 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:
%\begin{small}
%\beq
%linlam& : & linear(lam( \lx E\ x))\If  linx( \lx E\ x)\\
%& & \qquad \If (\PI{x}{exp} linear(x)\Imp linear(E\ x)
$$ linear(lam( \lx E\ x))\If  \dots \fbox{$(\PI{x}{exp} linear(x)\Imp
  linear(E\ x)$)}$$ 
%\end{small}
%\item The eigenvariable condition ensures no overlap. %with static program
\item Thus dynamic assumptions extend the current database in a
  \textbf{regular} way, so that static and dynamic clauses never
  \textbf{overlap} (eigenvariable condition).
\item Idea: {\bf Restrict} negation to programs 
  where every assumption is parametric.

\enit
\mends
%% 12
\twoslide{Regular World Assumption}{}
\bit
% \item Example: checking whether a $\l$-term is \texttt{closed}:
% \[\begin{array}{l}
% \PI{E}{exp}closed(lam\ E) \If \PI {x } {exp}\ cclosed( 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 A manifestation of the \textbf{Regular World Assumption}: we
 establish in advance  the  class of ``possible worlds'' where programs can 
end up into.
\item A middle ground between programs that cannot make any extension
  (Horn/CWA) and those whose extensions are completely unpredictable (OWA).
% \item
% % This restriction is a simple way to ensure no overlap between
%  % dynamic and static clauses; 
% Other decidable conditions for non-overlap 
% possible.
% \item  extensions are enforced to be regular.

% \enit\mend
% \twoslide{Regular World Assumption}{2/2}
% \bit
\item Not covered: for example, the encoding of the implication
  introduction rule 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 We have shown that this restriction is both elegant and pragmatically
  adequate (and conservative \wrt Horn logic).
\enit
\mends


\twoslide{Complementing Partially Applied Terms}{}
\bit
\item $\lx (E\ x)$ matches every term of the appropriate type.
\item $\lx \fbox{$E$}$ matches only those terms (of the appropriate
  type) that \textbf{do not} depend on $x$.
\item The complement of $\lx \fbox{$E$}$ is  the set of terms that  
\textbf{must} depend on $x$.
\item The crux of the matter is whether a pattern is \emph{fully
    applied}, \ie if  all bound variables appearing in the binder are
  mentioned in the scope of a logic variable.
\item Partially applied terms not closed under term complement, if not
  internalized in a \textbf{strict} type theory.


\enit
\mends
\twoslide{Synthesis of the negation of \texttt{linear}}{1/3}
\bit
\item 
Consider $ linx(\lx app\ (E_1\ x) \ \fbox{$E_2$})\If  linx(\lx E_1\
x)$. 
Head is not \emph{fully applied}: $x$ does not occur in $E_2$. 
\item For the sake of this presentation just a notation: $E\ x^1$
  (must depend) $E\ x^0$ (must not). In real life different kind of
  \emph{application} in a type theory of
  \textbf{strictness}, where $E\ x^1$ is the complement of $E\ x^0$
  and symmetrically.
\item We normalize it in:
$$ linx(\lx app\ (E_1\ x) \ \fbox{$(E_2\ x^0)$})\If linx(\lx E_1\ x)$$

\item Its negation is not problematic.
\beq
\neg linx(\lx app\ (E_1\ x) \ \fbox{$(E_2\ x^1)$})\If \neg linx(\lx E_1\ x)
\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 $e$
 is {\bf not} linear if there is some function which
does \emph{not} use its argument or uses it \emph{more than
  once}. $\Lambda x.\, e$ is not linear if  not linear in its
  first argument or if its body is not linear: how to negate a
  hypothetical and parametric goal?
\item Mimic a failure derivation to provide a proof 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}  parameters, 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))\\
& & \quad\If (\PI{y}{exp} \fbox{$\top_{linx}$}\Imp linx (\lx E\ x\ y)).
\eneq
\bit
\item Compute $y\oftp exp\vd\mnota(\top_{linx})=\neg 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))\\
  & & \quad\If (\PI{y}{exp} \fbox{$\neg linx(\lx y)$}\Imp linx (\lx
  E\ x\ y)).  \eneq
\item  Negate the body: \beq
\neg \ald(linxlm)& : &\neg linx(\lx lam(\ly E\ x\ y))\\
& & \quad\If (\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ 
y)).  
\eneq 
\enit
\mends

%\input{ex}
%% 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{complementable} 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}{}
% \begin{center}
% \fbox{ 4. Elimination of Negation in a Logical Framework:}
% \vsk
% Part (b) Term Complement.

% \bit
% \item Higher-Order Term Complement
% \item Strict Types
% \item Algebra of Simple Terms
% \enit
% \end{center}\mends
% \begin{slide}{}
%   \slidetitle{ Term Complement}
%  \begin{itemize} \itemsep 0pt
%  \item Recall: complement of the head of a clause requires
%    \textbf{term} complement.
% \item
% A term $M$  with free variables as the intensional representation
% of its \emph{ground} instances, denoted  $\| M \|$.
% \item
% \emph{Unification} of two terms $`N=M$' as \emph{intersection}  
% of their ground instances: $\|N\|\cap\|M\|$.
% \item
% The {\em complement} of   $M$, $\mnot(M)$, is the set of 
% ground terms which are not instances of $M$, \ie are not in $\| M \|$.
% \item 'Relative Complement':
% all the ground 
% instances of a given (finite) set of terms which are not instances of 
% another given one:
% \[ \{ M_1 \mdots M_n \} - \{ N_1 \mdots N_m \} \] 
% \end{itemize}
%   \vfill
%  \end{slide}
% %\begin{slide}{}
%  %\slidetitle{More in general}
% % \begin{itemize} \itemsep 0pt
% %\item 'Multiple Complement': by De Morgan rules:
% %\beq
% % \mnot\{0,s(s(Y))\}& =& \mnot(0)\cap\mnot(s(s(Y)))\\
% %&=&  s(X)\cap \{0,s(0)\}\\
% %&=&  \{s(0)\}
% %\eneq
% %  \item 'Relative Complement':
% %all the ground 
% %instances of a given (finite) set of terms which are not instances of 
% %another given one. 
% %\[ \{ t_1 \mdots t_n \} - \{ u_1 \mdots u_m \} \]
% %\item
% %Example:
% %\beq
% %s(X) - \{0,s(s(Y)))\}& =& s(X)\cap\mnot\{0,s(s(Y))\} \\
% %&=& s(X)\cap s(0)= s(0)
% %\eneq
% %\enit
% %\vfill
% %\end{slide}

% \begin{slide}{}
% \slidetitle{Higher-Order Term Complement}
% \bit

% \item Need to extend term complement to the simply-typed $\l$-calculus, to compute, for example:
% \ben
% \item  $\mnotd(linx(\lx \fbox{$x$} \ ))$: not problematic.
% \item $\mnotd(linx(\lx app\ (E_1\ x) \ \fbox{$E_2$}\ )\If linx(\lx E_1\ 
%   x))$  
% \enen
% \item Note that the bound variable $x$ {\em does\/} not occur in the
%   (pattern variable) argument $E_2$. 
 
% \item Common technique: encoding a $\eta$-redex, where $x\not\in
%   FV(e)$: 
% \beq \rep{\Lambda x\,.\,  (e\ x)} & = & lam(\lamb{x}{exp} (\fbox{$app\ 
%     E$} \ ) \ x) 
% \eneq \enit \mends

% \begin{slide} 
% \myslidetitle{Fully vs.\ Partially Applied Patterns}{1/2}
% \bit
% \item Problem: a pattern $(\lambda x\ldot E\ x)$  matches any term
% of appropriate type; $(\lambda x\ldot E)$ matches only ground
% terms $(\lambda x\ldot M)$ where $M$ does  \textbf{not depend} on $x$. 
% \item The crux of the matter is whether a pattern is \emph{fully
%     applied}: all bound variables appearing in the binder are
%   mentioned in the scope of a logic variable.
  
% \item In $(\lx app\ (E_1\ x) \ E_2)$, the first argument $(E_1\ x) $
%   is fully applied, while the second one $E_2$ is not.
  
% \item Complement of fully applied terms is a simple extension of the
%   \fo case, by keeping track of bound variables.


% \enit\mends


% \begin{slide}
% \myslidetitle{Fully vs.\ Partially Applied Patterns}{2/2}
% \bit

% \item The complement of $(\lx app\ (E_1\ x) \ E_2)$ 
% contains every  ground terms
%   $(\lambda x\ldot app\ (M_1\ x) \ ( M_2\ x))$,
%  such that $M_2$ \textbf{must} use $x$.
% \item
%     The simply typed $\l$-calculus theory is not strong enough to
%   directly represent the complement of partially applied patterns.

% \item  Lugiez  [1995] modifies the language 
% of terms to promote constraints to first-class objects.
% The technical handling of those objects is awkward.

% \item We choose to have a notion of \emph{strictness} in the language
%   to express variable occurrence constraints.  \enit \mends
% \begin{slide}
% \myslidetitle{Strict Types}{1/2}\bit
% \item We \emph{internalize} strictness as a type system, 
% generalizing the language of simple types to include: 
% \ben
% \item \emph{strict functions} of type $A \RImp B$ (which are
%   guaranteed to depend on their argument)
% \item \emph{invariant functions} of type $A \ZImp B$ (which are
%   guaranteed \textbf{not} to depend on their argument)
% \item The full function space $A \TImp B$
%  \enen
% \item Under the Howard-Curry isomorphism, this yields a relative of the implicational fragment of relevance logic \textbf{R}.
% \enit
% \mends
% \begin{slide}
% \myslidetitle{Strict Types}{2/2}


% \[ \begin{array}{rrcl}
%  \mbox{\textit{Labels}} & k & \bnfas & 1 \bnfalt 0 \bnfalt u \\
%  \mbox{\textit{Types}} & A & \bnfas &  a \bnfalt A_1 \GImp{k} A_2 \\
%  \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam x^k\oftp
% A\ldot M \bnfalt (M \ N)^k \\
%  \mbox{\textit{Contexts}} & \Gamma & \bnfas & \cdot \bnfalt \Gamma, x\oftp A
%  \end{array} \]

% \bit
% \item Three labels: 1 'must occur', 0 'must not occur', u 'undetermined',  three different forms of abstraction and application. 
% \item Typing judgment: $\Gamma;\Omega;\Delta\vd M\hastype A$.
% \item Calculus is well-behaved.
% \enit
% \mends
% %\begin{slide}
% %  \slidetitle{Toward Term Complement} \bit
% %\item We have a calculus which is potentially strong enough to
% %  represent the complement of \ho patterns.
% %\item  Complement must  satisfy the  boolean rules for negation: 
% %\ben
% %\item (Disjointness) It is not the case that  $M\in\|N\|$ and
% %  $M\in\|\mnot(N)\|$.
% %\item (Exhaustivity)  $M\in\|N\|$ or   $M\in\|\mnot(N)\|$.  
% %\enen
% %\item Disjointness entailed by: not the case that both
% %  $\GG_1;\O_1;(\D_1,x\oftp C)\vd M\hastype A$ and $\GG_2;(\O_2,x\oftp
% %  C);\D_2\vd M\hastype A$.
% %\item Exhaustivity does not hold in general in the presence of
% %  intuitionistic application.
% % \enit
% %  \mends
% \begin{slide}
% \slidetitle{Simple Terms}
% \bit
% \item We give a complement algorithm that is sound and complete
%   for the natural embedding of the simply-typed $\lambda$-calculus:
% \[ 
% \begin{array}{rrcl}
% \mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
% A\ldot M \bnfalt(h\ \ol{M_n^1}) \bnfalt (E\ \ol{x_n^k})
% \end{array} \]
% \item 
% Partially applied terms are made fully applied with \textbf{vacuous} variables:
% $$(\lx app\ (E\ x^u) (\fbox{$F\ x^0$} \ ))$$
% \item Complement requires complementing the labels.
% \[\begin{array}{l}
% \mnot(\lx app\ (E\ x^u) (\fbox{$F\ x^0$} \ )) = \\
% \qquad\qquad \{\lx x, \lx lam( \ly (E'\ x^u\ y^u))),\\
% \qquad\qquad \lx app\ (H\ x^u) \ (\fbox{$G\ x^1$} \ )\}
% \end{array}\]
% %{\bf Theorem } 
% %Simple terms are closed under complement.
% %\item \newcommand{\cu}{(\GG, x\oftp C);\Omega;\Delta}
% %  \newcommand{\cxtr}{\GG;\O; (\D, x\oftp C)} \newcommand{\cxto}{\GG;
% %    (\O,x\oftp C);\D} 
% %Crucial property: {\bf (tightening)}.
% % If $\cu\vd M\hastype A$,
% %  then $\cxtr\vd M\hastype A$ or $\cxto\vd M\hastype A$.  
% %\item Now exhaustivity holds.

% \enit \mends

% \begin{slide}
%   \slidetitle{The Algebra of Simple Terms} 
% \bit
% \item We extend \ho pattern unification to simple terms in the form of
%   intersection.
  
% \item \textbf{Finite} sets of most general unifiers exist.
% % \item {\bf Theorem } $M\in\|N_1\|$ and $M\in\|N_2\|$ iff
% %   $M\in\|N_1\cap N_2\|$.

% \item From complement and intersection we can define any boolean operations: in particular, the {\em relative} complement operation, for
%  $\cal M$ and $\cal N$ finite sets of terms of the same type:
% \beq
% \cal M - \cal N & = & \cal M\cap (\mnot (\cal N))
% \eneq
% \item The set of \emph{finite} sets of simple terms (over a signature)
%   as a \emph{boolean} algebra under set union, pattern intersection
%   and complementation and extensional identity (on sets of ground
%   terms).
% \enit
% \mends
%\twoslide{Examples}{}\bit
%\item Complementing a simple term:
%\[\begin{array}{l}
%\cdot\vd\mnot(\lx app\ (E\ x^u) (\fbox{$F\ x^0$})) = \\
%\qquad\qquad \{\lx x, \lx lam( \ly (E'\ x^u\ y^u))),\\
%\qquad\qquad \lx app\ (H\ x^u) \ (\fbox{$G\ x^1$})\}
%\end{array}\]
%\item Unifying simple terms:
%\[\begin{array}{l}
%\cdot\vd\lx app\ (E\ x^1) \ (E'\ x^u)\cap \lx app\ (F\ x^u) \ (F'\ x^1) =\\
%\qquad\qquad \{\lx app\ (G\ x^1) \ (G'\ x^1)\}
%\end{array}\]
%\enit\mends
\twoslide{Complete definition of $\neg$\texttt{linear}}{}
\beq
\neg linapp_1 & : & \neg linear(app\ F\ G)\If \neg linear(F).\\
\neg linapp_2 & : & \neg linear(app\ F\ G)\If  \neg linear(G).\\
\neg linlam_1& : & \neg linear(lam\ \lx E\ x)\If \neg linx( \lx E\ x).\\
\neg linlam_2& : & \neg linear(lam\ \lx E\ x)\\
&&\qquad\If (\PI{y}{exp} (\neg linx(\lx y)\And linear(y))\\
&&\qquad\qquad\Imp\neg  linear(E\ y)).\\
\neg linxap_1& :& \neg linx(\lx app\ (F\ x^1) \ (G\ x^1)).\\
\neg linxap_2& : & \neg linx(\lx app\ (F\ x^0) \ (G\ x^0)).\\
\neg linxap_3& : & \neg linx(\lx app\ (F\ x^1) \ (G\ x^0))\If \neg linx(\lx
 F\ x^1).\\ 
 \neg linxap_4& : & \neg linx(\lx app\ (F\ x^0) \ (G\ x^1))\If \neg linx(\lx G\
 x^1).\\ 
\neg linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\If\\
& & \qquad(\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ y)).
\eneq
\mends


% \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 \TImp 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}{}
% \begin{center}
% \fbox{5. Contributions and Future Work}
% \bit
% \item
% A complement algorithm for a useful class of third-order hereditary
% Harrop formulae

% \item A relative complement algorithm for \ho patterns internalized
%   into a strict type theory
% \enit

% \end{center}\mends
\begin{slide}{}
 \slidetitle{Conclusions}
 \bit
\item Negation is useful in logical frameworks such as Hereditary
  Harrop Formulae, but it is difficult to allow.
\item We have approached the problem of adding negation by a
  source-to-source \textbf{transformation} that eliminates negation in
  favor of positive definitions.
\item We have found a middle ground between CWA and OWA in the Regular World 
Assumption. 
\item We have isolated a significant fragment of HHF, where clause
  complementation 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).

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

\item Implement this pre-compiler in languages such as $L_{\lambda}$
  [Miller '91],
  and possibly in general purpose systems such as Isabelle.
\item Investigate the transformational approach to  negation in
  sub-structural calculi and languages (Lolli, Forum, Linear LF).
 \enit
 \mends
\end{document}


