On computational interpretations of the modal logic S4. II. The lambda-evQ-calculus

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 II, we repair the non-computational defect of the
${\lambda_{\rm S4}}$-calculus of Part I by deriving an entirely
different interpretation. Quotation closures are not provided
{\em ex abrupto},but are built from more primitive combinators.
There is almost no freedom of choice here, and we are forced to use
variants of the $\lambda\sigma$-calculus, i.e.\ descriptions of
interpreters as formal languages. We end up defining an infinite
tower of interpreters, which provides an interesting analogy with
Lisp's reflexive tower. This is another argument backing the thesis
that the meaning of modal constructions in S4 corresponds to
\verb/eval/ and \verb/quote/.
... mehr