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 \text{tt ev/}Q$ and negative:
the typed calculi do not terminate, the subsystems $\mathrm{\Sigma }$ and
${\mathrm{\Sigma }}_H$ that propagate substitutions, quotations andevaluations
downwards do not terminate either in the untyped case, and the
untyped ${\lambda \text{tt ev/}Q}_H$-calculus is not confluent.
However, the typed versions of $\mathrm{\Sigma }$ and ${\mathrm{\Sigma }}_H$ do terminate,
so the typed $\lambda \text{tt ev/}Q$-calculus is confluent.
It follows that the typed $\lambda \text{tt ev/}Q$-calculus is a
conservative extension of the typed ${\lambda }_{\mathrm{S}4}$-calculus.

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