項書換え系の意味論と自由連続代数

直井 徹  稲垣 康善  

誌名
電子情報通信学会論文誌 D   Vol.J71-D   No.6   pp.942-949
発行日: 1988/06/25
Online ISSN: 
DOI: 
Print ISSN: 0913-5713
論文種別: 論文
専門分野: オートマトン,言語理論,計算論
キーワード: 


本文: PDF(743.8KB)>>
論文を購入




あらまし: 
無あいまい線形項書換え系を抽象的な計算機械としてとらえ,その意味論をScott的な枠組みによって与える.そのためにまず,項の書換えを無限木(無限項)に対して拡張する.次に,Wadsworthらによってλ計算の意味論に関連して提案され,Huet-Lévyによって項書換え系のために修正された近似正規形の概念を無限木へと拡張する.この概念を利用して,必ずしも停止するとは限らない書換えの極限を定式化することにより,項書換え系の意味は,無限木の集合上のべき等な連続写像として与えられる.次に,この意味論を代数的な観点から検討する.まず,この写像から導かれる無限木の集合上の同値関係が,代入と両立するような合同関係であることを示す.この結果を用いて,この合同関係から定まる商代数はADJの提案した連続代数となっていること,および,この同値関係が妥当であるようなすべての連続代数からなるクラスに対する自由代数となっていることが導かれる.