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.