Confluence Proofs of Lambda-Mu-Calculi by Z Theorem
| Autor: | Yuki Honda, Koji Nakazawa, Ken-etsu Fujita |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Discrete mathematics
Reduction (recursion theory) Logic 010102 general mathematics 06 humanities and the arts 0603 philosophy ethics and religion Mathematical proof Lambda 01 natural sciences TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES History and Philosophy of Science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Confluence 060302 philosophy Computer Science::Programming Languages 0101 mathematics Mathematics |
| Zdroj: | Studia Logica. 109:917-936 |
| ISSN: | 1572-8730 0039-3215 |
| Popis: | This paper applies Dehornoy et al.’s Z theorem and its variant, called the compositional Z theorem, to prove confluence of Parigot’s $$\lambda \mu $$ -calculi extended by the simplification rules. First, it is proved that Baba et al.’s modified complete developments for the call-by-name and the call-by-value variants of the $$\lambda \mu $$ -calculus with the renaming rule, which is one of the simplification rules, satisfy the Z property. It gives new confluence proofs for them by the Z theorem. Secondly, it is shown that the compositional Z theorem can be applied to prove confluence of the call-by-name and the call-by-value $$\lambda \mu $$ -calculi with both simplification rules, the renaming and the $$\mu \eta $$ -rules, whereas it is hard to apply the ordinary parallel reduction technique or the original Z theorem by one-pass definition of mappings for these variants. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink