Funcons-beta : Trees.cbs | PRETTY | PDF
Trees
[
Datatype trees
Funcon tree
Funcon tree-root-value
Funcon tree-branch-sequence
Funcon single-branching-sequence
Funcon forest-root-value-sequence
Funcon forest-branch-sequence
Funcon forest-value-sequence
]
Meta-variables
T <: values
Datatype
trees(T) ::= tree( _:T, _:(trees(T))*)
trees(T)
consists of finitely-branching trees with elements of type T
.
When V:T
, tree(V)
is a leaf, and tree(V,B_1,...,B_n)
is a tree with
branches B_1
, …, B_n
.
Funcon
tree-root-value(_:trees(T)) : =>(T)?
Rule
tree-root-value tree(V:T, _*:(trees(T))*) ~> V
Funcon
tree-branch-sequence(_:trees(T)) : =>(trees(T))*
Rule
tree-branch-sequence tree(_:T, B*:(trees(T))*) ~> B*
Funcon
single-branching-sequence(_:trees(T)) : =>T+
single-branching-sequence B
extracts the values in B
starting from
the root, provided that B
is at most single-branching; otherwise it fails.
Rule
single-branching-sequence tree(V:T) ~> V
Rule
single-branching-sequence tree(V:T, B:trees(T))
~> left-to-right( V, single-branching-sequence B)
Rule
single-branching-sequence tree(_:T, _:trees(T), _+:(trees(T))+) ~> fail
A sequence of trees corresponds to a forest, and the selector funcons
on trees B
extend to forests B*
:
Funcon
forest-root-value-sequence(_:(trees(T))*) : =>T*
Rule
forest-root-value-sequence(B:trees(T), B*:(trees(T))*)
~>(tree-root-value B , forest-root-value-sequence B*)
Rule
forest-root-value-sequence( ) ~>( )
Funcon
forest-branch-sequence(_:(trees(T))*) : =>T*
Rule
forest-branch-sequence(B:trees(T), B*:(trees(T))*)
~>(tree-branch-sequence B , forest-branch-sequence B*)
Rule
forest-branch-sequence( ) ~>( )
Funcon
forest-value-sequence(_:(trees(T))*) : =>T*
forest-value-sequence B*
provides the values from a left-to-right pre-order
depth-first traversal.
Rule
forest-value-sequence(tree(V:T, B1*:(trees(T))*), B2*:(trees(T))*)
~>(V , forest-value-sequence B1*, forest-value-sequence B2*)
Rule
forest-value-sequence( ) ~>( )
Other linearizations of trees can be added: breadth-first, right-to-left, C3, etc.