\documentclass{article}
 \usepackage{lcom}
\usepackage{amsfonts}
 \usepackage{latexsym}
 \usepackage{cdsty}  % section rather than chapter
\title{An example of negation elimination in hereditary Harrop formulae}
\author{Alberto Momigliano}
\date{}
\begin{document}
\maketitle
Consider the language of the untyped $\l$-calculus:
\beq
e & \bnfas & x \bnfalt \Lambda x \, .\,  e \bnfalt e_1\, e_2
\eneq 
We encode these expressions as terms in (labeled) hereditary Harrop 
formulae via the usual techniques of higher-order abstract
syntax  as canonical forms over the following signature:
\beq
\Sigma  & = & exp\hastype \mbox{\textrm{type}}, lam\hastype (exp\Imp 
exp)\Imp exp, app \hastype exp \Imp (exp\Imp exp)
\eneq
The representation function is given by:
\beq
\rep{x} & = & x\\
\rep{\Lambda x\,.\, e} &=& lam\ (\lamb{x}{exp} \rep{e})\\
\rep{e_1\ e_2} & = &app\ \rep{e_1}\ \rep{e_2}
\eneq
A term is \emph{linear} if every functional subterm uses
each of its arguments  exactly once: in particular, we
 make sure that a function is linear in its first argument
and then recurring on its body.
\beq
linlam& : & linear(lam\ \lx E\ x)\\
& & \qquad \If linx( \lx E\ x)\\
& & \qquad \If (\PI{x}{exp} linear(x)\Imp linear(E\ x)).\\
linapp & : & linear(app\ E_1\ E_2)\\
& & \qquad \If linear(E_1)\\
& & \qquad \If linear(E_2).\\
\vsk
linxx& : & linx(\lx x).\\
linxap1& : & linx(\lx app\ (E_1\ x) \ E_2)\\
& & \qquad \If  linx(\lx E_1\ x).\\
linxap2& : & 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
This is clearly a decision procedure, which can be complemented; an
expression is {\em not\/} linear if there is some  function which either does not use
its argument or uses them more than once. The following is obtained
via the clause complementation algorithm described in my thesis; note
that `$\neg$' is \emph{not} a connective but a name constructor for atoms.
\beq
\neg linlam1& : & \neg linear(lam\ \lx E\ x)\\
& & \qquad\If  \neg linx( \lx E\ x).\\
\neg linlam2& : & \neg linear(lam\ \lx E\ x)\\
& & \qquad\If   (\PI{x}{exp} \neg linx(\lx y) \And linear(x)\Imp \neg linear(E\ x)).\\
\neg linapp1 & : & \neg linear(app\ E_1\ E_2)\\
& & \qquad\If  \neg linear(E_1).\\
\neg linapp2 & : & \neg linear(app\ E_1\ E_2)\\
& & \qquad\If \neg linear(E_2).\\
\vsk
\neg linxap0& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x^1)).\\
\neg linxap1& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^1))\\
& & \qquad\If \neg linx(\lx E_1\ x).\\
\neg linxap2& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x))\\
& & \qquad\If \neg linx(\lx E_2\ x).\\
\neg linxap3& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\\
& & \qquad\If  \neg linx(\lx E_1\ x)\And\neg linx(\lx E_2\ x) .\\
\neg 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
where  $(E_1\ x^1)$ denotes that $E_1$ \emph{must} depend on $x$, \ie it 
strict in $x$; the semantics of this annotation is given
by the strict $\l$-calculus, again described in my dissertation.
\end{document}


