### Abstract

We give a proof of strong normalizability of the typed λ-calculas extended by an arbitrary convergent term rewriting system, which provides the affirmative answer to the open problem proposed in Breazu-Tannen [1]. Klop [6] showed that a combined system of the untyped λ-calculus and convergent term rewriting system is not Church-Rosser in general, though both are Church-Rosser. It is well-known that the typed λ-calculus is convergent (Church-Rosser and terminating). Breazu-Tannen [1] showed that a combined system of the typed λ-calculus and an arbitrary Church-Rosser term rewriting system is again Church-Rosser. Our strong normalization result in this paper shows that the combined system of the typed λ-calculus and an arbitrary convergent term rewriting system is again convergent. Our strong normalizability proof is easily extended to the case of the second order (polymorphically) typed lambda calculus and the case in which μ-reduction rule is added.

Original language | English |
---|---|

Title of host publication | Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989 |

Editors | G. H. Gonnet |

Publisher | Association for Computing Machinery |

Pages | 357-363 |

Number of pages | 7 |

ISBN (Electronic) | 0897913256 |

DOIs | |

Publication status | Published - 1989 Jul 17 |

Event | 1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989 - Portland, United States Duration: 1989 Jul 17 → 1989 Jul 19 |

### Publication series

Name | Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC |
---|---|

Volume | Part F130182 |

### Other

Other | 1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989 |
---|---|

Country | United States |

City | Portland |

Period | 89/7/17 → 89/7/19 |

### ASJC Scopus subject areas

- Mathematics(all)

## Fingerprint Dive into the research topics of 'Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system'. Together they form a unique fingerprint.

## Cite this

*Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989*(pp. 357-363). (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC; Vol. Part F130182). Association for Computing Machinery. https://doi.org/10.1145/74540.74582