A Coinductive Confluence Proof for Infinitary Lambda-Calculus.
Author: Łukasz Czajka
Paper Information
| Title: | A Coinductive Confluence Proof for Infinitary Lambda-Calculus. |
| Authors: | Łukasz Czajka |
| Proceedings: | RTA-TLCA 2014 LNCS Proceedings |
| Editor: | Gilles Dowek |
| Keywords: | confluence, infinitary lambda-calculus, coinduction, infinitary rewriting |
| Abstract: | ABSTRACT. We give a coinductive proof of confluence, up to equivalence of root-active subterms, of infinitary lambda-calculus. We also show confluence of Böhm reduction (with respect to root-active terms) in infinitary lambda-calculus. In contrast to previous proofs, our proof makes heavy use of coinduction and does not employ the notion of descendants. |
| Pages: | 15 |
| Talk: | Jul 14 16:30 |
| Paper: |  |