Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system

Mitsuhiro Okada

研究成果: Conference contribution

35 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトルProceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989
編集者G. H. Gonnet
出版社Association for Computing Machinery
ページ357-363
ページ数7
ISBN(電子版)0897913256
DOI
出版ステータスPublished - 1989 7月 17
イベント1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989 - Portland, United States
継続期間: 1989 7月 171989 7月 19

出版物シリーズ

名前Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC
Part F130182

Other

Other1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989
国/地域United States
CityPortland
Period89/7/1789/7/19

ASJC Scopus subject areas

  • 数学 (全般)

フィンガープリント

「Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル