On computational interpretations of the modal logic S4. IIIa. Termination, confluence, conservativity of lambda-evQ

A language of constructions for minimal logic is the
$\lambda$-calculus, where cut-elimination is encoded as
$\beta$-reduction. We examine corresponding languages for the
minimal version of the modal logic S4, with notions of reduction
that encodes cut-elimination for the corresponding sequent system.
It turns out that a natural interpretation of the latter
constructions is a $\lambda$-calculus extended by an idealized
version of Lisp's \verb/eval/ and \verb/quote/ constructs.

In this Part IIIa, we examine the termination and confluence
properties of the ${\lambda\mbox{\tt ev\/}Q}$ and negative:
the typed calculi do not terminate, the subsystems $\Sigma$ and
$\Sigma_H$ that propagate substitutions, quotations andevaluations
downwards do not terminate either in the untyped case, and the
untyped ${\lambda\mbox{\tt ev\/}Q}_H$-calculus is not confluent.
However, the typed versions of $\Sigma$ and $\Sigma_H$ do terminate,
so the typed ${\lambda\mbox{\tt ev\/}Q}$-calculus is confluent.
It follows that the typed ${\lambda\mbox{\tt ev\/}Q}$-calculus is a
conservative extension of the typed ${\lambda_{\rm S4}}$-calculus.

Part IIIb will cover the confluence of the typed
... mehr${\lambda\mbox{\tt ev\/}Q}_H$-calculus,
which is not dealt with here.