\section{Strict Types}
\label{strcttypes}
 
The relevance logic project emerged in the early sixties out of 
Anderson and Belnap's disatisfaction with the so-called `paradoxes of 
implication'', let it be material, intuitionistic or strict, 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{AB75} followed after a long while (1991) by 
the the second tome, under the collaboration of too many logicians to 
mention here.  While the jury is still out on the long-lasting 
validity of the project--as a matter of fact it may be safely argued 
that now linear logic has superseded the Entailment logic as 
\textbf{the} logic of resources' use and also from the philosophical 
point of view new theories of conditionals (as Veltmann's) may be 
taking the lead--our interest and aim is much narrower.  Indeed our 
goal is to provide, through the Howard-Curry isomorphism a type-system 
which is capable of internalizing the dependency constrains on 
variables in $\l$-terms that seem to be of chief importance in the 
formalization of \ho disunification and which have received a 
non-logical treatment in Lugiez's work.  More explicitly the type 
system can express and check statements about whether % and how often
an expression uses (arbitrarily often) an argument mentioned in its 
binder.  Thus the linear $\l$-calculus is a special case of this: the 
issue of `occurring only once' can nevertheless be captured by 
introducing the linear connectives.  The peculiarity of this 
formulation is the introduction of a vacuous functional type with its 
respective connectives to denote an expression that \emph{ought not} to 
depend from its argument.  For this reason and following Girard's and 
Belnap's \cite{SH?} suggestion we will refer to this calculus as 
\emph{strict} logic, leaving the relevant label to other calculi which 
may also satisfy other principles such as distributivity connecting the various 
connectives.


\subsection{The system $\lc$}

Types (Formulae) language:
\beq
A & \bnfas & P\mid A\Imp B\mid A\RImp B
\mid A\ZImp B
\eneq
Terms (Proof) language:
\beq M & \bnfas
x \mid c\mid \lom x:A.M\mid M M^u\mid \lr x:A.M\mid M M^1\mid \lt x:A.M\mid M\_ ^0
\eneq 
We use an underscore version of $M^0$ in $0$-application since in the abstraction the 
argument is not used and hence the result of the application does not 
depend on $M^0$.

Judgment: $\GG;\Delta \prvs A$, where the former context is 
intuitionistic and the latter strict (must occur at least once: 
contraction, no weakening).  The calculus is minimal, that is, with 
exactly one consequence in the judgment, hence a three-zone 
formulation is what is needed.
\smallskip
% Signature: as usual. 
% \beq
% \Sigma & : & \bnfas \cdot\mid \Sigma, c:A
% \eneq
% Contexts are \textbf{sets}; this builds in contraction, but not weakening;
% exchange is immaterial, since there is no ordering.
% \beq
% \Delta & : & \bnfas \cdott\mid \Delta, x:A
% \eneq
Curry type system (natural deduction).
%\footnote{Rules for 
%constants are analogous to the one for variables, which can be 
%formally justified as in \cite{Bar9?} by seeing constants as 
%specially named variables. This is different from \cite{Cervesato97lics}, don't 
%know why}
 For better readability we use $\eset$ to 
denote the empty context instead of $\cdot$
\begin{figure}
\[
\begin{array}{cc}
\ianc{c\in\Sigma}{\GG; \Delta  \prv_{\Sigma} c: A}{Idc}
\vsk
\ianc{}{\GG;x : A \prv_{\Sigma} x:A} {IdR}
& 
\ianc{}{(\GG,x : A); \eset  \prv_{\Sigma} x:A}{IdI}\vsk
\ianc{(\GG,x : A) ; \Delta \prvs M: B}{\GG;\Delta\prvs(\lom x :A.M) : 
A\Imp B} {\Imp I}
&
\ianc{\GG;\Delta\prvs M : A \Imp B \quad\quad \GG;\eset \prvs N  : A}
{\GG;\Delta \prvs M N :B}{\Imp E}\vsk
\ianc{\GG ; (\Delta,x : A) \prvs M: B}{\GG;\Delta\prvs(\lr x :A.M) : 
A\RImp B}{\RImp I}
&
\ianc{\GG;\Delta_{1}\prvs M : A \RImp B \quad\quad \GG;\Delta_{2} \prvs N  : A}
{\GG;\Delta_{1}\cup \Delta_{2} \prvs M N^1 :B}{\RImp E}\vsk
\ianc{\GG ; \Delta \prvs M: B}{\GG;\Delta\prvs(\l^{0} x :A.M) : 
A\ZImp B}{\ZImp I}
&
\ianc{\GG;\Delta\prvs M : A \ZImp B 
% \quad\quad \GG;\eset \prvs \_ N : A
}
{\GG;\Delta  \prvs M  \_^0 :B}{\ZImp E}
\end{array}
\]
\caption{Typing rules for $\lc$}
\end{figure}


Note how the strictness constraints is preserved in the elimination 
rule: you can always apply an intuitionistic term to a strict function 
(losing the dependencies), but not viceversa: thus $N:A$ in ($\Imp E$) 
is a proof from the empty strict context.  Remark also the 
set-theoretic union $\cup$ of strict contexts in ($\RImp E$), which 
constrains $N:A$ to appear in the first or the second or both 
contexts.  Subtly, his is the only difference compared to the 
\emph{linear} calculus: if instead of unioning sets, we only juxtapose 
the non-intuitionistic context as a multiset, we obtain the 
elimination rule for linear implication: the difference between linear 
and strict implication in the difference between multisets and sets in 
a zoned calculus, let it be sequents or natural.  % Thanks Girard 
Example : fix a signature

\newcommand{\jj}{\justifies}
% \begin{Examplen}
\begin{figure}
\prooftree
\[ \mbox{} \jj x : A \RImp A\RImp B \prv x : A \RImp A\RImp B \using 
IdR \]
 \qquad 
 \[ \mbox{} \jj y : A\prv y: A \using IdR\]
 \using \RImp E
\justifies
\[
x : A \RImp A\RImp B , y :A\prv x y^1 : A\RImp B \qquad y : A\prv y: A
\using \RImp E
\justifies
\[
 x : A \RImp A\RImp B ,y: A\prv (x y^1)  y^1 : B
 \using \RImp I
 \justifies
 \[
 x : A \RImp A\RImp B  \prv \lr y . (x y^1)  y^1 : A\RImp B
 \using \RImp I
 \justifies
\prv \lr x.\lr y. (x y^1)  y^1  : A \RImp A\RImp B\RImp (A\RImp 
B)
\]
\]
\]
\endprooftree
% \end{Examplen} 
\caption{Derivation of $A \RImp A\RImp B\RImp (A\RImp B)$}
\end{figure}


Note again the usage of set-theoretic union of strict context.  
Nothing is intuitionistic, hence the latter are not mentioned with in 
the previous example.  W.r.t.\ the identity rules, you may convince 
yourself of their validity proving $ \prv A \Imp B \RImp B$,  $ \prv A\RImp B 
\Imp A$, but $\not \prv A \Imp B \RImp A$.  It is immediate to give a 
sequent style formulation for the propositional calculus with three 
implications and furthermore relate cut-free derivations with normal 
deduction an in \cite{Pfe94a}.

\subsection{Reductions}
% Let us recall that the only allowed applications combinations are R-R, 
% R-I, I-I: hence the following $\beta$-reductions.  
We assume the usual 
notion of free and bound variables, capture-free substitution and we 
identify $\alpha$-convertible terms. 
\[
\begin{array}{llll}
 R-R & (\lr x:A.M)  N^1 & \Lmap_{\beta} & [N/x]M\\
%    R-I & (\lr x:A.M)  N & \Lmap_{\beta} & [N/x]M\\
    I-I & (\lom x:A.M)  N & \Lmap_{\beta} & [N/x]M    \\
     N-N & (\lt x:A.M)  \_^0 & \Lmap_{\beta} & M\\
%     N-I & (\lt x:A.M)  N & \Lmap_{\beta} & [N/x]M\\
%     N-R & (\lt x:A.M) \rapp N & \Lmap_{\beta} & [N/x]M\\
%   R-N & (\lr x:A.M)\zapp  N & \Lmap_{\beta} & [N/x]M
\end{array}
\]
We add the rules for $\eta$-reductions, since they may come handy 
when defining the long $\be$-normal form:
\[
\begin{array}{llll}
  R-R & (\lr x:A.(M x^1)) & \Lmap_{\eta} & M\\
%  R-I & (\lr x:A.M \rapp x) & \Lmap_{\eta} & M\\  it is I R impossible
    I-I    & (\lom x:A.(M x)) & \Lmap_{\eta} & M\\
     N-N      & (\lt x:A.(M  \_^0)) & \Lmap_{\eta} & M
\end{array}
\]

It\marginpar{I may drop this paragraph}
 may also be illuminating to consider validity and completeness \wrt 
combinators (the axiomatic formulation).  Remember that $S,K$ is a 
\emph{basis} for positive intuitionistic logic.  Since $K$ or $K^{*}$ 
are fallacies in their naive (intuitionistic) reading, we need to 
explicitly assume $I$.  We end up with the following basis for the 
system $\lc$:
\beq
I& :  & A \RImp A\\
S& :  & A \RImp B \RImp .(B\RImp C) \RImp (A \RImp C)\\
P& :  & A \RImp (B \RImp C \RImp(B \RImp A\RImp C))\\
C& :  & (A \RImp A\RImp B)\RImp (A\RImp B)
\eneq 
The connection to the sequent version is intuitively
% \footnote{Mmmh, 
% fishy: cut is clearly eliminable, why $S$ is essential for the 
% deduction theorem, though I do not have a proof of this.} 
clear: $I$ is axiom, $S$ cut, $P$ is exchange, $C$ 
contraction\footnote{For non-commutative systems, it is not sufficient 
to drop $P$.  This is explored in the rich theory of the so-called 
\emph{ticket entailment} \cite{AB75}, which essentially corresponds to 
constraining MP to be at most of second degree: functions are allowed 
to be applied only as \emph{major} premises of a MP inference step.  
Exchange would apparently trivialize this condition}.
Soundness is just an exercise in natural deduction, while completeness 
requires a modification of the bracket abstraction (deduction theorem) 
argument.  This is better accomplished with the Fitch style of natural 
derivation devised in \cite{AB75}.  In this formulation of the 
calculus of strict implication set of labels (cfr.\ $LDS$) are 
associated to hypothesis: MP unions those sets (not a surprise, given 
our previous discussion on the strict arrow elimination rule).  
Implication is allowed to be introduced only if the label of the 
hypothesis is properly subtractable from the label of the conclusion, 
\ie if the assumption has been ``used'' in the derivation of the 
latter.  Note that this tabulation technique is actually proposed in 
the implementation of strict logic programming in \cite{Bol91}.
  
% We could conjecture a similar result for the full system \textbf{R} of 
% strict logic with respect to the opportune lambda-calculus, but this 
% is not directly of interest for us.  Similarly, for the moment we will 
% not go in further details as far as strict implication is concerned 
% although there are many results in the literature that could gain more 
% weight in the proposition-as-types interpretation\footnote{For 
% instance the so-called `relevance' property: in every valid strict 
% function space, domain and co-domain must share a base type,}.
% \end{document}
\subsection{Properties of $\lc$}

We now want to check the subject reduction and expansion 
property; hence we need to 
establish the relative inversion and substitution lemmata: we follow 
\cite{Bar9?}'s account.

\begin{Lemma} [Inversion] 
 \mbox{}
\begin{itemize}
	\item[Iapp] $\GG;\Delta \prvs M N :B \Rightarrow \exists A: \GG;\Delta 
	\prvs M: A \Imp B \And \GG;\Delta \prvs N :A$

	\item[Sapp] $\GG;\Delta \prvs M  N^1:B \Rightarrow \exists 
	A,\Delta_{1},\Delta_{2}: \Delta =_{set} \Delta_{1} \cup \Delta_{2} \ s.t.\ \GG;\Delta_{1} 
	\prvs M: A \RImp B \And \GG;\Delta_{2} \prvs N :A$

	\item[Napp] $\GG;\Delta \prvs M \_^0 :B \Rightarrow \exists A: \GG;\Delta 
	\prvs M: A \ZImp B %\And \GG;\Delta \prvs \_ :A
$

	\item[Iabs] $\GG;\Delta\prvs(\lom x :A.M) : C \Rightarrow \exists A,B: 
	C =_{\tau} A \Imp B \ s.t.\ (\GG,x : A) ; \Delta \prvs M: B$

	\item[Sabs] $\GG;\Delta\prvs(\lr x :A.M) : C \Rightarrow \exists A,B: 
	C =_{\tau} A \RImp B \ s.t.\ \GG ; (\Delta,x : A) \prvs M: B$ 
	 
	\item[Nabs] $\GG;\Delta\prvs(\lt x :A.M) : C \Rightarrow \exists A,B: 
	C =_{\tau} A \ZImp B \ s.t.\ \GG ; \Delta \prvs M: B$
\end{itemize}
\end{Lemma}
\begin{proof} By inspection
\end{proof}
% \end{document}
\begin{Lemma} [Substitution] 
\mbox{}
\begin{enumerate}
	\item  $(\GG, x:A);\Delta \prvs M :B \And \GG;\Delta \prvs  N :B 
	\Rightarrow \GG;\Delta \prvs [N/x]M :A$

	\item  $\GG;(\Delta, x:A) \prvs M :B \And \GG;\Delta \prvs  N :B 
	\Rightarrow \GG;\Delta \prvs [N/x]M :A$
\end{enumerate}
\end{Lemma}
\begin{proof}
By induction on the structure of $ (\GG, x:A);\Delta \prvs M :B$ and 
$\GG;(\Delta, x:A) \prvs M :B $ respectively.
\end{proof}
\begin{Proposition} [Subject reduction and expansion for $\lc$]
\mbox{}

\ben
	\item $\GG;\Delta \prvs M:A \mbox{\, and $M 
\Lmap^{*}_{\beta} M'$\,}\Rightarrow  \GG;\Delta \prvs M':A$
		\item $\GG;\Delta \prvs M:A \mbox{\, and $M 
\Lmap^{*}_{\eta} M'$\,}\Rightarrow  \GG;\Delta \prvs M':A$.
\enen
\end{Proposition}  
\begin{proof}
(Sketch). (1) By induction on $\Imp^{*}_{\beta}$. In the base case consider in 
turn each kind of $\beta$-redex. Apply  
inversion and conclude by the substitution lemma. Otherwise apply the 
inductive hypothesis. (2)
\end{proof}

\subsection{Canonical forms for $\lc$}
We present a (Curry) type system for $\lc$. For future use in unification 
we actually present the system for \emph(canonical) forms, \ie terms
in $\be$ long normal form. This is realized by the two mutually
recursive judgments:

\newcommand{\da}{\downarrow}
\newcommand{\bua}{\Uparrow}

\ben
\item$\GG;\Delta\prvs M \da A$: $M$ is atomic of type $A$
\item$\GG;\Delta\prvs M \bua A$: $M$ is canonical of type $A$.
\enen
\begin{figure}[h]
\[
\begin{array}{cc}
\ianc{}{\GG;x : A \prv_{\Sigma} x\da A} {cIdR}
& 
\ianc{}{(\GG,x : A); \eset  \prv_{\Sigma} x\da A}{cIdI}\vsk
\ianc{\GG;\Delta \prv_{\Sigma} x\da P}{\GG;\Delta \prv_{\Sigma} x\bua P} {cAt}
& 
\ianc{c\in\Sigma}{\GG; \Delta  \prv_{\Sigma} c\da A}{cIdc}\vsk
\ianc{(\GG,x : A) ; \Delta \prvs M\bua B}{\GG;\Delta\prvs(\lom x :A.M) \bua 
A\Imp B} {c\Imp I}
&
\ianc{\GG;\Delta\prvs M \da A \Imp B \quad\quad \GG;\eset \prvs N  \bua A}
{\GG;\Delta \prvs M N \da B}{c\Imp E}\vsk
\ianc{\GG ; (\Delta,x : A) \prvs M\bua B}{\GG;\Delta\prvs(\lr x :A.M) \bua 
A\RImp B}{c\RImp I}
&
\ianc{\GG;\Delta_{1}\prvs M \da A \RImp B \quad\quad \GG;\Delta_{2} \prvs N  \bua A}
{\GG;\Delta_{1}\cup \Delta_{2} \prvs M N^1 \da B}{c\RImp E}\vsk
\ianc{\GG ; \Delta \prvs M\bua B}{\GG;\Delta\prvs(\l^{0} x :A.M) \bua 
A\ZImp B}{c\ZImp I}
&
\ianc{\GG;\Delta\prvs M \da A \ZImp B %\quad\quad \GG;\eset \prvs \_^0 \bua A
}
{\GG;\Delta  \prvs M  \_^0 \da B}{c\ZImp E}
\end{array}
\]
\caption{Canonical forms for $\lc$}
\end{figure}


\subsection{Strict Unification}\marginpar{switch 
back here to calculus without $\ZImp$}

This is temporary: hopefully it will be superseded by an opportune 
modification of the proof system in Cervesato \& Pfenning, inheriting 
the soundness and completeness proof.

\newcommand{\sn}{s_{n}}
\[
\begin{array}{l}
\textbf{main} rel-unify(\l x_k. F(\yn) \l x_k. F(\zm))\\
\quad	 (ffd (\l x_k. F(\yn), \l x_k. G(\zm))  \textbf{AND}
 ffd (\l x_k. F(\zm) \l x_k. F(\yn)))\\
\quad	\textbf{OR}\\
\quad	 ffs (\l x_k. F(\yn), \l x_k. F(\zm))\\
\quad	\textbf{OR}\\
\quad	fr(\l x_k. F(\yn),\l x_k. a(\tn))\\
\quad	\textbf{OR}\\
\quad	dec(\l x_k. a(\sn), \l x_k. a(\tn))\\

\skl
%Flex-Flex-diff  case
\textbf{proc} ffd (\l x_k. F(\yn), \l x_k. G(\zm))\\
\quad	matrix := []\\
\quad	\textbf{FOR} 1\leq i \leq n \textbf{DO}\\
\quad\quad		\textbf{IF} strict(y_i) \textbf{AND} 
\exists z_l   y_{i}=z_{l} \\ %insert argument rel()
\quad\quad		\textbf{AND} strict(z_{l}) \textbf{OR} int(z_{l})  \textbf{THEN}			
\\
\quad\quad		matrix := y_i::matrix\\
\quad\quad		\textbf{ELSE} \textbf{FAIL}\\ %not exists 		
\quad\quad		\textbf{FI}\\
\quad\quad		\textbf{IF} int(y_i)  \textbf{AND}  \exists z_l.   y_i=z_{l}  
		\textbf{AND} strict(z_l) \textbf{OR} int(z_l) \textbf{THEN}\\
\quad\quad		matrix := y_i::matrix\\
\quad\quad		\textbf{ELSE DO} nothing\\ %  not exists
\quad\quad		\textbf{FI}\\
\quad\quad		matrix:= rev(matrix)\\
\quad\quad		binder := binder(\l x_k. F(\yn))\\
\quad\quad		F:= binder.H(matrix)\\
\end{array}
\]
% Flex-Flex-same case
\[
\begin{array}{l}

\textbf{proc} ffs (\l x_k. F(\yn), \l x_k. F(\zm))\\
\quad	matrix := []\\
\quad	\textbf{IF} n \leq m \\
\quad	\textbf{FOR} 1\leq i\leq n \textbf{DO}\\
\quad\quad		\textbf{IF} int(y_i) \textbf{AND} y_i=z_i \textbf{THEN}\\
\quad\quad		matrix := y_i::matrix\\
\quad\quad		\textbf{ELSE} \textbf{DO} nothing \\% different
\quad\quad		\textbf{FI}\\
\quad\quad		\textbf{IF} strict(y_i) \textbf{ AND} y_i=z_i \textbf{THEN}\\
\quad\quad		matrix := y_i::matrix\\
\quad\quad		\textbf{ELSE FAIL} \\% different 
\quad\quad		\textbf{FI}\\
\quad\quad		matrix:= rev(matrix)\\
\quad\quad		binder := binder(\l x_k. F(\yn))\\
\quad\quad		F:= binder.H(matrix)\\
\quad	\textbf{ELSE} \\% m>n
\quad	ffs ( \l x_k. F(\zm), \l x_k. F(\yn))\\
\quad	\textbf{FI}\\

\end{array}
\]
Auxiliary\ predicates
\[
\begin{array}{l}
\textbf{proc} strict(x,\l x_k. F(\yn))\\
\tau_n \Imp \tau := type-of(F)\\
i:= lookup(x,\yn)\\
\textbf{IF} incoming-arrow(t_i) = \RImp \textbf{THEN}\\
tag:= R\\

\skl
\textbf{proc} int(x,\l x_k. F(\yn))\\
\tau_n \Imp \tau := type-of(F)\\
i:= lookup(x,\yn)\\
\textbf{IF} incoming-arrow(t_i) = \Imp \textbf{THEN}\\
tag:= I \\

\skl
\textbf{proc} binder (\l x_k. F(\yn))\\
	\textbf{FOR} 1\leq i \leq n \textbf{DO}\\
\quad		\textbf{IF} strict(x_i \l x_k. F(\yn)) \textbf{THEN}\\
\quad		binder := \lr :: binder\\
\quad		\textbf{ELSE}\\
\quad		binder := \l :: binder\\

\end{array}
\]


