Skip to main content

1995 | OriginalPaper | Buchkapitel

Strong normalization for subsystems of λ2 βηπ✻

verfasst von : Roberto Di Cosmo

Erschienen in: Isomorphisms of Types

Verlag: Birkhäuser Boston

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Our proof of confluence in Theorem 2.4.5 relies upon the strong normalization of $$\beta \underrightarrow {{\eta ^2}\pi * }$$ over the set of gentop normal forms, while we need the strong normalization of $$\beta \underrightarrow {^2{\eta ^2}\pi * }$$ less η top and SP top over the full set of terms in order to provide an effective weakly normalizing strategy for $$\beta \underrightarrow {^2{\eta ^2}\pi * }$$ in Theorem 2.5.2.

Metadaten
Titel
Strong normalization for subsystems of λ2 βηπ✻
verfasst von
Roberto Di Cosmo
Copyright-Jahr
1995
Verlag
Birkhäuser Boston
DOI
https://doi.org/10.1007/978-1-4612-2572-0_3