\section{Related Work on Strictness}
\label{sec:relstrict}

Church original definition of the set $\Lambda_{I}$ of (untyped) $\l$-terms \cite{Church41} has
this clause for abstraction:
\begin{center}
If $M\in\Lambda_{I}$ and $x\in FV(M)$, then $\lx M\in\Lambda_{I}$.
\end{center}
\ie in this language there cannot be any vacuous abstractions.  It can
be shown that the only difference between $\Lambda_{I}$ and
$\Lambda$ -- the usual definition of $\l$-terms -- is the lack of the
combinator $\mathbf{K}$.  Indeed, it can be shown that every term in
$\Lambda$ can be defined from $\Lambda_{I}$ and $\mathbf{K}$.  The $\l
I$-calculus is the theory of conversion restricted to $\Lambda_{I}$
terms.  This fragment was favored by Church over the nowadays usual
calculus, because, among other issues, it is strong enough to
represent every partial recursive function, albeit not in the most
efficient way: see \cite{Barendregt80} Chapter $2.2.2-2.2.5$ and more
extensively in Chapter $9$.  See \cite{Gabbay92} for an historical
account.

This would correspond in a simply typed setting to allowing
\emph{only} strict types: more formally if we denote with
$\Lambda^{\GImp{k}}$ the terms typable in a Curry  system based on the
$\GImp{k}$ function space, then $\Lambda^{\GImp{1}}=
\Lambda^{\GImp{u}}\cap \Lambda_{I}$, as noted for example in
\cite{Baker94}.

The  combinatory counterpart of this calculus
obviously excludes $\mathbf{K}$ and consists of $\mathbf{I,W,B, C}$,
see \cite{Curry58} and \cite{Barendregt80}, Appendix B for an alternative
basis. 
Those are the axioms of what Church called \emph{weak implicational
  logic} \cite{Church51}, \ie
identity, contraction, prefixing
and permutation. This establishes the link with an enterprise born from
a very different origin.

 The relevance logic project emerged in fact in the early
sixties out of Anderson and Belnap's dissatisfaction with the
so-called `paradoxes of implication', let it be material,
intuitionistic or strict (in the modal sense of Lewis and Langford);
 it was built on the work of Moh, Church, Parry
in the fifties\footnote{Some early work in the twenties in the Soviet
Union was, at the time, not accessible.} and climaxed with the
publication of the first volume of \emph{Entailment}
\cite{Anderson75} (the second one was published only in 1992
\cite{Anderson92}).  Following Girard's and Belnap's \cite{Belnap93} 
suggestion, we will \emph{not} refer to our calculus as
\emph{relevant}, but as \emph{strict} logic, as the former may also
satisfy other principles such as distributivity of arrow over
conjunction.

On an unrelated front, starting with Mycroft's seminal paper
\cite{Mycroft80}, compile-time analysis of functional programs
concentrated on  strictness analysis in order to get the best out of
call-by-value and call-by-need evaluation; first in terms of
abstract interpretation, later by using non-standard types to
represent these `intensional' information about functions
(see \cite{Jensen91} for a comparison of these two techniques).
However, earlier work  as
\cite{Kuo89} used non-standard primitive type to distinguish strict or
non-strict terms, closed only under intuitionistic implication.  Not
forgetting Wadler's early paper \cite{Wadler90} on using linear logic
for sharing analysis, Wright \cite{Wright91,Wright92}  seems the first one to have extended the
Curry-Howard isomorphism to (the implicational fragment of) relevance
logic and explicitly connected the two areas, although both \cite{Belnap74} and
\cite{Helman77} had previously recognized the link between strictness
and relevance\footnote{Note that we have became aware of this
  literature only after having fully developed our calculus which was
  modeled after the two-zoned linear logic calculus.}.

In \cite{Baker94} the author summarizes the above-mentioned idea
of expressing via types the reduction behavior of terms. He characterizes in an
operational sense the class of terms which need their argument, the
idea being that not only each terms need to be strict, but so does the
result of each application. $M$ is not strict if for all $N$ no
descendant of $N$ is in the normal form of $M\ N$. This class is then
shown to be equivalent to the Curry-typable fragment of $\Lambda_I$.

We now discuss the Curry typing system proposed there, which makes
available strict, invariant and intuitionistic types: yet, it is
biased towards enforcing strictness information, which ultimately lead
to a difference of expressive power from our calculus.  Some rules are
presented in Figure \ref{fig:clem}-- we omit the introduction rules
which are as expected -- transliterated in our notation.  There is
only one context, where variables carry their occurrence status as a
label. There are no different abstractors or applicators, but
different rules. Note that there is only one identity rule, the strict
one, so that e.g.\ $\lx x\hastype A\TImp A$ is not derivable, as it
can be given the more stringent type $A\RImp A$.  The elimination
rules are not syntax-directed, therefore not invertible, as the system
is essentially top-down driven. Let us concentrate on the elimination
rules: the side condition enforces the information ordering, so that
for example $A'\ZImp B\leq A\TImp B'$, provided that $A\leq A', B\leq
B'$. This allow to infer by strict application $\GG,\GG'\vd M\ 
N\hastype C$ from $\GG\vd M\hastype (A\TImp B)\RImp C$ and $\GG'\vd
A\ZImp B$. The latter is instead forbidden in our system by the
labeled reduction rules.  The rationale on the substitution operation
on context is that in $app\ZImp$ $A$ is not relevant to $B$, so all
hypothesis should be deleted. Instead, in order to preserve every
variable declaration, their strict label is changed into irrelevant.
This would amount to moving the strict variables in the irrelevant
context in our system. Note the difference with our rule, where the
latter variables are moved in the \emph{undetermined} context.
Similarly in $app\TImp$ strict labels turn into undetermined.
Moreover, having only one context, the author needs a strategy to deal
with same binding with different annotations; the solution is that
while propagating premises top-down a binding $x^1\oftp A$ supersedes
$x^u\oftp A$ which in turn supersedes $x^0\oftp A$.
 
The author goes on (see also \cite{Wright93}) detailing a system which
refines the strict calculus by allowing to \emph{count} usage,
motivated by \emph{sharing} analysis; thus $A\GImp{i} B$ denotes a
term where $A$ is used $i$ times to infer $B$. Undetermined usage is
then added via dummy variables.
%The system is  introduced in Wright's
%thesis \cite{Wright92},
This unfortunately leads to an undecidable type checking problem.


 \begin{figure}
   \[
   \begin{array}{c}
\ianc{}{ \GG[1:=0], x^1\oftp A\vd x\hastype A}{var}\vsk
 \ibnc{\GG\vd M\hastype A\RImp B}{\GG'\vd N\hastype A'}{\GG,\GG'\vd
   M\ N\hastype B}{app\RImp}\vsk
 \ibnc{\GG\vd M\hastype A\ZImp
   B}{\GG'\vd N\hastype A'}{\GG,\GG'[1:=0]\vd M\ N\hastype
   B}{app\ZImp}\vsk 
 \ibnc{\GG\vd M\hastype A\TImp B}{\GG'\vd N\hastype
   A'}{\GG,\GG'[1:=u]\vd M\ N\hastype B}{app\TImp}\vsk
  \mbox{All elimination rules have the condition $A'\leq A$}
   \end{array}
\]

   \caption{The system in \cite{Baker94}}
   \label{fig:clem}
 \end{figure}
In \cite{Wright96} Wright introduces  an \emph{Annotation Logic} as a
general framework for resource-conscious logics. The annotation logic has
formulae/types of the form $$A\bnfas X^k\bnfalt A\GImp{k} B$$ for any
annotation $k$ and has structural
and connective rules as well as annotation ones:
$$
\begin{array}{c}
  \ianc{\GG\vd A^i}{\GG^k\vd A^{ik}}{*k}\qquad
  \ianc{\GG,A^i\vd B}{\GG,A^{i+k}\vd B}{+k}
\end{array}
$$ 
The latter implement rules such as promotion/dereliction. By instantiation
with different algebras of annotation, we get systems as linear,
strict logic as well as various other usage logics. An abstract
normalization procedure is sketched, which  however needs commutative
conversions (e.g.\ the case contraction/arrow elimination) 
already in the purely implicational fragment. Another problem is that
properties as loosening should in our opinion be admissible rather
than primitive rules.

\subsubsection{Bunched Implication}

In a series of papers Pym et at.\ (see \cite{Pym99} and references
therein) introduce a \fo and its correspondent dependent type calculus
which aim to couple multiplicative and addititive implication. The two
are distinct by allowing two different constructors for contexts which
are called ``bunches''. This is different from a zoned calculus as
bunches can be nested. As expected, contraction and weakening are
allowed for additive assumptions but not for multiplicative ones. The
resulting logic can be seen as variant of relevant logic, as there is
no requirement that an argument to a multiplicative function must be
used only once, but only that it should not share with other variables in the
(proof) term. Thus, in out terminology $A\RImp ((A\TImp A\TImp B)\TImp
B) $ is derivable, but not $A\RImp ((A\RImp A\RImp B)\RImp B) $.
Moreover, the logic allows additive conjunction to distribute on
additive disjunction, which is not allowed in multiplicative additive
intuitionistic linear logic. Its naturality should follow from its
categorical semantics.  Its correspondent dependent type calculus,
dubbed \emph{RLF} is proposed as a resource conscious conservative
extension of LF.

\subsubsection{Relevant Logic Programming}

In \cite{Bollen91} the author presents his approach to
\emph{relevant}, \ie in our terminology strict \lp as part of his
dissertation on `Conditional Logic Programming' \cite{Bollen87}. He
makes a (weak) case for its utility in applications such as planning and
diagnosis, whose hypothetical queries should indeed use their
premises. The system boils down to a strict version of
N-Prolog. Unfortunately the author was only partially aware of
Girard's work on linear logic, and entirely not aware of
 the notion of uniform proof \cite{Miller91apal}, although he gives a brave
attempt to a mainly proof-theoretic approach: thus, as Gabbay and
McCarthy before, he embarks on an awfully complicated and low-level
description of an interpreter which enforces the usage requirement,
for, I think, the following fragment; note that there are two
conjunctions: $\&$ is additive and $\And$ multiplicative.

\[ \begin{array}{rrcl}
 \mbox{\textit{Assertions}} & A & \bnfas & P \bnfalt Q\RImp P\bnfalt
 A_1 \& A_2\bnfalt \forall x \,.\,A \\ 
\mbox{\textit{Queries}} & Q &
 \bnfas & P \bnfalt Q_1\And Q_2\bnfalt Q_1\Or Q_2 \bnfalt A\RImp Q\bnfalt \exists x \,.\,Q
\end{array}\]


If we were formulating a strict logical framework in the sense of
\cite{Cervesato96phd}, the former system would  therefore be a strict (no pun
intended) subset of the latter.

