KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-AAA400962

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. ... 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: 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