KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Goubault-Larrecq, Jean

Abstract:

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


Volltext §
DOI: 10.5445/IR/40196
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1996
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA401969
KITopen-ID: 40196
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,34.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page