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