KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
URN: urn:nbn:de:swb:90-AAA402965

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

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 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 c ... mehr


Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 1996
Sprache Englisch
Identifikator 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