% \$Id: forest.html,v 1.1 2003/10/01 07:22:16 connolly Exp \$
%

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.
```