KIT | KIT-Bibliothek | Impressum | Datenschutz

On computational interpretations of the modal logic S4. I. Cut elimination

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 first part, we analyze how cut-elimination works in the
standard sequent system for minimal S4, and where problems arise.
Bierman and De Paiva's proposal is a natural language of constructions
for this logic, but their calculus lacks a few rules that are
essential to eliminate all cuts. The ${\lambda_{\rm S4}}$-calculus,
namelyBierman and De Paiva's proposal extended with all needed rules,
is confluent. There is a polynomial-time algorithm to compute
principal typings of given terms, or answer that the given terms are
not typable. The typed ${\lambda_{\rm S4}}$-calculus terminates, and
normal forms are exactly constructions for cut-free proofs. Finally,
... mehr

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