Essentially Algebraic Structure for Kleene Algebra with Tests and Its Application to Semantics of While Programs

概要

論文の詳細を見る
Kozen and Smith showed existence of Kleene algebra with tests freely generated by a pair (β,Σ) of finite sets. Their key idea is the construction of Kleene algebra P_<β,Σ> with tests. We show existence of free algebra without assuming the finiteness of β and Σ. Moreover, we give a construction of Kleene algebra Q_<β,Σ> with tests for any sets β and Σ, and show that whenever P_<β,Σ> is defined (that is, whenever β is finite), Q_<β,Σ> is isomorphic to P_<β,Σ>. We use Q_<β,Σ> in an interpretation of while programs and we argue that it is really an interpretation by sets of runs.
一般社団法人情報処理学会の論文
2003-03-15