Transcribed by
Dan Connolly
from:
Forest-regular Languages and Tree-regular Languages
MURATA Makoto
May 26, 1995
%
forest(E, C): trait
includes
Integer,
List(Int),
Set(List[Int])
introduces
empty: → C
__{__} : E, C → C
__{} : E → C
__ || __ : C, C → C
tree: C → Bool
width : C → Int
Dom: C → Set[List[Int]]
auxDom: Set[List[Int]] → Set[List[Int]]
auxDom2: Int, Set[List[Int]] → Set[List[Int]]
forest: C, List[Int] → E
__ / __ : C, List[Int] → C
subtreeDom : C, List[Int] → Set[List[Int]]
asserts
% 2.1 Forest
C generated by empty, __{__}, ||
forall a: E, u,v,w: C, i, w1, u1: Int,
v1k, w2k, u1k, u2k, d, dd: List[Int],
sli: Set[List[Int]]
% "We abbreviate a<eps> as a" ... a{} will have to do.
a{} = a{empty};
% 2.2 tree
tree(a{u}) = true;
tree(empty) = false;
tree(u||v) = false;
% 2.3 forest width
width(empty) = 0;
width(a{u}) = 1;
width(u||v) = width(u) + width(v);
% 2.4 forest domain
Dom(empty) = {};
Dom(a{v}) = {{1}} ∪ auxDom(Dom(v));
auxDom({}) = {};
auxDom(insert(d, sli)) = insert((1 -| d), auxDom(sli));
Dom(v || w) = Dom(v) ∪ auxDom2(width(v), Dom(w));
auxDom2(i, {}) = {};
auxDom2(i, insert(w1 -| w2k, sli)) =
insert((w1 + i) -| w2k,
auxDom2(i, sli));
% 2.6 forest function
forest(a{v}, {1}) = a;
forest(a{v}, 1 -| v1k) = forest(v, v1k);
u1k ∈ Dom(v) ⇒ forest(v || w, u1k) = forest(v, u1k);
(\not ((u1 -| u2k) ∈ Dom(v))) ⇒
forest(v || w, u1 -| u2k) =
forest(w, (u1 + width(v)) -| u2k);
% 2.8 subtree
d ∈ Dom(u) ⇒ (Dom(u/d) = subtreeDom(u, d) ∧
forest(u/d, 1 -| v1k) = forest(u, d || v1k));
dd ∈ subtreeDom(u, d) = ∃ v1k (dd = 1 -| v1k ∧
(d || v1k) ∈ Dom(u));
implies
forall a,b,c,d: E, u: C
% Example 2.5
Dom(a{}) = {{1}};
Dom(a{b{} || c{}} || d{}) =
insert({1},
insert(1 -| {1},
insert(1 -| {2},
{{2}})));
%% Example 2.7
% (u = a{b{} || c{}} || d{}) =>
% forest(u, {1}) = a /\
% forest(u, 1 -| {1}) = b /\
% forest(u, 1 -| {2}) = c /\
% forest(u, {2}) = d;
%% Example 2.9
% (a{b{} || c{}} || d{})/{1} = a{b{} || c{}};
% (a{b{} || c{}} || d{})/{2} = d{};[Index]
HTML generated using lsl2html.