Authors: | Ghilezan, Silvia Kunčak, Viktor |

Title: | Confluence of untyped lambda calculus via simple types |

Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Volume: | 2202 |

First page: | 38 |

Last page: | 49 |

Conference: | 7th Italian Conference on Theoretical Computer Science, ICTCS 2001; Torino; Italy; 4 October 2001 through 6 October 2001 |

Issue Date: | 1-Jan-2001 |

Rank: | M21 |

ISBN: | 978-3-540-45446-5 |

ISSN: | 0302-9743 |

DOI: | 10.1007/3-540-45446-2_3 |

Abstract: | We present a new proof of confluence of the untyped lambda calculus by reducing the confluence of β-reduction in the untyped lambda calculus to the confluence of β-reduction in the simply typed lambda calculus. This is achieved by embedding typed lambda terms into simply typed lambda terms. Using this embedding, an auxiliary reduction, and β-reduction on simply typed lambda terms we define a new reduction on all lambda terms. The transitive closure of the reduction defined is β-reduction on all lambda terms. This embedding allows us to use the confluence of β-reduction on simply typed lambda terms and thus prove the confluence of the reduction defined. As a consequence we obtain the confluence of β-reduction in the untyped lambda calculus. |

Publisher: | Springer Link |

Show full item record

#### SCOPUS^{TM}

Citations

1
checked on Sep 17, 2022

#### Page view(s)

24
checked on Oct 1, 2022

#### Google Scholar^{TM}

Check
#### Altmetric

#### Altmetric

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.