KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Goubault-Larrecq, Jean


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

Volltext §
DOI: 10.5445/IR/40296
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-AAA402965
KITopen-ID: 40296
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,33.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page