Barral, Freiric (2008): Decidability for Non-Standard Conversions in Typed Lambda-Calculi. Dissertation, LMU München: Faculty of Mathematics, Computer Science and Statistics |

Preview |
PDF
BarralPhd.pdf 882kB |

**DOI**: 10.5282/edoc.9761

### 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 |

MD5 Checksum of the PDF-file: | 6c6a75927c636520ecde53b4d7e81491 |

Signature of the printed copy: | 0001/UMC 17635 |

ID Code: | 9761 |

Deposited On: | 09. Mar 2009 09:16 |

Last Modified: | 24. Oct 2020 06:27 |