\documentclass{article}
%\documentclass[amstex]{article}
\usepackage{latexsym,amssymb,amsthm,proof}
\newtheorem{definition}{\sc Definition}[section]
\newtheorem{theorem}[definition]{\sc Theorem}
\newtheorem{lemma}[definition]{\sc Lemma}
\newtheorem{fact}[definition]{\sc Fact}
\newtheorem{example}[definition]{\sc Example}
\renewcommand{\qedsymbol}{$\blacksquare$}

\title{$\lambda\rho$-calculus\footnote{This article is an abstract and
details will be published elsewhere.}}
\author{Yuichi Komori\\
\texttt{komori@math.s.chiba-u.ac.jp} \\
Department of Mathematics, \\
Faculty of Sciences,
Chiba University
\and Arato Cho\\
\texttt{aratoc@g.math.s.chiba-u.ac.jp} \\
Department of Mathematics, \\
Faculty of Sciences,
Chiba University
}
\date{}% Do not fill in the date

\begin{document}
\maketitle\thispagestyle{empty}

%\begin{center}
%\begin{tabular}{rl}
%{\sc Yuichi Komori} & 
%{\bf \LARGE$\lambda\rho$-calculus}\footnote{This article is an abstract and
%details will be published elsewhere.} \\
%{\sc Arato Cho}
%&
%\end{tabular}
%\end{center}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\noindent %{\footnotesize{\bf abstract.} 
In \cite{Komori2002}, one of the authors has posed a new system $\lambda\rho$-calculus
and stated without proof that the strong normalization theorem hold. We will give a proof
of it. While the type assignment system $TA_{\lambda}$ gives a natural deduction for
intuitionistic implicational logic (cf.\ \cite{Hindley0}), $TA_{\lambda\rho}$ gives a
natural deduction for classical implicational logic. Our system is simpler than Parigot's
$\lambda\mu$-calculus (cf.\ \cite{Parigot}).

%\noindent{\footnotesize {\sl Keywords:} $\lambda$-calculus, typed $\lambda$-calculus,
%normalization theorem, classical logic, $\lambda\rho$-calculus, $\lambda\mu$-calculus,
%${\rm LK}$.
% }

\section{The type free $\lambda\rho$-calculus}

\begin{definition}[$\lambda\rho$-terms]\rm
An infinite sequence of {\em $\lambda$-variables} is assumed to be given, and an infinite sequence of {\em $\rho$-variables} is assumed to be given. Then linguistic expressions called {\em $\lambda\rho$-terms} are defined thus:
\begin{enumerate}
\item each $\lambda$-variable is a $\lambda\rho$-term, called an {\em atom} or {\em atomic term};
\item if $M$ and $N$ are $\lambda\rho$-term then $(MN)$ is a $\lambda\rho$-term called an {\em application};
\item if $M$ is a $\lambda\rho$-term and $a$ is a $\rho$-variable then $(aM)$ is a $\lambda\rho$-term called an {\em absurd};
\item if $M$ is a $\lambda\rho$-term and $f$ is a $\lambda$-variable or a $\rho$-variable then $(\lambda f.M)$ is a $\lambda\rho$-term called an {\em abstract}. (If $f$ is a $\lambda$-variable or a $\rho$-variable, then it called a $\lambda$-abstract or a $\rho$-abstract respectively.)
\end{enumerate}
\end{definition}

$\lambda$-variables are denoted by $u$, $v$, $w$, $x$, $y$, $z$, with or without number-subscripts. $\rho$-variables are denoted by $a$, $b$, $c$, $d$, with or without number-subscripts. A {\em term-variable} means a $\lambda$-variable or a $\rho$-variable. Term-variables are denoted by $f$, $g$, $h$, with or without number-subscripts. Distinct letters denotes distinct variables unless otherwise stated.

A term $\lambda a.M$ is sometimes denoted by $\rho a.M$ if the variable $a$ is a $\rho$-variable.

Arbitrary $\lambda\rho$-terms are denoted by $L$, $M$, $N$, $P$, $Q$, $R$, $S$, $T$, with or without number-subscripts. For $\lambda\rho$-term we shall say just term.

%\begin{definition}[Free, bound]\rm
%A non-binding variable occurence $\underline{f}$ in a term $M$ is sad to be {\em bound}
% in $M$ if it is in the scope of an occurence of $\lambda f$ in $M$, otherwise it is
% {\em free} in $M$.
%
%A variable $f$ is said to be {\em bound} in $M$ if $M$ contains an occurence of $\lambda
% f$; and $f$ is said to be {\em free} in $M$ if $M$ contains a free occurence of $f$.
% The set of all variables free in $M$ is called
%\[FV(M).\]
%\end{definition}
%
$FV(M)$ is the set of all variables free in $M$. For example, $FV(\lambda xb.a(x(by))) = 
\{a, y\}$. 

\begin{definition}[$\beta\rho$-contraction]\rm
A { \em $\beta\rho$-redex} is any $\lambda\rho$-term of form $(aM)N$, $(\lambda x.M)N$ or $(\lambda a.M)N$; its contractum is $(aM)$, $[N/x]M$ or $\lambda a.([\lambda x.a(xN)/a]M)N$ respectively. The re-write rules are
\begin{eqnarray*}
(aM)N &\rhd_{1\beta\rho}& (aM),\\
(\lambda x.M)N &\rhd_{1\beta\rho}& [N/x]M,\\
(\lambda a.M)N &\rhd_{1\beta\rho}& \lambda a.([\lambda x.a(xN)/a]M)N.
\end{eqnarray*}
If $P$ containd a $\beta\rho$-redex-occurence $\underline{R}$ and $Q$ is the result of replacing this by its contractum, we say {\em $P$ $\beta\rho$-contracts to $Q$} ($P\rhd_{1\beta\rho}Q$).
\end{definition}

%\begin{definition}[$\beta\rho$-reduction]\rm
%A {\em $\beta\rho$-reduction} of a term $P$ is a finite or infinite sequence of
% $\beta\rho$-contractions with form
%\[\langle P_1,\underline{R_1},Q_1\rangle, \langle P_2,\underline{R_2},Q_2\rangle,
% \ldots\]
%where $P_1\equiv_{\alpha}P$ and $Q_{i}\equiv_{\alpha}P_{i+1}$ for $i=1,2,\ldots$. (The
% empty sequence is allowed.) We say a finite reduction is from $P$ to $Q$ if either it
% has $n\geq 1$ contractions and $Q_{n}\equiv_{\alpha}Q$ or it is empty and
% $P\equiv_{\alpha}Q$. A reduction from $P$ to $Q$ is said to terminate or end to $Q$.
% If there is a reduction from $P$ to $Q$ we say $P$ $\beta\rho$-reduces to $Q$, or
%\[P\rhd_{\beta\rho}Q.\]
%Note that $\alpha$-conversions are allowed in a $\beta\rho$-reduction.
%\end{definition}
%
The notion of {\em $\beta\rho$-reduction} and the notation
 $P\rhd_{\beta\rho}Q$ are defined as usual.

\begin{theorem}[Church-Rosser threorem for $\beta\rho$-reduction]
If $M\rhd_{\beta\rho}P$ and $M\rhd_{\beta\rho}Q$, then there exists $T$ such that
\begin{center}
$P\rhd_{\beta\rho}T$ and $Q\rhd_{\beta\rho}T$.
\end{center}
\end{theorem}

\begin{proof}
Simmlar to the case of $\beta$-reduction, see \cite{Hindley1}.
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Assgning types to terms}

\begin{definition}[Types]\rm
An infinite sequence of {\em type-variables} is assumed to given, distinct from the term-variables. {\em Types} are linguistic expressions defined thus:
\begin{enumerate}
\item each type-variable is a type called an {\em atom};
\item if $\sigma$ and $\tau$ are types then $(\sigma\to\tau)$ is a type called a {\em composite type}.
\end{enumerate}
\end{definition}

Type-variables are denoted by $p$, $q$, $r$ with or without number-subscripts, and distinct letters denote distinct variables unless otherwise stated.

Aribitrary types are denoted by lower-case Greek letters except $\lambda$ and $\rho$.

Parentheses will often (but not always) be omitted from types, and the reader should restore omitted ones in the way of association to the right.

\begin{definition}[Type-assignment]\rm
A {\em type-assignment} is any expression
\[M:\tau\]
where $M$ is a $\lambda\rho$-term or a $\rho$-variable and $\tau$ is a type; we call $M$ its {\em subject} and $\tau$ is its {\em predicate}.
\end{definition}

%\begin{definition}[Type-context]\rm
%A {\em type-context} $\Gamma$ is any finite, perhaps empty, set of type-assignments
%\[\Gamma=\{f_1:\tau_1,\ldots,f_n:\tau_n\}\]
%whose subjects are term-variables which are {\em consistent} in the sense that no
% term-variable is the subject of more than one assignment. For any such $\Gamma$ define
%\[Subjects(\Gamma)=\{f_1,\ldots,f_n\},\ \ \ Predicates(\Gamma)=\{\tau_1,\ldots,\tau_n\}.
%\]
%\end{definition}
%
%The result of removing from $\Gamma$ the assignment whose subject is $f$ (if $\Gamma$
% has one) is called
%\[\Gamma-f.\]
%$\Gamma$ is called an {\em $M$-context} if $Subjects(\Gamma)=FV(M)$.
%
%$\Gamma_{\lambda}$ and $\Gamma_{\rho}$ denote the subsets of $\Gamma$ of all assignments
% whose subjects are $\lambda$-variables and $\rho$-variables respectively.
%
%Note that a type-context is a set, not a sequence. Hence it dose not change when its
% members are permuted or repeated.
%
%\begin{definition}\rm
%We say $\Gamma_1$ is {\em consistent} with $\Gamma_2$ if $\Gamma_1\cup\Gamma_2$ is
% consistent; and $\Gamma_1$, \ldots, $\Gamma_n$ are {\em mulutually consistent} if their
% union is consistent.
%\end{definition}
%
%\begin{definition}[$TA_{\lambda\rho}$-formulae]\rm
%For any type-assignment $M:\tau$, the pair $\langle\Gamma;M:\tau\rangle$ is called {\em
% $TA_{\lambda\rho}$-formula} and is written as
%\[\Gamma_{\lambda}\mapsto\Gamma_{\rho},M:\tau\]
%(or just $\mapsto M:\tau$ if $\Gamma$ is empty). We shall call $M$ the subject of this
% formula and $\tau$ its predecate.
%\end{definition}
%
%The following abbreviations will often be used:
%\begin{center}
%$f_1:\sigma_1,\ldots,f_n:\sigma_n$\ \ \ for\ \ \ $\{f_1:\sigma_1,\ldots,f_n:\sigma_n\}$,
%\\
%$\Gamma,f_1:\sigma_1,\ldots,f_n:\sigma_n$\ \ \ for\ \ \ $\Gamma\cup\{f_1:\sigma_1,
%\ldots,f_n:\sigma_n\}$.
%\end{center}
%
\begin{definition}[The system $TA_{\lambda\rho}$]\rm
$TA_{\lambda\rho}$ is a Natural Deduction system. Its formulas are type-assignments.
$TA_{\lambda\rho}$ has no axioms and has four rules called $(\to E)$, $(\to I)$,
$(Absurd)$ and $(Rati)$, as follows.

{\bf Deduction rules of $TA_{\lambda\rho}$}:
\[
\infer[(\to E),]
{PQ:\tau}
{P:\sigma\to\tau & Q:\sigma}
\hspace{5mm}
\infer[(\to I),]
{\lambda x.P:\sigma\to\tau}{\deduce{P:\tau}{\deduce{\Pi}{\infer{x:\sigma}{}}}}
\]
\[
\infer[(Absurd),]
{aP:\sigma}{a:\tau & P:\tau}
\hspace{5mm}
\infer[(Rati).]
{\lambda a.P:\tau}{\deduce{P:\tau}{\deduce{\Pi}{\infer{a:\tau}{}}}}
\]
\end{definition}

\begin{example}[Peirce's Law]\label{Peirce's Law}
\[
\infer[(\to I)]
{\lambda ya.y(\lambda x. ax):((\alpha\to\beta)\to\alpha)\to\alpha}{
\infer[(Rati)]{\lambda a.y(\lambda x. ax):\alpha}{
\infer[(\to E)]{y(\lambda x. ax):\alpha}{
\infer{y:(\alpha\to\beta)\to\alpha}{}
&
\infer[(\to I)]{\lambda x. ax:\alpha\to\beta}{
\infer[(Absurd)]{ax:\beta}{\infer{a:\alpha}{} & \infer{x:\alpha}{}}
}
}
}
}
\]
The above $TA_{\lambda\rho}$-deduction is writen in more compact style:
\[
\infer[\lambda y]
{((\alpha\to\beta)\to\alpha)\to\alpha}{
\infer[\rho a]{\alpha}{
\infer[(\to E)]{\alpha}{
\infer{y:(\alpha\to\beta)\to\alpha}{}
&
\infer[\lambda x]{\alpha\to\beta}{
\infer{ax:\beta}{\infer{a:\alpha}{} & \infer{x:\alpha}{}}
}
}
}
}
\]
\end{example}
%
%
\section{Strong Normalization Theorem for $TA_{\lambda\rho}$}
$\beta\rho$-reductions of deductions of $TA_{\lambda\rho}$ correspond to
$\beta\rho$-reductions of $\lambda\rho$-terms. We prove the strong normalization
theorem for deductions of $TA_{\lambda\rho}$ ,that is, for every
deduction of $TA_{\lambda\rho}$ $\Pi$, all reductions starting at $\Pi$ are finite.
To prove the theorem, we introduce $*$-expansion and use the strong normalization
theorem for deductions of $TA_\lambda$.

\begin{definition}[$\circ$-translation]\rm
For every deduction of $TA_{\lambda\rho}$, of which the last rule is $Rati$, 
we define {\em $\circ$-translation} as follows:
\begin{enumerate}
\item $\Pi^\circ\equiv \Pi$\ , where $\Pi\equiv\vcenter{\deduce{M:\alpha}{\Pi}}$ and
    $\alpha$ is an atomic type;
\item $\Pi^\circ\equiv\vcenter{\infer{\lambda y.N:\beta\to\gamma}{
     \deduce{N:\gamma}{\deduce{(\Pi_2)^\circ}{\infer{y:\beta}{}}}}}$ \ \ , where
     $\Pi\equiv\vcenter{\infer{\lambda a.M:\beta\to\gamma}{\deduce{M:\beta\to\gamma}{\deduce{\Pi_1}
     {\infer{a:\beta\to\gamma}{}}} }}$\ \ and \\[3mm] \ $\Pi_2\equiv\vcenter{
     \infer{\lambda a.[\lambda x.a(xy)/a]My:\gamma}{\infer{[\lambda x.a(xy)/a]My:\gamma}
     {\deduce{[\lambda x.a(xy)/a]M:\beta\to\gamma}{\deduce{[\lambda x.a(xy)/a]\Pi_1}
     {\infer{\lambda x.a(xy):(\beta\to\gamma)\to\delta}{\infer{a(xy):\delta}{\infer{a:\gamma}{} &
     \infer{xy:\gamma}{\infer{x:\beta\to\gamma}{} & y:\beta}}}}} & y:\beta}}}$ \ \ .
\end{enumerate}
\end{definition}
%    and\\[3mm]
%if $\alpha$ is an atomic type, $(\Pi_1)^\circ\equiv\Pi_1$, and if $\alpha$ is $\beta\to\gamma$,
% $(\rho a.M^*)^\circ\equiv\lambda y.(\rho a.[\lambda x.a(xy)/a]M^*y)^\circ$.

\begin{definition}[$*$-expansion]\rm
For every deduction of $TA_{\lambda\rho}$, we define {\em $*$-expansion} as follows:
\begin{enumerate}
\item $(x:\alpha)^*\equiv x:\alpha$\ ;
\item $\Pi^* \equiv \vcenter{\infer{M^* N^*:\beta}{
     \deduce{M^*:\alpha\to\beta}{(\Pi_1)^*} & \deduce{N^*:\alpha}{(\Pi_2)^*}}}$ \ \ , where
     $\Pi \equiv \vcenter{\infer{MN:\beta}{\deduce{M:\alpha\to\beta}{\Pi_1} & 
     \deduce{N:\alpha}{\Pi_2}}}$\ \ ;
\item $\Pi^*\equiv \vcenter{\infer{\lambda x.M^*:\alpha\to\beta}
   {\deduce{M^*:\beta}{\deduce{(\Pi_1)^*}{\infer{x:\alpha}{}}}}}$ \ \ ,
    where $\Pi \equiv \vcenter{\infer
   {\lambda x.M:\alpha\to\beta}{\deduce{M:\beta}{\deduce{\Pi_1}{\infer{x:\alpha}{}}}}}$ \ ;
\item $\Pi^*\equiv \vcenter{\infer{aM^*:\beta}{a:\alpha & \deduce{M^*:\alpha}{(\Pi_1)^*}}}$
    \ \ , where $\Pi \equiv \vcenter{\infer{aM:\beta}{a:\alpha & \deduce{M:\alpha}{\Pi_1}}}$ \ \ ;
\item $\Pi^*\equiv(\Pi_1)^\circ$ \ \ , where $\Pi \equiv\vcenter{
    \infer{\lambda a.M:\alpha}{\deduce{M:\alpha}{\deduce{\Pi_2}{\infer{a:\alpha}{}}}}  }$ \ \ and
    \ \ $\Pi_1\equiv\vcenter{\infer{\lambda a.M^*:\alpha}{\deduce{M^*:\alpha}{\deduce{(\Pi_2)^*}
    {\infer{a:\alpha}{}}}}}$ \ .
\end{enumerate}
\end{definition}

\begin{definition}[$\beta a$-reduction]\rm
A {\em $\beta a$-reduction} is a $\beta\rho$-reduction which does not allow a contruction $(\lambda a.M)N\rhd_{1\beta\rho}\lambda a.([\lambda x.a(xN)/a]M)N$.
\end{definition}

\begin{theorem}[Strong normalization theorem for $\beta a$-reduction]
For every deduction $\Pi$ of $TA_{\lambda\rho}$, all $\beta a$-reductions starting at $\Pi$ are finite.
\end{theorem}

\begin{proof}
Similar to the case of $TA_\lambda$, see \cite{Hindley1}.
\end{proof}

\begin{theorem}[Strong normalization theorem for $TA_{\lambda\rho}$]
For every deduction $\Pi$ of $TA_{\lambda\rho}$, all $\beta\rho$-reductions starting at $\Pi$ are finite.
\end{theorem}

\begin{proof}
We can prove that $(\Pi_1)^* \rhd_{1\beta a} (\Pi_2)^*$ if $\Pi_1 \rhd_{1\beta\rho} \Pi_2$.
So we get a infinite sequence of $\beta a$-reductions from a infinite sequence of
$\beta\rho$-reductions. That is, strong normalization theorem for $\beta a$-reduction
leads strong normalization theorem for $TA_{\lambda\rho}$.
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{thebibliography}{99}
\bibitem[H97]{Hindley0} J.\ Roser Hindley. {\it Basic Simple Type Theory}, Vol.\ 42 of {\it Cambridge Tracts in Theoretical Computer Science}, Cambridge University Press, 1997.
\bibitem[HS86]{Hindley1} J.\ Roger Hindley and Jonathan P.\ Seldin. {\it Introduction to combinators and $\lambda$-calculus}, Vol.\ 1 of {\it London Mathematical Society Student Texts}, Cambridge University Press, 1986.
\bibitem[P92]{Parigot} Michel Parigot. {\it $\lambda\mu$-CALCULUS: AN ALGORITHMIC INTERPRETATION OF CLASSICAL NATURAL DEDUCTION}, Lecture Notes in Computer Science 624, 190-201, 1992.
\bibitem[K02]{Komori2002} Yuichi Komori. {\it $\lambda\rho$-Calculus: A Natural Deduction for Classical Logic}, BULLETIN OF THE SECTION OF LOGIC, VOL.\ 31, No.\ 2, 65-70, 2002.
\end{thebibliography}
\
\end{document}
