高階書換え系の停止性のための代数モデル1 特集●新しいソフトウェアの実現 高階書換え系の停止性のための代数モデル 浜名 誠 Klop によって提案された高階書換えの体系コンビナトリー簡約系 (Combinatory Reduction Systems, CRSs) が Fiore，Plotkin，Turi らによる構文の代数モデル Σ モノイドによって健全かつ完全にモデル化できることを示す． このモデルを整礎な推移的関係を持つものに制限すると，停止性を持つ CRS の完全な特徴付けができる．このこと を用いて，与えられた CRS の停止性を代数的な解釈によって示すという便利な手法を与える． We show that the structures of binding algebras and Σ-monoids by Fiore, Plotkin and Turi are sound and complete models
https://www.cs.gunma-u.ac.jp/~hamana/
