File: ref.tex

package info (click to toggle)
minlog 4.0.99.20100221-8
links: PTS, VCS
area: main
in suites: forky, sid
size: 7,060 kB
sloc: lisp: 112,614; makefile: 231; sh: 11
file content (5370 lines) | stat: -rw-r--r-- 218,471 bytes
parent folder | download | duplicates (5)
% $Id: ref.tex,v 1.28 2008/01/25 13:30:19 logik Exp $
% was: ea.tex,v 1.68 2001/08/13 12:55:02 schwicht Exp 
% \documentclass[11pt,draft,a4paper]{amsbook}
\documentclass[11pt,a4paper]{amsart}
% \documentclass[11pt,a4paper,fleqn]{article}
\usepackage{amsmath,amssymb,amsthm,bussproofs}

% for pdftex
\usepackage[backref]{hyperref}

\allowdisplaybreaks[4]

\parskip 0pt plus 1pt

% \input{preamb}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{claim*}{Claim}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem*{definition*}{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem*{example*}{Example}
\newtheorem{examples}[theorem]{Examples}
\newtheorem*{examples*}{Examples}
\newtheorem{remark}[theorem]{Remark}
\newtheorem*{remark*}{Remark}
\newtheorem*{acknowledgement*}{Acknowledgement}

\def\qedsymbol{{\ \vbox{\hrule\hbox{%
   \vrule height1.3ex\hskip0.8ex\vrule}\hrule}}\par}


% minlog.mac contains the macros for all tex-files of the minlog
% documentation in order to avoid code duplication and different
% notations.
\input{minlog.mac}

% \def\N{\mathbb{N}}

%% Comment out this definition
%% in your main document when preparing the final version
\def\mylabel#1{\label{#1}\marginpar{\tiny #1}}



\makeindex

\title{Minlog reference manual}

% \title{Minimal logic for computable functionals.  Minlog reference manual}
\author{}
% \author{Klaus Aehlig, Martin Ruckert and Helmut Schwichtenberg%
% \thanks{Mathematisches Institut der Universit\"at  M\"unchen,
% Theresienstra{\ss}e 39, D-80333 M\"unchen, Germany.  Phone
% +49 89 2394 4413, Fax +49 89 280 5248, 
% e-mail address \texttt{schwicht@rz.mathematik.uni-muenchen.de}}
% \address{Mathematisches Institut der Universit\"at  M\"unchen\\
% Theresienstra{\ss}e 39\\
% D-80333 M\"unchen, Germany}
% \email{$\{$aehlig,ruckert,schwicht$\}$@rz.mathematik.uni-muenchen.de}
% \urladdr{http://mathematik.uni-muenchen.de/schwicht}
% \thanks{}
% \keywords{extracted programs}
% \subjclass[2000]{Primary: 02Dxx; Secondary: 02Fxx}
\date{\today}

\begin{document}

% \begin{abstract} 
% We define a formal system based on minimal logic and inductively
% defined ground types.% -- Draft of \today
% \end{abstract}

\maketitle

\tableofcontents

\input{acknow}

\section{Introduction}
\mylabel{Intro}
\textsc{Minlog} is intended to reason about computable functionals,
using minimal logic.  It is an interactive prover with the following
features.
\begin{itemize}
\item Proofs are treated as first class objects: they can be normalized
and then used for reading off an instance if the proven formula is
existential, or changed for program development by proof
transformation.
\item To keep control over the complexity of extracted programs, we
follow Kreisel's proposal and aim at a theory with a strong language
and weak existence axioms.  It should be conservative over (a fragment
of) arithmetic.
\item \textsc{Minlog} is based on minimal rather than classical or
intuitionistic logic.  This more general setting makes it possible to
implement program extraction from classical proofs, via a refined
$A$-translation (cf.\ \cite{BergerBuchholzSchwichtenberg02}).
\item Constants are intended to denote computable functionals.
Since their (mathematically correct) domains are the Scott-Ershov
partial continuous functionals, this is the intended range of the
quantifiers.
\item Variables carry (simple) types, with free algebras as base types.
The latter need not be finitary (so we allow e.g.\ countably branching
trees), and can be simultaneously generated.  Type parameters (ML
style) are allowed, but we keep the theory predicative and disallow
type quantification.
\item To simplify equational reasoning, the system identifies
terms with the same normal form.  A rich collection of rewrite rules
is provided, which can be extended by the user.  Decidable predicates
are implemented via boolean valued functions, hence the rewrite
mechanism applies to them as well.
\end{itemize}
We now describe in more details some of these features.

\subsection{Simultaneous free algebras}
A free algebra is given by \emph{constructors}, for instance zero and
successor for the natural numbers.  We want to treat other data types
as well, like lists and binary trees.  When dealing with inductively
defined sets, it will also be useful to explicitely refer to the
generation tree.  Such trees are quite often countably branching, and
hence we allow infinitary free algebras from the outset.

The freeness of the constructors is expressed by requiring that their
ranges are disjoint and that they are injective.  Moreover, we view
the free algebra as a domain and require that its bottom element is
not in the range of the constructors.  Hence the constructors are
total and non-strict.  For the notion of totality cf.\ \cite[Chapter
8.3]{Stoltenberg94}.

In our intended semantics we do not require that every semantic object
is the denotation of a closed term, not even for finitary algebras.
One reason is that for normalization by evaluation (cf.\
\cite{BergerEberlSchwichtenberg03}) we want to allow term families in
our semantics.

% However, if a type $\tau$ is given by a finitary algebra, then we do
% require that every closed term of type $\tau$ whose value is a
% semantic numeral also reduces to the corresponding syntactic numeral;
% this is \textsc{Plotkin}'s adequacy theorem \cite{Plotkin77} (or
% \cite[p.130]{AmadioCurien98}), which holds for a call-by-name
% evaluation strategy.

To make a free algebra into a domain and still have the constructors
injective and with disjoint ranges, we model e.g.\ the natural numbers
as shown in Figure~\ref{F:nat}.
\begin{figure}
% \begin{picture}(168,108)
\begin{picture}(170,120)
\put(48,0){\makebox(0,0){$\bullet$}}
\put(36,0){\makebox(0,0){$\bot$}}
\put(48,0){\line(-1,1){24}}
\put(24,24){\makebox(0,0){$\bullet$}}
\put(12,24){\makebox(0,0){$0$}}
\put(48,0){\line(1,1){24}}
\put(72,24){\makebox(0,0){$\bullet$}}
\put(90,24){\makebox(0,0){$S \bot$}}

\put(72,24){\line(-1,1){24}}
\put(48,48){\makebox(0,0){$\bullet$}}
\put(30,48){\makebox(0,0){$S 0$}}
\put(72,24){\line(1,1){24}}
\put(96,48){\makebox(0,0){$\bullet$}}
\put(120,48){\makebox(0,0){$S(S \bot)$}}

\put(96,48){\line(-1,1){24}}
\put(72,72){\makebox(0,0){$\bullet$}}
\put(48,72){\makebox(0,0){$S(S 0)$}}
\put(96,48){\line(1,1){24}}
\put(120,72){\makebox(0,0){$\bullet$}}
\put(150,72){\makebox(0,0){$S(S(S \bot))$}}

\put(120,72){\line(-1,1){24}}
\put(96,96){\makebox(0,0){$\bullet$}}
\put(66,96){\makebox(0,0){$S(S(S 0))$}}
\put(120,72){\line(1,1){24}}
\put(147,99){\makebox(0,0){.}}
\put(150,102){\makebox(0,0){.}}
\put(153,105){\makebox(0,0){.}}
\put(159,111){\makebox(0,0){$\bullet$}}
\put(181,111){\makebox(0,0){$\infty$}}
\end{picture}
\caption{The domain of natural numbers}
\label{F:nat}
\end{figure}
Notice that for more complex algebras we usually need many more
\inquotes{infinite} elements; this is a consequence of the closure of
domains under suprema.  To make dealing with such complex structures
less annoying, we will normally restrict attention to the \emph{total}
elements of a domain, in this case -- as expected -- the elements
labelled $0$, $S 0$, $S(S 0)$ etc.


\subsection{Partial continuous functionals}
As already mentioned, the (mathematically correct) domains of
computable functionals have been identified by Scott and Ershov as the
partial continuous functionals; cf.\ \cite{Stoltenberg94}.  Since we
want to deal with computable functionals in our theory, we consider it
as mandatory to accommodate their domains.  This is also true if one
is interested in total functionals only; they have to be treated as
particular partial continuous functionals.  We will make use of
predicate constants $\Total_{\rho}$ with the total functionals of type
$\rho$ as the intended meaning.  To make formal arguments with
quantifiers relativized to total objects more managable, we use a
special sort of variables intended to range over such objects only.
For example, $\texttt{n0}, \texttt{n1}, \texttt{n2}, \dots,
\texttt{m0}, \dots$ range over total natural numbers, and $\verb#n^0#,
\verb#n^1#, \verb#n^2#, \dots$ are general variables.  This amounts to
an abbreviation of
\begin{alignat*}{2}
&\forall \hat{x}.\Total_{\rho}(\hat{x}) \to A &\quad\hbox{by}\quad& 
\forall x A,\\
&\exists \hat{x}.\Total_{\rho}(\hat{x}) \land A &\quad\hbox{by}\quad& 
\exists x A.
\end{alignat*}


\subsection{Primitive recursion, computable functionals}
The elimination constants corresponding to the constructors are called
primitive recursion operators $\rec$.  They are described in detail in
Section \ref{Pconst}.  In this setup, every closed term reduces to a
numeral.  

However, we shall also use constants for rather arbitrary computable
functionals, and axiomatize them according to their intended meaning
by means of rewrite rules.  An example is the general fixed point
operator $\fix$, which is axiomatized by $\fix F = F(\fix F)$.
Clearly then it cannot be true any more that every closed term reduces
to a numeral.  We may have non-terminating terms, but this just means
that not always it is a good idea to try to normalize a term.

An important consequence of admitting non-terminating terms is that
our notion of proof is not decidable: when checking e.g.\ whether two
terms are equal we may run into a non-terminating computation.  But we
still have semi-decidability of proofs, i.e., an algorithm to check
the correctness of a proof that can only give correct results, but may
not terminate.  In practice this is sufficient.

To avoid this somewhat unpleasant undecidability phenomenon, we may
also view our proofs as abbreviated forms of full proofs, with certain
equality arguments left implicit.  If some information sufficient to
recover the full proof (e.g.\ for each node a bound on the number of
rewrite steps needed to verify it) is stored as part of the proof,
then we retain decidability of proofs.


\subsection{Decidable predicates, axioms for predicates}
As already mentioned, decidable predicates are viewed via boolean
valued functions, hence the rewrite mechanism applies to them as well.

Equality is decidable for finitary algebras only; infinitary algebras
are to be treated similarly to arrow types.  For infinitary algebras
(extensional) equality\index{equality} is a predicate constant, with
appropriate axioms.  In a finitary algebra equality is a (recursively
defined) program constant.  Similarly, existence (or totality) is a
decidable predicate for finitary algebras, and given by predicate
constants $\Total_{\rho}$ for infinitary algebras as well as composed
types.  The axioms are listed in Subsection \ref{SS:AxiomConst}
of Section~\ref{S:AssumptionVarConst}.


\subsection{Minimal logic, proof transformation}
For generalities about minimal logic cf.\ \cite{TroelstraSchwichtenberg00}.
A concise description of the theory behind the present implementation
can be found in \inquotes{Minimal Logic for Computable Functions}
which is available on the \textsc{Minlog} page \texttt{www.minlog-system.de}.


\subsection{Comparison with Coq and Isabelle}
\mylabel{SS:Coq} \textsc{Coq} (cf.\ \texttt{coq.inria.fr}) has evolved
from a calculus of constructions defined by \textsc{Huet} \index{Huet}
and \textsc{Coquand}\index{Coquand}.  It is a constructive, but
impredicative system based on type theory.  More recently it has been
extended by \textsc{Paulin-Mohring}\index{Paulin-Mohring} to also
include inductively defined predicates.  Program extraction from
proofs has been implemented by \textsc{Paulin-Mohring},
\textsc{Filliatre}\index{Filliatre} and
\textsc{Letouzey}\index{Letouzey}, in the sense that \textsc{Ocaml}
programs are extracted from proofs.

The \textsc{Isabelle/HOL} system of \textsc{Paulson}\index{Paulson}
and \textsc{Nipkow}\index{Nipkow} has its roots in \textsc{Church}'s
theory of simple types and \textsc{Hilbert}'s Epsilon calculus.  It is
an inherently classical system; however, since many proofs in fact use
constructive arguments, in is conceivable that program extraction can
be done there as well.  This has been explored by \textsc{Berghofer}
in his thesis \cite{Berghofer03}.

Compared with the \textsc{Minlog} system, the following points are of
interest.
\begin{itemize}
\item The fact that in \textsc{Coq} a formula is just a map into the
type \texttt{Prop} (and in \textsc{Isabelle} into the type
\texttt{bool}) can be used to define such a function by what is called
\indexentry{strong elimination}, say by $f(\true) := A$ and $f(\false)
:= B$ with fixed formulas $A$ and $B$.  The problem is that then it is
impossible to assign an ordinary type (say in the sense of
\textsc{ML}) to a proof.  It is not clear how this problem for program
extraction can be avoided (in a clean way) for both \textsc{Coq} and
\textsc{Isabelle}.  In \textsc{Minlog} it does not exist due to the
separation of terms and formulas.
\item The impredicativity (in the sense of quantification over
predicate variables) built into \textsc{Coq} and \textsc{Isabelle} has
as a consequence that extracted programs need to abstract over type
variables, which is not allowed in program languages of the
\textsc{ML} family.  Therefore one can only allow outer universal
quantification over type and predicate variables in proofs to be used
for program extraction; this is done in the \textsc{Minlog} system
from the outset.  However, many uses of quantification over predicate
variables (like defining the logical connectives apart from $\to$ and
$\forall$) can be achieved by means of inductively defined predicates.
This feature is available in all three systems.
\item The distinction between properties with and without
computational content seems to be crucial for a reasonable program
extraction environment; this feature is available in all three
systems.  However, it also seems to be necessary to distinguish
between universal quantifiers with and without computational content,
as in \textsc{Berger}'s \cite{Berger93a}.  At present this feature is
availble in the \textsc{Minlog} system only.
\item \textsc{Coq} has records, whose fields may contain proofs and
may depend on earlier fields.  This can be useful, but does not seem
to be really essential.  If desired, in \textsc{Minlog} one can use
products for this purpose; however, proof objects have to be
introduced explicitely via assumptions.
\item \textsc{Minlog}'s automated proof search \texttt{search} tool is
based on \textsc{Miller}'s\index{Miller} \cite{Miller91b}; it produces
proofs in minimal logic.  In addition, \textsc{Coq} has many strong
tactics, for instance \texttt{Omega} for quantifier free
\textsc{Presburger}\index{Presburger} arithmetic, \texttt{Arith} for
proving simple arithmetic properties and \texttt{Ring} for proving
consequences of the ring axioms.  Similar tactics exist in
\textsc{Isabelle}.  These tactics tend to produce rather long proofs,
which is due to the fact that equality arguments are carried out
explicitely.  This is avoided in \textsc{Minlog} by relativizing every
proof to a set of rewrite rules, and identifyling terms and formulas
with the same normal form w.r.t.\ these rules.
\item In \textsc{Isabelle} as well as in \textsc{Minlog} the extracted
programs are provided as terms within the language, and a soundness
proof can be generated automatically.  For \textsc{Coq} (and similarly
for \textsc{Nuprl}) such a feature could at present only be achived by
means of some form of reflection.
\end{itemize}


\section{Types, with simultaneous free algebras as base types}
\mylabel{S:Types}
Generally we consider typed theories only.  Types are built from type
variables and type constants by algebra type formation \texttt{(alg
$\rho_1 \dots \rho_n$)}, arrow type formation $\rho \to \sigma$ and
product type formation $\rho \times \sigma$ (and possibly other type
constructors).

We have type constants \texttt{atomic}, \texttt{existential},
\texttt{prop} and \texttt{nulltype}.  They will be used to assign
types to formulas.  E.g.\ $\forall n\,n=0$ receives the type
$\texttt{nat} \to \texttt{atomic}$, and $\forall n,m \ex k\,n+m=k$
receives the type $\texttt{nat} \to \texttt{nat} \to
\texttt{existential}$.  The type \texttt{prop} is used for predicate
variables, e.g.\ $R$ of arity \texttt{nat,nat -> prop}.  Types of
formulas will be necessary for normalization by evaluation of proof
terms.  The type \texttt{nulltype} will be useful when assigning to a
formula the type of a program to be extracted from a proof of this
formula.  Types not involving the types \texttt{atomic},
\texttt{existential}, \texttt{prop} and \texttt{nulltype} are called
object types.

% \subsection{Type variables and constants}
Type variable\index{type variable} names are $\texttt{alpha},
\texttt{beta} \dots$; $\texttt{alpha}$ is provided by default.  To
have infinitely many type variables available, we allow appended
indices: $\texttt{alpha}1, \texttt{alpha}2, \texttt{alpha}3 \dots$
will be type variables.  The only type constants\index{type constant}
are $\texttt{atomic}, \texttt{existential}, \texttt{prop}$ and
$\texttt{nulltype}$.

\subsection{Generalitites for substitutions, type substitutions}
\mylabel{SS:GenSubst}
Generally, a substitution is a list $((x_1\ t_1) \dots (x_n\ t_n))$ of
lists of length two, with distinct variables $x_i$ and such that for
each $i$, $x_i$ is different from $t_i$.  It is understood as
simultaneous substitution.  The default equality is \texttt{equal?};
however, in the versions ending with \texttt{-wrt} (for \inquotes{with
respect to}) one can provide special notions of equality.  To construct
substitutions we have
\begin{alignat*}{2}
&\texttt{(make-substitution \textsl{args} \textsl{vals})}%
\index{make-substitution@\texttt{make-substitution}} 
\\
&\texttt{(make-substitution-wrt \textsl{arg-val-equal?}\ \textsl{args} 
\textsl{vals})}%
\index{make-substitution-wrt@\texttt{make-substitution-wrt}} 
\\
&\texttt{(make-subst \textsl{arg} \textsl{val})}%
\index{make-subst@\texttt{make-subst}} 
\\
&\texttt{(make-subst-wrt \textsl{arg-val-equal?}\ \textsl{arg} \textsl{val})}%
\index{make-subst-wrt@\texttt{make-subst-wrt}} 
\\
&\texttt{empty-subst}\index{empty-subst@\texttt{empty-subst}} 
\end{alignat*}
Accessing a substitution is done via the usual access operations
for association list: \texttt{assoc} and \texttt{assoc-wrt}.
We also provide
\begin{alignat*}{2}
&\texttt{(restrict-substitution-wrt \textsl{subst} \textsl{test?})}%
\index{restrict-substitution-wrt@\texttt{restrict-substitution-wrt}} 
\\
&\texttt{(restrict-substitution-to-args \textsl{subst} \textsl{args})}%
\index{restrict-substitution-to-args@\texttt{restrict-substitution-to-args}} 
\\
&\texttt{(substitution-equal?\ \textsl{subst1} \textsl{subst2})}%
\index{substitution-equal?@\texttt{substitution-equal?}} 
\\
&\texttt{(substitution-equal-wrt?\ \textsl{arg-equal?}\ \textsl{val-equal?}\ 
\textsl{subst1} \textsl{subst2})}%
\index{substitution-equal-wrt?@\texttt{substitution-equal-wrt?}} 
\\
&\texttt{(subst-item-equal-wrt?\ \textsl{arg-equal?}\ \textsl{val-equal?}\ 
\textsl{item1} \textsl{item2})}%
\index{subst-item-equal-wrt?@\texttt{subst-item-equal-wrt?}} 
\\
&\texttt{(consistent-substitutions-wrt?}
\\
&\qquad\texttt{\textsl{arg-equal?}\ 
\textsl{val-equal?}\ \textsl{subst1} \textsl{subst2})}%
\index{consistent-substitutions-wrt?@\texttt{consistent-substitutions-wrt?}} 
\end{alignat*}

\emph{Composition}\index{composition} $\vartheta \sigma$ of two
substitutions
\begin{align*}
\vartheta &= ((x_1\ s_1) \dots (x_m\ s_m)),
\\
\sigma &= ((y_1\ t_1) \dots (y_n\ t_n))
\end{align*}
is defined as follows.  In the list $((x_1\ s_1\sigma) \dots (x_m\
s_m\sigma)\ (y_1\ t_1) \dots (y_n\ t_n))$ remove all bindings $(x_i\
s_i\sigma)$ with $s_i\sigma = x_i$, and also all bindings $(y_j\ t_j)$
with $y_j \in \{x_1, \dots, x_n\}$.  It is easy to see that
composition is associative, with the empty substitution as unit.
We provide
\begin{alignat*}{2}
\texttt{(compose-substitutions-wrt}\ 
&\texttt{\textsl{substitution-proc} \textsl{arg-equal?}}
\\
&\texttt{\textsl{arg-val-equal?}\ \textsl{subst1} \textsl{subst2}})%
\index{compose-substitutions-wrt@\texttt{compose-substitutions-wrt}} 
\end{alignat*}

We shall have occasion to use these general substitution procedures
for the following kinds of substitutions
\[
\begin{tabular}{|l|l|l|l|}
\hline
for                  
&called          
&domain equality 
&arg-val-equality
\\
\hline
type variables       
&\texttt{tsubst}\index{tsubst@\texttt{tsubst}}
&\texttt{equal?}
&\texttt{equal?}
\\
object variables     
&\texttt{osubst}\index{osubst@\texttt{osubst}}
&\texttt{equal?}
&\texttt{var-term-equal?}\index{var-term-equal?@\texttt{var-term-equal?}}
\\
predicate variables  
&\texttt{psubst}\index{psubst@\texttt{psubst}}
&\texttt{equal?}
&\texttt{pvar-cterm-equal?}%
\index{pvar-cterm-equal?@\texttt{pvar-cterm-equal?}}
\\
assumption variables
&\texttt{asubst}\index{asubst@\texttt{asubst}}
&\texttt{avar=?}\index{avar=?@\texttt{avar=?}}
&\texttt{avar-proof-equal?}%
\index{avar-proof-equal?@\texttt{avar-proof-equal?}}
\\
\hline
\end{tabular}
\]
The following substitutions will make sense for a
\[
\begin{tabular}{|l|l|}
\hline
type
&\texttt{tsubst}
\\
term
&\texttt{tsubst} and \texttt{osubst}
\\
formula
&\texttt{tsubst} and \texttt{osubst} and \texttt{psubst}
\\
proof
&\texttt{tsubst} and \texttt{osubst} and \texttt{psubst} and \texttt{asubst}
\\
\hline
\end{tabular}
\]

In particular, for \indexentry{type substitutions} \texttt{tsubst}
we have
\begin{alignat*}{2}
&\texttt{(type-substitute \textsl{type} \textsl{tsubst})}%
\index{type-substitute@\texttt{type-substitute}} 
\\
&\texttt{(type-subst \textsl{type} \textsl{tvar} \textsl{type1})}%
\index{type-subst@\texttt{type-subst}} 
\\
&\texttt{(compose-t-substitutions \textsl{tsubst1} \textsl{tsubst2})}%
\index{compose-t-substitutions@\texttt{compose-t-substitutions}} 
\end{alignat*}
A display function for type substitutions is
\begin{align*}
&\texttt{(display-t-substitution \textsl{tsubst})}%
\index{display-t-substitution@\texttt{display-t-substitution}} 
\end{align*}

\subsection{Simultaneous free algebras as base types}
We allow the formation of inductively generated types $\mu
\vec{\alpha}\,\vec{\kappa}$, where $\vec{\alpha} =
\alpha_1,\dots,\alpha_n$ is a list of distinct type variables, and
$\vec{\kappa}$ is a list of \inquotes{constructor types} whose
argument types contain $\alpha_1,\dots,\alpha_n$ in strictly positive
positions only.

For instance, $\mu\alpha(\alpha, \alpha \to \alpha)$ is the type of
natural numbers; here the list $(\alpha, \alpha \to \alpha)$ stands
for two generation principles: $\alpha$ for \inquotes{there is a
natural number} (the number $0$), and $\alpha \to \alpha$ for
\inquotes{for every natural number there is another one} (its
successor).

Let an infinite supply of \emph{type variables} $\alpha, \beta$ be
given.  Let $\vec{\alpha} = (\alpha_j)_{j=1,\dots,m}$ be a list of
distinct type variables.  \emph{Types} $\rho, \sigma, \tau, \mu, \nu
\in \Types$ and \emph{constructor types} $\kappa \in
\constrtypes(\vec{\alpha})$ are defined inductively as follows.
\begin{align*}
&\frac{\vec{\rho}, \vec{\sigma}_1, \dots, \vec{\sigma}_n \in \Types}
{\vec{\rho} \to (\vec{\sigma}_1 \to \alpha_{j_1}) \to \dots
\to (\vec{\sigma}_n \to \alpha_{j_n}) \to \alpha_j \in 
\constrtypes(\vec{\alpha})} \quad\hbox{($n \ge 0$)}
\\
&\frac{\kappa_1, \dots, \kappa_n \in \constrtypes(\vec{\alpha})}
{(\mu \vec{\alpha}\,(\kappa_1, \dots, \kappa_n))_j \in \Types} 
\quad\hbox{($n \ge 1$, $j=1,\dots,m$)}\qquad
\frac{\rho, \sigma \in \Types}{\rho \to \sigma \in \Types}
\end{align*}
Here $\vec{\rho}$ is short for a list $\rho_1,\dots,\rho_k$ ($k\ge 0$)
of types and $\vec{\rho} \to \sigma$ means $\rho_1 \to \dots \to
\rho_k \to \sigma$, associated to the right.  We shall use $\mu, \nu$
for types of the form $(\mu \vec{\alpha}\,(\kappa_1, \dots,
\kappa_n))_j$ only, and for types $\vec{\tau}=
(\tau_j)_{j=1,\dots,m}$ and a constructor type $\kappa = \vec{\rho}
\to (\vec{\sigma}_1 \to \alpha_{j_1}) \to \dots \to (\vec{\sigma}_n
\to \alpha_{j_n}) \to \alpha_j \in \constrtypes(\vec{\alpha})$ let
\[
\kappa[\vec{\tau}] :=
\vec{\rho} \to (\vec{\sigma}_1 \to \tau_{j_1}) \to \dots \to
(\vec{\sigma}_n \to \tau_{j_n}) \to \tau_j.
\]

\begin{examples*}
\begin{alignat*}{2}
&\unit &&:= \mu \alpha\,\alpha,
\\
&\boole &&:= \mu \alpha\,(\alpha,\alpha),
\\
&\nat &&:= \mu \alpha\,(\alpha,\alpha \to \alpha),
\\
&\ytensor(\alpha_1)(\alpha_2) &&:= 
\mu \alpha.  \alpha_1 \to \alpha_2 \to \alpha,
\\
&\ypair(\alpha_1)(\alpha_2) &&:= 
\mu \alpha.  (\unit \to \alpha_1) \to (\unit \to \alpha_2) \to \unit \to 
\alpha,
\\
&\yplus(\alpha_1)(\alpha_2) &&:= 
\mu \alpha.  (\alpha_1 \to \alpha, \alpha_2 \to \alpha),
\\
&\lst(\alpha_1) &&:= \mu \alpha\,(\alpha,\alpha_1 \to \alpha \to \alpha),
\\
% &\rho \times \sigma &&:= \mu \alpha.\rho \to \sigma \to \alpha,
% \\
% &\rho + \sigma &&:= \mu \alpha\,(\rho \to \alpha, \sigma \to \alpha),
% \\
&(\tree, \tlist) &&:= \mu (\alpha,\beta)\,
(\alpha, \beta \to \alpha, \beta, \alpha \to \beta \to \beta),
\\
&\btree &&:= \mu \alpha\,(\alpha, \alpha \to \alpha \to \alpha),
\\
&\C{O} &&:= \mu \alpha\,
(\alpha, \alpha \to \alpha, (\nat \to \alpha) \to \alpha),
\\
&\C{T}_0 &&:= \nat,
\\
&\C{T}_{n+1} &&:= \mu \alpha\,(\alpha, (\C{T}_n \to \alpha) \to \alpha).
\end{alignat*}
Note that we could have defined our primitive $\rho \times \sigma$ by
$\mu \alpha.\rho \to \sigma \to \alpha$.  However, this may lead to
complex terms when it comes to extract programs from proofs.
Therefore we stick to using $\rho \times \sigma$ as a primitive.
\end{examples*}

% \subsection{Types of formulas}
% % We also have ground types \texttt{atomic}, \texttt{existential},
% \texttt{prop} and \texttt{top}; they will be used to assign types to
% formulas.  E.g.\ $\forall n\,n=0$ receives the type $\texttt{nat} \to
% \texttt{atomic}$, and $\forall n,m \ex k\,n+m=k$ receives the type
% $\texttt{nat} \to \texttt{nat} \to \texttt{existential}$.  (Logical)
% falsity $\bot$\index{falsity!logical} receives the type \texttt{top}.
% The ground type \texttt{prop} is used for predicate variables, e.g.\
% $R$ of arity \texttt{nat,nat -> prop}.  Types of formulas will be
% necessary for normalization by evaluation of proof terms.  Types not
% involving the ground types \texttt{atomic}, \texttt{existential},
% \texttt{prop} and \texttt{top} are called object types.

To add and remove names for type variables, we use
\begin{align*}
&\texttt{(add-tvar-name \textsl{name1} \dots)} 
\index{add-tvar-name@\texttt{add-tvar-name}}
\\
&\texttt{(remove-tvar-name \textsl{name1} \dots)} 
\index{remove-tvar-name@\texttt{remove-tvar-name}}
\end{align*}
We need a constructor, accessors and a test for type variables. 
\begin{alignat*}{2}
&\texttt{(make-tvar \textsl{index} \textsl{name})} 
&\quad& \text{constructor}
\\
&\texttt{(tvar-to-index \textsl{tvar})} && \text{accessor}
\index{tvar-to-index@\texttt{tvar-to-index}}
\\
&\texttt{(tvar-to-name \textsl{tvar})} && \text{accessor}
\index{tvar-to-name@\texttt{tvar-to-name}}
\\
&\texttt{(tvar?\ \textsl{x}).}
\index{tvar?@\texttt{tvar?}}
\end{alignat*}
To generate new type variables we use
\begin{align*}
&\texttt{(new-tvar \textsl{type})}
\index{new-tvar@\texttt{new-tvar}}
\end{align*}

% Ground types are added and removed by
% \begin{align*}
% % &\texttt{(add-ground-type \textsl{symbol} \textsl{symbol1} \dots)}
% \index{add-ground-type@\texttt{add-ground-type}}
% \\
% % &\texttt{(remove-ground-type \textsl{type})}.
% \index{remove-ground-type@\texttt{remove-ground-type}}
% % \end{align*}
% Executing \texttt{(add-ground-type \textsl{symbol} \textsl{symbol1}
% \dots)} causes \texttt{symbol} to be ad\-ded as name for the newly
% created ground type, and the optional symbols \textsl{symbol1} \dots
% to be reserved as names for variables of that type.  

To introduce simultaneous free algebras we use
\[
\texttt{add-algebras-with-parameters}
\index{add-algebras-with-parameters@\texttt{add-algebras-with-parameters}}, 
\quad \hbox{abbreviated
\texttt{add-param-algs}
\index{add-param-algs@\texttt{add-param-algs}}}.
\]
An example is
\begin{verbatim}
(add-param-algs 
  (list "labtree" "labtlist") 'alg-typeop 2
  '("LabLeaf" "alpha1=>labtree")
  '("LabBranch" "labtlist=>alpha2=>labtree")
  '("LabEmpty" "labtlist")
  '("LabTcons" "labtree=>labtlist=>labtlist" pairscheme-op))
\end{verbatim}
This simultaneously introduces the two free algebras \texttt{labtree}
and \texttt{labtlist}, both finitary, whose constructors are
\texttt{LabLeaf}, \texttt{LabBranch}, \texttt{LabEmpty} and
\texttt{LabTcons} (written as an infix pair operator, hence right
associative).  The constructors are introduced as
\inquotes{self-evaluating} constants; they play a special role in our
semantics for normalization by evaluation.

In case there are no parameters we use \texttt{add-algs}%
\index{add-algs@\texttt{add-algs}}, and in case there is no
need for a simultaneous definition we use \texttt{add-alg}%
\index{add-alg@\texttt{add-alg}} or \texttt{add-param-alg}%
\index{add-param-alg@\texttt{add-param-alg}}.

For already introduced algebras we need constructors and accessors
\begin{align*}
&\texttt{(make-alg \textsl{name} \textsl{type1} \dots)}
\index{make-alg@\texttt{make-alg}}
\\
&\texttt{(alg-form-to-name \textsl{alg})}
\index{alg-form-to-name@\texttt{alg-form-to-name}}
\\
&\texttt{(alg-form-to-types \textsl{alg})}
\index{alg-form-to-types@\texttt{alg-form-to-types}}
\\
&\texttt{(alg-name-to-simalg-names \textsl{alg-name})}
\index{alg-name-to-simalg-names@\texttt{alg-name-to-simalg-names}}
\\
&\texttt{(alg-name-to-token-types \textsl{alg-name})}
\index{alg-name-to-token-types@\texttt{alg-name-to-token-types}}
\\
&\texttt{(alg-name-to-typed-constr-names \textsl{alg-name})}
\index{alg-name-to-typed-constr-names@\texttt{alg-name-to-typed-constr-names}}
\\
&\texttt{(alg-name-to-tvars \textsl{alg-name})}
\index{alg-name-to-tvars@\texttt{alg-name-to-tvars}}
\\
&\texttt{(alg-name-to-arity \textsl{alg-name})}
\index{alg-name-to-arity@\texttt{alg-name-to-arity}}
\end{align*}
We also provide the tests
\begin{alignat*}{2}
&\texttt{(alg-form?\ \textsl{x})} &\quad& \text{incomplete test}
\index{alg-form?@\texttt{alg-form?}}
\\
&\texttt{(alg?\ \textsl{x})} && \text{complete test}
\index{alg?@\texttt{alg?}}
\\
&\texttt{(finalg?\ \textsl{type})} && \text{incomplete test}
\index{finalg?@\texttt{finalg?}}
\\
&\texttt{(ground-type?\ \textsl{x})} && \text{incomplete test}
\index{ground-type?@\texttt{ground-type?}}
\end{alignat*}

We require that there is at least one nullary constructor in every
free algebra; hence, it has a \inquotes{canonical inhabitant}.  For
arbitrary types this need not be the case, but occasionally
(e.g.\ for general logical problems, like to prove the drinker
formula) it is useful.  Therefore
\begin{align*}
&\texttt{(make-inhabited \textsl{type} \textsl{term1} \dots)}
\index{make-inhabited@\texttt{make-inhabited}}
\end{align*}
marks the optional term as the canonical inhabitant if it is provided,
and otherwise creates a new constant of that type, which is taken to
be the canonical inhabitant.  We also have
\[
\texttt{(type-to-canonical-inhabitant \textsl{type})},
\]
which returns the canonical inhabitant; it is an error to apply this
procedure to a non-inhabited type.  We do allow non-inhabited types to
be able to implement some aspects of
\cite{Hofmann99,AehligSchwichtenberg00}

To remove names for algebras we use
\begin{align*}
&\texttt{(remove-alg-name \textsl{name1} \dots)} 
\index{remove-alg-name@\texttt{remove-alg-name}}
\end{align*}

\textbf{Examples.}
Standard examples for finitary free algebras are the type \texttt{nat}
of unary natural numbers, and the type \texttt{btree} of binary
trees.  The domain $\C{I}_{\texttt{nat}}$ of unary natural
numbers is defined (as in \cite{BergerEberlSchwichtenberg03}) as a
solution to a domain equation.

We always provide the finitary free algebra \texttt{unit} consisting
of exactly one element, and \texttt{boole} of booleans; objects of
the latter type are (cf.\ loc.\ cit.)\ \texttt{true}, \texttt{false} and
families of terms of this type, and in addition the bottom object of
type \texttt{boole}.

Tests:
\begin{align*}
% &\texttt{(alg?\ \textsl{type})%
% \index{alg?@\texttt{alg?}}} \\
% %
% &\texttt{(finalg?\ \textsl{type})%
% \index{finalg?@\texttt{finalg?}}}\\
%
% &\texttt{(ground-type?\ \textsl{type})}
% \index{ground-type?@\texttt{ground-type?}}\\
&\texttt{(arrow-form?\ \textsl{type})}
\index{arrow-form?@\texttt{arrow-form?}}
\\
&\texttt{(star-form?\ \textsl{type})}
\index{star-form?@\texttt{star-form?}}
\\
&\texttt{(object-type?\ \textsl{type})}    
\index{object-type?@\texttt{object-type?}}
\end{align*}

We also need constructors and accessors for arrow types 
\begin{alignat*}{2}
&\texttt{(make-arrow \textsl{arg-type} \textsl{val-type})}      
\index{make-arrow@\texttt{make-arrow}}
&\quad& \text{constructor} 
\\
&\texttt{(arrow-form-to-arg-type \textsl{arrow-type})} 
\index{arrow-form-to-arg-type@\texttt{arrow-form-to-arg-type}}
&& \text{accessor} 
\\
&\texttt{(arrow-form-to-val-type \textsl{arrow-type})} 
\index{arrow-form-to-val-type@\texttt{arrow-form-to-val-type}}
&& \text{accessor}
\end{alignat*}
and star types
\begin{alignat*}{2}
&\texttt{(make-star \textsl{type1} \textsl{type2})}             
\index{make-star@\texttt{make-star}}
&\quad& \text{constructor} 
\\
&\texttt{(star-form-to-left-type \textsl{star-type})}  
\index{star-form-to-left-type@\texttt{star-form-to-left-type}}
&& \text{accessor} 
\\
&\texttt{(star-form-to-right-type star-type)} 
\index{star-form-to-right-type@\texttt{star-form-to-right-type}}
&& \text{accessor.}   
\end{alignat*}
For convenience we also have
\begin{alignat*}{2}
&\texttt{(mk-arrow \textsl{type1} \dots\ \textsl{type})}
\index{mk-arrow@\texttt{mk-arrow}}
\\
&\texttt{(arrow-form-to-arg-types \textsl{type} <\textsl{n}>)} 
\index{arrow-form-to-arg-types@\texttt{arrow-form-to-arg-types}}
&\quad& \text{all (first $n$) argument types} 
\\
&\texttt{(arrow-form-to-final-val-type \textsl{type})}     
\index{arrow-form-to-final-val-type@\texttt{arrow-form-to-final-val-type}}
&& \text{type of final value.}
\end{alignat*}
To check and to display a type we have
\begin{align*}
&\texttt{(type?\ \textsl{x})}
\index{type?@\texttt{type?}}
\\
&\texttt{(type-to-string \textsl{type}).}
\index{type-to-string@\texttt{type-to-string}}
\end{align*}

\textbf{Implementation.}
Type variables are implemented as lists:
\[
\texttt{(tvar \textsl{index} \textsl{name})}.
\]


\section{Variables}
\mylabel{Variables}
A variable of an object type is interpreted by a continuous functional
(object) of that type.  We use the word \inquotes{variable} and not
\inquotes{program variable}, since continuous functionals are not
necessarily computable.  For readable in- and output, and also for
ease in parsing, we may reserve certain strings as names for variables of
a given type, e.g.\ $\texttt{n}, \texttt{m}$ for variables of type
\texttt{nat}.  Then also $\texttt{n0}, \texttt{n1}, \texttt{n2}, \dots,
\texttt{m0}, \dots$ can be used for the same purpose. 

In most cases we need to argue about existing (i.e.\ total) objects
only.  For the notion of totality we have to refer to \cite[Chapter
8.3]{Stoltenberg94}; particularly relevant here is exercise 8.5.7.  To
make formal arguments with quantifiers relativized to total objects
more managable, we use a special sort of variables intended to range
over such objects only.  For example, $\texttt{n0}, \texttt{n1},
\texttt{n2}, \dots, \texttt{m0}, \dots$ range over total natural
numbers, and $\verb#n^0#, \verb#n^1#, \verb#n^2#, \dots$ are general
variables.  We say that the \emph{degree of totality}\index{degree of
totality} for the former is $1$, and for the latter $0$.

% \subsection*{Interface}
% To add and remove names for variables of a given type (e.g.\
$\texttt{n}, \texttt{m}$ for variables of type \texttt{nat}), we use
\begin{align*}
&\texttt{(add-var-name \textsl{name1} \dots\ \textsl{type})} 
\index{add-var-name@\texttt{add-var-name}}
\\
&\texttt{(remove-var-name \textsl{name1} \dots\ \textsl{type})} 
\index{remove-var-name@\texttt{remove-var-name}}
\\
&\texttt{(default-var-name \textsl{type}).}
\index{default-var-name@\texttt{default-var-name}}
\end{align*}
The first variable name added for any given type becomes the default
variable name.  If the system creates new variables of this type, they
will carry that name.  For complex types it sometimes is necessary to
talk about variables of a certain type without using a specific name.
In this case one can use the empty string to create a so called
numerated variable (see below).  The parser is able to produce this
kind of canonical variables from type expressions.

We need a constructor, accessors and tests for variables. 
\begin{alignat*}{2}
&\texttt{(make-var \textsl{type} \textsl{index} \textsl{t-deg} \textsl{name})} &\quad& \text{constructor}
\\
&\texttt{(var-to-type \textsl{var})} && \text{accessor}
\index{var-to-type@\texttt{var-to-type}}
\\
&\texttt{(var-to-index \textsl{var})} && \text{accessor}
\index{var-to-index@\texttt{var-to-index}}
\\
&\texttt{(var-to-t-deg \textsl{var})} && \text{accessor}
\index{var-to-t-deg@\texttt{var-to-t-deg}}
\\
&\texttt{(var-to-name \textsl{var})} && \text{accessor}
\index{var-to-name@\texttt{var-to-name}}
\\
&\texttt{(var-form?\ \textsl{x})} && \text{incomplete test}
\index{var-form?@\texttt{var-form?}}
\\
&\texttt{(var?\ \textsl{x}).} && \text{complete test}
\index{var?@\texttt{var?}}
\end{alignat*}
It is guaranteed that \texttt{equal?} is a valid test for equality of
variables.  Moreover, it is guaranteed that parsing a displayed
variable reproduces the variable; the converse need not be the case
(we may want to convert it into some canonical form).

For convenience we have the function 
\begin{alignat*}{2}
&\texttt{(mk-var \textsl{type} <\textsl{index}> <\textsl{t-deg}>
 <\textsl{name}>).}
\index{mk-var@\texttt{mk-var}}
\end{alignat*}
The type is a required argument; however, the remaining arguments are
optional.  The default for the name string is the value returned by
\begin{alignat*}{2}
&\texttt{(default-var-name \textsl{type})}
\index{default-var-name@\texttt{default-var-name}}
\end{alignat*}
If there is no default name, a numerated variable is created.  The
default for the totality is \inquotes{total}.

Using the empty string as the name, we can create so called numerated
variables.  We further require that we can test whether a given
variable belongs to those special ones, and that from every numerated
variable we can compute its index:
\begin{align*}
&\texttt{(numerated-var?\ \textsl{var})}
\index{numerated-var?@\texttt{numerated-var}}
\\
&\texttt{(numerated-var-to-index \textsl{numerated-var}).}
\index{numerated-var-to-index@\texttt{numerated-var-to-index}}
\end{align*}
It is guaranteed that \texttt{make-var} used with the empty name string 
is a bijection
\[
\Types \times \D{N} \times \TDegs \to \NumVars
\]
with inverses \texttt{var-to-type}, \texttt{numerated-var-to-index}
and \texttt{var-to-t-deg}.
% \footnote{Here equality is to be understood as equality for the
% respective \inquotes{types}, e.g.\ the first equation is to be understood as
% % {\tt 
% (equal-vars?\ 
%  (type-and-index-to-var
%   (var-to-type numerated-var)
%   (numerated-var-to-index numerated-var)) 
%  numerated-var)
% }
% % is a truth value for every scheme object {\tt numerated-var} such that
% {\tt (numerated-var?\ numerated-var)} is a truth value.
% }% :
% % \begin{verbatim}
% (type-and-index-to-var
%  (var-to-type numerated-var)
%  (numerated-var-to-index numerated-var)) = numerated-var

% (var-to-type (type-and-index-to-var type index)) = type
% (numerated-var-to-index 
%  (type-and-index-to-var type index)) = index

% (numerated-var?\ (type-and-index-to-var type index)) = }t
% \end{verbatim}
Although these functions look like an ad hoc extension of the
interface that is convenient for normalization by evaluation, there is
also a deeper background: these functions can be seen as the
\inquotes{computational content} of the well-known phrase \inquotes{we
assume that there are infinitely many variables of every type}.
Giving a constructive proof for this statement would require to give
infinitely many examples of variables for every type.  This of course
can only be done by specifying a function (for every type) that
enumerates these examples.  To make the specification finite we
require the examples to be given in a uniform way, i.e.\ by a function
of two arguments.  To make sure that all these examples are in fact
different, we would have to require \texttt{make-var} to
be injective.  Instead, we require (classically equivalent)
\texttt{make-var} to be a bijection on its image, as
again, this can be turned into a computational statement by requiring
that a witness (i.e.\ an inverse function) is given.

Finally, as often the exact knowledge of infinitely many variables of
every type is not needed we require that, either by using the above
functions or by some other form of definition, functions
\begin{align*}
&\texttt{(type-to-new-var \textsl{type})}
\index{type-to-new-var@\texttt{type-to-new-var}}
\\
&\texttt{(type-to-new-partial-var \textsl{type})}
\index{type-to-new-partial-var@\texttt{type-to-new-partial-var}}
\end{align*}
are defined that return a (total or partial) variable of the requested
type, different from all variables that have ever been returned by any
of the specified functions so far.

Occasionally we may want to create a new variable with the same name
(and degree of totality) as a given one.  This is useful e.g.\ for
bound renaming.  Therefore we supply
\begin{align*}
&\texttt{(var-to-new-var \textsl{var}).}
\index{var-to-new-var@\texttt{var-to-new-var}}
\end{align*}

\textbf{Implementation.}
Variables are implemented as lists:
\[
\texttt{(var \textsl{type} \textsl{index} \textsl{t-deg} \textsl{name})}.
\]


\section{Constants}
\mylabel{Pconst}
Every constant (or more precisely, object constant) has a type and
denotes a computable (hence continuous) functional of that type.  We
have the following three kinds of constants:
\begin{itemize}
\item constructors, kind \texttt{constr},
\item constants with user defined rules (also called program(mable)
  constant, or pconst), kind \texttt{pconst},
\item constants whose rules are fixed, kind \texttt{fixed-rules}.
\end{itemize}
The latter are built into the system: recursion operators for
arbitrary algebras, equality and existence operators for finitary
algebras, and existence elimination.  They are typed in parametrized
form, with the actual type (or formula) given by a type (or type and
formula) substitution that is also part of the constant.  For
instance, equality is typed by $\alpha \to \alpha \to \boole$ and a
type substitution $\alpha \mapsto \rho$.  This is done for clarity
(and brevity, e.g.\ for large $\rho$ in the example above), since one
should think of the type of a constant in this way.

For constructors and for constants with fixed rules, by efficiency
reasons we want to keep the object denoted by the constant (as needed
for normalization by evaluation) as part of it.  It depends on the
type of the constant, hence must be updated in a given proof whenever
the type changes by a type substitution.

\subsection{Rewrite and computation rules for program constants}
\mylabel{SS:RewCompRules}
For every program constant $c^\rho$ we assume that some rewrite rules
of the form $c\vec{K} \cnv N$ are given, where $\FV(N) \subseteq
\FV(\vec{K})$ and $c\vec{K}$, $N$ have the same type (not necessarily
a ground type).  Moreover, for any two rules $c\vec{K} \cnv N$ and
$c\vec{K}' \cnv N'$ we require that $\vec{K}$ and $\vec{K}'$ are of
the same length, called the \emph{arity}\index{arity!of a program
constant} of $c$.  The rules are divided into \emph{computation
rules}\index{computation rule} and proper \emph{rewrite
rules}\index{rewrite rule}.  They must satisfy the requirements listed
in \cite{BergerEberlSchwichtenberg03}.  The idea is that a computation
rule can be understood as a description of a computation in a suitable
\emph{semantical} model, provided the syntactic constructors
correspond to semantic ones in the model, whereas the other rules
describe \emph{syntactic} transformations.

There a more general approach was used: one may enter into components
of products.  Then instead of one arity one needs several
\inquotes{type informations} $\vec{\rho} \to \sigma$ with $\vec{\rho}$
a list of types, $0$'s and $1$'s indicating the left or right part of
a product type.  For example, if $c$ is of type $\tau \to (\tau \to
\tau \to \tau) \times (\tau \to \tau)$, then the rules $cy0xx \cnv a$
and $cy1 \cnv b$ are admitted, and $c$ comes with the type
informations $(\tau,0,\tau,\tau \to \tau) \to \tau$ and $(\tau,1) \to
(\tau \to \tau)$. -- However, for simplicity we only deal with a
single arity here.

Given a set of rewrite rules, we want to treat some rules - which we
call \indexentry{computation rules} - in a different, more efficient
way.  The idea is that a computation rule can be understood as a
description of a computation in a suitable 
\indexentry{semantical model}, provided the syntactic constructors 
correspond to semantic ones in the model, whereas the other rules
describe \emph{syntactic} transformations.

In order to define what we mean by computation rules, we need the
notion of a \indexentry{constructor pattern}.  These are special terms
defined inductively as follows.
\begin{itemize}
\item  Every variable is a constructor pattern.
\item If $c$ is a constructor and $P_1,\dots,P_n$ are constructor
patterns (or projection markers 0 or 1), such that $c \vec{P}$ is of
ground type, then $c\vec{P}$ is a constructor pattern.
\end{itemize}
From the given set of rewrite rules we choose a subset $\Comp$
with the following properties.
\begin{itemize}
\item If $c\vec{P} \cnv Q \in \Comp$, then $P_1,\dots,P_n$ are constructor 
patterns or projection markers.
\item The rules are left-linear, i.e.\ if $c\vec{P} \cnv Q \in \Comp$,
then every variable in $c\vec{P}$ occurs only once in $c\vec{P}$.
\item The rules are non-overlapping, i.e.~for different rules 
$c\vec{K}\cnv M$ and $c\vec{L}\cnv N$ in $\Comp$ the left hand sides
$c\vec{K}$ and $c\vec{L}$ are non-unifiable.
\end{itemize}
We write $c\vec{M} \cnv_{\comp} Q$ to indicate that the rule is in
$\Comp$.  All other rules will be called (proper) rewrite rules,
written $c\vec{M} \cnv_{\rew} K$.

In our reduction strategy computation rules will always be applied
first, and since they are non-overlapping, this part of the reduction
is unique.  However, since we allowed almost arbitrary rewrite rules,
it may happen that in case no computation rule applies a term may be
rewritten by different rules $\notin \Comp$.  In order to obtain a
deterministic procedure we then select the first applicable rewrite rule
(This is a slight simplification of \cite{BergerEberlSchwichtenberg03},
where special functions $\select_c$ were used for this purpose).

\subsection{Recursion over simultaneous free algebras}
\mylabel{SS:RecSFA}
We now explain what we mean by recursion\index{recursion} over
simultaneous free algebras.  The inductive structure of the types
$\vec{\mu} = \mu\vec{\alpha}\,\vec{\kappa}$ corresponds to two sorts
of constants.  With the \emph{constructors} $\constr_i^{\vec{\mu}}
\colon \kappa_i[\vec{\mu}]$ we can construct elements of a type
$\mu_j$, and with the \emph{recursion operators}\index{recursion
operator} $\rec_{\mu_j}^{\vec{\mu}, \vec{\tau}}$ we can construct
mappings from $\mu_j$ to $\tau_j$ by recursion on the structure of
$\vec{\mu}$.  So in \texttt{(Rec arrow-types)},
\texttt{arrow-types} is a list $\mu_1 \to \tau_1, \dots, \mu_k \to
\tau_k$.  Here $\mu_1, \dots, \mu_k$ are the algebras defined
simultaneously and $\tau_1, \dots, \tau_k$ are the result types.

For convenience in our later treatment of proofs (when we want to
normalize a proof by (1) translating it into a term, (2) normalizing
this term and (3) translating the normal term back into a proof), we
also allow all-formulas $\forall x_1^{\mu_1} A_1, \dots, \forall
x_k^{\mu_k} A_k$ instead of \texttt{arrow-types}: they are treated as
$\mu_1 \to \tau(A_1)$, \dots, $\mu_k \to \tau(A_k)$ with $\tau(A_j)$
the type of $A_j$.

Recall the definition of types and constructor types in
Section~\ref{S:Types}, and the examples given there.  In order to define
the type of the recursion operators w.r.t.\ $\vec{\mu} =
\mu\vec{\alpha}\, \vec{\kappa}$ and result types $\vec{\tau}$, we
first define for
\[
\kappa_i = \vec{\rho} \to (\vec{\sigma}_1 \to \alpha_{j_1}) \to \dots \to
(\vec{\sigma}_n \to \alpha_{j_n}) \to \alpha_j \in
\constrtypes(\vec{\alpha})
\]
the \emph{step type}
\begin{align*}
\ST_i^{\vec{\mu}, \vec{\tau}} := \vec{\rho} \to 
&(\vec{\sigma}_1 \to \mu_{j_1}) \to \dots \to
(\vec{\sigma}_n \to \mu_{j_n}) \to 
\\
&(\vec{\sigma}_1 \to \tau_{j_1}) \to \dots \to
(\vec{\sigma}_n \to \tau_{j_n}) \to \tau_j.
\end{align*}
Here $\vec{\rho}, (\vec{\sigma}_1 \to \mu_{j_1}), \dots,
(\vec{\sigma}_n \to \mu_{j_n})$ correspond to the \emph{components}
% (or \emph{parameters}) 
of the object of type $\mu_j$ under
consideration, and $(\vec{\sigma}_1 \to \tau_{j_1}), \dots,
(\vec{\sigma}_n \to \tau_{j_n})$ to the previously defined values.
The recursion operator $\rec_{\mu_j}^{\vec{\mu}, \vec{\tau}}$ has type
\[
\rec_{\mu_j}^{\vec{\mu}, \vec{\tau}} \colon
\ST_1^{\vec{\mu}, \vec{\tau}} \to \dots \to \ST_k^{\vec{\mu}, \vec{\tau}}
\to \mu_j \to \tau_j.
\]

We will often write $\rec_j^{\vec{\mu}, \vec{\tau}}$ for
$\rec_{\mu_j}^{\vec{\mu}, \vec{\tau}}$, and omit the upper indices
$\vec{\mu}, \vec{\tau}$ when they are clear from the context.  In case
of a non-simultaneous free algebra, i.e.\ of type $\mu
\alpha\,(\kappa)$, for $\rec_\mu^{\mu, \tau}$ we normally write
$\rec_\mu^\tau$.

A simple example for simultaneous free algebras is
\[
(\tree, \tlist) := \mu (\alpha,\beta)\,
(\alpha, \beta \to \alpha, \beta, \alpha \to \beta \to \beta).
\]
The constructors are
\begin{align*}
&\leaf^{\tree} := \constr_1^{(\tree, \tlist)},
\\
&\branch^{\tlist \to \tree} := \constr_2^{(\tree, \tlist)},
\\
&\empt^{\tlist} := \constr_3^{(\tree, \tlist)},
\\
&\tcons^{\tree \to \tlist \to \tlist} := \constr_4^{(\tree, \tlist)}.
\end{align*}
An example for a recursion constant is
\begin{alignat*}{2}
&\texttt{(const Rec $\delta_1 \to \delta_2 \to \delta_3 \to \delta_4 \to 
\tree \to \alpha_1$}
\\
&\qquad \qquad \qquad 
\texttt{$(\alpha_1 \mapsto \tau_1, \alpha_2 \mapsto \tau_2)$)} 
\index{Rec@\texttt{Rec}}
\\
\intertext{with}
&\delta_1 := \alpha_1,
\\
&\delta_2 := \tlist \to \alpha_2 \to \alpha_1,
\\
&\delta_3 := \alpha_2,
\\
&\delta_4 := \tree \to \tlist \to \alpha_1 \to \alpha_2 \to \alpha_2.
\end{alignat*}
Here the fact that we deal with a simultaneous recursion (over
\texttt{tree} and \texttt{tlist}), and that we define a constant of
type $\tree \to \dots$, can all be inferred from what is given: the
type $\tree \to \dots$ is right there, and for \texttt{tlist} we can
look up the simultaneously defined algebras.

For the external representation (i.e.\ display) we use the shorter
notation
\[
\texttt{(Rec $\tree \to \tau_1$ $\tlist \to \tau_2$)}.
\]
% $$\texttt{(Rec $\tree \to \alpha_1$ $\tlist \to \alpha_2$ $(\alpha_1
% \mapsto \tau_1, \alpha_2 \mapsto \tau_2)$)}.$$

% A simplified version (without the recursive calls) of the recursion
% operator is the following generalized if-then-else operator.
% \begin{alignat*}{2}
% % &\texttt{(const If $\alpha_1 \to \alpha_1 \to \tree \to \alpha_1$
% $(\alpha_1 \mapsto \tau_1)$).} 
% \index{If@\texttt{If}}
% % \end{alignat*}
% A shorter notation would be $\texttt{(if-at $\tree \to \tau_1$)}$, but
% again we prefer the more systematic one above.

As already mentioned, it is also possible that the object constant
\texttt{Rec} comes with formulas instead of types, as the assumption
constant \texttt{Ind} below.  This is due to our desire not to
duplicate code when normalizing proofs, but rather translate the proof
into a term first, normalize the term and then translate back into a
proof.  For the last step we must have the original formulas of the
induction operator available.

To see a concrete example, let us recursively define addition $+
\colon \tree \to \tree \to \tree$ and $\oplus \colon \tlist \to \tree
\to \tlist$.  The recursion equations to be satisfied are
\begin{alignat*}{2}
&+\,\leaf &&= \lambda a a,
\\
&+(\branch\,\bs) &&= \lambda a.\branch(\oplus\,\bs\,a),\\[6pt]
&\oplus\,\empt &&= \lambda a\,\empt,
\\
&\oplus(\tcons\,b\,\bs) &&= \lambda a.\tcons(+\,b\,a)(\oplus\,\bs\,a).
\end{alignat*}
We define $+$ and $\oplus$ by means of the recursion operators
$\rec_{\tree}$ and
$\rec_{\tlist}$ with result types
\begin{align*}
\tau_1 &:= \tree \to \tree,
\\
\tau_2 &:= \tree \to \tlist.
\end{align*}
The step terms are
\begin{align*}
M_1 &:= \lambda a a,
\\
M_2 &:= \lambda \bs \lambda g^{\tau_2} \lambda a.\branch(g\,a),
\\
M_3 &:= \lambda a\,\empt,
\\
M_4 &:= \lambda b \lambda \bs \lambda f^{\tau_1} \lambda g^{\tau_2} \lambda a.
\tcons(f\,a)(g\,a).
\end{align*}
Then
\begin{align*}
+ &:= \rec_{\tree} \vec{M} \colon 
\tree \to \tree \to \tree,
\\
\oplus &:= \rec_{\tlist} \vec{M} \colon 
\tlist \to \tree \to \tlist.
\end{align*}

To explain the \emph{conversion relation}\index{conversion relation},
it will be useful to employ the following notation.  Let
$\vec{\mu} = \mu \vec{\alpha}\,\vec{\kappa}$,
\[
\kappa_i = \rho_1 \to \dots \to \rho_m \to 
(\vec{\sigma}_1 \to \alpha_{j_1}) \to \dots \to
(\vec{\sigma}_n \to \alpha_{j_n}) \to \alpha_j \in
\constrtypes(\vec{\alpha}),
\]
and consider $\constr_i^{\vec{\mu}} \vec{N}$.  Then we write
$\vec{N}^P = N_1^P, \dots, N_m^P$ for the \emph{parameter arguments}
$N_1^{\rho_1}, \dots, N_m^{\rho_m}$ and $\vec{N}^R = N_1^R, \dots,
N_n^R$ for the \emph{recursive arguments} $N_{m+1}^{\vec{\sigma}_1 \to
\mu_{j_1}}, \dots, N_{m+n}^{\vec{\sigma}_n \to \mu_{j_n}}$, and
$n^R$ for the number $n$ of recursive arguments.

We define a \emph{conversion relation} $\cnv_\rho$ between terms of
type $\rho$ by
\begin{align}
(\lambda xM)N &\cnv \subst{M}{x}{N}\label{betaconv}
\\
\lambda x.Mx &\cnv M\quad\hbox{if $x \notin \FV(M)$,
$M$ not an abstraction}\label{etaconv}
\\
(\rec_j^{\vec{\mu}, \vec{\tau}} \vec{M})^{\mu_j \to \tau_j}
(\constr_i^{\vec{\mu}} \vec{N}) &\cnv
M_i \vec{N}
\bigl( (\rec_{j_1}^{\vec{\mu}, \vec{\tau}} \vec{M}) \circ N_1^R\bigr) \dots
\bigl( (\rec_{j_n}^{\vec{\mu}, \vec{\tau}} \vec{M}) \circ N_n^R\bigr)
\label{recconv}
\end{align}
Here we have written $\rec_j^{\vec{\mu}, \vec{\tau}}$ for
$\rec_{\mu_j}^{\vec{\mu}, \vec{\tau}}$, and $\circ$ means composition.

\subsection{Internal representation of constants}
Every object constant has the internal representation
\begin{align*}
\texttt{(const\ } 
&\hbox{ \textsl{object-or-arity} \textsl{name} \textsl{uninst-type-or-formula} 
\textsl{subst}}
\\
&\hbox{\textsl{t-deg} \textsl{token-type} 
\textsl{arrow-types-or-repro-formulas}\texttt{)},}
\end{align*}
where \textsl{subst} may have type, object and assumption variables in
its domain.  The type of the constant is the result of carrying out
this substitution in \textsl{uninst-type-or-formula} (if this is a
type; otherwise first substitute and then convert the formula into a
type); free type variables may again occur in this type.  Note that a
formula will occur if \textsl{name} is \texttt{Ex-Intro} or
\texttt{Ex-Elim}, and may occur if it is \texttt{Rec}.
Examples for object constants are
\begin{alignat*}{2}
&\texttt{(const Compose $(\alpha {\to} \beta) {\to} (\beta {\to} \gamma) {\to}
\alpha {\to} \gamma$ 
$(\alpha \mapsto \rho, \beta \mapsto \sigma, \gamma \mapsto \tau)$ \dots)}
\index{Compose@\texttt{Compose}}
\\
&\texttt{(const Eq $\alpha \to \alpha \to \boole$ 
$(\alpha \mapsto \textsl{finalg})$ \dots)} 
\index{Eq@\texttt{Eq}}
\\
&\texttt{(const E $\alpha \to \boole$ 
$(\alpha \mapsto \textsl{finalg} \dots)$)} 
\index{E@\texttt{E}}
\\
&\texttt{(const Ex-Elim $\ex x^\alpha P(x) \to (\forall x^\alpha.  P(x)
\to Q) \to Q$}
\\ 
&\qquad\qquad\qquad\quad \texttt{$(\alpha \mapsto \tau, P^{(\alpha)}
\mapsto \set{z^\tau}{A}, Q \mapsto \set{}{B})$ \dots)}
\index{Ex-Elim@\texttt{Ex-Elim}}
\end{alignat*}
\textsl{object-or-arity} is an object if this object cannot be
changed, e.g.\ by allowing user defined rules for the constant;
otherwise, the associated object needs to be updated whenever a new
rule is added, and we have the arity of those rules instead.  The
rules are of crucial importance for the correctness of a proof, and
should not be invisibly buried in the denoted object taken as part of
the constant (hence of any term involving it).  Therefore we keep the
rules of a program constant and also its denoted objects (depending on
type substitutions) at a central place, a global variable
\texttt{PROGRAM-CONSTANTS} which assigns to every name of such a
constant the constant itself (with uninstantiated type), the rules
presently chosen for it and also its denoted objects (as association
list with type substitutions as keys).  When a new rule has been
added, the new objects for the program constant are computed, and the
new list to be associated with the program constant is written in
\texttt{PROGRAM-CONSTANTS} instead.  All information on a program
constant exept its denoted object and its computation and rewrite
rules (i.e.\ its type, degree of totality, arity and token type) is
stable and hence can be kept as part of it.  The \emph{token
type}\index{token type} can be either \texttt{const} (i.e.\ constant
written as application) or one of: \texttt{postfix-op},
\texttt{prefix-op}, \texttt{binding-op}, \texttt{add-op},
\texttt{mul-op}, \texttt{rel-op}, \texttt{and-op}, \texttt{or-op},
\texttt{imp-op} and \texttt{pair-op}.

Constructor, accessors and tests for all kinds of constants:
\begin{alignat*}{2}
&\texttt{(make-const \textsl{obj-or-arity} \textsl{name} \textsl{kind} 
\textsl{uninst-type} \textsl{tsubst}}
\\
&\quad \texttt{\textsl{t-deg} \textsl{token-type}
. \textsl{arrow-types-or-repro-formulas})}%
\index{make-const@\texttt{make-const}}
% &\quad& \text{constructor} 
\\
&\texttt{(const-to-object-or-arity \textsl{const})}%
\index{const-to-object-or-arity@\texttt{const-to-object-or-arity}}
% && \text{accessor} 
\\
&\texttt{(const-to-name \textsl{const})}%
\index{const-to-name@\texttt{const-to-name}}
% && \text{accessor} 
\\
&\texttt{(const-to-kind \textsl{const})}%
\index{const-to-kind@\texttt{const-to-kind}}
% && \text{accessor} 
\\
&\texttt{(const-to-uninst-type \textsl{const})}%
\index{const-to-uninst-type@\texttt{const-to-uninst-type}}
% && \text{accessor} 
\\
&\texttt{(const-to-tsubst \textsl{const})}%
\index{const-to-tsubst@\texttt{const-to-tsubst}}
% && \text{accessor} 
\\
&\texttt{(const-to-t-deg \textsl{const})}%
\index{const-to-t-deg@\texttt{const-to-t-deg}}
% && \text{accessor} 
\\
&\texttt{(const-to-token-type \textsl{const})}%
\index{const-to-token-type@\texttt{const-to-token-type}}
% && \text{accessor} 
\\
&\texttt{(const-to-arrow-types-or-repro-formulas \textsl{const})}%
\index{const-to-arrow-types-or-repro-formulas@\texttt{const-to-arrow-types-or{\dots}}}
% && \text{accessor} 
\\
&\texttt{(const?\ \textsl{x})}%
\index{const?@\texttt{const?}}
% && \text{test} 
\\
&\texttt{(const=?\ \textsl{x} \textsl{y})}                       
\index{const=?@\texttt{const=?}}
% && \text{test.}
\end{alignat*}
The type substitution \textsl{tsubst} must be restricted to the type
variables in \texttt{uninst-type}.
\texttt{arrow-types-or-repro-formulas} are only present for the
\texttt{Rec} constants.  They are needed for the reproduction case.

From these we can define
\begin{alignat*}{2}
&\texttt{(const-to-type \textsl{const})}%
\index{const-to-type@\texttt{const-to-type}} 
\\
&\texttt{(const-to-tvars \textsl{const})}%
\index{const-to-tvars@\texttt{const-to-tvars}}
\end{alignat*}

A \emph{constructor}\index{constructor} is a special constant with no
rules.  We maintain an association list \texttt{CONSTRUCTORS}
assigning to every name of a constructor an association list
associating with every type substitution (restricted to the type
parameters) the corresponding instance of the constructor.  We provide
\begin{alignat*}{2}
&\texttt{(constr-name? \textsl{string})}%
\index{constr-name?@\texttt{constr-name?}}
\\ 
&\texttt{(constr-name-to-constr \textsl{name} <\textsl{tsubst}>)}%
\index{constr-name-to-constr@\texttt{constr-name-to-constr}}
\\ 
&\texttt{(constr-name-and-tsubst-to-constr \textsl{name} \textsl{tsubst})}%
\index{constr-name-and-tsubst-to-constr@\texttt{constr-name-and-tsubst{\dots}}},
\end{alignat*}
where in \texttt{(constr-name-to-constr \textsl{name}
<\textsl{tsubst}>)}, \textsl{name} is a string or else of the
form \texttt{(Ex-Intro \textsl{formula})}.  If the optional
\textsl{tsubst} is not present, the empty substitution is used.

For given algebras one can display the associated constructors with their
types by calling
\begin{alignat*}{2}
&\texttt{(display-constructors \textsl{alg-name1} \dots)}%
\index{display-constructors@\texttt{display-constructors}}.
\end{alignat*}

We also need procedures recovering information from the string denoting
a program constant (via \texttt{PROGRAM-CONSTANTS}):
\begin{alignat*}{2}
&\texttt{(pconst-name-to-pconst \textsl{name})}%
\index{pconst-name-to-pconst@\texttt{pconst-name-to-pconst}}
\\
&\texttt{(pconst-name-to-comprules \textsl{name})}%
\index{pconst-name-to-comprules@\texttt{pconst-name-to-comprules}}
\\
&\texttt{(pconst-name-to-rewrules \textsl{name})}%
\index{pconst-name-to-rewrules@\texttt{pconst-name-to-rewrules}}
\\
&\texttt{(pconst-name-to-inst-objs \textsl{name})}%
\index{pconst-name-to-inst-objs@\texttt{pconst-name-to-inst-objs}}
\\
&\texttt{(pconst-name-and-tsubst-to-object \textsl{name} \textsl{tsubst})}%
% \index{pconst-name-and-tsubst-to-object@\texttt{pconst-name-and-tsubst-to-object}}
\\
&\texttt{(pconst-name-to-object \textsl{name})}%
\index{pconst-name-to-object@\texttt{pconst-name-to-object}}.
\end{alignat*}

One can display the program constants together with their current
computation and rewrite rules by calling
\begin{alignat*}{2}
&\texttt{(display-program-constants \textsl{name1} \dots)}%
\index{display-program-constants@\texttt{display-program-constants}}.
\end{alignat*}

To add and remove program constants we use
\begin{align*}
&\texttt{(add-program-constant \textsl{name} \textsl{type} <\textsl{rest}>)}
\index{add-program-constant@\texttt{add-program-constant}}
\\
&\texttt{(remove-program-constant \textsl{symbol})};
\index{remove-program-constant@\texttt{remove-program-constant}}
\end{align*}
\textsl{rest} consists of an initial segment of the following list:
\texttt{t-deg} (default $0$), \texttt{token-type} (default
\texttt{const}) and \texttt{arity} (default maximal number of argument
types).

To add and remove computation and rewrite rules we have
\begin{align*}
&\texttt{(add-computation-rule \textsl{lhs} \textsl{rhs})} 
\index{add-computation-rule@\texttt{add-computation-rule}}
\\
&\texttt{(add-rewrite-rule \textsl{lhs} \textsl{rhs})}
\index{add-rewrite-rule@\texttt{add-rewrite-rule}}
\\
&\texttt{(remove-computation-rules-for \textsl{lhs})}
\index{remove-computation-rules-for@\texttt{remove-computation-rules-for}}
\\
&\texttt{(remove-rewrite-rules-for \textsl{lhs}).}
\index{remove-rewrite-rules-for@\texttt{remove-rewrite-rules-for}}
\end{align*}

To generate our constants with fixed rules we use
\begin{alignat*}{2}
&\texttt{(finalg-to-=-const \textsl{finalg})}            
\index{finalg-to-=-const@\texttt{finalg-to-=-const}}
&\quad& \text{equality} 
\\
&\texttt{(finalg-to-e-const \textsl{finalg})}            
\index{finalg-to-e-const@\texttt{finalg-to-e-const}}
&& \text{existence} 
\\
&\texttt{(arrow-types-to-rec-const .\ \textsl{arrow-types})}            
\index{arrow-types-to-rec-const@\texttt{arrow-types-to-rec-const}}
&& \text{recursion} 
\\
&\texttt{(ex-formula-and-concl-to-ex-elim-const }
\\
&\texttt{\qquad \textsl{ex-formula}
\textsl{concl})}%
\index{ex-formula-and-concl-to-ex-elim-const@\texttt{ex-for{\dots}-to-ex-elim-const}}
\end{alignat*}

Similarly to \texttt{arrow-types-to-rec-const} we also define the
procedure \texttt{all-formulas-to-rec-const}.  It will be used in to
achieve normalization of proofs via translating them in terms.

[Noch einf\"ugen: \texttt{arrow-types-to-cases-const} und zur
Behandlung von Beweisen \texttt{all-formulas-to-cases-const}]


\section{Predicate variables and constants}
\mylabel{S:Psyms}
\subsection{Predicate variables}
\mylabel{SS:PredVars}
A predicate variable of arity\index{arity!of a predicate variable}
$\rho_1, \dots, \rho_n$ is a placeholder for a formula $A$
with distinguished (different) variables $x_1, \dots, x_n$ of types
$\rho_1, \dots, \rho_n$.  Such an entity is called a
\indexentry{comprehension term}, written $\set{x_1, \dots, x_n}{A}$.
% We also allow predicate constants
% with a fixed intended meaning (e.g.\ $\bot$\index{bottom}).  Predicate
% variables and constants are both called predicate symbols.

Predicate variable names are provided in the form of an association
list, which assigns to the names their arities.  By default we have
the predicate variable \texttt{bot}\index{bottom} of arity
\texttt{(arity)}, called (logical) falsity.  It is viewed as a
predicate variable rather than a predicate constant, since (when
translating a classical proof into a constructive one) we want to
substitute for \texttt{bot}.

Often we will argue about \emph{Harrop formulas}\index{Harrop formula}
only, i.e.\ formulas without computational content.  For convenience
we use a special sort of predicate variables intended to range over
comprehension terms with Harrop formulas only.  For example,
$\texttt{P0}, \texttt{P1}, \texttt{P2}, \dots, \texttt{Q0}, \dots$
range over comprehension terms with Harrop formulas, and $\verb#P^0#,
\verb#P^1#, \verb#P^2#, \dots$ are general predicate variables.  We
say that \emph{Harrop degree}\index{Harrop degree} for the former is
$1$, and for the latter $0$.

% \subsection*{Interface}
We need constructors and accessors for arities
\begin{align*}
&\texttt{(make-arity \textsl{type1} \dots)}
\index{make-arity@\texttt{make-arity}}
\\
&\texttt{(arity-to-types \textsl{arity})}
\index{arity-to-types@\texttt{arity-to-types}}
\end{align*}
To display an arity we have
\[
\texttt{(arity-to-string \textsl{arity})}
\index{arity-to-string@\texttt{arity-to-string}}
\]

We can test whether a string is a name for a predicate variable, and
if so compute its associated arity:
\begin{align*}
&\texttt{(pvar-name?\ \textsl{string})}
\index{pvar-name?@\texttt{pvar-name?}}
\\
&\texttt{(pvar-name-to-arity \textsl{pvar-name})}
\index{pvar-name-to-arity@\texttt{pvar-name-to-arity}}
\end{align*}

To add and remove names for predicate variables of a given arity
(e.g.\ $\texttt{Q}$ for predicate variables of arity \texttt{nat}), we
use
\begin{align*}
&\texttt{(add-pvar-name \textsl{name1} \dots\ \textsl{arity})}%
\index{add-pvar-name@\texttt{add-pvar-name}}
\\
&\texttt{(remove-pvar-name \textsl{name1} \dots)}%
\index{remove-pvar-name@\texttt{remove-pvar-name}}
\end{align*}

We need a constructor, accessors and tests for predicate variables.
% Note that the arity is not necessary as an argument for
% \texttt{make-pvar}, since it can be read off from
% \texttt{pvar-name}.
\begin{alignat*}{2}
&\texttt{(make-pvar \textsl{arity} \textsl{index} \textsl{h-deg} 
\textsl{name})}
\index{make-pvar@\texttt{make-pvar}}
&\quad& \text{constructor}
\\
&\texttt{(pvar-to-arity \textsl{pvar})}
\index{pvar-to-arity@\texttt{pvar-to-arity}} 
&& \text{accessor}
\\
&\texttt{(pvar-to-index \textsl{pvar})} 
\index{pvar-to-index@\texttt{pvar-to-index}} 
&& \text{accessor}
\\
&\texttt{(pvar-to-h-deg \textsl{pvar})} 
\index{pvar-to-h-deg@\texttt{pvar-to-h-deg}} 
&& \text{accessor}
\\
&\texttt{(pvar-to-name \textsl{pvar})} 
\index{pvar-to-name@\texttt{pvar-to-name}} 
&& \text{accessor}
\\
&\texttt{(pvar?\ \textsl{x})} 
\index{pvar?@\texttt{pvar?}} 
\\
&\texttt{(equal-pvars?\ \textsl{pvar1} \textsl{pvar2})}
\index{equal-pvars?@\texttt{equal-pvars?}} 
\end{alignat*}

For convenience we have the function 
\begin{alignat*}{2}
&\texttt{(mk-pvar \textsl{arity} <\textsl{index}> <\textsl{h-deg}> 
<\textsl{name}>)}
\end{alignat*}
The arity is a required argument; the remaining arguments are
optional.  The default for \textsl{index} is $-1$, for \textsl{h-deg}
is $1$ (i.e.\ Harrop-formula) and for \textsl{name} it is given by
\texttt{(default-pvar-name \textsl{arity})}.

It is guaranteed that parsing a displayed predicate variable
reproduces the predicate variable; the converse need not be the case
(we may want to convert it into some canonical form).


\subsection{Predicate constants}
\mylabel{SS:PredConsts} 
We also allow \emph{predicate constants}\index{predicate constant}.
The general reason for having them is that we need predicates to be
axiomatized, e.g.\ \texttt{Equal} and \texttt{Total} (which are
\emph{not} placeholders for formulas).  Prime formulas built from
predicate constants do not give rise to extracted terms, and cannot be
substituted for.

Notice that a predicate constant does not change its name under a type
substitution; this is in contrast to predicate (and other) variables.
Notice also that the parser can infer from the arguments the types
$\rho_1 \dots \rho_n$ to be substituted for the type variables in the
uninstantiated arity of $P$.

% Discarded 01-08-20
% We also allow \indexentry{predicate constants}; they are viewed as
% constants with fixed rules.  For equality \texttt{Eq} and existence
% \texttt{Ex} there are such rules (e.g.\ $x=x \cnv T$), but for
% predicate constants intended to be axiomatized there are no such
% rules.  The need for predicate constants comes up when e.g.\ an
% inductively defined set is expressed via a formula stating the
% existence of a generation tree; the kernel of this formula is to be
% axiomatized, using the tree constructors.  Since predicate constants
% are constants with fixed rules, they do not give rise to extracted
% terms, and cannot be substituted for.

% A predicate constant does not change its name under a type
% substitution; this is in contrast to predicate (and other) variables.
% To enable the parser to infer its type, generally a predicate constant
% is to be displayed in the form $(P \rho_1 \dots \rho_n)$, where
% $\rho_1 \dots \rho_n$ are the types to be substituted for the type
% variables in the uninstantiated type of $P$.  However, quite often the
% type substitution can be inferred by the parser from the types of the
% arguments.  This is the case e.g.\ for equality and existence, where
% we can parse $x^{\alpha} = x^{\alpha}$ and $E x$ as well as $n^{\nat}
% = n^{\nat}$ and $E n$.  This happens quite regularly for all constants
% whose type involves type variables (i.e.\ of token type
% \texttt{constscheme} rather than \texttt{const}).

% \subsection*{Interface}
% 
To add and remove names for predicate constants of a given arity, we
use
\begin{align*}
&\texttt{(add-predconst-name \textsl{name1} \dots\ \textsl{arity})}%
\index{add-predconst-name@\texttt{add-predconst-name}}
\\
&\texttt{(remove-predconst-name \textsl{name1} \dots)}%
\index{remove-predconst-name@\texttt{remove-predconst-name}}
\end{align*}
We need a constructor, accessors and tests for predicate constants.
\begin{alignat*}{2}
&\texttt{(make-predconst \textsl{uninst-arity} \textsl{tsubst} \textsl{index} 
\textsl{name})}
\index{make-predconst@\texttt{make-predconst}}
&\quad& \text{constructor}
\\
&\texttt{(predconst-to-uninst-arity \textsl{predconst})}
\index{predconst-to-uninst-arity@\texttt{predconst-to-uninst-arity}} 
&& \text{accessor}
\\
&\texttt{(predconst-to-tsubst \textsl{predconst})} 
\index{predconst-to-tsubst@\texttt{predconst-to-tsubst}} 
&& \text{accessor}
\\
&\texttt{(predconst-to-index \textsl{predconst})} 
\index{predconst-to-index@\texttt{predconst-to-index}} 
&& \text{accessor}
\\
&\texttt{(predconst-to-name \textsl{predconst})} 
\index{predconst-to-name@\texttt{predconst-to-name}} 
&& \text{accessor}
\\
&\texttt{(predconst?\ \textsl{x})} 
\index{predconst?@\texttt{predconst?}} 
\end{alignat*}
Moreover we need
\begin{alignat*}{2}
&\texttt{(predconst-name? \textsl{name})}%
\index{predconst-name?@\texttt{predconst-name?}}
\\
&\texttt{(predconst-name-to-arity \textsl{predconst-name})}.%
\index{predconst-name-to-arity@\texttt{predconst-name-to-arity}}
\\
&\texttt{(predconst-to-string \textsl{predconst})}.%
\index{predconst-to-string@\texttt{predconst-to-string}}
\end{alignat*}


\subsection{Inductively defined predicate constants}
\mylabel{SS:IDPredConsts} 
As we have seen, type variables allow for a general treatment of
inductively generated types $\mu \vec{\alpha} \,\vec{\kappa}$.
Similarly, we can use predicate variables to inductively generate
predicates $\mu \vec{X} \,\vec{K}$.  

More precisely, we allow the formation of inductively generated
predicates $\mu \vec{X} \,\vec{K}$, where $\vec{X} =
(X_j)_{j=1,\dots,N}$ is a list of distinct predicate variables, and
$\vec{K} = (K_i)_{i=1,\dots,k}$ is a list of constructor formulas (or
\inquotes{clauses}\index{clause}) containing $X_1,\dots,X_N$ in
strictly positive positions only.

To introduce inductively defined predicates we use
\[
\texttt{add-ids}\index{add-ids@\texttt{add-ids}}.
\]
An example is
\begin{verbatim}
(add-ids (list (list "Ev" (make-arity (py "nat")) "algEv")
               (list "Od" (make-arity (py "nat")) "algOd"))
         '("Ev 0" "InitEv")
         '("allnc n.Od n -> Ev(n+1)" "GenEv")
         '("Od 1" "InitOd")
         '("allnc n.Ev n -> Od(n+1)" "GenOd"))
\end{verbatim}
This simultaneously introduces the two inductively defined predicate
constants \texttt{Ev} and \texttt{Od}, by the clauses given.  The
presence of an algebra name after the arity (here \texttt{algEv} and
\texttt{algOd}) indicates that this inductively defined predicate
constant is to have computational content.  Then all clauses with this
constant in the conclusion must provide a constructor name (here
\texttt{InitEv}, \texttt{GenEv}, \texttt{InitOd}, \texttt{GenOd}).  If
the constant is to have no computational content, then all its clauses
must be invariant (under realizability, a.k.a.\ \inquotes{negative}).

Here are some further examples of inductively defined predicates:
\begin{verbatim}
(add-ids 
  (list (list "Even" (make-arity (py "nat")) "algEven"))
  '("Even 0" "InitEven")
  '("allnc n.Even n -> Even(n+2)" "GenEven"))

(add-ids 
  (list (list "Acc" (make-arity (py "nat")) "algAcc"))
  '("allnc n.(all m.m<n -> Acc m) -> Acc n" "GenAccSup"))

(add-ids (list (list "OrID" (make-arity) "algOrID"))
         '("P^1 -> OrID" "InlOrID")
         '("P^2 -> OrID" "InrOrID"))

(add-ids 
  (list (list "EqID" (make-arity (py "alpha") (py "alpha")) 
              "algEqID"))
  '("allnc x^ EqID x^ x^" "GenEqID"))

(add-ids (list (list "ExID" (make-arity) "algExID"))
         '("allnc x^.Q^ x^ -> ExID" "GenExID"))

(add-ids 
  (list (list "FalsityID" (make-arity) "algFalsityID")))
\end{verbatim}


\section{Terms and objects}
\mylabel{Terms}
Terms are built from (typed) variables and constants by abstraction,
application, pairing, formation of left and right components (i.e.\
projections) and the \texttt{if}-construct.

The \texttt{if}-construct\index{if-construct@\texttt{if}-construct}
distinguishes cases according to the outer constructor form; the
simplest example (for the type \texttt{boole}) is \emph{if-then-else}.
Here we do not want to evaluate all arguments right away, but rather
evaluate the test argument first and depending on the result evaluate
at most one of the other arguments.  This phenomenon is well known in
functional languages; e.g.\ in \textsc{Scheme} the
\texttt{if}-construct is called a \emph{special form} as opposed to an
operator.  In accordance with this terminology we also call our
\texttt{if}-construct a special form\index{special form}.  It will be
given a special treatment in \texttt{nbe-term-to-object}.

Usually it will be the case that every closed term of an sfa ground
type reduces via the computation rules to a constructor term, i.e.\ a
closed term built from constructors only.  However, we do not require
this.

% \subsection*{Interface}
We have constructors, accessors and tests for variables
\begin{alignat*}{2}
&\texttt{(make-term-in-var-form var)}        
\index{make-term-in-var-form@\texttt{make-term-in-var-form}}
&\quad& \text{constructor} 
\\
% &\texttt{(term-in-var-form-to-string \textsl{term})}  
% \index{term-in-var-form-to-string@\texttt{term-in-var-form-to-string}}
% && \text{accessor,} \\
&\texttt{(term-in-var-form-to-var \textsl{term})}     
\index{term-in-var-form-to-var@\texttt{term-in-var-form-to-var}}
&& \text{accessor,} 
\\
&\texttt{(term-in-var-form?\ \textsl{term})}          
\index{term-in-var-form?@\texttt{term-in-var-form?}}
&& \text{test,}
\end{alignat*}
for constants
\begin{alignat*}{2}
&\texttt{(make-term-in-const-form \textsl{const})}    
\index{make-term-in-const-form@\texttt{make-term-in-const-form}}
&\quad& \text{constructor} 
\\
&\texttt{(term-in-const-form-to-const \textsl{term})} 
\index{term-in-const-form-to-const@\texttt{term-in-const-form-to-const}}
&& \text{accessor} 
\\
&\texttt{(term-in-const-form?\ \textsl{term})}         
\index{term-in-const-form?@\texttt{term-in-const-form?}}
&& \text{test,}
\end{alignat*}
for abstractions
\begin{alignat*}{2}
&\texttt{(make-term-in-abst-form \textsl{var} \textsl{term})}   
\index{make-term-in-abst-form@\texttt{make-term-in-abst-form}}
&\quad& \text{constructor} 
\\
&\texttt{(term-in-abst-form-to-var \textsl{term})}     
\index{term-in-abst-form-to-var@\texttt{term-in-abst-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(term-in-abst-form-to-kernel \textsl{term})}  
\index{term-in-abst-form-to-kernel@\texttt{term-in-abst-form-to-kernel}}
&& \text{accessor} 
\\
&\texttt{(term-in-abst-form?\ \textsl{term})}          
\index{term-in-abst-form?@\texttt{term-in-abst-form?}}
&& \text{test,}
\end{alignat*}
for applications
\begin{alignat*}{2}
&\texttt{(make-term-in-app-form \textsl{term1} \textsl{term2})} 
\index{make-term-in-app-form@\texttt{make-term-in-app-form}}
&\quad& \text{constructor} 
\\
&\texttt{(term-in-app-form-to-op \textsl{term})}       
\index{term-in-app-form-to-op@\texttt{term-in-app-form-to-op}}
&& \text{accessor} 
\\
&\texttt{(term-in-app-form-to-arg \textsl{term})}      
\index{term-in-app-form-to-arg@\texttt{term-in-app-form-to-arg}}
&& \text{accessor} 
\\
&\texttt{(term-in-app-form?\ \textsl{term})}           
\index{term-in-app-form?@\texttt{term-in-app-form?}}
&& \text{test,}
\end{alignat*}
for pairs
\begin{alignat*}{2}
&\texttt{(make-term-in-pair-form \textsl{term1} \textsl{term2})}  
\index{make-term-in-pair-form@\texttt{make-term-in-pair-form}}
&\quad& \text{constructor} 
\\
&\texttt{(term-in-pair-form-to-left \textsl{term})}      
\index{term-in-pair-form-to-left@\texttt{term-in-pair-form-to-left}}
&& \text{accessor} 
\\
&\texttt{(term-in-pair-form-to-right \textsl{term})}     
\index{term-in-pair-form-to-right@\texttt{term-in-pair-form-to-right}}
&& \text{accessor} 
\\
&\texttt{(term-in-pair-form?\ \textsl{term})}            
\index{term-in-pair-form?@\texttt{term-in-pair-form?}}
&& \text{test,}
\end{alignat*}
for the left and right component of a pair
\begin{alignat*}{2}
&\texttt{(make-term-in-lcomp-form \textsl{term})}        
\index{make-term-in-lcomp-form@\texttt{make-term-in-lcomp-form}}
&\quad& \text{constructor} 
\\
&\texttt{(make-term-in-rcomp-form \textsl{term})}        
\index{make-term-in-rcomp-form@\texttt{make-term-in-rcomp-form}}
&& \text{constructor} 
\\
&\texttt{(term-in-lcomp-form-to-kernel \textsl{term})}   
\index{term-in-lcomp-form-to-kernel@\texttt{term-in-lcomp-form-to-kernel}}
&& \text{accessor} 
\\
&\texttt{(term-in-rcomp-form-to-kernel \textsl{term})}   
\index{term-in-rcomp-form-to-kernel@\texttt{term-in-rcomp-form-to-kernel}}
&& \text{accessor} 
\\
&\texttt{(term-in-lcomp-form?\ \textsl{term})}           
\index{term-in-lcomp-form?@\texttt{term-in-lcomp-form?}}
&& \text{test} 
\\
&\texttt{(term-in-rcomp-form?\ \textsl{term})}           
\index{term-in-rcomp-form?@\texttt{term-in-rcomp-form?}}
&& \text{test}
\end{alignat*}
and for \texttt{if}-constructs
\begin{alignat*}{2}
&\texttt{(make-term-in-if-form \textsl{test} \textsl{alts} .\ \textsl{rest})}
\index{make-term-in-if-form@\texttt{make-term-in-if-form}}
&\quad& \text{constructor} 
\\
&\texttt{(term-in-if-form-to-test \textsl{term})}         
\index{term-in-if-form-to-test@\texttt{term-in-if-form-to-test}}
&& \text{accessor} 
\\
&\texttt{(term-in-if-form-to-alts \textsl{term})}         
\index{term-in-if-form-to-alts@\texttt{term-in-if-form-to-alts}}
&& \text{accessor} 
\\
&\texttt{(term-in-if-form-to-rest \textsl{term})}         
\index{term-in-if-form-to-rest@\texttt{term-in-if-form-to-rest}}
&& \text{accessor} 
\\
&\texttt{(term-in-if-form?\ \textsl{term})}               
\index{term-in-if-form?@\texttt{term-in-if-form?}}
&& \text{test.}
\end{alignat*}
where in \texttt{make-term-in-if-form}, \textsl{rest} is either empty
or an all-formula.

It is convenient to have more general application constructors and
accessors available, where application takes arbitrary many arguments
and works for ordinary application as well as for component formation.
\begin{alignat*}{2}
&\texttt{(mk-term-in-app-form \textsl{term} \textsl{term1} \dots)}
\index{mk-term-in-app-form@\texttt{mk-term-in-app-form}}
&\quad& \text{constructor} 
\\
&\texttt{(term-in-app-form-to-final-op \textsl{term})} 
\index{term-in-app-form-to-final-op@\texttt{term-in-app-form-to-final-op}}
&& \text{accessor} 
\\
&\texttt{(term-in-app-form-to-args \textsl{term})} 
\index{term-in-app-form-to-args@\texttt{term-in-app-form-to-args}}
&& \text{accessor,}
\end{alignat*}
Also for abstraction it is convenient to have a more general constructor
taking arbitrary many variables to be abstracted one after the other
\begin{alignat*}{2}
&\texttt{(mk-term-in-abst-form \textsl{var1} \dots\ \textsl{term})}.
\index{mk-term-in-abst-form@\texttt{mk-term-in-abst-form}}
\end{alignat*}
We also allow vector notation for recursion (cf.\ Joachimski and Matthes
\cite{JoachimskiMatthes03}).

Moreover we need
\begin{alignat*}{2}
&\texttt{(term?\ \textsl{x})}
\index{term?@\texttt{term?}}
\\
&\texttt{(term=?\ \textsl{term1} \textsl{term2})}
\index{term=?@\texttt{term=?}}
\\
&\texttt{(terms=?\ \textsl{terms1} \textsl{terms2})}
\index{terms=?@\texttt{terms=?}}
\\
&\texttt{(term-to-type \textsl{term})}
\index{term-to-type@\texttt{term-to-type}}
\\
&\texttt{(term-to-free \textsl{term})}
\index{term-to-free@\texttt{term-to-free}}
\\
&\texttt{(term-to-bound \textsl{term})}
\index{term-to-bound@\texttt{term-to-bound}}
\\
&\texttt{(term-to-t-deg \textsl{term})}
\index{term-to-t-deg@\texttt{term-to-t-deg}}
\\
&\texttt{(synt-total?\ \textsl{term})}
\index{synt-total?@\texttt{synt-total?}}
\\
&\texttt{(term-to-string \textsl{term})}.
\index{term-to-string@\texttt{term-to-string}}
\end{alignat*}

% To take care of arithmetical terms, we use
% \begin{alignat*}{2}
% %
% &\texttt{(mk-+ <terms>)}               \\
% &\texttt{(mk-- <terms>)}               \\
% &\texttt{(mk-max <terms>)}             \\
% &\texttt{(mk-min <terms>)}             \\
% &\texttt{(mk-* <terms>)} 
% %
% \end{alignat*}

\subsection{Normalization}
We need an operation which transforms a term into its normal form
w.r.t.\ the given computation and rewrite rules.  Here we base our
treatment on \emph{normalization by evaluation} introduced in
\cite{BergerSchwichtenberg91a}, and extended to arbitrary computation
and rewrite rules in \cite{BergerEberlSchwichtenberg03}.

For normalization by evaluation we need semantical \emph{objects}.
For an arbitrary ground type every term family of that type is an
object.  For an sfa ground type, in addition the constructors have
semantical counterparts.  The freeness of the constructors is
expressed by requiring that their ranges are disjoint and that they
are injective.  Moreover, we view the free algebra as a domain and
require that its bottom element is not in the range of the
constructors.  Hence the constructors are total and non-strict.  Then
by applying \texttt{nbe-reflect} followed by \texttt{nbe-reify} we can
normalize every term, where normalization refers to the computation as
well as the rewrite rules.

% \subsection*{Interface}
An object consists of a semantical value and a type.  
\begin{alignat*}{2}
&\texttt{(nbe-make-object \textsl{type} \textsl{value})} 
\index{nbe-make-object@\texttt{nbe-make-object}}
&\quad& \text{constructor} 
\\
&\texttt{(nbe-object-to-type \textsl{object})}  
\index{nbe-object-to-type@\texttt{nbe-object-to-type}}
&& \text{accessor} 
\\
&\texttt{(nbe-object-to-value \textsl{object})} 
\index{nbe-object-to-value@\texttt{nbe-object-to-value}}
&& \text{accessor} 
\\
&\texttt{(nbe-object?\ \textsl{x})}             
\index{nbe-object?@\texttt{nbe-object?}}
&& \text{test.}
\end{alignat*}
To work with objects, we need
\begin{alignat*}{2}
&\texttt{(nbe-object-apply \textsl{function-obj} \textsl{arg-obj})}
\index{nbe-object-apply@\texttt{nbe-object-apply}}
\end{alignat*}
Again it is convenient to have a more general application operation
available, which takes arbitrary many arguments and works for ordinary
application as well as for component formation. We also need an
operation composing two unary function objects.
\begin{alignat*}{2}
&\texttt{(nbe-object-app \textsl{function-obj} \textsl{arg-obj1} \dots)} 
\index{nbe-object-app@\texttt{nbe-object-app}} 
\\
&\texttt{(nbe-object-compose \textsl{function-obj1} \textsl{function-obj2})}
\index{nbe-object-compose@\texttt{nbe-object-compose}} 
\end{alignat*}
For ground type values we need constructors, accessors and tests.  To
make constructors \inquotes{self-evaluating}, a constructor value has
the form 
\[
\hbox{\texttt{(constr-value \textsl{name} \textsl{objs}
\textsl{delayed-constr})},}
\]
where \textsl{delayed-constr} is a procedure of zero arguments which
evaluates to this very same constructor.  This is necessary to avoid
having a cycle (for nullary constructors, and only for those).
\begin{alignat*}{2}
&\texttt{(nbe-make-constr-value \textsl{name} \textsl{objs})} 
\index{nbe-make-constr-value@\texttt{nbe-make-constr-value}}
&\quad& \text{constructor} 
\\
&\texttt{(nbe-constr-value-to-name \textsl{value})}    
\index{nbe-constr-value-to-name@\texttt{nbe-constr-value-to-name}}
&& \text{accessor} \\
&\texttt{(nbe-constr-value-to-args \textsl{value})}    
&& \text{accessor} 
\\
&\texttt{(nbe-constr-value-to-constr \textsl{value})}  
\index{nbe-constr-value-to-constr@\texttt{nbe-constr-value-to-constr}}
&& \text{accessor} 
\\
&\texttt{(nbe-constr-value?\ \textsl{value})}          
\index{nbe-constr-value?@\texttt{nbe-constr-value?}}
&& \text{test} 
\\
&\texttt{(nbe-fam-value?\ \textsl{value})}             
\index{nbe-fam-value?@\texttt{nbe-fam-value?}}
&& \text{test.}
\end{alignat*}
The essential function which \inquotes{animates}\index{animation} the
program constants according to the given computation and rewrite rules
is
\begin{align*}
&\texttt{(nbe-pconst-and-tsubst-and-rules-to-object}
\index{nbe-pconst-and-tsubst-and-rules-to-object@\texttt{nbe-pconst-{\dots}-to-object}}
\\
&\qquad \texttt{\textsl{pconst}\ \textsl{tsubst}\ \textsl{comprules}\  
\textsl{rewrules})}
\end{align*}
Using it we can the define an \indexentry{evaluation} function, which
assigns to a term and an environment a semantical object:
\begin{alignat*}{2}
&\texttt{(nbe-term-to-object \textsl{term} \textsl{bindings})} 
\index{nbe-term-to-object@\texttt{nbe-term-to-object}}
&\quad& \text{evaluation.}
\end{alignat*}
Here \textsl{bindings} is an association list assigning objects of the
same type to variables.  In case a variable is not assigned anything
in \textsl{bindings}, by default we assign the constant term family of
this variable, which always is an object of the correct type.

The interpretation of the program constants requires some auxiliary
functions (cf.\ \cite{BergerEberlSchwichtenberg03}):
\begin{alignat*}{2}
&\texttt{(nbe-constructor-pattern?\ \textsl{term})} 
\index{nbe-constructor-pattern?@\texttt{nbe-constructor-pattern?}}
&\quad& \text{test} 
\\
&\texttt{(nbe-inst?\ \textsl{constr-pattern} \textsl{obj})}  
\index{nbe-inst?@\texttt{nbe-inst?}}
&& \text{test} 
\\
&\texttt{(nbe-genargs \textsl{constr-pattern} \textsl{obj})} 
\index{nbe-genargs@\texttt{nbe-genargs}}
&& \text{generalized arguments} 
\\
% &\texttt{(nbe-select \textsl{pconst} \textsl{term})} 
% && \text{selects a rewrite rule} \\
&\texttt{(nbe-extract \textsl{termfam})} 
\index{nbe-extract@\texttt{nbe-extract}}
&& \text{extracts a term from a family} 
\\
&\texttt{(nbe-match \textsl{pattern} \textsl{term})}
\index{nbe-match@\texttt{nbe-match}}
\end{alignat*}
Then we can define
\begin{alignat*}{2}
&\texttt{(nbe-reify \textsl{object})}
\index{nbe-reify@\texttt{nbe-reify}}
&\quad& \text{reification} 
\\
&\texttt{(nbe-reflect \textsl{term})} 
\index{nbe-reflect@\texttt{nbe-reflect}}
&& \text{reflection}
\end{alignat*}
and by means of these
\begin{alignat*}{2}
&\texttt{(nbe-normalize-term \textsl{term})}
\index{nbe-normalize-term@\texttt{nbe-normalize-term}}
&\quad& \text{normalization,} 
\end{alignat*}
abbreviated \texttt{nt}\index{nt@\texttt{nt}}.

The \texttt{if}-form needs a special treatment.  In particular, for a
full normalization of terms (including permutative conversions), we
define a preprocessing step that $\eta$ expands the alternatives of
all \texttt{if}-terms.  The result contains \texttt{if}-terms with
ground type alternatives only.

\subsection{Substitution}
Recall the generalities on substitutions in Section~\ref{SS:GenSubst}.

We define simultaneous substitution for type and object variables in a
term, via \texttt{tsubst} and \texttt{subst}.  It is assumed that
\texttt{subst} only affects those vars whose type is not changed by 
\texttt{tsubst}.

In the abstraction case of the recursive definition, the abstracted
variable may need to be renamed.  However, its type can be affected by
\texttt{tsubst}.  Then the renaming cannot be made part of
\texttt{subst}, because the condition above would be violated.
Therefore we carry along a procedure renaming variables, which
remembers the renaming of variables done so far.
\begin{alignat*}{2}
&\texttt{(term-substitute \textsl{term} \textsl{tosubst})}%
\index{term-substitute@\texttt{term-substitute}} 
\\
&\texttt{(term-subst \textsl{term} \textsl{arg} \textsl{val})}%
\index{term-subst@\texttt{term-subst}} 
\\
&\texttt{(compose-o-substitutions \textsl{subst1} \textsl{subst2})}%
\index{compose-o-substitutions@\texttt{compose-o-substitutions}} 
\end{alignat*}
The \texttt{o} in \texttt{compose-o-substitutions} indicates that we
substitute for \emph{object} variables.  However, since this is the
most common form of substitution, we also write
\texttt{compose-substitutions}%
\index{compose-substitutions@\texttt{compose-substitutions}} instead.

Display functions for substitutions are
\begin{align*}
&\texttt{(display-substitution \textsl{subst})}%
\index{display-substitution@\texttt{display-substitution}} 
\\
&\texttt{(substitution-to-string \textsl{subst})}%
\index{substitution-to-string@\texttt{substitution-to-string}} 
\end{align*}


\section{Formulas and comprehension terms}
\mylabel{S:Formulas}
A prime formula\index{formula!prime} can have the form
\begin{itemize}
\item \texttt{(atom r)} with a term r of type boole, 
\item \texttt{(predicate a r1 ... rn)} with a predicate variable or
constant \texttt{a} and terms \texttt{r1} \dots \texttt{rn}.
\end{itemize}
Formulas are built from prime formulas by
\begin{itemize}
\item  implication \texttt{(imp \textsl{formula1} \textsl{formula2})}
\item  conjunction \texttt{(and \textsl{formula1} \textsl{formula2})}
\item  tensor \texttt{(tensor \textsl{formula1} \textsl{formula2})}
\item  all quantification  \texttt{(all \textsl{x} \textsl{formula})}
\item  existential quantification  \texttt{(ex \textsl{x} \textsl{formula})}
\item all quantification \texttt{(allnc \textsl{x} \textsl{formula})}
without computational content
\item existential quantification \texttt{(exnc \textsl{x}
\textsl{formula})} without computational content
\end{itemize}
Moreover we have classical existential quantification in an arithmetical
and a logical form:
\begin{alignat*}{2}
&\texttt{(exca (\textsl{x1}\dots) \textsl{formula})} 
\index{exca@\texttt{exca}}
&\quad& \text{arithmetical version} 
\\
&\texttt{(excl (\textsl{x1} \dots) \textsl{formula})} 
\index{excl@\texttt{excl}}
&& \text{logical version.}
\end{alignat*}
Here we allow that the quantified variable is formed without \verb#^#,
i.e.\ ranges over total objects only.

Formulas can be \emph{unfolded}\index{formula!unfolded} in the sense
that the all classical existential quantifiers are replaced according
to their definiton.  Inversely a formula can be
\emph{folded}\index{formula!folded} in the sense that classical
existential quantifiers are introduced wherever possible.

\emph{Comprehension terms}\index{comprehension term} have the form
\texttt{(cterm \textsl{vars} \textsl{formula})}.  Note that
\textsl{formula} may contain further free variables.

% \subsection*{Interface}
Tests:
\begin{align*}
&\texttt{(atom-form?\ \textsl{formula})} 
\index{atom-form?@\texttt{atom-form?}}
\\
% &\texttt{(pvar-form?\ \textsl{formula})}
% \index{pvar-form?@\texttt{pvar-form?}}
% \\
% &\texttt{(predconst-form?\ \textsl{formula})}
% \index{predconst-form?@\texttt{predconst-form?}}
% \\
&\texttt{(predicate-form?\ \textsl{formula})}
\index{predicate-form?@\texttt{predicate-form?}}
\\
&\texttt{(prime-form?\ \textsl{formula})}
\index{prime-form?@\texttt{prime-form?}}
\\
&\texttt{(imp-form?\ \textsl{formula})}
\index{imp-form?@\texttt{imp-form?}}
\\
&\texttt{(and-form?\ \textsl{formula})}
\index{and-form?@\texttt{and-form?}}
\\
&\texttt{(tensor-form?\ \textsl{formula})}
\index{tensor-form?@\texttt{tensor-form?}}
\\
&\texttt{(all-form?\ \textsl{formula})}
\index{all-form?@\texttt{all-form?}}
\\
&\texttt{(ex-form?\ \textsl{formula})}
\index{ex-form?@\texttt{ex-form?}}
\\
&\texttt{(allnc-form?\ \textsl{formula})}
\index{allnc-form?@\texttt{allnc-form?}}
\\
&\texttt{(exnc-form?\ \textsl{formula})}
\index{exnc-form?@\texttt{exnc-form?}}
\\
&\texttt{(exca-form?\ \textsl{formula})}
\index{exca-form?@\texttt{exca-form?}}
\\
&\texttt{(excl-form?\ \textsl{formula})}
\index{excl-form?@\texttt{excl-form?}}
\end{align*}
and also
\begin{align*}
&\texttt{(quant-prime-form?\ \textsl{formula})}
\index{quant-prime-form?@\texttt{quant-prime-form?}}
\\
&\texttt{(quant-free?\ \textsl{formula}).}
\index{quant-free?@\texttt{quant-free?}}
\end{align*}

We need constructors and accessors for prime formulas
\begin{alignat*}{2}
&\texttt{(make-atomic-formula \textsl{boolean-term})}
\index{make-atomic-formula@\texttt{make-atomic-formula}}
\\
&\texttt{(make-predicate-formula \textsl{predicate} \textsl{term1} \dots)}
\index{make-predicate-formula@\texttt{make-predicate-formula}}
\\
&\texttt{atom-form-to-kernel}
\index{atom-form-to-kernel@\texttt{atom-form-to-kernel}}
\\
&\texttt{predicate-form-to-predicate}
\index{predicate-form-to-predicate@\texttt{predicate-form-to-predicate}}
\\
&\texttt{predicate-form-to-args.}
\index{predicate-form-to-args@\texttt{predicate-form-to-args}}
\end{alignat*}
We also have constructors for special atomic formulas
\begin{alignat*}{2}
&\texttt{(make-eq \textsl{term1} \textsl{term2})} 
\index{make-eq@\texttt{make-eq}}
&\quad& \text{constructor for equalities}
\\
&\texttt{(make-= \textsl{term1} \textsl{term2})} 
\index{make-=@\texttt{make-=}}
&\quad& \text{constructor for equalities on finalgs}
\\
&\texttt{(make-total \textsl{term})} 
\index{make-total@\texttt{make-total}}
&\quad& \text{constructor for totalities}
\\
&\texttt{(make-e \textsl{term})} 
\index{make-e@\texttt{make-e}}
&\quad& \text{constructor for existence on finalgs}
\\
&\texttt{truth}
\index{truth@\texttt{truth}}
\\
&\texttt{falsity}
\index{falsity@\texttt{falsity}}
\\
&\texttt{falsity-log.}
\index{falsity-log@\texttt{falsity-log}}
\end{alignat*}
We need constructors and accessors for implications
\begin{alignat*}{2}
&\texttt{(make-imp \textsl{premise} \textsl{conclusion})}       
\index{make-imp@\texttt{make-imp}}
&\quad& \text{constructor} 
\\
&\texttt{(imp-form-to-premise \textsl{imp-formula})}   
\index{imp-form-to-premise@\texttt{imp-form-to-premise}}
&& \text{accessor} 
\\
&\texttt{(imp-form-to-conclusion \textsl{imp-formula})}
\index{imp-form-to-conclusion@\texttt{imp-form-to-conclusion}}
&& \text{accessor,}
\end{alignat*}
conjunctions
\begin{alignat*}{2}
&\texttt{(make-and \textsl{formula1} \textsl{formula2})}    
\index{make-and@\texttt{make-and}}
&\quad& \text{constructor} 
\\
&\texttt{(and-form-to-left \textsl{and-formula})}   
\index{and-form-to-left@\texttt{and-form-to-left}}
&& \text{accessor} 
\\
&\texttt{(and-form-to-right \textsl{and-formula})}
\index{and-form-to-right@\texttt{and-form-to-right}}
&& \text{accessor,}
\end{alignat*}
tensors
\begin{alignat*}{2}
&\texttt{(make-tensor \textsl{formula1} \textsl{formula2})}    
\index{make-tensor@\texttt{make-tensor}}
&\quad& \text{constructor} 
\\
&\texttt{(tensor-form-to-left \textsl{tensor-formula})}   
\index{tensor-form-to-left@\texttt{tensor-form-to-left}}
&& \text{accessor} 
\\
&\texttt{(tensor-form-to-right \textsl{tensor-formula})}
\index{tensor-form-to-right@\texttt{tensor-form-to-right}}
&& \text{accessor,}
\end{alignat*}
universally quantified formulas
\begin{alignat*}{2}
&\texttt{(make-all \textsl{var} \textsl{formula})}           
\index{make-all@\texttt{make-all}}
&\quad& \text{constructor} 
\\
&\texttt{(all-form-to-var \textsl{all-formula})}    
\index{all-form-to-var@\texttt{all-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(all-form-to-kernel \textsl{all-formula})} 
\index{all-form-to-kernel@\texttt{all-form-to-kernel}}
&& \text{accessor,} 
\end{alignat*}
existentially quantified formulas
\begin{alignat*}{2}
&\texttt{(make-ex \textsl{var} \textsl{formula})}           
\index{make-ex@\texttt{make-ex}}
&\quad& \text{constructor} 
\\
&\texttt{(ex-form-to-var \textsl{ex-formula})}    
\index{ex-form-to-var@\texttt{ex-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(ex-form-to-kernel \textsl{ex-formula})} 
\index{ex-form-to-kernel@\texttt{ex-form-to-kernel}}
&& \text{accessor,} 
\end{alignat*}
universally quantified formulas without computational content
\begin{alignat*}{2}
&\texttt{(make-allnc \textsl{var} \textsl{formula})}           
\index{make-allnc@\texttt{make-allnc}}
&\quad& \text{constructor} 
\\
&\texttt{(allnc-form-to-var \textsl{allnc-formula})}    
\index{allnc-form-to-var@\texttt{allnc-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(allnc-form-to-kernel \textsl{allnc-formula})} 
\index{allnc-form-to-kernel@\texttt{allnc-form-to-kernel}}
&& \text{accessor,} 
\end{alignat*}
existentially quantified formulas without computational content
\begin{alignat*}{2}
&\texttt{(make-exnc \textsl{var} \textsl{formula})}           
\index{make-exnc@\texttt{make-exnc}}
&\quad& \text{constructor} 
\\
&\texttt{(exnc-form-to-var \textsl{exnc-formula})}    
\index{exnc-form-to-var@\texttt{exnc-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(exnc-form-to-kernel \textsl{exnc-formula})} 
\index{exnc-form-to-kernel@\texttt{exnc-form-to-kernel}}
&& \text{accessor,} 
\end{alignat*}
existentially quantified formulas in the sense of classical arithmetic
\begin{alignat*}{2}
&\texttt{(make-exca \textsl{var} \textsl{formula})}           
\index{make-exca@\texttt{make-exca}}
&\quad& \text{constructor} 
\\
&\texttt{(exca-form-to-var \textsl{exca-formula})}    
\index{exca-form-to-var@\texttt{exca-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(exca-form-to-kernel \textsl{exca-formula})} 
\index{exca-form-to-kernel@\texttt{exca-form-to-kernel}}
&& \text{accessor,} 
\end{alignat*}
existentially quantified formulas in the sense of classical logic
\begin{alignat*}{2}
&\texttt{(make-excl \textsl{var} \textsl{formula})}           
\index{make-excl@\texttt{make-excl}}
&\quad& \text{constructor} 
\\
&\texttt{(excl-form-to-var \textsl{excl-formula})}    
\index{excl-form-to-var@\texttt{excl-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(excl-form-to-kernel \textsl{excl-formula})} 
\index{excl-form-to-kernel@\texttt{excl-form-to-kernel}}
&& \text{accessor.} 
\end{alignat*}
For convenience we also have as generalized constructors
\begin{alignat*}{2}
&\texttt{(mk-imp \textsl{formula} \textsl{formula1} {\dots})} 
\index{mk-imp@\texttt{mk-imp}}
&\quad&\text{implication} 
\\
&\texttt{(mk-neg \textsl{formula1} {\dots})} 
\index{mk-neg@\texttt{mk-neg}}
&& \text{negation} 
\\
&\texttt{(mk-neg-log \textsl{formula1} {\dots})} 
\index{mk-neg-log@\texttt{mk-neg-log}}
&& \text{logical negation} 
\\
&\texttt{(mk-and \textsl{formula} \textsl{formula1} {\dots})} 
\index{mk-and@\texttt{mk-and}}
&& \text{conjunction} 
\\
&\texttt{(mk-tensor \textsl{formula} \textsl{formula1}\! {\dots}\!)} 
\index{mk-tensor@\texttt{mk-tensor}}
&& \text{tensor} 
\\
&\texttt{(mk-all \textsl{var1} {\dots}\ \textsl{formula})} 
\index{mk-all@\texttt{mk-all}}
&& \text{all-formula} 
\\
&\texttt{(mk-ex \textsl{var1} {\dots}\ \textsl{formula})} 
\index{mk-ex@\texttt{mk-ex}}
&& \text{ex-formula} 
\\
&\texttt{(mk-allnc \textsl{var1} {\dots}\ \textsl{formula})} 
\index{mk-allnc@\texttt{mk-allnc}}
&& \text{allnc-formula} 
\\
&\texttt{(mk-exnc \textsl{var1} {\dots}\ \textsl{formula})} 
\index{mk-exnc@\texttt{mk-exnc}}
&& \text{exnc-formula} 
\\
&\texttt{(mk-exca \textsl{var1} {\dots}\ \textsl{formula})} 
\index{mk-exca@\texttt{mk-exca}}
&& \text{classical ex-formula (arithmetical)} 
\\
&\texttt{(mk-excl \textsl{var1} {\dots}\ \textsl{formula})} 
\index{mk-excl@\texttt{mk-excl}}
&& \text{classical ex-formula (logical)}
\end{alignat*}
and as generalized accessors
\begin{alignat*}{2}
&\texttt{(imp-form-to-premises-and-final-conclusion \textsl{formula})}
\\
%\index{imp-form-to-premises-and-final-conclusion@\texttt{imp-form-to-premises-and-final-conclusion}}\\
&\texttt{(tensor-form-to-parts \textsl{formula})}
\index{tensor-form-to-parts@\texttt{tensor-form-to-parts}}
\\
&\texttt{(all-form-to-vars-and-final-kernel \textsl{formula})}
\index{all-form-to-vars-and-final-kernel@\texttt{all-form-to-vars-and{\dots}}}
\\
&\texttt{(ex-form-to-vars-and-final-kernel \textsl{formula})}
\index{ex-form-to-vars-and-final-kernel@\texttt{ex-form-to-vars-and{\dots}}}
\end{alignat*}
and similarly for \texttt{exca}-forms and \texttt{excl}-forms.
Occasionally it is convenient to have
\begin{alignat*}{2}
&\texttt{(imp-form-to-premises \textsl{formula} <\textsl{n}>)}
\index{imp-form-to-premises@\texttt{imp-form-to-premises}}
&\quad& \text{all (first $n$) premises} 
\\
&\texttt{(imp-form-to-final-conclusion \textsl{formula} <\textsl{n}>)}
\index{imp-form-to-final-conclusion@\texttt{imp-form-to-final-conclusion}}
\end{alignat*}
where the latter computes the final conclusion (conclusion after
removing the first $n$ premises) of the formula.

It is also useful to have some general procedures working for
arbitrary quantified formulas.  We provide
\begin{alignat*}{2}
&\texttt{(make-quant-formula \textsl{quant} \textsl{var1} \dots\ 
\textsl{kernel})} 
\index{make-quant-formula@\texttt{make-quant-formula}}
&\quad& \text{constructor} 
\\
&\texttt{(quant-form-to-quant \textsl{quant-form})}       
\index{quant-form-to-quant@\texttt{quant-form-to-quant}}
&& \text{accessor} 
\\
&\texttt{(quant-form-to-vars \textsl{quant-form})}        
\index{quant-form-to-vars@\texttt{quant-form-to-vars}}
&& \text{accessor} 
\\
&\texttt{(quant-form-to-kernel \textsl{quant-form})}      
\index{quant-form-to-kernel@\texttt{quant-form-to-kernel}}
&& \text{accessor} 
\\
&\texttt{(quant-form?\ \textsl{x})}                       
\index{quant-form?@\texttt{quant-form?}}
&& \text{test.}
\end{alignat*}
and for convenience also
\[
\texttt{(mk-quant \textsl{quant} \textsl{var1} \dots\
\textsl{formula})\index{mk-quant@\texttt{mk-quant}}.}
\]
To fold and unfold formulas we have
\begin{align*}
&\texttt{(fold-formula \textsl{formula})} 
\index{fold-formula@\texttt{fold-formula}}
\\
&\texttt{(unfold-formula \textsl{formula}).}
\index{unfold-formula@\texttt{unfold-formula}}
\end{align*}
To test equality of formulas up to normalization and $\alpha$-equality
we use
\begin{align*}
&\texttt{(classical-formula=?\ \textsl{formula1} \textsl{formula2})} 
\index{classical-formula=?@\texttt{classical-formula=?}}
\\
&\texttt{(formula=?\ \textsl{formula1} \textsl{formula2}),}
\index{formula=?@\texttt{formula=?}}
% &\texttt{(formulas=?\\textsl{formulas1} \textsl{formulas2}),}
\end{align*}
where in the first procedure we unfold before comparing.

Morever we need
\begin{align*}
&\texttt{(formula-to-free\ \textsl{formula}),} 
\index{formula-to-free@\texttt{formula-to-free}}
\\
&\texttt{(nbe-formula-to-type\ \textsl{formula}),}
\index{nbe-formula-to-type@\texttt{nbe-formula-to-type}}
\\
&\texttt{(formula-to-prime-subformulas\ \textsl{formula}),} 
\index{formula-to-prime-subformulas@\texttt{formula-to-prime-subformulas}}
\end{align*}

Constructors, accessors and a test for comprehension terms are
\begin{alignat*}{2}
&\texttt{(make-cterm \textsl{var1} \dots\ \textsl{formula})} 
\index{make-cterm@\texttt{make-cterm}}
&\quad& \text{constructor} 
\\
&\texttt{(cterm-to-vars \textsl{cterm})}       
\index{cterm-to-vars@\texttt{cterm-to-vars}}
&& \text{accessor} 
\\
&\texttt{(cterm-to-formula \textsl{cterm})}    
\index{cterm-to-formula@\texttt{cterm-to-formula}}
&& \text{accessor} 
\\
&\texttt{(cterm?\ \textsl{x})}                 
\index{cterm?@\texttt{cterm?}}
&& \text{test.}
\end{alignat*}
Moreover we need
\begin{align*}
&\texttt{(cterm-to-free \textsl{cterm})}    
\index{cterm-to-free@\texttt{cterm-to-free}} 
\\
&\texttt{(cterm=?\ \textsl{x})}                 
\index{cterm=?@\texttt{cterm=?}} 
\\
&\texttt{(classical-cterm=?\ \textsl{x})}                 
\index{classical-cterm=?@\texttt{classical-cterm=?}}
\\
&\texttt{(fold-cterm \textsl{cterm})} 
\index{fold-cterm@\texttt{fold-cterm}}
\\
&\texttt{(unfold-cterm \textsl{cterm}).}
\index{unfold-cterm@\texttt{unfold-cterm}}
\end{align*}

Normalization of formulas is done with
\begin{alignat*}{2}
&\texttt{(normalize-formula \textsl{formula})}
\index{normalize-formula@\texttt{normalize-formula}}
&\quad& \text{normalization,} 
\end{alignat*}
abbreviated \texttt{nf}\index{nt@\texttt{nf}}.

To check equality of formulas we use
\begin{alignat*}{2}
&\texttt{(classical-formula=? \textsl{formula1} \textsl{formula2})}
\index{classical-formula=?@\texttt{classical-formula=?}}
\\
&\texttt{(formula=? \textsl{formula1} \textsl{formula2})}
\index{formula=?@\texttt{formula=?}}
\end{alignat*}
where the former unfolds the classical existential quantifiers and
normalizes all subterms in its formulas.

Display functions for formulas and comprehension terms are
\begin{alignat*}{2}
&\texttt{(formula-to-string \textsl{formula})}
\index{formula-to-string@\texttt{formula-to-string}}
\\
&\texttt{(cterm-to-string \textsl{cterm})}.
\index{cterm-to-string@\texttt{cterm-to-string}}
\end{alignat*}
The former is abbreviated \texttt{nf}\index{nf@\texttt{nf}}.

We can define simultaneous substitution for type, object and predicate
variables in a formula, via \texttt{tsubst}, \texttt{subst} and
\texttt{psubst}.  It is assumed that \texttt{subst} only affects those
variables whose type is not changed by \texttt{tsubst}, and that
\texttt{psubst} only affects those predicate variables whose arity is
not changed by \texttt{tsubst}.

In the quantifier case of the recursive definition, the abstracted
variable may need to be renamed.  However, its type can be affected by
\texttt{tsubst}.  Then the renaming cannot be made part of
\texttt{subst}, because then the condition above would be violated.
Therefore we carry along a procedure \texttt{rename}\index{rename}
renaming variables, which remembers the renaming of variables done so
far.

We will also need formula substitution to compute the formula of an
assumption constant.  However, there (type and) predicate variables
are (implicitely) considered to be bound.  Therefore, we also have to
carry along a procedure
\texttt{prename}\index{prename@\texttt{prename}} renaming predicate
variables, which remembers the renaming of predicate variables done so
far.
\begin{alignat*}{2}
&\texttt{(formula-substitute \textsl{formula} \textsl{topsubst})}%
\index{formula-substitute@\texttt{formula-substitute}} 
\\
&\texttt{(formula-subst \textsl{formula} \textsl{arg} \textsl{val})}%
\index{formula-subst@\texttt{formula-subst}} 
\\
&\texttt{(cterm-substitute \textsl{cterm} \textsl{topsubst})}%
\index{cterm-substitute@\texttt{cterm-substitute}} 
\\
&\texttt{(cterm-subst \textsl{cterm} \textsl{arg} \textsl{val})}%
\index{cterm-subst@\texttt{cterm-subst}} 
\end{alignat*}

Display functions for predicate substitutions are
\begin{align*}
&\texttt{(display-p-substitution \textsl{psubst})}%
\index{display-p-substitution@\texttt{display-p-substitution}} 
\\
&\texttt{(p-substitution-to-string \textsl{psubst})}%
\index{p-substitution-to-string@\texttt{p-substitution-to-string}} 
\end{align*}


\section{Assumption variables and constants}
\mylabel{S:AssumptionVarConst}
\subsection{Assumption variables}
Assumption variables are for proofs what variables are for terms.  The
main difference, however, is that assumption variables have formulas
as types, and that formulas may contain free variables.  Therefore we
must be careful when substituting terms for variables in assumption
variables.  Our solution (as in Matthes' thesis \cite{Matthes98}) is
to consider an assumption variable as a pair of a (typefree)
identifier and a formula, and to take equality of assumption variables
to mean that both components are equal.  Rather than using symbols as
identifiers we prefer to use numbers (i.e.\ indices).  However,
sometimes it is useful to provide an optional string as name for
display purposes.

% \subsection*{Interface}
We need a constructor, accessors and tests for assumption variables.
\begin{alignat*}{2}
&\texttt{(make-avar \textsl{formula} \textsl{index} \textsl{name})}
\index{make-avar@\texttt{make-avar}}
&\quad& \text{constructor} 
\\
&\texttt{(avar-to-formula \textsl{avar})} 
\index{avar-to-formula@\texttt{avar-to-formula}}
&& \text{accessor} 
\\
&\texttt{(avar-to-index \textsl{avar})}   
\index{avar-to-index@\texttt{avar-to-index}}
&& \text{accessor} 
\\
&\texttt{(avar-to-name \textsl{avar})}    
\index{avar-to-name@\texttt{avar-to-name}}
&& \text{accessor} 
\\
&\texttt{(avar?\ \textsl{x})}             
\index{avar?@\texttt{avar?}}
&& \text{test} 
\\
&\texttt{(avar=?\ \textsl{avar1} \textsl{avar2})}  
\index{avar?@\texttt{avar=?}}
&& \text{test.}
\end{alignat*}
For convenience we have the function 
\begin{alignat*}{2}
&\texttt{(mk-avar \textsl{formula} <\textsl{index}> <\textsl{name}>)}
\end{alignat*}
The formula is a required argument; however, the remaining arguments
are optional.  The default for the name string is \texttt{u}.  We also
require that a function
\begin{align*}
&\texttt{(formula-to-new-avar \textsl{formula})}
\end{align*}
is defined that returns an assumption variable of the requested
formula different from all assumption variables that have ever been
returned by any of the specified functions so far.

% \textbf{Implementation.}
% %
% Assumption variables are implemented as lists:
% %
% $$\texttt{(avar \textsl{formula} \textsl{index} \textsl{name})}.$$


% \subsection*{Assumption constants}
% \mylabel{S:Aconst}

An assumption constant appears in a proof, as an axiom, a theorem or a
global assumption.  Its formula is given as an
\inquotes{uninstantiated formula}, where only type and predicate
variables can occur freely; these are considered to be bound in the
assumption constant.  In the proof the bound type variables are
implicitely instantiated by types, and the bound predicate variables
by comprehension terms (the arity of a comprehension term is the
type-instantiated arity of the corresponding predicate variable).
Since we do not have type and predicate quantification in formulas,
the assumption constant contains these parts left implicit in the
proof: \texttt{tsubst} and \texttt{pinst} (which will become a
\texttt{psubst}, once the arities of predicate variables are
type-instantiated with \texttt{tsubst}).

So we have assumption constants of the following kinds:
\begin{itemize}
\item axioms,
\item theorems, and
\item global assumptions.
\end{itemize}

To normalize a proof we will first translate it into a term, then
normalize the term and finally translate the normal term back into a
proof.  To make this work, in case of axioms we pass to the term
appropriate formulas: all-formulas for induction, an existential
formula for existence introduction, and an existential formula
together with a conclusion for existence elimination.  During
normalization of the term these formulas are passed along.  When the
normal form is reached, we have to translate back into a proof.  Then
these formulas are used to reconstruct the axiom in question.

Internally, the formula of an assumption constant is split into an
uninstantiated formula where only type and predicate variables can
occur freely, and a substitution for at most these type and predicate
variables.  The formula assumed by the constant is the result of
carrying out this substitution in the uninstantiated formula.  Note
that free variables may again occur in the assumed formula.  For
example, assumption constants axiomatizing the existential quantifier
will internally have the form
\begin{alignat*}{2}
&\texttt{(aconst Ex-Intro $\forall \hat{x}^\alpha.\hat{P}(\hat{x}) \to 
\ex \hat{x}^\alpha \hat{P}(\hat{x})$
$(\alpha \mapsto \tau, \hat{P}^{(\alpha)} \mapsto \set{\hat{z}^\tau}{A})$)}
\index{Ex-Intro@\texttt{Ex-Intro}}
\\
&\texttt{(aconst Ex-Elim $\ex \hat{x}^\alpha \hat{P}(\hat{x}) \to 
(\forall \hat{x}^\alpha.  \hat{P}(\hat{x})
\to \hat{Q}) \to \hat{Q}$}
\\ 
&\qquad\qquad\qquad\qquad \texttt{$(\alpha \mapsto \tau, \hat{P}^{(\alpha)}
\mapsto \set{\hat{z}^\tau}{A}, \hat{Q} \mapsto \set{}{B})$)}
\index{Ex-Elim@\texttt{Ex-Elim}}
\end{alignat*}

\textbf{Interface for general assumption constants.}
To avoid duplication of code it is useful to formulate some procedures
generally for arbitrary assumption constants\index{assumption
constant}, i.e.\ for all of the forms listed above.
\begin{alignat*}{2}
&\texttt{(make-aconst \textsl{name} \textsl{kind} \textsl{uninst-formula}
\textsl{tpsubst}}
\\
&\qquad \texttt{\textsl{repro-formula1} \dots)}       
\index{make-aconst@\texttt{make-aconst}}
&\quad& \text{constructor} 
\\
&\texttt{(aconst-to-name \textsl{aconst})}       
\index{aconst-to-name@\texttt{aconst-to-name}}
&& \text{accessor} 
\\
&\texttt{(aconst-to-kind \textsl{aconst})}       
\index{aconst-to-kind@\texttt{aconst-to-kind}}
&& \text{accessor} 
\\
&\texttt{(aconst-to-uninst-formula \textsl{aconst})}       
\index{aconst-to-uninst-formula@\texttt{aconst-to-uninst-formula}}
&& \text{accessor} 
\\
&\texttt{(aconst-to-tpsubst \textsl{aconst})}       
\index{aconst-to-tpsubst@\texttt{aconst-to-tpsubst}}
&& \text{accessor} 
\\
&\texttt{(aconst-to-repro-formulas \textsl{aconst})}       
\index{aconst-to-repro-formulas@\texttt{aconst-to-repro-formulas}}
&& \text{accessor} 
\\
&\texttt{(aconst?\ \textsl{x})}                     
\index{aconst?@\texttt{aconst?}}
&& \text{test.}
\end{alignat*}
To construct the formula associated with an aconst, it is useful to
separate the instantiated formula from the variables to be
generalized.  The latter can be obtained as free variables in
inst-formula.  We therefore provide
\begin{alignat*}{2}
&\texttt{(aconst-to-inst-formula \textsl{aconst})}       
\index{aconst-to-inst-formula@\texttt{aconst-to-inst-formula}} 
\\
&\texttt{(aconst-to-formula \textsl{aconst})}       
\index{aconst-to-formula@\texttt{aconst-to-formula}} 
\end{alignat*}
We also provide
\begin{alignat*}{2}
&\texttt{(aconst? \textsl{aconst})}       
\index{aconst?@\texttt{aconst?}} 
\\
&\texttt{(aconst=?\ \textsl{aconst1} \textsl{aconst2})}       
\index{aconst=?@\texttt{aconst=?}}
\\
&\texttt{(aconst-without-rules?\ \textsl{aconst})}       
\index{aconst-without-rules?@\texttt{aconst-without-rules?}}
\\
&\texttt{(aconst-to-string\ \textsl{aconst})}       
\index{aconst-to-string@\texttt{aconst-to-string}}
\end{alignat*}

\subsection{Axiom constants}
\mylabel{SS:AxiomConst}
% \paragraph{Axioms}
% \mylabel{SS:Ax}
We use the natural numbers as a prototypical finitary algebra; recall
Figure~\ref{F:nat}.  Assume that $n$, $p$ are variables of type
$\nat$, $\boole$.  Let $\Eq$ denote the equality relation in the
model.  Recall the domain of type $\boole$, consisting of $\true$,
$\false$ and the bottom element $\bottom$.  The boolean valued
functions equality $=_{nat} \colon \nat \to \nat \to \boole$ and
existence (definedness, totality) $e_{nat} \colon \nat \to \boole$
need to be continuous.  So we have
\begin{align*}
\eqrel{0}{0} &\Eq \true          
\\
\eqrel{0}{S \hat{n}} \Eq \eqrel{S \hat{n}}{0} &\Eq \false 
&e(0) &\Eq \true
\\
\eqrel{S \hat{n}_1}{S \hat{n}_2} &\Eq \eqrel{\hat{n}_1}{\hat{n}_2}
&e(S \hat{n}) &\Eq e(\hat{n})
\\
\eqrel{\bottom_{nat}}{\hat{n}} \Eq \eqrel{\hat{n}}{\bottom_{nat}} &\Eq \bottom
&e(\bottom_{\nat}) &\Eq \bottom
\\
\eqrel{\infty_{nat}}{\hat{n}} \Eq \eqrel{\hat{n}}{\infty_{nat}} &\Eq \bottom
&e(\infty_{\nat}) &\Eq \bottom
\end{align*}
Write $T$, $F$ for $\atom(\true)$, $\atom(\false)$, $r=s$ for
$\atom(\eqrel{r}{s})$ and $E(r)$ for $\atom(e(r))$.  We stipulate as
axioms
\begin{alignat*}{2}
&T
&\quad&\texttt{Truth-Axiom}\index{Truth-Axiom@\texttt{Truth-Axiom}}
\\[1ex]
&\hat{x} \Eq \hat{x}
&\quad&\text{\texttt{Eq-Refl}\index{Eq-Refl@\texttt{Eq-Refl}}}
\\
&\hat{x}_1 \Eq \hat{x}_2 \to \hat{x}_2 \Eq \hat{x}_1
&\quad&\text{\texttt{Eq-Symm}\index{Eq-Symm@\texttt{Eq-Symm}}}
\\
&\hat{x}_1 \Eq \hat{x}_2 \to \hat{x}_2 \Eq \hat{x}_3 \to 
\hat{x}_1 \Eq \hat{x}_3
&\quad&\text{\texttt{Eq-Trans}\index{Eq-Trans@\texttt{Eq-Trans}}}
\\[1ex]
&\forall \hat{x} \hat{f}_1 \hat{x} \Eq \hat{f}_2 \hat{x} \to
\hat{f}_1 \Eq \hat{f}_2
&&\text{\texttt{Eq-Ext}%
\index{Extensionality@\texttt{Extensionality}}}
\\
&\hat{x}_1 \Eq \hat{x}_2 \to \hat{P}(\hat{x}_1) \to \hat{P}(\hat{x}_2)
&\quad&\text{\texttt{Eq-Compat}%
\index{Compatibility@\texttt{Compatibility}}}
% \\[1ex]
% &\hat{n}_1 \Eq \hat{n}_2 \to E(\hat{n}_1) \to E(\hat{n}_2) \to
% \hat{n}_1 = \hat{n}_2
% &&\text{\texttt{Eq-to-=}}\index{Eq-to-=@\texttt{Eq-to-=}}
% \\
% &\hat{n}_1 = \hat{n}_2 \to \hat{n}_1 \Eq \hat{n}_2
% &&\text{\texttt{=-to-Eq}}\index{equals-to-Eq@\texttt{=-to-Eq}}
% \\[1ex]
% &\Total(\hat{n}) \to E(\hat{n})
% &&\text{\texttt{Total-to-E}}\index{Total-to-E@\texttt{Total-to-E}}
% \\
% &E(\hat{n}) \to \Total(\hat{n})
% &&\text{\texttt{E-to-Total}}\index{E-to-Total@\texttt{E-to-Total}}
% \\[1ex]
% &c_1 \vec{\hat{x}}_1 \Eq c_2 \vec{\hat{x}}_2 \to F
% &&\text{\texttt{Constr-Disjoint}}%
% \index{Constr-Disjoint@\texttt{Constr-Disjoint@}}
% \\
% &c \vec{\hat{x}}_1 \Eq c \vec{\hat{x}}_2 \to \hat{x}_{1i} \Eq \hat{x}_{2i}
% &&\text{\texttt{Constr-Inj}}%
% \index{Constr-Inj@\texttt{Constr-Inj@}}
\\[1ex]
&\Total_{\rho \to\sigma}(\hat{f}) \leftrightarrow
\forall \hat{x}.\Total_{\rho}(\hat{x}) \to \Total_{\sigma}(\hat{f} \hat{x})
&&\text{\texttt{Total}}\index{Total@\texttt{Total}}
\\
&\Total_{\rho}(c)
&&\text{\texttt{Constr-Total}}\index{Constr-Total@\texttt{Constr-Total}}
\\
&\Total(c \vec{\hat{x}}) \to \Total(\hat{x}_i)
&&\text{\texttt{Constr-Total-Args}}%
\index{Constr-Total-Args@\texttt{Constr-Total-Args}}
% \\
% &\Total_{\rho}(\bottom) \to F
% &&\text{\texttt{Bottom-not-Total}}%
% \index{Bottom-Not-Total@\texttt{Bottom-Not-Total}}
\\
\intertext{and for every finitary algebra, e.g.\ \texttt{nat}}
&\hat{n}_1 \Eq \hat{n}_2 \to E(\hat{n}_1) \to
\hat{n}_1 = \hat{n}_2
&&\text{\texttt{Eq-to-=-1-nat}\index{Eq-to-=-1-nat@\texttt{Eq-to-=-1-nat}}}
\\
&\hat{n}_1 \Eq \hat{n}_2 \to E(\hat{n}_2) \to
\hat{n}_1 = \hat{n}_2
&&\text{\texttt{Eq-to-=-2-nat}\index{Eq-to-=-2-nat@\texttt{Eq-to-=-2-nat}}}
\\
&\hat{n}_1 = \hat{n}_2 \to \hat{n}_1 \Eq \hat{n}_2
&&\text{\texttt{=-to-Eq-nat}\index{equals-to-Eq-nat@\texttt{=-to-Eq-nat}}}
\\
&\hat{n}_1 = \hat{n}_2 \to E(\hat{n}_1)
&&\text{\texttt{=-to-E-1-nat}\index{equals-to-E-1-nat@\texttt{=-to-E-1-nat}}}
\\
&\hat{n}_1 = \hat{n}_2 \to E(\hat{n}_2)
&&\text{\texttt{=-to-E-2-nat}\index{equals-to-E-2-nat@\texttt{=-to-E-2-nat}}}
\\
&\Total(\hat{n}) \to E(\hat{n})
&&\text{\texttt{Total-to-E-nat}\index{Total-to-E-nat@\texttt{Total-to-E-nat}}}
\\
&E(\hat{n}) \to \Total(\hat{n})
&&\text{\texttt{E-to-Total-nat}\index{E-to-Total-nat@\texttt{E-to-Total-nat}}}
\end{alignat*}
Here $c$ is a constructor.  Notice that in $\Total(c \vec{\hat{x}})
\to \Total(\hat{x}_i)$, the type of $(c \vec{\hat{x}})$ need not be a
finitary algebra, and hence $\hat{x}_i$ may have a function type.
% Further notice that $\Total_{\rho}(\bottom) \to F$ is also necessary
% for $\rho$ an infinitary ground type.

\begin{remark*}
  $(E(\hat{n}_1) \to \hat{n}_1 = \hat{n}_2) \to (E(\hat{n}_2) \to
  \hat{n}_1 = \hat{n}_2) \to \hat{n}_1 \Eq \hat{n}_2$ is \emph{not}
  valid in our intended model (see Figure~\ref{F:nat}), since we have
  \emph{two} distinct undefined objects $\bottom_{nat}$ and
  $\infty_{nat}$.
\end{remark*}

We abbreviate
\begin{alignat*}{2}
&\forall \hat{x}.\Total_{\rho}(\hat{x}) \to A &\quad\hbox{by}\quad& 
\forall x A,\\
&\exists \hat{x}.\Total_{\rho}(\hat{x}) \land A &\quad\hbox{by}\quad& 
\exists x A.
\end{alignat*}
Formally, these abbreviations appear as axioms
\begin{alignat*}{2}
&\forall x \hat{P}(x) \to
\forall \hat{x}. \Total(\hat{x}) \to \hat{P}(\hat{x})
&\quad&\texttt{All-AllPartial}\index{All-AllPartial@\texttt{All-AllPartial}}
\\
&(\forall \hat{x}. \Total(\hat{x}) \to \hat{P}(\hat{x})) \to
\forall x \hat{P}(x)
&\quad&\texttt{AllPartial-All}\index{AllPartial-All@\texttt{AllPartial-All}}
\\
&\exists x \hat{P}(x) \to
\exists \hat{x}. \Total(\hat{x}) \land \hat{P}(\hat{x})
&\quad&\texttt{Ex-ExPartial}\index{Ex-ExPartial@\texttt{Ex-ExPartial}}
\\
&(\exists \hat{x}. \Total(\hat{x}) \land \hat{P}(\hat{x})) \to
\exists x \hat{P}(x)
&\quad&\texttt{ExPartial-Ex}\index{ExPartial-Ex@\texttt{ExPartial-Ex}}
\\
\intertext{and for every finitary algebra, e.g.\ \texttt{nat}}
&\forall n \hat{P}(n) \to
\forall \hat{n}. E(\hat{n}) \to \hat{P}(\hat{n})
&\quad&\texttt{All-AllPartial-nat}%
\index{All-AllPartial-nat@\texttt{All-AllPartial-nat}}
\\
&(\exists \hat{n}. E(\hat{n}) \land \hat{P}(\hat{n})) \to
\exists n \hat{P}(n)
&\quad&\texttt{ExPartial-Ex-nat}%
\index{ExPartial-Ex-nat@\texttt{ExPartial-Ex-nat}}
\end{alignat*}
Notice that \texttt{AllPartial-All-nat}%
\index{AllPartial-All-nat@\texttt{AllPartial-All-nat},} i.e.\ $(\forall
\hat{n}. E(\hat{n}) \to \hat{P}(\hat{n})) \to \forall n
\hat{P}(n)$ is provable (since $E(n) \cnv T$).  Similarly,
\texttt{Ex-ExPartial-nat}%
\index{Ex-ExPartial-nat@\texttt{Ex-ExPartial-nat}}, i.e.\
$\exists n \hat{P}(n) \to
\exists \hat{n}. E(\hat{n}) \land \hat{P}(\hat{n})$ is provable.

Finally we have axioms for the existential quantifier
\begin{alignat*}{2}
&\forall \hat{x}^\alpha.\hat{P}(\hat{x}) \to 
\ex \hat{x}^\alpha \hat{P}(\hat{x})
&\quad&\text{\texttt{Ex-Intro}\index{Ex-Intro@\texttt{Ex-Intro}}}
\\
&\ex \hat{x}^\alpha \hat{P}(\hat{x}) \to 
(\forall \hat{x}^\alpha.  \hat{P}(\hat{x})
\to \hat{Q}) \to \hat{Q}
&\quad&\text{\texttt{Ex-Elim}\index{Ex-Elim@\texttt{Ex-Elim}}}
\end{alignat*}

The assumption constants corresponding to these axioms are
\begin{alignat*}{2}
&\texttt{truth-aconst}\index{truth-aconst@\texttt{truth-aconst}}
&\quad&\text{for \texttt{Truth-Axiom}\index{Truth-Axiom@\texttt{Truth-Axiom}}}
\\[1ex]
&\texttt{eq-refl-aconst}\index{eq-refl-aconst@\texttt{eq-refl-aconst}}
&\quad&\text{for \texttt{Eq-Refl}\index{Eq-Refl@\texttt{Eq-Refl}}}
\\
&\texttt{eq-symm-aconst}\index{eq-symm-aconst@\texttt{eq-symm-aconst}}
&\quad&\text{for \texttt{Eq-Symm}\index{Eq-Symm@\texttt{Eq-Symm}}}
\\
&\texttt{eq-trans-aconst}\index{eq-trans-aconst@\texttt{eq-trans-aconst}}
&\quad&\text{for \texttt{Eq-Trans}\index{Eq-Trans@\texttt{Eq-Trans}}}
\\[1ex]
&\texttt{ext-aconst}\index{ext-aconst@\texttt{ext-aconst}}
&\quad&\text{for \texttt{Eq-Ext}\index{Eq-Ext@\texttt{Eq-Ext}}}
\\
&\texttt{eq-compat-aconst}\index{eq-compat-aconst@\texttt{eq-compat-aconst}}
&\quad&\text{for \texttt{Eq-Compat}\index{Eq-Compat@\texttt{Eq-Compat}}}
\\
&\texttt{total-aconst}\index{total-aconst@\texttt{total-aconst}}
&\quad&\text{for \texttt{Total}\index{Total@\texttt{Total}}}
\\[1ex]
&\texttt{(finalg-to-eq-to-=-1-aconst finalg)}%
\index{finalg-to-eq-to-=-1-aconst@\texttt{finalg-to-eq-to-=-1-aconst}}
&\quad&\text{for \texttt{Eq-to-=-1}\index{Eq-to-=-1@\texttt{Eq-to-=-1}}}
\\
&\texttt{(finalg-to-eq-to-=-2-aconst finalg)}%
\index{finalg-to-eq-to-=-2-aconst@\texttt{finalg-to-eq-to-=-2-aconst}}
&\quad&\text{for \texttt{Eq-to-=-2}\index{Eq-to-=-2@\texttt{Eq-to-=-2}}}
\\
&\texttt{(finalg-to-=-to-eq-aconst finalg)}%
\index{finalg-to-=-to-eq-aconst@\texttt{finalg-to-=-to-eq-aconst}}
&\quad&\text{for \texttt{=-to-Eq}\index{=-to-Eq@\texttt{=-to-Eq}}}
\\
&\texttt{(finalg-to-=-to-e-1-aconst finalg)}%
\index{finalg-to-=-to-e-1-aconst@\texttt{finalg-to-=-to-e-1-aconst}}
&\quad&\text{for \texttt{=-to-E-1}\index{=-to-E-1@\texttt{=-to-E-1}}}
\\
&\texttt{(finalg-to-=-to-e-2-aconst finalg)}%
\index{finalg-to-=-to-e-2-aconst@\texttt{finalg-to-=-to-e-2-aconst}}
&\quad&\text{for \texttt{=-to-E-2}\index{=-to-E-2@\texttt{=-to-E-2}}}
\\
&\texttt{(finalg-to-total-to-e-aconst finalg)}%
\index{finalg-to-total-to-e-aconst@\texttt{finalg-to-total-to-e-aconst}}
&\quad&\text{for \texttt{Total-to-E}\index{Total-to-E@\texttt{Total-to-E}}}
\\
&\texttt{(finalg-to-e-to-total-aconst finalg)}%
\index{finalg-to-e-to-total-aconst@\texttt{finalg-to-e-to-total-aconst}}
&\quad&\text{for \texttt{E-to-Total}\index{E-to-Total@\texttt{E-to-Total}}}
\\[1ex]
&\texttt{all-allpartial-aconst}%
\index{all-allpartial-aconst@\texttt{all-allpartial-aconst}}
&\quad&\text{for \texttt{All-AllPartial}%
\index{All-AllPartial@\texttt{All-AllPartial}}}
\\
&\texttt{allpartial-all-aconst}%
\index{allpartial-all-aconst@\texttt{allpartial-all-aconst}}
&\quad&\text{for \texttt{AllPartial-All}%
\index{AllPartial-All@\texttt{AllPartial-All}}}
\\
&\texttt{ex-expartial-aconst}%
\index{ex-expartial-aconst@\texttt{ex-expartial-aconst}}
&\quad&\text{for \texttt{Ex-ExPartial}%
\index{Ex-ExPartial@\texttt{Ex-ExPartial}}}
\\
&\texttt{expartial-ex-aconst}%
\index{expartial-ex-aconst@\texttt{expartial-ex-aconst}}
&\quad&\text{for \texttt{ExPartial-Ex}%
\index{ExPartial-Ex@\texttt{ExPartial-Ex}}}
\\[1ex]
&\texttt{(finalg-to-all-allpartial-aconst finalg)}%
\index{finalg-to-all-allpartial-aconst@\texttt{finalg-to-all-allpartial-aconst}}
&\quad&\text{for \texttt{All-AllPartial}%
\index{All-AllPartial@\texttt{All-AllPartial}}}
\\
&\texttt{(finalg-to-expartial-ex-aconst finalg)}%
\index{finalg-to-expartial-ex-aconst@\texttt{finalg-to-expartial-ex-aconst}}
&\quad&\text{for \texttt{ExPartial-Ex}%
\index{ExPartial-Ex@\texttt{ExPartial-Ex}}}
\end{alignat*}

% \paragraph{Induction axioms for simultaneous free algebras}
% \mylabel{SS:IndSFA}
We now spell out what precisely we mean by induction\index{induction}
over simultaneous free algebras $\vec{\mu} =
\mu\vec{\alpha}\,\vec{\kappa}$, with goal formulas $\forall
x_j^{\mu_j}\, \hat{P}_j(x_j)$.  For the constructor type
\[
\kappa_i = \vec{\rho} \to (\vec{\sigma}_1 \to \alpha_{j_1}) \to \dots \to
(\vec{\sigma}_n \to \alpha_{j_n}) \to \alpha_j \in
\constrtypes(\vec{\alpha})
\]
we have the \emph{step formula}
\begin{align*}
D_i := \forall y_1^{\rho_1},\dots,y_m^{\rho_m},
y_{m+1}^{\vec{\sigma}_1 \to \mu_{j_1}},\dots,
y_{m+n}^{\vec{\sigma}_n \to \mu_{j_n}}.
&\forall \vec{x}^{\vec{\sigma}_1}\,
\hat{P}_{j_1}(y_{m+1}\vec{x}) \to \dots \to 
\\
&\forall \vec{x}^{\vec{\sigma}_n}\,
\hat{P}_{j_n}(y_{m+n}\vec{x}) \to 
\\
&\hat{P}_j(\constr_i^{\vec{\mu}}(\vec{y})).
\end{align*}
Here $\vec{y} = y_1^{\rho_1},\dots,y_m^{\rho_m},
y_{m+1}^{\vec{\sigma}_1 \to \mu_{j_1}},\dots,
y_{m+n}^{\vec{\sigma}_n \to \mu_{j_n}}$ are the
\emph{components} of the object $\constr_i^{\vec{\mu}}(\vec{y})$
of type $\mu_j$ under consideration, and
\[
\forall \vec{x}^{\vec{\sigma}_1}\,
\hat{P}_{j_1}(y_{m+1}\vec{x}), \dots,
\forall \vec{x}^{\vec{\sigma}_n}\,
\hat{P}_{j_n}(y_{m+n}\vec{x})
\]
are the hypotheses available when proving the induction step.  The
induction axiom $\ind_{\mu_j}$\index{Ind@\texttt{Ind}} then
proves the formula
\[
\ind_{\mu_j} \colon
D_1 \to \dots \to D_k \to \forall x_j^{\mu_j}\, \hat{P}_j(x_j).
\]
We will often write $\ind_j$ for $\ind_{\mu_j}$.

An example is
\begin{alignat*}{2}
&E_1 \to E_2 \to E_3 \to E_4 \to \forall x_1^\tree \hat{P}_1(x_1)
\\
\intertext{with}
&E_1 := \hat{P}_1(\leaf),
\\
&E_2 := \forall x^{\tlist}.\hat{P}_2(x) \to \hat{P}_1(\branch(x)),
\\
&E_3 := \hat{P}_2(\empt),
\\
&E_4 := \forall x_1^{\tree},x_2^{\tlist}. \hat{P}_1(x_1) \to 
\hat{P}_2(x_2) \to \hat{P}_2(\tcons(x_1,x_2)).
\end{alignat*}
Here the fact that we deal with a simultaneous induction (over
\texttt{tree} and \texttt{tlist}), and that we prove a formula of the
form $\forall x^\tree \dots$, can all be inferred from what is given:
the $\forall x^\tree \dots$ is right there, and for \texttt{tlist} we
can look up the simultaneously defined algebras.  -- The internal
representation is
\begin{alignat*}{2}
&\texttt{(aconst Ind $E_1 \to E_2 \to E_3 \to E_4 \to 
\forall x_1^\tree \hat{P}_1(x_1)$}
\\
&\qquad \qquad \qquad 
\texttt{$(\hat{P}_1 \mapsto \set{x_1^\tree}{A_1}, 
\hat{P}_2 \mapsto \set{x_2^\tlist}{A_2})$)} 
\index{Ind@\texttt{Ind}}
\end{alignat*}

A simplified version (without the recursive calls) of the induction
axiom is the following cases axiom.
\begin{alignat*}{2}
&\texttt{(aconst Cases $E_1 \to E_2 \to 
\forall x_1^\tree \hat{P}_1(x_1)$ 
$(\hat{P}_1 \mapsto \set{x_1^\tree}{A_1})$)} 
\index{Cases@\texttt{Cases}}
\\
\intertext{with}
&E_1 := \hat{P}_1(\leaf),
\\
&E_2 := \forall x^{\tlist} \hat{P}_1(\branch(x)).
\end{alignat*}
However, rather than using this as an assumption constant we will --
parallel to the
\texttt{if}-construct\index{if-construct@\texttt{if}-construct} for
terms -- use a
\texttt{cases}-construct\index{cases-construct@\texttt{cases}-construct}
for proofs.  This does not change our notion of proof; it is done to
have the \texttt{if}-construct in the extracted programs.

The assumption constants corresponding to these axioms are generated by
\begin{alignat*}{2}
&\texttt{(all-formulas-to-ind-aconst \textsl{all-formula1} \dots)} 
\index{all-formulas-to-ind-aconst@\texttt{all-formulas-to-ind-aconst}} 
&\quad&\text{for \texttt{Ind}\index{Ind@\texttt{Ind}}}
\\
&\texttt{(all-formula-to-cases-aconst \textsl{all-formula})} 
\index{all-formula-to-cases-aconst@\texttt{all-formula-to-cases-aconst}} 
&\quad&\text{for \texttt{Cases}\index{Cases@\texttt{Cases}}}
\end{alignat*}

% To deal with equality we need
% \begin{alignat*}{2}
% %
% &\texttt{(refl-at \textsl{finalg})} 
% \index{refl-at@\texttt{refl-at}}
% &\quad&\colon x=x\\
% %
% &\texttt{(=-ax-at \textsl{finalg})} 
% \index{equal-ax-at@\texttt{=-ax-at}}
% &&\colon x_1 = x_2 \to \hat{P} x_1 \to \hat{P} x_2.
% %
% \end{alignat*}

For the introduction and elimination axioms
\texttt{Ex-Intro}\index{Ex-Intro@\texttt{Ex-Intro}} and
\texttt{Ex-Elim}\index{Ex-Elim@\texttt{Ex-Elim}} for the existential
quantifier we provide
\begin{align*}
&\texttt{(ex-formula-to-ex-intro-aconst ex-formula)}%
\index{ex-formula-to-ex-intro-aconst@\texttt{ex-formula-to-ex-intro-aconst}}
\\
&\texttt{(ex-formula-and-concl-to-ex-elim-aconst ex-formula concl)}%
\index{ex-formula-and-concl-to-ex-elim-const@\texttt{ex-for{\dots}-to-ex-elim-const}}
\end{align*}
and similarly for \texttt{exnc} instead of \texttt{ex}.

To deal with inductively defined predicate constants, we need
additional axioms with names \inquotes{Intro}\index{Intro} and 
\inquotes{Elim}\index{Elim}, which can be generated by
\begin{align*}
&\texttt{(number-and-idpredconst-to-intro-aconst i idpc)}%
\index{number-and-idpredconst-to-intro-aconst@\texttt{number-and-idpredconst-to-intro-aconst}}
\\
&\texttt{(imp-formulas-to-elim-aconst imp-formula1\ \dots)};%
\index{imp-formulas-to-elim-aconst@\texttt{imp-formulas-to-elim-aconst}}
\end{align*}
here an \texttt{imp-formula} is expected to have the form $I(\vec{x}) \to A$.


\subsection{Theorems}
\mylabel{SS:Theorems}
A theorem is a special assumption constant.  
% A typical example is
% the transitivity of the successor function, with the internal
% representation
% \begin{alignat*}{2}
% %
% &\texttt{(aconst Trans-Suc $\forall k,m,n.  k<m \to k<n+1 \to k<n$ 
% \textsl{empty-subst})} 
% \index{Trans-Suc@\texttt{Trans-Suc}}
% %
% \end{alignat*}
Theorems are normally created after successfully completing an
interactive proof.  One may also create a theorem from an explicitely
given (closed) proof.  The command is
\begin{alignat*}{2}
&\texttt{(add-theorem \textsl{string} .\ \textsl{opt-proof})}%    
\index{add-theorem@\texttt{add-theorem}}
&\quad&\text{or \texttt{save}\index{save@\texttt{save}}}
\end{alignat*}
From a theorem name we can access its aconst, its (original) proof and
also its instantiated proof by
\begin{align*}
&\texttt{(theorem-name-to-aconst \textsl{string})}
\index{theorem-name-to-aconst@\texttt{theorem-name-to-aconst}} 
\\
&\texttt{(theorem-name-to-proof \textsl{string})}
\index{theorem-name-to-proof@\texttt{theorem-name-to-proof}} 
\\
&\texttt{(theorem-name-to-inst-proof \textsl{string})}
\index{theorem-name-to-inst-proof@\texttt{theorem-name-to-inst-proof}} 
% \\
% &\texttt{(theorem-name-to-eterm \textsl{string})}
% \index{theorem-name-to-eterm@\texttt{theorem-name-to-eterm}} 
\end{align*}
We also provide
\begin{align*}
&\texttt{(remove-theorem \textsl{string1} \dots)}
\index{remove-theorem@\texttt{remove-theorem}} 
\\
&\texttt{(display-theorems \textsl{string1} \dots)}    
\index{display-theorems@\texttt{display-theorems}}
\end{align*}

% \paragraph{Simple consequences of the axioms}
% \mylabel{SS:ConseqAx}
Initially we provide the following theorems
\begin{alignat*}{2}
&\atom(p) \to p = \true
&\quad&\text{\texttt{Atom-True}\index{Atom-True@\texttt{Atom-True}}}
\\
&(\atom(p) \to F) \to p = \false
&&\text{\texttt{Atom-False}\index{Atom-False@\texttt{Atom-False}}}
\\
&F \to \atom(p)
&&\text{\texttt{Efq-Atom}\index{Efq-Atom@\texttt{Efq-Atom}}}
\\
&((\atom(p) \to F) \to F) \to \atom(p)
&&\text{\texttt{Stab-Atom}\index{Stab-Atom@\texttt{Stab-Atom}}}
\\
\intertext{and for every finitary algebra, e.g.\ \texttt{nat}}
&n=n
&&\text{\texttt{=-Refl-nat}%
\index{equalfinalg-Refl-nat@\texttt{=-Refl-nat}}}
\\
&\hat{n}_1 = \hat{n}_2 \to \hat{n}_2 = \hat{n}_1
&&\text{\texttt{=-Symm-nat}%
\index{equalfinalg-Symm-nat@\texttt{=-Symm-nat}}}%
\\
&\hat{n}_1 = \hat{n}_2 \to \hat{n}_2 = \hat{n}_3 \to \hat{n}_1 = \hat{n}_3
&&\text{\texttt{=-Trans-nat}%
\index{equalfinalg-Trans-nat@\texttt{=-Trans-nat}}}
\end{alignat*}

% \begin{lemma}[\texttt{Atom-True}\index{Atom-True@\texttt{Atom-True}}]
% $\atom(p) \to p = \true$.
% \end{lemma}

\begin{proof}[Proof of \texttt{Atom-True}]
By \texttt{Ind}.  In case $\true$ use \texttt{Eq-Compat} with
$\true \Eq \eqrel{\true}{\true}$ to infer
$\atom(\eqrel{\true}{\true})$ (i.e.\ $\true = \true$) from
$\atom(\true)$.  In case $\false$ use \texttt{Eq-Compat} with
$\false \Eq \eqrel{\false}{\true}$ to infer
$\atom(\eqrel{\false}{\true})$ (i.e.\ $\false = \true$) from
$\atom(\false)$.
\end{proof}

% \begin{lemma}[\texttt{Atom-False}\index{Atom-False@\texttt{Atom-False}}]
% $(\atom(p) \to F) \to p = \false$.
% \end{lemma}

\begin{proof}[Proof of \texttt{Atom-False}]
Use \texttt{Ind}, and \texttt{Truth-Axiom} in both cases.  -- Notice
that the more general $(\atom(\hat{p}) \to F) \to \hat{p} = \false$
does \emph{not} hold with $\bottom$ for $\hat{p}$, since
$\eqrel{\bottom}{\false} \Eq \bottom$.
\end{proof}

% \begin{lemma}[\texttt{Efq-Atom}\index{Efq-Atom@\texttt{Efq-Atom}}]
% $F \to \atom(p)$.
% \end{lemma}

\begin{proof}[Proof of \texttt{Efq-Atom}]
Again by \texttt{Ind}.  In case $\true$ use \texttt{Truth-Axiom}, and
the case $\false$ is obvious.
\end{proof}

% We can even prove the following stronger stability lemma, which
% can be seen as establishing the principle of \indexentry{indirect
% proof} (i.e.\ of classical logic) for decidable formulas.

% \begin{lemma}[\texttt{Stab-Atom}\index{Stab-Atom@\texttt{Stab-Atom}}]
% $((\atom(p) \to F) \to F) \to \atom(p)$.
% \end{lemma}

\begin{proof}[Proof of \texttt{Stab-Atom}]
By \texttt{Ind}.  In case $\true$ use \texttt{Truth-Axiom}, and the
case $\false$ is obvious.
\end{proof}

\begin{remark*}
Notice that from $\texttt{Efq-Atom}$ one easily obtains $F \to A$ for
every formula $A$ all whose strictly positions occurrences of prime
formulas are of the form $\atom(r)$, by induction on $A$.  For all
other formulas we shall make use of the global assumption
$\texttt{Efq} \colon F \to \hat{P}$ (cf.\ Section~\ref{SS:GlobalAss}).
Similarly, Notice that from $\texttt{Stab-Atom}$ one again obtains
$((A \to F) \to F) \to A$ for every formula $A$ all whose strictly
positions occurrences of prime formulas are of the form $\atom(r)$, by
induction on $A$.  For all other formulas we shall make use of the
global assumption $\texttt{Stab} \colon ((\hat{P} \to F) \to F) \to
\hat{P}$ (cf.\ Section~\ref{SS:GlobalAss}).
\end{remark*}

% \begin{lemma}[\texttt{Eq-to-=}\index{Eq-to-=@\texttt{Eq-to-=}}]
% $\hat{n}_1 \Eq \hat{n}_2 \to E(\hat{n}_1) \to E(\hat{n}_2) \to
% \hat{n}_1 = \hat{n}_2$.
% \end{lemma}

% \begin{proof}
% By \texttt{Gen-Ind} on $\hat{n}_1$.  In case $\bottom$ notice that the
% premise $E(\bottom)$ and the conclusion $\bottom = \hat{n}_2$ are both
% equivalent to $\atom(\bottom)$.  

% In case $0$ for $\hat{n}_1$ we distinguish subcases according to the
% constructor form of $\hat{n}_2$.  In the subcase $\bottom$ for
% $\hat{n}_2$ we argue as before.  In the subcase $0$ for $\hat{n}_2$
% the conclusion $0=0$ follows from $\texttt{Truth-Axiom}$.  In the
% subcase $S \hat{n}_2$ for $\hat{n}_2$ from $0 \Eq S \hat{n}_2$ infer
% $F$ by $\texttt{Constr-Disjoint}$ and then $0 = S \hat{n}_2$ from
% $\texttt{Efq-Atom}$.

% In the step case for $\hat{n}_1$ we again distinguish subcases
% according to the constructor form of $\hat{n}_2$.  The subcases
% $\bottom$ and $0$ for $\hat{n}_2$ are treated as before.  In the
% subcase $S \hat{n}_2$ for $\hat{n}_2$ from $S \hat{n}_1 \Eq S
% \hat{n}_2$ infer $\hat{n}_1 \Eq \hat{n}_2$ by $\texttt{Constr-Inj}$,
% and also from $E(S \hat{n}_i)$ infer $E(\hat{n}_i)$ using $e(S
% \hat{n}) \Eq e(\hat{n})$.  Now the IH yields $\hat{n}_1 = \hat{n}_2$,
% hence $S \hat{n}_1 = S \hat{n}_2$, using $\eqrel{S \hat{n}_1}{S
% \hat{n}_2} \Eq \eqrel{\hat{n}_1}{\hat{n}_2}$.
% \end{proof}

% \begin{lemma}[\texttt{=-to-Eq}\index{equals-to-Eq@\texttt{=-to-Eq}}]
% $\hat{n}_1 = \hat{n}_2 \to \hat{n}_1 \Eq \hat{n}_2$.
% \end{lemma}

% \begin{proof}
% By \texttt{Gen-Ind} on $\hat{n}_1$.  In case $\bottom$ the premise is
% equivalent to $\atom(\bottom)$.  Now use $\texttt{Bottom-to-F}$
% and $\texttt{Efq-Eq}$.

% In case $0$ for $\hat{n}_1$ we distinguish subcases according to the
% constructor form of $\hat{n}_2$.  In the subcase $\bottom$ for
% $\hat{n}_2$ we argue as before.  In the subcase $0$ for $\hat{n}_2$
% the conclusion $0 \Eq 0$ follows from $\texttt{Eq-Refl}$.  In the
% subcase $S \hat{n}_2$ for $\hat{n}_2$ the premise $0 = S \hat{n}_2$ is
% equivalent to $\atom(\bottom)$.  Now again use $\texttt{Bottom-to-F}$
% and $\texttt{Efq-Eq}$.

% In the step case for $\hat{n}_1$ we again distinguish subcases
% according to the constructor form of $\hat{n}_2$.  The subcases
% $\bottom$ and $0$ for $\hat{n}_2$ are treated as before.  In the
% subcase $S \hat{n}_2$ for $\hat{n}_2$ from $S \hat{n}_1 = S \hat{n}_2$
% infer $\hat{n}_1 = \hat{n}_2$ (using $\eqrel{S \hat{n}_1}{S \hat{n}_2}
% \Eq \eqrel{\hat{n}_1}{\hat{n}_2}$).  Now the IH yields $\hat{n}_1 \Eq
% \hat{n}_2$, hence $S \hat{n}_1 \Eq S \hat{n}_2$, using
% $\texttt{Eq-Compat}$ and $\texttt{Eq-Refl}$.
% \end{proof}

% \begin{lemma}[\texttt{=-to-E}\index{equals-to-E@\texttt{=-to-E}}]
% $\hat{n}_1 = \hat{n}_2 \to E(\hat{n}_i)$.
% \end{lemma}

% \begin{proof}
% By \texttt{Gen-Ind} on $\hat{n}_1$.  In case $\bottom$ the premise is
% equivalent to $\atom(\bottom)$.  Now use $\texttt{Bottom-to-F}$
% and $\texttt{Efq-Atom}$.

% In case $0$ for $\hat{n}_1$ we distinguish subcases according to the
% constructor form of $\hat{n}_2$.  In the subcase $\bottom$ for
% $\hat{n}_2$ we argue as before.  In the subcase $0$ for $\hat{n}_2$
% the conclusion $E(0)$ follows from $\texttt{Atom-True}$.  In the
% subcase $S \hat{n}_2$ for $\hat{n}_2$ the premise $0 = S \hat{n}_2$ is
% equivalent to $\atom(\bottom)$.  Now again use $\texttt{Bottom-to-F}$
% and $\texttt{Efq-Atom}$.

% In the step case for $\hat{n}_1$ we again distinguish subcases
% according to the constructor form of $\hat{n}_2$.  The subcases
% $\bottom$ and $0$ for $\hat{n}_2$ are treated as before.  In the
% subcase $S \hat{n}_2$ for $\hat{n}_2$ from $S \hat{n}_1 = S \hat{n}_2$
% infer $\hat{n}_1 = \hat{n}_2$ (using $\eqrel{S \hat{n}_1}{S \hat{n}_2}
% \Eq \eqrel{\hat{n}_1}{\hat{n}_2}$).  The IH yields $E(\hat{n}_i)$,
% hence $E(S \hat{n}_i)$, using $e(S \hat{n}_i) \Eq e(\hat{n}_i)$.
% \end{proof}

% \begin{lemma}[\texttt{Total-to-E}\index{Total-to-E@\texttt{Total-to-E}}]
% $\Total(\hat{n}) \to E(\hat{n})$.
% \end{lemma}

% \begin{proof}
% By \texttt{Gen-Ind}.  In case $\bottom$ use \texttt{Bottom-not-Total}
% and \texttt{Efq-Atom}, and in case $0$ use $E(0)$.  For the step prove
% \[
% (\Total(\hat{n}) \to E(\hat{n})) \to \Total(S \hat{n}) \to E(S
% \hat{n}),
% \]
% using $\Total(S \hat{n}) \to \Total(\hat{n})$, i.e.\
% \texttt{Constr-Total-Args}, and $E(\hat{n}) \to E(S \hat{n})$; the
% latter follows from $e(S \hat{n}) \Eq e(\hat{n})$.
% \end{proof}

% \begin{lemma}[\texttt{E-to-Total}\index{E-to-Total@\texttt{E-to-Total}}]
% $E(\hat{n}) \to \Total(\hat{n})$.
% \end{lemma}

% \begin{proof}
% By \texttt{Gen-Ind}.  In case $\bottom$ use $\texttt{Bottom-to-F}
% \colon \atom(\bottom) \to F$ and $\texttt{Efq-Total} \colon
% F \to \Total(\bottom)$, and in case $0$ use $\texttt{Constr-Total}$.
% For the step prove
% \[
% (E(\hat{n}) \to \Total(\hat{n})) \to E(S \hat{n}) \to \Total(S
% \hat{n}),
% \]
% using $E(S \hat{n}) \to E(\hat{n})$ (from $e(S \hat{n}) \Eq 
% e(\hat{n})$), and $\Total(\hat{n}) \to \Total(S \hat{n})$; the
% latter follows from $\Total(S)$, i.e.\ $\texttt{Constr-Total}$.
% \end{proof}

% Then one can derive from general induction the form of induction
% one normally wants to apply.

% \begin{lemma}[\texttt{Ind}]
% \mylabel{L:Ind}
% $\hat{P}(0) \to (\forall n.\hat{P}(n) \to \hat{P}(S n)) \to 
% \forall n \hat{P}(n)$.
% \end{lemma}

% \begin{proof}%[Proof of \texttt{Ind} for $\nat$]
% By general induction applied to the formula $E(\hat{n}) \to
% \hat{P}(\hat{n})$.  In case $\bottom$ use $\texttt{E-to-Total}$ and
% $\texttt{Bottom-not-Total}$ to conclude $E(\bottom) \to F$, and then
% the global assumption $\texttt{Efq} \colon F \to \hat{P}(\bottom)$.
% The case $0$ is clear, and in the step case we need to prove $\forall
% \hat{n}.(E(\hat{n}) \to \hat{P}(\hat{n})) \to E(S \hat{n}) \to
% \hat{P}(S \hat{n})$ from $\forall \hat{n}.E(\hat{n}) \to
% \hat{P}(\hat{n}) \to \hat{P}(S \hat{n})$.  This follows from
% $\texttt{Constr-Total-Args}$, yielding $E(S \hat{n}) \to E(\hat{n})$.
% \end{proof}

% \begin{remark}
% Notice that every instance
% \[
% \subst{A}{x}{0} \to (\forall n.\subst{A}{x}{n} \to \subst{A}{x}{S n}) \to 
% \forall n \subst{A}{x}{n}
% \]
% of \texttt{Ind} for a formula $A$ without strictly positive
% occurrences of predicate variables can be derived without using the
% global assumption $\texttt{Efq}$.
% \end{remark}

% \begin{lemma}[\texttt{=-Refl-nat}%
% \index{equalfinalg-Refl-nat@\texttt{=-Refl-nat}}]
% $n=n$.
% \end{lemma}

\begin{proof}[Proof of \texttt{=-Refl-nat}]
Use \texttt{Ind}, and \texttt{Truth-Axiom} in both cases. -- Notice
that $\hat{n} = \hat{n}$ does \emph{not} hold, since
$\eqrel{\bottom}{\bottom} \Eq \bottom$.
\end{proof}

% We can also derive easily
% \begin{alignat*}{2}
% %
% &\hat{n}_1 = \hat{n}_2 \to \hat{n}_2 = \hat{n}_1
% &\quad&\text{\texttt{=-Symm-nat}}%
% \index{equalfinalg-Symm-nat@\texttt{=-Symm-nat}}
% \\
% &\hat{n}_1 = \hat{n}_2 \to \hat{n}_2 = \hat{n}_3 \to \hat{n}_1 = \hat{n}_3
% &\quad&\text{\texttt{=-Trans-nat}}%
% \index{equalfinalg-Trans-nat@\texttt{=-Trans-nat}}
% \\[1ex]
% &\hat{n}_1 = \hat{n}_2 \to E(\hat{n}_i)
% \\
% &0 = S \hat{n} \to F
% \\
% &S \hat{n}_1 = S \hat{n}_2 \to \hat{n}_1 = \hat{n}_2
% \\[1ex]
% &E(S \hat{n}) \to E(\hat{n})
% \\
% &E(0)
% \\
% &E(\hat{n}) \to E(S \hat{n})
%
% \end{alignat*}

% The following theorems are proved easily by boolean induction.
% \begin{alignat*}{2}
% %
% &\texttt{(aconst Efq-thm $\forall p.  F \to p$ \textsl{empty-subst})} 
% \index{Efq-thm@\texttt{Efq-thm}}
% \\
% &\texttt{(aconst Stab-thm $\forall p.  ((p \to F) \to F) \to p$ 
% \textsl{empty-subst})} 
% \index{Stab-thm@\texttt{Stab-thm}}
% \\
% &\texttt{(aconst Atomtrue $\forall p.  p \to p = \true$ 
% \textsl{empty-subst})} 
% \index{Atomtrue@\texttt{Atomtrue}}
% \\
% &\texttt{(aconst Atomfalse $\forall p.  (p \to F) \to p = \false$ 
% \textsl{empty-subst})} 
% \index{Atomfalse@\texttt{Atomfalse}}
% %
% \end{alignat*}

Here are some other examples of theorems; we give the internal
representation as assumption constants, which show how the assumed
formula is split into an uninstantiated formula and a substitution, in
this case a type substitution $\alpha \mapsto \rho$, an object
substitution $f^{\alpha \to \nat} \mapsto g^{\rho \to \nat}$ and a
predicate variable substitution $\hat{P}^{(\alpha)} \mapsto
\set{\hat{z}^\rho}{A}$.
\begin{alignat*}{2}
&\texttt{(aconst Cvind-with-measure-11}
\\
&\qquad \qquad \qquad\texttt{$
\forall f^{\alpha \to \nat}.
\bigl(\forall x^\alpha.\forall y(f(y) {<} f(x)  \to \hat{P}(y)) \to 
\hat{P}(x) \bigr) \to
\forall x \hat{P}(x)$}
\\
&\qquad \qquad \qquad 
\texttt{$(\alpha \mapsto \rho, 
f^{\alpha \to \nat} \mapsto g^{\rho \to \nat},
\hat{P}^{(\alpha)} \mapsto \set{\hat{z}^\rho}{A})$).} 
\index{Cvind-with-measure-11@\texttt{Cvind-with-measure-11}}
\\
&\texttt{(aconst Minpr-with-measure-l11}
\\
&\qquad \qquad \qquad\texttt{$
\forall f^{\alpha \to \nat}.
\excl x^\alpha \hat{P}(x) \to \excl x.\hat{P}(x) !
\forall y.f(y) {<} f(x)  \to \hat{P}(y) \to \bot$}
\\
&\qquad \qquad \qquad
\texttt{$(\alpha \mapsto \rho, 
f^{\alpha \to \nat} \mapsto g^{\rho \to \nat},
\hat{P}^{(\alpha)} \mapsto \set{\hat{z}^\rho}{A})$).} 
\index{Minpr-with-measure-l11@\texttt{Minpr-with-measure-l11}}
\end{alignat*}
Here $\excl$ is the classical existential quantifier defined by $\excl
x A := \forall x(A \to \bot) \to \bot$ with the logical form of
falsity $\bot$ (as opposed to the arithmetical form $(\texttt{atom}\
\false)$).  \texttt{l} indicates \inquotes{logic} (we have used the
logical form of falsity), the first \texttt{1} that we have one
predicate variable $\hat{P}$, and the second that we quantify over just one
variable $x$.  Both theorems can easily be generalized to more such
parameters.

When dealing with classical logic it will be useful to have
\begin{alignat*}{2}
&(\hat{P} \to \hat{P}_1) \to 
((\hat{P} \to \bot) \to \hat{P}_1) \to \hat{P}_1
&\quad&\text{\texttt{Cases-Log}\index{Cases-Log@\texttt{Cases-Log}}}
\end{alignat*}
The proof uses the global assumption \texttt{Stab-Log} (see below) for
$\hat{P}_1$; hence we cannot extract a term from it.

The assumption constants corresponding to these theorems are
generated by
\begin{alignat*}{2}
&\texttt{(theorem-name-to-aconst \textsl{name})}%
\index{theorem-name-to-aconst@\texttt{theorem-name-to-aconst}} 
\end{alignat*}

\subsection{Global assumptions}
\mylabel{SS:GlobalAss}
A global assumption\index{global assumption} is a special assumption
constant.  It provides a proposition whose proof does not concern us
pre\-sent\-ly.  Global assumptions are added, removed and displayed by
\begin{align*}
&\texttt{(add-global-assumption \textsl{name} \textsl{formula})}    
\index{add-global-assumption@\texttt{add-global-assumption}}
\quad \hbox{(abbreviated \texttt{aga}\index{aga@\texttt{aga}})}
\\
&\texttt{(remove-global-assumption \textsl{string1} \dots)}    
\index{remove-global-assumption@\texttt{remove-global-assumption}} 
\\
&\texttt{(display-global-assumptions \textsl{string1} \dots)}    
\index{display-global-assumptions@\texttt{display-global-assumptions}}
\end{align*}

We initially supply global assumptions for ex-falso-quodlibet and
stability, both in logical and arithmetical form (for our two
forms of falsity).
\begin{alignat*}{2}
&\bot \to \hat{P}
&\quad&\text{\texttt{Efq-Log}\index{Efq-Log@\texttt{Efq-Log}}}
\\
&((\hat{P} \to \bot) \to \bot) \to \hat{P}
&\quad&\text{\texttt{Stab-Log}\index{Stab-Log@\texttt{Stab-Log}}}
\\
&F \to \hat{P}
&\quad&\text{\texttt{Efq}\index{Efq@\texttt{Efq}}}
\\
&((\hat{P} \to F) \to F) \to \hat{P}
&\quad&\text{\texttt{Stab}\index{Stab@\texttt{Stab}}}
\end{alignat*}
The assumption constants corresponding to these global assumptions are
generated by
\begin{alignat*}{2}
&\texttt{(global-assumption-name-to-aconst \textsl{name})}%
\index{global-assumption-name-to-aconst@\texttt{global-ass{dots}-name-to-aconst}} 
\end{alignat*}


\section{Proofs}
\mylabel{Proof}
Proofs are built from assumption variables and assumption constants
(i.e.\ axioms, theorems and global assumption) by the usual rules of
natural deduction, i.e.\ introduction and elimination rules for
implication, conjunction and universal quantification.  From a proof
we can read off its \emph{context}\index{context}, which is an ordered
list of object and assumption variables.

\subsection{Constructors and accessors}
We have constructors, accessors and tests for assumption variables
\begin{alignat*}{2}
&\texttt{(make-proof-in-avar-form \textsl{avar})}        
\index{make-proof-in-avar-form@\texttt{make-proof-in-avar-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-avar-form-to-avar \textsl{proof})}    
\index{proof-in-avar-form-to-avar@\texttt{proof-in-avar-form-to-avar}}
&& \text{accessor,} 
\\
&\texttt{(proof-in-avar-form?\ \textsl{proof})}          
\index{proof-in-avar-form?@\texttt{proof-in-avar-form?}}
&& \text{test,}
\end{alignat*}
for assumption constants
\begin{alignat*}{2}
&\texttt{(make-proof-in-aconst-form \textsl{aconst})}     
\index{make-proof-in-aconst-form@\texttt{make-proof-in-aconst-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-aconst-form-to-aconst \textsl{proof})} 
\index{proof-in-aconst-form-to-aconst@\texttt{proof-in-aconst-form-to-aconst}}
&& \text{accessor} 
\\
&\texttt{(proof-in-aconst-form?\ \textsl{proof})}         
\index{proof-in-aconst-form?@\texttt{proof-in-aconst-form?}}
&& \text{test,}
\end{alignat*}
for implication introduction
\begin{alignat*}{2}
&\texttt{(make-proof-in-imp-intro-form \textsl{avar} \textsl{proof})}
\index{make-proof-in-imp-intro-form@\texttt{make-proof-in-imp-intro-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-imp-intro-form-to-avar \textsl{proof})}  
\index{proof-in-imp-intro-form-to-avar@\texttt{proof-in-imp-intro-form-to-avar}}
&&\text{accessor}
\\
&\texttt{(proof-in-imp-intro-form-to-kernel \textsl{proof})}
\index{proof-in-imp-intro-form-to-kernel@\texttt{pr{\dots}-imp-intro-form-to-kernel}}
&&\text{accessor}
\\
&\texttt{(proof-in-imp-intro-form?\ \textsl{proof})}        
\index{proof-in-imp-intro-form?@\texttt{proof-in-imp-intro-form?}}
&& \text{test,}
\end{alignat*}
for implication elimination
\begin{alignat*}{2}
&\texttt{(make-proof-in-imp-elim-form \textsl{proof1} \textsl{proof2})} 
\index{make-proof-in-imp-elim-form@\texttt{make-proof-in-imp-elim-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-imp-elim-form-to-op \textsl{proof})}   
\index{proof-in-imp-elim-form-to-op@\texttt{proof-in-imp-elim-form-to-op}}
&& \text{accessor} 
\\
&\texttt{(proof-in-imp-elim-form-to-arg \textsl{proof})}  
\index{proof-in-imp-elim-form-to-arg@\texttt{proof-in-imp-elim-form-to-arg}}
&& \text{accessor} 
\\
&\texttt{(proof-in-imp-elim-form?\ \textsl{proof})}       
\index{proof-in-imp-elim-form?@\texttt{proof-in-imp-elim-form?}}
&& \text{test,}
\end{alignat*}
for and introduction
\begin{alignat*}{2}
&\texttt{(make-proof-in-and-intro-form \textsl{proof1} \textsl{proof2})}  
\index{make-proof-in-and-intro-form@\texttt{make-proof-in-and-intro-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-and-intro-form-to-left \textsl{proof})} 
\index{proof-in-and-intro-form-to-left@\texttt{pr{\dots}and-intro-form-to-left}}
&&\text{accessor}
\\
&\texttt{(proof-in-and-intro-form-to-right \textsl{proof})}
\index{proof-in-and-intro-form-to-right@\texttt{pr{\dots}and-intro-form-to-right}}
&&\text{accessor}
\\
&\texttt{(proof-in-and-intro-form?\ \textsl{proof})}       
\index{proof-in-and-intro-form?@\texttt{proof-in-and-intro-form?}}
&& \text{test,}
\end{alignat*}
for and elimination
\begin{alignat*}{2}
&\texttt{(make-proof-in-and-elim-left-form \textsl{proof})}        
\index{make-proof-in-and-elim-left-form@\texttt{make-proof-in-and-elim-l{\dots}}}
&\quad& \text{constructor} 
\\
&\texttt{(make-proof-in-and-elim-right-form \textsl{proof})}
\index{make-proof-in-and-elim-right-form@\texttt{make-proof-in-and-elim-r{\dots}}}
&& \text{constructor} 
\\
&\texttt{(proof-in-and-elim-left-form-to-kernel \textsl{proof})}  
\index{proof-in-and-elim-left-form-to-kernel@\texttt{proof-in-and-elim{\dots}}}
&& \text{accessor} 
\\
&\texttt{(proof-in-and-elim-right-form-to-kernel \textsl{proof})} 
\index{proof-in-and-elim-right-form-to-kernel@\texttt{proof-in-and-elim{\dots}}}
&& \text{accessor} 
\\
&\texttt{(proof-in-and-elim-left-form?\ \textsl{proof})}          
\index{proof-in-and-elim-left-form?@\texttt{proof-in-and-elim-left-form?}}
&& \text{test} 
\\
&\texttt{(proof-in-and-elim-right-form?\ \textsl{proof})}         
\index{proof-in-and-elim-right-form?@\texttt{proof-in-and-elim-right-form?}}
&& \text{test,}
\end{alignat*}
for all introduction
\begin{alignat*}{2}
&\texttt{(make-proof-in-all-intro-form \textsl{var} \textsl{proof})}
\index{make-proof-in-all-intro-form@\texttt{make-proof-in-all-intro-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-all-intro-form-to-var \textsl{proof})}      
\index{proof-in-all-intro-form-to-var@\texttt{pr{\dots}all-intro-form-to-var}}
&& \text{accessor} 
\\
&\texttt{(proof-in-all-intro-form-to-kernel \textsl{proof})}   
\index{proof-in-all-intro-form-to-kernel@\texttt{pr{\dots}all-intro-form-to-kernel}}
&& \text{accessor} 
\\
&\texttt{(proof-in-all-intro-form?\ \textsl{proof})}           
\index{proof-in-all-intro-form?@\texttt{proof-in-all-intro-form?}}
&& \text{test,}
\end{alignat*}
for all elimination
\begin{alignat*}{2}
&\texttt{(make-proof-in-all-elim-form \textsl{proof} \textsl{term})} 
\index{make-proof-in-all-elim-form@\texttt{make-proof-in-all-elim-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-all-elim-form-to-op \textsl{proof})}        
\index{proof-in-all-elim-form-to-op@\texttt{proof-in-all-elim-form-to-op}}
&& \text{accessor} 
\\
&\texttt{(proof-in-all-elim-form-to-arg \textsl{proof})}       
\index{proof-in-all-elim-form-to-arg@\texttt{proof-in-all-elim-form-to-arg}}
&& \text{accessor} 
\\
&\texttt{(proof-in-all-elim-form?\ \textsl{proof})}            
\index{proof-in-all-elim-form?@\texttt{proof-in-all-elim-form?}}
&& \text{test}
\end{alignat*}
and for \texttt{cases}-constructs
\begin{alignat*}{2}
&\texttt{(make-proof-in-cases-form \textsl{test} \textsl{alt1} \dots)}       
\index{make-proof-in-cases-form@\texttt{make-proof-in-cases-form}}
&\quad& \text{constructor} 
\\
&\texttt{(proof-in-cases-form-to-test \textsl{proof})}         
\index{proof-in-cases-form-to-test@\texttt{proof-in-cases-form-to-test}}
&& \text{accessor} 
\\
&\texttt{(proof-in-cases-form-to-alts \textsl{proof})}         
\index{proof-in-cases-form-to-alts@\texttt{proof-in-cases-form-to-alts}}
&& \text{accessor} 
\\
&\texttt{(proof-in-cases-form-to-rest \textsl{proof})}         
\index{proof-in-cases-form-to-rest@\texttt{proof-in-cases-form-to-rest}}
&& \text{accessor} 
\\
&\texttt{(proof-in-cases-form?\ \textsl{proof})}               
\index{proof-in-cases-form?@\texttt{proof-in-cases-form?}}
&& \text{test.}
\end{alignat*}
It is convenient to have more general introduction and elimination
operators that take arbitrary many arguments.  The former works for
implication-introduction and all-introduction, and the latter for
implication-elimination, and-elimination and all-elimination.
\begin{alignat*}{2}
&\texttt{(mk-proof-in-intro-form \textsl{x1} \dots\ \textsl{proof})}
\index{mk-proof-in-intro-form@\texttt{mk-proof-in-intro-form}}
\\
&\texttt{(mk-proof-in-elim-form \textsl{proof} \textsl{arg1} \dots)}
\index{mk-proof-in-elim-form@\texttt{mk-proof-in-elim-form}}
\\
&\texttt{(proof-in-intro-form-to-kernel-and-vars \textsl{proof})}
\index{proof-in-intro-form-to-kernel-and-vars@\texttt{proof-in-intro-form-to{\dots}}}
\\
&\texttt{(proof-in-elim-form-to-final-op \textsl{proof})}
\index{proof-in-elim-form-to-final-op@\texttt{pr{\dots}elim-form-to-final-op}}
\\
&\texttt{(proof-in-elim-form-to-args \textsl{proof}).}     
\index{proof-in-elim-form-to-args@\texttt{proof-in-elim-form-to-args}}
\end{alignat*}
\texttt{(mk-proof-in-intro-form \textsl{x1} \dots\ \textsl{proof})} is
formed from proof by first abstracting \textsl{x1}, then \textsl{x2}
and so on.  Here \textsl{x1}, \textsl{x2} \dots can be assumption or
object variables.  We also provide
\begin{alignat*}{2}
&\texttt{(mk-proof-in-and-intro-form \textsl{proof} \textsl{proof1} \dots)}
\index{mk-proof-in-and-intro-form@\texttt{mk-proof-in-and-intro-form}}
\end{alignat*}

In our setup there are axioms rather than rules for the existential
quantifier.  However, sometimes it is useful to construct proofs as if
an existence introduction rule would be present; internally then an
existence introduction axiom is used.
\begin{alignat*}{2}
&\texttt{(make-proof-in-ex-intro-form \textsl{term} \textsl{ex-formula}
\textsl{proof-of-inst})}
\index{make-proof-in-ex-intro-form@\texttt{make-proof-in-ex-intro-form}}
\\
&\texttt{(mk-proof-in-ex-intro-form\ .\ }
\\
&\quad\texttt{\textsl{terms-and-ex-formula-and-proof-of-inst})}%
\index{mk-proof-in-ex-intro-form@\texttt{mk-proof-in-ex-intro-form}}
\end{alignat*}

Moreover we need
\begin{alignat*}{2}
&\texttt{(proof?\ \textsl{x})}
\index{proof?@\texttt{proof?}}
\\
&\texttt{(proof=?\ \textsl{proof1} \textsl{proof2})}
\index{proof=?@\texttt{proof=?}}
\\
&\texttt{(proofs=?\ \textsl{proofs1} \textsl{proofs2})}
\index{proofs=?@\texttt{proofs=?}}
\\
&\texttt{(proof-to-formula \textsl{proof})}
\index{proof-to-formula@\texttt{proof-to-formula}}
\\
&\texttt{(proof-to-context \textsl{proof})}
\index{proof-to-context@\texttt{proof-to-context}}
\\
&\texttt{(proof-to-free \textsl{proof})}
\index{proof-to-free@\texttt{proof-to-free}}
\\
&\texttt{(proof-to-free-avars \textsl{proof})}
\index{proof-to-free-avars@\texttt{proof-to-free-avars}}
\\
&\texttt{(proof-to-bound-avars \textsl{proof})}
\index{proof-to-bound-avars@\texttt{proof-to-bound-avars}}
\\
&\texttt{(proof-to-free-and-bound-avars \textsl{proof})}
\index{proof-to-free-and-bound-avars@\texttt{proof-to-free-and-bound-avars}}
\\
&\texttt{(proof-to-aconsts-without-rules \textsl{proof}).}
\index{proof-to-aconsts-without-rules@\texttt{proof-to-aconsts-without-rules}}
\\
&\texttt{(proof-to-aconsts \textsl{proof}).}
\index{proof-to-aconsts@\texttt{proof-to-aconsts}}
\end{alignat*}
To work with contexts we need
\begin{alignat*}{2}
&\texttt{(context-to-vars\ \textsl{context})}
\index{context-to-vars@\texttt{context-to-vars}}
\\
&\texttt{(context-to-avars\ \textsl{context})}
\index{context-to-avars@\texttt{context-to-avars}}
\\
&\texttt{(context=?\ \textsl{context1} \textsl{context2}).}
\index{context=?@\texttt{context=?}}
\end{alignat*}

\subsection{Normalization}
Normalization of proofs will be done by reduction to normalization of
terms.  (1) Construct a term from the proof.  To do this properly,
create for every free avar in the given proof a new variable whose
type comes from the formula of the avar; store this information.  Note
that in this construction one also has to create new variables for the
bound avars.  Similary to avars we have to treat assumption constants
which are not axioms, i.e.\ theorems or global assumptions.  (2)
Normalize the resulting term.  (3) Reconstruct a normal proof from
this term, the end formula and the stored information.  -- The critical
variables are carried along for efficiency reasons.

To assign recursion constants to induction constants, we need to
associate type variables with predicate variables, in such a way that
we can later refer to this assignment.  Therefore we carry along a
procedure \texttt{pvar-to-tvar} which remembers the assignment done so far
(cf.\ \texttt{make-rename}).

Due to our distinction between general variables $\verb#x^0#,
\verb#x^1#, \verb#x^2#, \dots$ and variables $\texttt{x0},
\texttt{x1}, \texttt{x2}, \dots$ intended to range over existing
(i.e.\ total) objects only, $\eta$-conversion of proofs cannot be done
via reduction to $\eta$-conversion of terms.  To see this, consider
the proof
\[
\AxiomC{$\forall \hat{x} P \hat{x}$}
\AxiomC{$x$}
\BinaryInfC{$P x$}
\UnaryInfC{$\forall x P x$}
\UnaryInfC{$\forall \hat{x} P \hat{x} \to \forall x P x$}
\DisplayProof
\]
The proof term is $\lambda u \lambda x. u x$.  If we $\eta$-normalize
this to $\lambda u u$, the proven formula would be all $\forall
\hat{x} P \hat{x} \to \forall \hat{x} P \hat{x}$.  Therefore we split
\texttt{nbe-normalize-proof} into
\texttt{nbe-normalize-proof-without-eta} and \texttt{proof-to-eta-nf}.

Moreover, for a full normalization of proofs (including permutative
conversions) we need a preprocessing step that $\eta$-expands each
ex-elim axiom such that the conclusion is atomic or existential.



% \subsection*{Interface}
We need the following functions.
\begin{alignat*}{2}
&\texttt{(proof-and-genavar-var-alist-to-pterm \textsl{pvar-to-tvar}  
\textsl{proof})}
\\
&\texttt{(npterm-and-var-genavar-alist-and-formula-to-proof}
\\
&\quad \texttt{\textsl{npterm} \textsl{var-genavar-alist} \textsl{crit}
\textsl{formula})}
\\
&\texttt{(elim-npterm-and-var-genavar-alist-to-proof}
\\
&\quad \texttt{\textsl{npterm} \textsl{var-genavar-alist} \textsl{crit})}.
\end{alignat*}
Then we can define \texttt{nbe-normalize-proof}%
\index{nbe-normalize-proof@\texttt{nbe-normalize-proof}}, abbreviated
\texttt{np}\index{np@\texttt{np}}.

\subsection{Substitution}
In a proof we can substitute
\begin{itemize}
\item types for type variables (by a type variable substitution
\texttt{tsubst}),
\item terms for variables (by a substitution \texttt{subst}),
\item comprehension terms for predicate variables (by a predicate
variable substitution \texttt{psubst}), and
\item proofs for assumption variables (by a assumption variable
substitution \texttt{asubst}).
\end{itemize}
It is assumed that \texttt{subst} only affects those vars whose type
is not changed by \texttt{tsubst}, \texttt{psubst} only affects those
predicate variables whose arity is not changed by \texttt{tsubst}, and
that \texttt{asubst} only affects those assumtion variabless whose
formula is not changed by \texttt{tsubst}, \texttt{subst} and
\texttt{psubst}.

In the abstraction cases of the recursive definition, the abstracted
variable (or assumption variable) may need to be renamed.  However,
its type (or formula) can be affected by \texttt{tsubst} (or
\texttt{tsubst}, \texttt{subst} and \texttt{psubst}).  Then the
renaming cannot be made part of \texttt{subst} (or \texttt{asubst}),
because the condition above would be violated.  Therefore we carry
along procedures \texttt{rename} renaming variables and
\texttt{arename} for assumption variables, which remember the renaming
done so far.

All these substitutions can be packed together, as an argument
\texttt{topasubst} for \texttt{proof-substitute}.
\begin{alignat*}{2}
&\texttt{(proof-substitute \textsl{proof} \textsl{topasubst})}
\index{proof-substitute@\texttt{proof-substitute}}
\end{alignat*}
If we want to substitute for a single variable only (which can be a
type-, an object-, a predicate - or an assumption-variable), then
we can use
\begin{alignat*}{2}
&\texttt{(proof-subst \textsl{proof} \textsl{arg} \textsl{val})}
\index{proof-subst@\texttt{proof-subst}}
\end{alignat*}

The procedure \texttt{expand-theorems} expects a proof and a test
whether a string denotes a theorem to be replaced by its proof.  The
result is the (normally quite long) proof obtained by replacing the
theorems by their saved proofs.
\begin{alignat*}{2}
&\texttt{(expand-theorems \textsl{proof} \textsl{name-test?})}
\index{expand-theorems@\texttt{expand-theorems}}
\end{alignat*}

\subsection{Display}
There are many ways to display a proof.  We normally use
\texttt{display-proof} for a linear representation, showing the
formulas and the rules used.  When we in addition want to check the
correctness of the proof, we can use \texttt{check-and-display-proof}.

However, we also provide a readable type-free lambda expression via
\texttt{(proof-to-expr
\textsl{proof})}\index{proof-to-expr@\texttt{proof-to-expr}}.

To display proofs we use the following functions.  In case the
optional proof argument is not present, the current proof of an
interactive proof development is taken instead.
\begin{alignat*}{2}
&\texttt{(display-proof\ .\ \textsl{opt-proof})}
\index{display-proof@\texttt{display-proof}}
&\quad& \text{abbreviated \texttt{dp}\index{dp@\texttt{dp}}}
\\
&\texttt{(check-and-display-proof\ .\ \textsl{opt-proof})}
\index{check-and-display-proof@\texttt{check-and-display-proof}}
&\quad& \text{abbreviated \texttt{cdp}\index{dp@\texttt{cdp}}}
\\
&\texttt{(display-pterm\ .\ \textsl{opt-proof})}
\index{display-pterm@\texttt{display-pterm}}
&\quad& \text{abbreviated \texttt{dpt}\index{dpt@\texttt{dpt}}}
\\
&\texttt{(display-proof-expr\ .\ \textsl{opt-proof})}
\index{display-proof-expr@\texttt{display-proof-expr}}
&\quad& \text{abbreviated \texttt{dpe}\index{dpe@\texttt{dpe}}}
\end{alignat*}
We also provide versions which normalize the proof first:
\begin{alignat*}{2}
&\texttt{(display-normalized-proof\ .\ \textsl{opt-proof})}
\index{display-normalized-proof@\texttt{display-normalized-proof}}
&\quad& \text{abbreviated \texttt{dnp}\index{dnp@\texttt{dnp}}}
\\
&\texttt{(display-normalized-pterm\ .\ \textsl{opt-proof})}
\index{display-normalized-pterm@\texttt{display-normalized-pterm}}
&\quad& \text{abbreviated \texttt{dnpt}\index{dnpt@\texttt{dnpt}}}
\\
&\texttt{(display-normalized-proof-expr\ .\ \textsl{opt-proof})}
\index{display-normalized-proof-expr@\texttt{display-normalized-proof-expr}}
&\quad& \text{abbreviated \texttt{dnpe}\index{dnpe@\texttt{dnpe}}}
\end{alignat*}

\subsection{Classical logic}
\texttt{(proof-of-stab-at
\textsl{formula})}\index{proof-of-stab-at@\texttt{proof-of-stab-at}}
generates a proof of $((A \to F) \to F) \to A$.  For $F$, $T$ one takes
the obvious proof, and for other atomic formulas the proof using cases
on booleans.  For all other prime or existential formulas one takes an
instance of the global assumption \texttt{Stab}: $((\hat{P} \to F) \to
F) \to \hat{P}$.  Here the argument \textsl{formula} must be unfolded.
For the logical form of falsity we take \texttt{(proof-of-stab-log-at
\textsl{formula})}\index{proof-of-stab-log-at@\texttt{proof-of-stab-log-at}},
and similary for ex-falso-quodlibet we provide
\begin{alignat*}{2}
&\texttt{(proof-of-efq-at \textsl{formula})}%
\index{proof-of-efq-at@\texttt{proof-of-efq-at}}
\\
&\texttt{(proof-of-efq-log-at \textsl{formula})}%
\index{proof-of-efq-log-at@\texttt{proof-of-efq-log-at}}
\end{alignat*}
Using these functions we can then define \texttt{(reduce-efq-and-stab
\textsl{proof})}\index{reduce-efq-and-stab@\texttt{reduce-efq-and-stab}},
which reduces all instances of stability and ex-falso-quodlibet axioms
in a proof to instances of these global assumptions with prime or
existential formulas, or (if possible) replaces them by their proofs.

With \texttt{rm-exc}\index{rm-exc@\texttt{rm-exc}} we can transform a
proof involving classical existential quantifiers in another one
without, i.e.\ in minimal logic.  The Exc-Intro and Exc-Elim theorems
are replaced by their proofs, using \texttt{expand-theorems}.


\section{Interactive theorem proving with partial proofs}
\mylabel{Pproof}
\subsection{Partial proofs}
A partial proof is a proof with holes, i.e.\ special
assumption variables (called goal variables) \texttt{v}, \texttt{v1},
\texttt{v2} \dots whose formulas must be closed.  We assume that every
goal variable \texttt{v} has a single occurrence in the proof.  We
then select a (not necessarily maximal) subproof \texttt{vx1...xn}
with distinct object or assumption variables \texttt{x1...xn}.  Such a
subproof is called a \emph{goal}\index{goal}.  When interactively
developing a partial proof, a goal \texttt{vx1...xn} is replaced by
another partial proof, whose context is a subset of \texttt{x1...xn}
(i.e.\ the context of the goal with \texttt{v} removed).

To gain some flexibility when working on our goals, we do not at each
step of an interactive proof development traverse the partial proof
searching for the remaining goals, but rather keep a list of all open
goals together with their numbers as we go along.  We maintain a
global variable \texttt{PPROOF-STATE} containing a list of three
elements: (1) \texttt{num-goals}, an alist of entries \texttt{(number
  goal drop-info hypname-info)}, (2) \texttt{proof} and (3)
\texttt{maxgoal}, the maximal goal number used.

At each stage of an interactive proof development we have access
to the current proof and the current goal by executing
\begin{alignat*}{2}
&\texttt{(current-proof)}\index{current-proof@\texttt{current-proof}}
\\ 
&\texttt{(current-goal)}\index{current-goal@\texttt{current-goal}}
\end{alignat*}

\subsection{Interactive theorem proving}
For interactively building proofs we need
\begin{alignat*}{2}
&\texttt{(goal-to-goalvar \textsl{goal})}%
\index{goal-to-goalvar@\texttt{goal-to-goalvar}} 
\\
&\texttt{(goal-to-context \textsl{goal})}%
\index{goal-to-context@\texttt{goal-to-context}} 
\\
&\texttt{(goal-to-formula \textsl{goal})}%
\index{goal-to-formula@\texttt{goal-to-formula}} 
\\ 
&\texttt{(goal=?\ \textsl{proof} \textsl{goal})}%
\index{goal=?@\texttt{goal=?}}
\\
&\texttt{(goal-subst \textsl{proof} \textsl{goal} \textsl{proof1})}%
\index{goal-subst@\texttt{goal-subst}} 
\\
&\texttt{(pproof-state-to-num-goals)}%
% \index{pproof-state-to-num-goals@\texttt{pproof-state-to-num-goals}}
\\ 
&\texttt{(pproof-state-to-proof)}%
\index{pproof-state-to-proof@\texttt{pproof-state-to-proof}}
\\ 
&\texttt{(pproof-state-to-formula)}%
\index{pproof-state-to-formula@\texttt{pproof-state-to-formula}}
\\ 
&\texttt{(display-current-goal)}%
\index{display-current-goal@\texttt{display-current-goal}} 
\\
&\texttt{(display-current-goal-with-normalized-formulas)}%
\index{display-current-goal-with-normalized-formulas@\texttt{display-current-goal-with{\dots}}}
\\ 
% &\texttt{(display-current-proof)}%
% \index{display-current-proof@\texttt{display-current-proof}} 
% \\ 
% &\texttt{(display-current-pterm)}%
% \index{display-current-pterm@\texttt{display-current-pterm}} 
% \\ 
&\texttt{(display-current-pproof-state)}%
\index{display-current-pproof-state@\texttt{display-current-num-goals{\dots}}} 
\end{alignat*}

We list some commands for interactively building proofs.

\subsubsection{set-goal}  An interactive proof starts with \texttt{(set-goal
\textsl{formula})}\index{set-goal@\texttt{set-goal}}, i.e.\ with
setting a goal.  Here \textsl{formula} should be closed; if it is not,
universal quantifiers are inserted automatically.

\subsubsection{normalize-goal}  \texttt{(normalize-goal
\textsl{goal})}\index{normalize-goal@\texttt{normalize-goal}}
(abbreviated \texttt{ng}\index{ng@\texttt{ng}}) replaces every formula
in the goal by its normal form.

\subsubsection{assume}  With \texttt{(assume \textsl{x1}
\dots)}\index{assume@\texttt{assume}} we can move universally
quantified variables and hypotheses into the context.  The variables
must be given names (known to the parser as valid variable names for
the given type), and the hypotheses should be identified by numbers
or strings.

\subsubsection{use}  In \texttt{(use \textsl{x}
. \textsl{elab-path-and-terms})}\index{use@\texttt{use}}, \textsl{x} is
\begin{itemize}
\item a number or string identifying a hypothesis form the context,
\item the string \inquotes{Truth-Axiom},
\item the name of a theorem or global assumption.  If it is a global
assumption whose final conclusion is a nullary predicate variable
distinct from $\bot$ (e.g.\ \texttt{Efq-Log} or \texttt{Stab-Log}),
this predicate variable is substituted by the goal formula.
\item a closed proof,
\item a formula with free variables from the context, generating a new
goal.
\end{itemize}
The optional \textsl{elab-path-and-terms} is a list consisting of
symbols \texttt{left} or \texttt{right}, giving directions in case the
used formula contains conjunctions, and of terms.  The universal
quantifiers of the used formula are instantiated (via
\texttt{pattern-unify}\index{pattern-unify@\texttt{pattern-unify}})
with appropriate terms in case a conclusion has the form of the goal.
The terms provided are substituted for those variables that cannot be
instantiated by pattern unification (e.g.\ using $\forall x.P x \to
\bot$ for the goal $\bot$).  For the instantiated premises new goals
are created.
          
\subsubsection{use-with}  This is a more verbose form of \texttt{use}, where
the terms are not inferred via unification, but have to be given
explicitely.  Also, for the instantiated premises one can indicate how
they are to come about.  So in \texttt{(use-with \textsl{x}
. \textsl{x-list})}\index{use-with@\texttt{use-with}}, \textsl{x} is
as in \texttt{use}, and \textsl{x-list} is a list consisting of
\begin{itemize}
\item a number or string identifying a hypothesis form the context,
\item the name of a theorem or global assumption,
\item a closed proof,
\item the string \inquotes{?} (value of \texttt{DEFAULT-GOAL-NAME}),
generating a new goal,
\item a symbol \texttt{left} or \texttt{right},
\item a term, whose free variables are added to the context,
\item a type, which is substituted for the first type variable,
\item a comprehension term, which is substituted for the first predicate
variable.
\end{itemize}

Notice that new free variables not in the ordered context can be
introduced in \texttt{use-with}.  They will be present in the newly
generated goals.  The reason is that proofs should be allowed to
contain free variables.  This is necessary to allow logic in ground
types where no constant is available (e.g\ to prove $\forall x Px \to
\forall x \neg Px \to \bot$).

Notice also that there are situations where \textsl{use-with} can be
applied but \textsl{use} can not.  For an example, consider the goal
$P(S(k+l))$ with the hypothesis $\forall l P(k+l)$ in the context.
Then \textsl{use} cannot find the term $S l$ by matching; however,
applying \textsl{use-with} to the hyposthesis and the term $S l$
succeeds (since $k+S l$ and $S(k+l)$ have the same normal form).

\subsubsection{inst-with}  \texttt{inst-with} does for forward chaining the
same as use-with for backward chaining.  It replaces the present goal
by a new one, with one additional hypothesis obtained by instantiating
a previous one.  Notice that this effect could also be obtained by
cut.  In \texttt{(inst-with \textsl{x}
. \textsl{x-list})}\index{inst-with@\texttt{inst-with}}, \textsl{x} is
\begin{itemize}
\item a number or string identifying a hypothesis form the context,
\item the name of a theorem or global assumption,
\item a closed proof,
\item a formula with free variables from the context, generating a new
goal.
\end{itemize}
and \textsl{x-list} is a list consisting of
\begin{itemize}
\item a number or string identifying a hypothesis form the context,
\item the name of a theorem or global assumption,
\item a closed proof,
\item the string \inquotes{?} (value of \texttt{DEFAULT-GOAL-NAME}),
generating a new goal,
\item a symbol \texttt{left} or \texttt{right},
\item a term, whose free variables are added to the context,
\item a type, which is substituted for the first type variable,
\item a comprehension term, which is substituted for the first predicate
variable.
\end{itemize}

\subsubsection{inst-with-to}  
\texttt{inst-with-to}\index{inst-with-to@\texttt{inst-with-to}}
expects a string as its last argument, which is used (via
\texttt{name-hyp}) to name the newly introduced instantiated
hypothesis.

\subsubsection{cut} The command \texttt{(cut
\textsl{A})}\index{cut@\texttt{cut}} replaces the goal $B$ by the two
new goals $A$ and $A \to B$.

\subsubsection{strip} To move (all or $n$) universally quantified variables 
and hypotheses of the current goal into the context, we uns the
command \texttt{(strip)}\index{strip@\texttt{strip}} or \texttt{(strip
n)}.

\subsubsection{drop} In
\texttt{(drop .\ x-list)}\index{drop@\texttt{drop}}, x-list is a list
of numbers or strings identifying hypotheses from the context.  A new
goal is created, which differs from the previous one only in display
aspects: the listed hypotheses are hidden (but still present).  If
x-list is empty, all hypotheses are hidden.

\subsubsection{name-hyp} The command 
\texttt{name-hyp}\index{name-hyp@\texttt{name-hyp}} expects an index
$i$ and a string.  Then a new goal is created, which differs from the
previous one only in display aspects: the string is used to label the
$i$th hypothesis.

\subsubsection{split} The command 
\texttt{(split)}\index{split@\texttt{split}} 
expects a conjunction $A \land B$ as goal and splits it into the
two new goals $A$ and $B$.

\subsubsection{get} To be able to work on a goal different from that on 
top of the goal stack, we have have to move it up using \texttt{(get
\textsl{n})}\index{get@\texttt{get}}.

\subsubsection{undo} With
\texttt{(undo .\ \textsl{n})}\index{undo@\texttt{undo}}, the last $n$
steps of an interactive proof can be made undone.  \texttt{(undo)}
 has the same effect as \texttt{(undo 1)}.

\subsubsection{ind} \texttt{(ind)}\index{ind@\texttt{ind}} expects a
goal $\forall x^\rho A$ with $\rho$ an algebra.  Let $c_1, \dots, c_n$
be the constructors of the algebra $\rho$.  Then $n$ new goals
$\forall \vec{x}_i.  \subst{A}{x}{x_{1i}} \to \dots \to
\subst{A}{x}{x_{ki}} \to \subst{A}{x}{c_i \vec{x}_i}$ are generated.

\texttt{(ind \textsl{t})} expects a goal $\subst{A}{x}{t}$.  It
computes the algebra $\rho$ as type of the term $t$.  Then again 
$n$ new goals $\forall \vec{x}_i.  \subst{A}{x}{x_{1i}} \to \dots \to
\subst{A}{x}{x_{ki}} \to \subst{A}{x}{c_i \vec{x}_i}$ are generated.

\subsubsection{simind} \texttt{(simind \textsl{all-formula1}
\dots)}\index{simind@\texttt{simind}} also expects a goal $\forall
x^\rho A$ with $\rho$ an algebra.  Then we have to provide the other
all formulas to be proved simultaneously with the given one.

\subsubsection{intro} \texttt{(intro i .\ terms)}\index{intro@\texttt{intro}}
expects as goal an inductively defined predicate.  The $i$-th
introduction axiom for this predicate is applied, via \texttt{use}
(hence \texttt{terms} may have to be provided).

\subsubsection{elim} \texttt{(elim)}\index{elim@\texttt{elim}} expects a
goal $I(\vec{t}) \to \subst{A}{\vec{x}}{\vec{t}}$.  Then the
(strengthened) clauses are generated as new goals, via \texttt{use-with}.

\subsubsection{ex-intro} In \texttt{(ex-intro
\textsl{term})}\index{ex-intro@\texttt{ex-intro}}, the user provides a
term to be used for the present (existential) goal.
\texttt{(exnc-intro \textsl{x})}\index{exnc-intro@\texttt{exnc-intro}}
works similarly for the \texttt{exnc}-quanhtifier.

\subsubsection{ex-elim} In \texttt{(ex-elim
\textsl{x})}\index{ex-elim@\texttt{ex-elim}}, \textsl{x} is
\begin{itemize}
\item a number or string identifying an existential hypothesis from 
the context,
\item the name of an existential global assumption or theorem,
\item a closed proof on an existential formula,
\item an existential formula with free variables from the context, 
genera\-ting a new goal.
\end{itemize}
Let $\ex y A$ be the existential formula identified by \textsl{x}.
The user is then asked to provide a proof for the present goal,
assuming that a $y$ satisfying $A$ is available.  \texttt{(exnc-elim
\textsl{x})}\index{exnc-elim@\texttt{exnc-elim}} works similarly for
the \texttt{exnc}-quanhtifier.

\subsubsection{by-assume-with} Suppose we are proving a goal $G$
from an existential hypothesis $ExHyp \colon \ex y A$.  Then the
natural way to use this hypothesis is to say \inquotes{by $ExHyp$
assume we have a $y$ satisfying $A$}.  Correspondingly we provide
\texttt{(by-assume-with \textsl{x} \textsl{y}
\textsl{u})}\index{by-assume-with@\texttt{by-assume-with}}.  Here
\textsl{x} -- as in \texttt{ex-elim} -- identifies an existential
hypothesis, and we assume (i.e.\ add to the context) the variable $y$
and -- with label $u$ -- the kernel $A$.  \texttt{(by-assume-with
\textsl{x} \textsl{y} \textsl{u})} is implemented by the sequence
\texttt{(ex-elim \textsl{x})}, \texttt{(assume \textsl{y}
\textsl{u})}, \texttt{(drop \textsl{x})}. \texttt{by-exnc-assume-with}%
\index{by-exnc-assume-with@\texttt{by-exnc-assume-with}}
works similarly for the \texttt{exnc}-quantifier.

\subsubsection{cases} \texttt{(cases)}\index{cases@\texttt{cases}} expects a
goal $\forall x^\rho A$ with $\rho$ an algebra.  Assume that $c_1,
\dots, c_n$ are the constructors of the algebra $\rho$.  Then $n$ new
(simplified) goals $\forall \vec{x}_i \subst{A}{x}{c_i \vec{x}_i}$ are
generated.

\texttt{(cases \textsl{t})} expects a goal $\subst{A}{x}{t}$.  It
computes the algebra $\rho$ as type of the term $t$.  Then again $n$
new goals $\forall \vec{x}_i \subst{A}{x}{c_i \vec{x}_i}$ are
generated.

\texttt{(cases \textsl{'auto})} expects an
atomic goal and checks whe\-ther its boolean kernel contains an if-term
whose test is neither an if-term nor contains bound variables.  With
the first such test \texttt{(cases \textsl{test})} is called.

\subsubsection{casedist} \texttt{(casedist \textsl{t})} replaces the goal 
$A$ containing a boolean term $t$ by two new goals $(\texttt{atom}\ t)
\to \subst{A}{t}{\true}$ and $((\texttt{atom}\ t) \to \false) \to
\subst{A}{t}{\false}$.

\subsubsection{simp}
In \texttt{(simp \textsl{opt-dir} \textsl{x} .
  \textsl{elab-path-and-terms})}\index{simp@\texttt{simp}}, the
optional argument \textsl{opt-dir} is either the string
\inquotes{\texttt{<-}} or missing.  \textsl{x} is
\begin{itemize}
\item a number or string identifying a hypothesis form the context,
\item the name of a theorem or global assumption,
\item a closed proof,
\item a formula with free variables from the context, generating a new
goal.
\end{itemize}
The optional \textsl{elab-path-and-terms} is a list consisting of
symbols \texttt{left} or \texttt{right}, giving directions in case the
used formula contains conjunctions, and of terms.  The universal
quantifiers of the used formula are instantiated with appropriate
terms to match a part of the goal.  The terms provided are substituted
for those variables that cannot be inferred.  For the instantiated
premises new goals are created.  This generates a used formula, which
is to be an atom, a negated atom or $t \approx s$.  If it as a
(negated) atom, it is checked whether the kernel or its normal form is
present in the goal.  If so, it is replace by \texttt{T} (or
\texttt{F}).  If it is an equality $t=s$ or $t \approx s$ with $t$ or
its normal form present in the goal, $t$ is replaced by $s$.  In case
\inquotes{\texttt{<-}} exchange $t$ and $s$.

\subsubsection{simp-with}  This is a more verbose form of \texttt{simp},
where the terms are not inferred via matching, but have to be given
explicitely.  Also, for the instantiated premises one can indicate how
they are to come about.  So in \texttt{(simp-with \textsl{opt-dir}
  \textsl{x} .  \textsl{x-list})}\index{simp-with@\texttt{simp-with}},
\textsl{opt-dir} and \textsl{x} are as in \texttt{simp}, and
\textsl{x-list} is a list consisting of
\begin{itemize}
\item a number or string identifying a hypothesis form the context,
\item the name of a theorem or global assumption,
\item a closed proof,
\item the string \inquotes{?} (value of \texttt{DEFAULT-GOAL-NAME}),
generating a new goal,
\item a symbol \texttt{left} or \texttt{right},
\item a term, whose free variables are added to the context,
\item a type, which is substituted for the first type variable,
\item a comprehension term, which is substituted for the first predicate
variable.
\end{itemize}

% \subsubsection{simp, simpeq} \texttt{(simp x)}\index{simp@\texttt{simp}} 
% expects a known fact of the form $r^{\boole}$, $\neg r^{\boole}$ or
% $t=s$.  In case $r^{\boole}$ the boolean term $r^{\boole}$ in the goal
% is replaced by $T$, and in case $\neg r^{\boole}$ by $F$.  In case
% $t=s$ the goal is written in the form $\subst{A}{x}{t}$.  Using
% Compat-Rev $\forall x,y.x=y \to P y \to P x$ with $\set{x}{A}$ for
% $P$, $t$ for $x$ and $s$ for $y$ the goal $\subst{A}{x}{t}$ is
% replaced by $\subst{A}{x}{s}$.

% In \texttt{(simp \textsl{x})}\index{simp@\texttt{simp}}, \textsl{x} is
% \begin{itemize}
% \item a number or string identifying a hypothesis form the context,
% \item the name of a theorem or global assumption, or
% \item a closed proof,
% \end{itemize}
% in each case for $r^{\boole}$, $\neg r^{\boole}$ or $t=s$.

% Similarly, \texttt{(simpeq x)}\index{simpeq@\texttt{simpeq}} needs to
% know $t \approx s$.  The goal is written in the form
% $\subst{A}{x}{t}$.  Using Eq-Compat-Rev $\forall x,y. x \approx y \to P y
% \to P x$ with $\set{x}{A}$ for $P$, $t$ for $x$ and $s$ for $y$ the
% goal $\subst{A}{x}{t}$ is replaced by $\subst{A}{x}{s}$.

\subsubsection{min-pr} In \texttt{(min-pr \textsl{x} \textsl{measure})}%
\index{min-pr@\texttt{min-pr}}, \textsl{x} is
\begin{itemize}
\item a number or string identifying a classical existential hypothesis 
from the context,
\item the name of a classical existential global assumption or theorem,
\item a closed proof on a classical existential formula,
\item a classical existential formula with free variables from the context, 
generating a new goal.
\end{itemize}
The result is a new implicational goal, whose premise provides the
(classical) existence of instances with least measure.

\subsubsection{exc-intro} In \texttt{(exc-intro
\textsl{terms})}\index{exc-intro@\texttt{exc-intro}}, the user provides
terms to be used for the present (classical existential) goal.

\subsubsection{exc-elim} In \texttt{(exc-elim
\textsl{x})}\index{exc-elim@\texttt{exc-elim}}, \textsl{x} is
\begin{itemize}
\item a number or string identifying a classical existential hypothesis 
from the context,
\item the name of a classical existential global assumption or theorem,
\item a closed proof on a classical existential formula,
\item a classical existential formula with free variables from the context, 
generating a new goal.
\end{itemize}
Let $\exca \vec{y} \vec{A}$ or $\excl \vec{y} \vec{A}$ be the
classical existential formula identified by \textsl{x}.  The user is
then asked to provide a proof for the present goal, assuming that terms
$\vec{y}$ satisfying $\vec{A}$ are available.

\subsubsection{pair-elim} In 
\texttt{(pair-elim)}\index{pair-elim@\texttt{pair-elim}}, a goal
$\forall p P(p)$ is replaced by the new goal $\forall x_1, x_2
P(\pair{x_1}{x_2})$.


\section{Search}
Following \textsc{Miller}\index{Miller} \cite{Miller91b} and
\textsc{Berger}\index{Berger}, we have implemented a proof search
algorithm for minimal logic.  To enforce termination, every assumption
can only be used a fixed number of times.

We begin with a short description of the theory involved.

$Q$ always denotes a $\forall \exists \forall$-prefix, say $\forall
\vec{x} \exists \vec{y} \forall \vec{z}$, with distinct variables.  We
call $\vec{x}$ the \emph{signature variables}, $\vec{y}$ the
\emph{flexible variables} and $\vec{z}$ the \emph{forbidden variables}
of $Q$, and write $Q_\exists$ for the existential part $\exists
\vec{y}$ of $Q$.

\emph{$Q$-terms}\index{Q-term@$Q$-term} are inductively defined by the
following clauses.
\begin{itemize}
\item If $u$ is a universally quantified variable in $Q$ or a
constant, and $\vec{r}$ are $Q$-terms, then $u \vec{r}$ is a $Q$-term.
\item For any flexible variable $y$ and distinct forbidden variables
$\vec{z}$ from $Q$, $y \vec{z}$  is a $Q$-term.
%$
\item If $r$ is a $Q \forall z$-term, then $\lambda z r$ is a
$Q$-term.
\end{itemize}
Explicitely, $r$ is a $Q$-term iff all its free variables are in $Q$,
and for every subterm $y \vec{r}$ of $r$ with $y$ free in $r$ and flexible
in $Q$, the $\vec{r}$ are distinct variables either $\lambda$-bound in $r$
(such that $y \vec{r}$ is in the scope of this $\lambda$) or else
forbidden in $Q$.

\emph{$Q$-goals}\index{Q-goal@$Q$-goal} and
\emph{$Q$-clauses}\index{Q-clause@$Q$-clause} are simultaneously
defined by
\begin{itemize}
\item If $\vec{r}$ are $Q$-terms, then $P \vec{r}$ is a $Q$-goal as well as a
$Q$-clause.
\item If $D$ is a $Q$-clause and $G$ is a $Q$-goal, then $D \to G$
is a $Q$-goal.
\item If $G$ is a $Q$-goal and $D$ is a $Q$-clause, then $G \to D$
is a $Q$-clause.
\item If $G$ is a $Q\forall x$-goal, then $\forall x G$ is a $Q$-goal.
\item If $\subst{D}{y}{Y \vec{z}}$ is a $\forall \vec{x} \exists \vec{y}, Y
\forall \vec{z}$-clause, then $\forall y D$ is a $\forall \vec{x} \exists \vec{y}
\forall \vec{z}$-clause.
\end{itemize}
Explicitely, a formula $A$ is a \emph{$Q$-goal}\index{Q-goal@$Q$-goal}
iff all its free variables are in $Q$, and for every subterm $y \vec{r}$
of $A$ with $y$ either existentially bound in $A$ (with $y \vec{r}$ in the
scope) or else free in $A$ and flexible in $Q$, the $\vec{r}$ are distinct
variables either $\lambda$- or universally bound in $A$ (such that $y
\vec{r}$ is in the scope) or else free in $A$ and forbidden in $Q$.

A \emph{$Q$-sequent}\index{Q-sequent@$Q$-sequent} has the form $\C{P}
\seqarrow G$, where $\C{P}$ is a list of $Q$-clauses and $G$ is a
$Q$-goal.

A \emph{$Q$-substitution}\index{Q-substitution@$Q$-substitution} is a
substitution of $Q$-terms.

A \emph{unification problem} $\C{U}$ consists of a $\forall
\exists \forall$-prefix $Q$ and a conjunction $C$ of equations between
$Q$-terms of the same type, i.e.\ $\bigland_{i=1}^n r_i = s_i$.  We
may assume that each such equation is of the form $\lambda \vec{x} r =
\lambda \vec{x} s$ with the same $\vec{x}$ (which may be empty) and $r, s$ of
ground type.

A \emph{solution} to such a unification problem $\C{U}$ is a
$Q$-substitution $\varphi$ such that for every $i$, $r_i \varphi = s_i
\varphi$ holds (i.e.\ $r_i \varphi$ and $s_i \varphi$ have the same
normal form).  We sometimes write $C$ as $\vec{r} = \vec{s}$, and (for
obvious reasons) call it a list of unification pairs.

We work with lists of sequents instead of single sequents; they all
are $Q$-sequents for the same prefix $Q$.  One then searches for a
$Q$-substitution $\varphi$ and proofs of the $\varphi$-substituted
sequents.
\texttt{intro-search}\index{intro-search@\texttt{intro-search}} takes
the first sequent and extends $Q$ by all universally quantified
variables $x_1 \dots$.  It then calls
\texttt{select}\index{select@\texttt{select}}, which selects (using
\texttt{or}) a fitting clause.  If one is found, a new prefix $Q'$
(raising the new flexible variables) is formed, and the $n$ ($\ge 0$)
new goals with their clauses (and also all remaining sequents) are
substituted with $\texttt{star} \circ \rho$, where \texttt{star} is
the \inquotes{rai\-sing} substitution and $\rho$ is the mgu.  For this
constellation \texttt{intro-search} is called again.  In case of
success, one obtains a $Q'$-substitution $\varphi'$ and proofs of the
$\texttt{star} \circ \rho \circ \varphi'$ -substituted new sequents.
Let $\varphi := (\rho \circ \varphi') {\restriction} Q_\ex$, and take
the first $n$ proofs of these to build a proof of the
$\varphi$-substituted (first) sequent originally considered by
\texttt{intro-search}.

Compared with Miller \cite{Miller91b}, we make use of several
simplifications, optimizations and extensions, in particular the
following.
\begin{itemize}
\item Instead of arbitrarily mixed prefixes we only use those of
the form $\forall \ex \forall$.  Nipkow in \cite{Nipkow91} already
had presented a version of Miller's pattern unification algorithm for
such prefixes, and Miller in \cite[Section~9.2]{Miller91b} notes that
in such a situation any two unifiers can be transformed into each
other by a variable renaming substitution.  Here we restrict ourselves
to $\forall \ex \forall$-prefixes throughout, i.e.\ in the proof
search algorithm as well.
\item The order of events in the pattern unification algorithm is
changed slightly, by postponing the raising step until it is really
needed.  This avoids unnecessary creation of new higher type
variables.  -- Already Miller noted in \cite[p.515]{Miller91b} that
such optimizations are possible.
\item The extensions concern the (strong) existential quantifier, which
has been left out in Miller's treatment, and also conjunction.  The
latter can be avoided in principle, but of course is a useful thing to
have.
\end{itemize}


% \subsection*{Interface}  
\texttt{(search \textsl{m} \textsl{(name1 m1)}
\dots)}\index{search@\texttt{search}} expects for \textsl{m} a default
value for multiplicity (i.e.\ how often assumptions are to be used),
for \textsl{name1} $\dots$
\begin{itemize}
\item numbers of hypotheses from the present context or 
\item names for theorems or global assumptions, 
\end{itemize}
and for \textsl{m1} \dots multiplicities (positive integers for global
assumptions or theorems).  A search is started for a proof of the goal
formula from the given hypotheses with the given multiplicities and in
addition from the other hypotheses (but not any other global
assumptions or theorems) with \textsl{m} or \texttt{mult-default}.  To
exclude a hypothesis from being tried, list it with multiplicity $0$.


\section{Computational content of classical proofs}
\mylabel{Classical}
This section is based on \cite{BergerBuchholzSchwichtenberg02}.  We
restrict to formulas in the language $\{\bot, \to, \forall \}$ in this
section, and - as in the paper - make use of a special nullary
predicate variable $X$.

A formula is \emph{relevant}\index{formula!relevant} if it
ends with (logical) falsity.  \emph{Definite}\index{formula!definite}
and \emph{goal}\index{formula!goal} formulas are defined by a
simultaneous recursion, as in \cite{BergerBuchholzSchwichtenberg02}.
\begin{alignat*}{2}
&\texttt{(atr-relevant?\ \textsl{formula})}%
\index{atr-relevant?@\texttt{atr-relevant?}} 
\\
&\texttt{(atr-definite?\ \textsl{formula})}%
\index{atr-definite?@\texttt{atr-definite?}} 
\\
&\texttt{(atr-goal?\ \textsl{formula})}%
\index{atr-goal?@\texttt{atr-goal?}} 
\end{alignat*}
To implement \cite[Lemma~3.1]{BergerBuchholzSchwichtenberg02}, we need 
to construct proofs from formulas:
\begin{alignat*}{2}
&N_D\colon ((D \to \bot) \to X) \to D^X   
&\quad&\text{for $D$ relevant}
\\
&M_D\colon D \to D^X
\\     
&K_G\colon G \to G^X                   
&\quad&\text{for $G$ irrelevant}
\\
&H_G\colon G^X \to (G \to X) \to X 
\end{alignat*}
This is done by
\begin{alignat*}{2}
&\texttt{(atr-rel-definite-proof \textsl{formula})}%
\index{atr-rel-definite-proof@\texttt{atr-rel-definite-proof}} 
\\
&\texttt{(atr-arb-definite-proof \textsl{formula})}%
\index{atr-arb-definite-proof@\texttt{atr-arb-definite-proof}} 
\\
&\texttt{(atr-irrel-goal-proof \textsl{formula})}%
\index{atr-irrel-goal-proof@\texttt{atr-irrel-goal-proof}} 
\\
&\texttt{(atr-arb-goal-proof \textsl{formula})}%
\index{atr-arb-goal-proof@\texttt{atr-arb-goal-proof}} 
\end{alignat*}
Next we need to implement
\cite[Lemma~3.2]{BergerBuchholzSchwichtenberg02}, which says that
for goal formulas $\vec{G} = G_1, \dots, G_n$ we can derive in minimal
logic augmented with a special predicate variable $X$
\[
(\vec{G} \to X) \to \vec{G}^X \to X.
\]
In our implementation this function is called
\begin{alignat*}{2}
&\texttt{(atr-goals-to-x-proof \textsl{goal1} \dots)}%
\index{atr-goals-to-x-proof@\texttt{atr-goals-to-x-proof}} 
\end{alignat*}
Finally we implement
\cite[Theorem~3.3]{BergerBuchholzSchwichtenberg02}, which says the
following.  Assume that for definite formulas $\vec{D}$ and goal
formulas $\vec{G}$ we can derive in minimal logic
\[
\vec{D} \to (\forall \vec{y}.\vec{G} \to \bot) \to \bot.
\]
Then we can also derive in intuitionistic logic augmented with the
special predicate variable $X$
\[
\vec{D} \to (\forall \vec{y}.\vec{G} \to X) \to X.
\]
In particular, substitution of the formula
\[
\ex \vec{y}.\vec{G} := \ex \vec{y}.G_1 \land \dots \land G_n
\]
for $X$ yields a derivation in intuitionistic logic of
\[
\vec{D} \to \ex \vec{y}.\vec G.
\]
This is done by
\begin{alignat*}{2}
&\texttt{(atr-min-excl-proof-to-x-proof \textsl{min-excl-proof})}%
\index{atr-min-excl-proof-to-x-proof@\texttt{atr-min-excl-proof-to-x-proof}} 
\\
&\texttt{(atr-min-excl-proof-to-intuit-ex-proof \textsl{min-excl-proof})}%
\index{atr-min-excl-proof-to-intuit-ex-proof@\texttt{atr-min-\dots-to-intuit-ex-proof}} 
\end{alignat*}

See section \ref{S:ExtrTerms} for an interpretation of the symbols of the
extracted terms in Minlog's output.

\section{Extracted terms}
\mylabel{S:ExtrTerms}
We assign to every formula $A$ an object $\tau(A)$ (a type or the
symbol $\texttt{nulltype}$).  $\tau(A)$ is intended to be the type of the
program to be extracted from a proof of $A$.  
%% To an atomic formula
%% consisting of a predicate variable with arguments we assign a new type
%% variable.
%% \begin{align*}
%% \tau( P\vec{r}) &:= \begin{cases}
%% \texttt{nulltype} &\text{if $P$ is a predicate constant}
%% \\
%% \alpha_P  &\text{if $P$ is a predicate variable}
%% \end{cases}
%% \\
%% \tau(A \to B) &:= \begin{cases}
%% \tau(B) &\text{if $\tau(A)=\texttt{nulltype}$}
%% \\
%% \texttt{nulltype} &\text{if $\tau(B)=\texttt{nulltype}$}
%% \\
%% \tau(A) \to \tau(B) &\text{otherwise}\end{cases}
%% \\
%% \tau(A \land B) &:= \begin{cases}
%% \texttt{nulltype} &\text{if $\tau(A) = \tau(B) = \texttt{nulltype}$}
%% \\
%% \tau(B) &\text{if $\tau(A)=\texttt{nulltype}$}
%% \\
%% \tau(A) &\text{if $\tau(B)=\texttt{nulltype}$}
%% \\
%% \tau(A) \times \tau(B) &\text{otherwise}\end{cases}
%% \\
%% \tau(\forall x^\rho A) &:= \begin{cases}
%% \texttt{nulltype} &\text{if $\tau(A)=\texttt{nulltype}$}
%% \\
%% \rho \to \tau(A) &\text{otherwise}\end{cases}
%% \\
%% \tau(\ex x^\rho A) &:= \begin{cases}
%% \rho &\text{if $\tau(A) = \texttt{nulltype}$}
%% \\
%% \rho \times \tau(A) &\text{otherwise}\end{cases}
%% \end{align*}
This is done by
\begin{alignat*}{2}
&\texttt{(formula-to-et-type \textsl{formula})}%
\index{formula-to-et-type@\texttt{formula-to-et-type}} 
\end{alignat*}
In \texttt{formula-to-et-type} we assign type variables to the
predicate variables.  For to be able to later refer to this
assignment, we use a global variable \texttt{PVAR-TO-TVAR-ALIST},
which memorizes the assigment done so far.  Later reference is
necessary, because such type variables will appear in extracted
programs of theorems involving predicate variables, and in a given
development there may be many auxiliary lemmata containing the same
predicate variable.  A fixed \texttt{pvar-to-tvar} refers to and
updates \texttt{PVAR-TO-TVAR-ALIST}.

When we want to execute the program, we have to replace the constant
\texttt{cL} corresponding to a lemma \texttt{L} by the extracted
program of its proof, and the constant \texttt{cGA} corresponding to a
global assumption \texttt{GA} by an assumed extracted term to be
provided by the user.  This can be achieved by adding computation
rules for \texttt{cL} and \texttt{cGA}.  We can be rather flexible
here and enable/block rewriting by using
\texttt{animate}/\texttt{deanimate} as desired.  Notice that the type
of the extracted term provided for a \texttt{cGA} must be the
extracted type of the assumed formula.  When predicate variables are
present, one must use the type variables assigned to them in
\texttt{PVAR-TO-TVAR-ALIST}.
\begin{alignat*}{2}
&\texttt{(animate \textsl{thm-or-ga-name}\ .\ \textsl{opt-eterm})}
\index{animate@\texttt{animate}}
\\
&\texttt{(deanimate \textsl{thm-or-ga-name})}
\index{deanimate@\texttt{deanimate}}
\end{alignat*}

We can define, for a given derivation $M$ of a formula $A$ with
$\tau(A) \ne \texttt{nulltype}$, its \emph{extracted
term}\index{extracted term} (or \emph{extracted
program}\index{extracted program}) $\et{M}$ of type $\tau(A)$.
%% \begin{align*}
%% \et{u^A} &:= u^{\tau(A)}
%% \\
%% \et{c^A} &:= \text{a term of type $\tau(A)$ (see below)}
%% \\
%% \et{\lambda u^A M} &:= \begin{cases}
%% \et{M} &\text{if $\tau(A)=\texttt{nulltype}$}
%% \\
%% \lambda u^{\tau(A)}\et{M} &\text{otherwise}\end{cases}
%% \\
%% \et{M^{A\to B}N} &:= \begin{cases}
%% \et{M} &\text{if $\tau(A)=\texttt{nulltype}$}
%% \\
%% \et{M}\et{N} &\text{otherwise}\end{cases}
%% \\
%% \et{\pair{M^{A}}{N^{B}}} &:= \begin{cases}
%% \et{N} &\text{if $\tau(A)=\texttt{nulltype}$}
%% \\
%% \et{M} &\text{if $\tau(B)=\texttt{nulltype}$}
%% \\
%% \pair{\et{M}}{\et{N}} &\text{otherwise}\end{cases}
%% \\
%% \et{M^{A \land B} \texttt{left}} &:= \begin{cases}
%% \et{M} &\text{if $\texttt{nulltype} \in \{\tau(A), \tau(B)\}$}
%% \\
%% \et{M} \texttt{left} &\text{otherwise}\end{cases}
%% \\
%% \et{M^{A \land B} \texttt{right}} &:= \begin{cases}
%% \et{M} &\text{if $\texttt{nulltype} \in \{\tau(A), \tau(B)\}$}
%% \\
%% \et{M} \texttt{right} &\text{otherwise}\end{cases}
%% \\
%% \et{\lambda x^\rho M} &:= \lambda x^\rho \et{M}
%% \\
%% \et{Mt} &:= \et{M}t
%% \end{align*}
We also need extracted terms for the axioms.  For induction we take
recursion, for the proof-by-cases axiom we take the cases-construct for
terms;  for the other axioms the extracted terms are rather clear.
Term extraction is implemented by
\begin{alignat*}{2}
&\texttt{(proof-to-extracted-term \textsl{proof})}%
\index{proof-to-extracted-term@\texttt{proof-to-extracted-term}} 
\end{alignat*}

The following table gives the symbols of Minlog's output and the corresponding
notation in the $\lambda$-calculus.

\begin{center}
\begin{tabular}{|l|c|c|}\hline
 \textbf{Explanation} & \textbf{Symbol} & \textbf{Minlog's Output} \\ \hline
 $\lambda$-abstraction: & $\lambda x. M$ & \texttt{([x]M)}\\ \hline
 pair: & $\langle M {\;|\;} N \rangle$ & \texttt{(M@N)} \\ \hline
 left element of a pair: & $(M \; 0)$ & \texttt{left M}\\ \hline
 right element of a pair: &$(M \; 1)$ & \texttt{right M} \\ \hline
 arrow for types: &$\typeTo$ & \texttt{=>} \\ \hline
 product for types:  &$\times$ & \texttt{@@} \\ \hline
 recursion operator: &$\C{R}$ & \texttt{$\C{R}$} \\ \hline
\end{tabular}
\end{center}


It is also possible to give an internal proof of soundness.  This can
be done by
\begin{alignat*}{2}
&\texttt{(proof-to-soundness-proof \textsl{proof})}%
\index{proof-to-soundness-proof@\texttt{proof-to-soundness-proof}} 
\end{alignat*}


\section{Reading formulas in external form}
\mylabel{Reading} A formula can be produced from an external
representation, for example a string, using the \verb}pt} function.
It has one argument, a string denoting a formula, that is converted to
the internal representation of the formula.  For the following
syntactical entities parsing functions are provided:
\begin{alignat*}{2}
&\texttt{(py \textsl{string})}\index{py@\texttt{py}}
&\quad& \hbox{for parsing types}
\\
&\texttt{(pv \textsl{string})}\index{pv@\texttt{pv}}
&\quad& \hbox{for parsing variables}
\\
&\texttt{(pt \textsl{string})}\index{pt@\texttt{pt}}
&\quad& \hbox{for parsing terms}
\\
&\texttt{(pf \textsl{string})}\index{pf@\texttt{pf}}
&\quad& \hbox{for parsing formulas}
\end{alignat*}

The conversion occurs in two steps: lexical analysis and parsing.

\subsection{Lexical analysis\index{lexical analysis}}  In this stage the
string is brocken into short sequences, called \emph{tokens}\index{token}.

A token can be one of the following:
\begin{itemize}
\item An alphabetic symbol: A sequence of letters \verb}a}--\verb}z}
and \verb}A}--\verb}Z}.  Upper and lower case letters are considered
different.
\item A number: A sequence of digits \verb}0}--\verb}9}
\item A punctuation mark: One of the characters: \verb}(} \verb})}
\verb}[} \verb}]} \verb}.} \verb},} \verb};}
\item A special symbol: A sequence of characters, that are neither letters,
digits, punctuation marks nor white space.
\end{itemize}

For example: \verb}abc}, \verb}ABC} and \verb}A} are alphabetic
symbols, \verb}123}, \verb}0123} and \verb}7} are numbers, \verb}(} is
a punctuation mark, and \verb}<=}, \verb}+}, and \verb}#:-^} are
special symbols.

Tokens are always character sequences of maximal length belonging to
one of the above categories.  Therefore \verb}fx} is a single
alphabetic symbol not two and likewise \verb}<+} is a single special
symbol.  The sequence \verb}alpha<=(-x+z)}, however, consists of the 8
tokens \verb}alpha}, \verb}<=}, \verb}(}, \verb}-}, \verb}x},
\verb}+}, \verb}z}, and \verb})}.  Note that the special symbols
\verb}<=} and \verb}-} are separated by a punctuation mark, and the
alphabetic symbols \verb}x} and \verb}z} are separated by the special
symbol \verb}+}.

If two alphabetic symbols, two special symbols, or two numbers follow
each other they need to be separated by white space (spaces, newlines,
tabs, formfeeds, etc.).  Except for a few situations mentioned below,
whitespace has no significance other than separating tokens.  It can
be inserted and removed between any two tokens without affecting the
significance of the string.

Every token has a \indexentry{token type}, and a value.  The token
type is one of the following: number, var-index, var-name, const,
pvar-name, predconst, type-symbol, pscheme-symbol, postfix-op,
prefix-op, binding-op, add-op, mul-op, rel-op, and-op, or-op, imp-op,
pair-op, if-op, postfix-jct, prefix-jct, and-jct, or-jct, tensor-jct,
imp-jct, quantor, dot, hat, underscore, comma, semicolon, arrow, lpar,
rpar, lbracket, rbracket.

The possible values for a token depend on the token type and are
explained below.

New tokens can be added using the function
\[
\texttt{(add-token \textsl{string} \textsl{token-type} \textsl{value})}.
\]
The inverse is the function
\[
\texttt{(remove-token \textsl{string})}.
\]
A list of all currently defined tokens sorted by token types can be
obtained by the function
\[
\texttt{(display-tokens)}.
\]

\subsection{Parsing}
The second stage, \indexentry{parsing}, extracts structure form the
sequence of tokens.

\emph{Types}.  Type-symbols are types; the value of a type-symbol
must be a type.  If $\sigma$ and $\tau$ are types, then
$\sigma$\verb};}$\tau$ is a type (pair type) and
$\sigma$\verb}=>}$\tau$ is a type (function type).  Parentheses can be
used to indicate proper nesting.  For example \verb}boole} is a
predefined type-symbol and hence, \verb}(boole;boole)=>boole} is again a
type.  The parentheses in this case are not strictly necessary, since
\verb};} binds stronger than \verb}=>}.  Both operators associate to
the right.

\emph{Variables}.  Var-names are variables; the value of a var-name
token must be a pair consisting of the type and the name of the
variable (the same name string again!  This is not nice and may be
later, we find a way to give the parser access to the string that is
already implicit in the token).  For example to add a new boolean
variable called ``flag'', you have to invoke the function
\texttt{(add-token "flag" 'var-name (cons 'boole "flag"))}.  This will
enable the parser to recognize ``\verb/flag3/'', ``\verb/flag^/'', or
``\verb/flag^14/'' as well.

Further, types, as defined above, can be used to construct variables.

A variable given by a name or a type can be further modified.  If it
is followed by a \verb}^}, a partial variable is constructed.  Instead
of the \verb}^} a \verb}_} can be used to specify a total variable.

Total variables are the default and therefore, the \verb}_} can be
omitted.

As another modifier, a number can immediately follow, with no
whitespace in between, the \verb}^} or the \verb}_}, specifying a
specific variable index.

In the case of indexed total variables given by a variable name or a
type symbol, again the \verb}_} can be omitted.  The number must then
follow, with no whitespace in between, directly after the variable
name or the type.

Note: This is the only place where whitespace is of any significance
in the input.  If the \verb}^}, \verb}_}, type name or variable name
is separated from the following number by whitespace, this number is
no longer considered to be an index for that variable but a numeric
term in its own right.

For example, assuming that \verb}p} is declared as a variable of type
\verb}boole}, we have:
\begin{itemize}
\item \verb}p} a total variable of type boole with name p and no index.
\item \verb}p_} a total variable of type boole with name p and no index.
\item \verb}p^} a partial variable of type boole with name p and no index.
\item \verb}p2} a total variable of type boole with name p and index 2.
\item \verb}p_2} a total variable of type boole with name p and index 2.
\item \verb}p^2} a partial variable of type boole with name p and index 2.
\item \verb}boole} a total anonymous variable of type boole with no index.
\item \verb}boole_} a total anonymous variable of type boole with no index.
\item \verb}boole^} a partial anonymous variable of type boole with no index.
\item \verb}boole_2} a total anonymous variable of type boole with index 2.
\item \verb}boole2} a total anonymous variable of type boole with index 2.
\item \verb}boole^2} a partial anonymous variable of type boole with index 2.
\item \verb}boole 2} a total anonymous variable of type boole applied to 
the numeric term 2.
\item \verb}(boole)2} a total anonymous variable of type boole applied 
to the numeric term 2.
\item \verb}(boole)_2} a total anonymous variable of type boole with index 2.
\item \verb}boole=>boole^2} a partial anonymous variable of type 
function of boole to boole with index 2. 
\end{itemize}
\emph{Terms} are built from atomic terms using application and
operators.

An atomic term is one of the following: a constant, a variable, a
number, a conditional, or any other term enclosed in parentheses.

Constants have \verb}const} as token type, and the respective term in
internal form as value.  There are also composed constants, so-called
\emph{constant schemata}\index{constant scheme}.  A constant schema
has the form of the name of the constant schema (token type
\texttt{constscheme}) followed by a list of types, the whole thing
enclosed in parentheses.  There are a few built in constant schemata:
\verb}(Rec <typelist>)}\index{Rec@\texttt{Rec}} is the recursion over
the types given in the type list; \verb}(EQat <type>)} is the equality
for the given type; \verb}(Eat <type>)} is the existence predicate for
the given type.  The constant schema \verb}EQat} can also be written
as the relational infix operator \verb}=}; the constant schemata
\verb}Eat} can also be written as the prefix operator \verb}E}.

For a number, the user defined function \verb}make-numeric-term} is
called with the number as argument.  The return value of
\verb}make-numeric-term} should be the internal term representation of
the number.

To form a conditional term, the if operator \verb}if} followed by a
list of atomic terms is enclosed in square brackets.  Depending on the
constructor of the first term, the selector, a conditional term can be
reduced to one of the remaining terms.

From these atomic terms, compound terms are built not only by
application but also using a variety of operators, that differ in
binding strength and associativity.

Postfix operators (token type \verb}postfix-op}) bind strongest, next
in binding strength are prefix operators (token type
\verb}prefix-op}), next come binding operators (token type
\verb}binding-op}).

A binding operator is followed by a list of variables and finally a
term.  There are two more variations of binding operators, that bind
much weaker and are discussed later.

Next, after the binding operators, is plain application.
Juxtaposition of two terms means applying the first term to the
second.  Sequences of applications associate to the left.  According
to the \indexentry{vector notation} convention the meaning of
application depends on the type of the first term.  Two forms of
applications are defined by default: if the type of the first term is
of \verb}arrow-form?}  then \verb}make-term-in-app-form} is used; for
the type of a free algebra we use the corresponding form of recursion.
However, there is one exception: if the first term is of type
\verb}boole} application is read as a short-hand for the
\inquotes{if\dots then \dots else} construct (which is a special form)
rather than boolean recursion.  The user may use the function
\verb}add-new-application}
\index{add-new-application@\texttt{add-new-application}} to add new
forms of applications.  This function takes two arguments, a predicate
for the type of the first argument, and a function taking the two
terms and returning another term intended to be the result of this
form of application.  Predicates are tested in the inverse order of
their definition, so more general forms of applications should be
added first.

By default these new forms of application are \emph{not} used for
output; but the user might declare that certain terms should be output
as formal application. \emph{When doing so it is the user's responisbility
to make sure that the syntax used for the output can still be parsed
correctly by the parser!}
To do so the function \texttt{(add-new-application-syntax pred toarg toop)}
can be used, where the first argument has to be a predicate (i.e., a function
mapping terms to \verb}#t} and \verb}#f}) telling whether this special
form of application can be used. If so, the arguments \texttt{toarg} and
\texttt{toop} have to be functions mapping the term to operator and
argument of this ``application'' respectively.


After that, we have binary operators written in infix notation.  In
order of decreasing binding strength these are: 
\begin{itemize}
\item multiplicative operators, leftassociative, token type \verb}mul-op}; 
\item additive operators, leftassociative, token type \verb}add-op}; 
\item relational operators, not associative, token type \verb}rel-op}; 
\item boolean and operators, leftassociative, token type \verb}and-op}; 
\item boolean or operators, leftassociative, token type \verb}or-op}; 
\item boolean implication operators, rightassociative, token type 
\verb}imp-op};
\item pairing operators, rightassociative, token type \verb}pair-op}.
\end{itemize}

On the top level, we have two more forms of binding operators, one
using the dot ``\verb}.}'', the other using square brackets
``\verb}[ ]}''.  Recall that a binding operator is followed by a list
of variables and a term.  This notation can be augmented by a period
``\verb}.}''  following after the variable list and before the term.
In this case the scope of the binding extends as far to the right as
possible.  Bindings with the lambda operator can also be specified by
including the list of variables in square brackets.  In this case,
again, the scope of the binding extends as far as possible.

Predefined operators are \texttt{E} and \texttt{=} as described above,
the binding operator \texttt{lambda}, and the pairing operator
\verb}@} with two prefix operators \texttt{left} and \texttt{right}
for projection.

The value of an operator token is a function that will obtain the
internal representation of the component terms as arguments and
returns the internal representation of the whole term.

If a term is formed by application, the function
\verb}make-gen-application} is called with two subterms and returns
the compound term.  The default here (for terms with an arrow type) is
to make a term in application form.  However other rules of
composition might be introduced easily.

\emph{Formulas} are built from atomic formulas using junctors and
quantors.

The simplest atomic formulas are made from terms using the implicit
predicate ``atom''. The semantics of this predicate is well defined
only for terms of type boole.  Further, a predicate constant (token
type \verb}predconst}) or a predicate variable (token type
\verb}pvar}) followed by a list of atomic terms is an atomic formula.
Lastly, any formula enclosed in parentheses is considered an atomic
formula.

The composition of formulas using junctors and quantors is very
similar to the composition of terms using operators and binding.  So,
first postfix junctors, token type \verb}postfix-jct}, are applied,
next prefix junctors, token type \verb}prefix-jct}, and quantors,
token type \verb}quantor}, in the usual form: quantor, list of
variables, formula.  Again, we have a notation using a period after
the list of variables, making the scope of the quantor as large as
possible.  Predefined quantors are \texttt{ex}, \texttt{excl},
\texttt{exca}, and \texttt{all}.

The remaining junctors are binary junctors written in infix form.  In
order of decreasing binding strength we have: 
\begin{itemize}
\item conjunction junctors, leftassociative, token type \verb}and-jct}; 
\item disjunction junctors, leftassociative, token type \verb}or-jct}; 
\item tensor junctors, rightassociative, token type \verb}tensor-jct}; 
\item implication junctors, rightassociative, token type \verb}imp-jct}.  
\end{itemize}
Predefined junctors are \verb}&} (and), \verb}!} (tensor), and
\verb}->} (implication).

The value of junctors and quantors is a function that will be called
with the appropriate subformulas, respectively variable lists, to
produce the compound formula in internal form.


\frenchspacing
\bibliography{minlog}
\bibliographystyle{amsplain}
% \bibliographystyle{plain}

\printindex

\end{document}


%%% Local Variables: 
%%% mode: latex-math
%%% TeX-master: t
%%% End: