Decidability for Non-Standard Conversions in Typed Lambda-Calculi

Barral, Freiric (2008): Decidability for Non-Standard Conversions in Typed Lambda-Calculi. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

This thesis studies the decidability of conversions in typed lambda-calculi, along with the algorithms allowing for this decidability. Our study takes in consideration conversions going beyond the traditional beta, eta, or permutative conversions (also called commutative conversions). To decide these conversions, two classes of algorithms compete, the algorithms based on rewriting, here the goal is to decompose and orient the conversion so as to obtain a convergent system, these algorithms then boil down to rewrite the terms until they reach an irreducible forms; and the "reduction free" algorithms where the conversion is decided recursively by a detour via a meta-language. Throughout this thesis, we strive to explain the latter thanks to the former.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: typed lambda calculus, conversion, reduction, decidability, normalization by evaluation
• Themengebiete: 500 Naturwissenschaften und Mathematik > 510 Mathematik ; 500 Naturwissenschaften und Mathematik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 6. Juni 2008
• 1. Bericht­erstatter:in: Hofmann, Martin