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: Faculty of Mathematics, Computer Science and Statistics

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.

• Item Type: Theses (Dissertation, LMU Munich)
• Keywords: typed lambda calculus, conversion, reduction, decidability, normalization by evaluation
• Subjects: 500 Natural sciences and mathematics > 510 Mathematics; 500 Natural sciences and mathematics
• Faculties: Faculty of Mathematics, Computer Science and Statistics
• Language: English
• Date of oral examination: 6. June 2008
• 1. Referee: Hofmann, Martin
• Signature of the printed copy: 0001/UMC 17635