saturate.anubis
5.44 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
*Project* The Anubis Project
*Title* A saturation process.
*Copyright* Copyright (c) Alain Prouté 2004.
*Author* Alain Prouté
*Overview*
This file contains a tool for performing some general saturation process on finite sets
(actually lists). This process is often useful when problems concerning graphs must be
handled. It is used several times in 'filtering/make_parser.anubis' for constructing
automatons.
Consider an arbitrary type $T (which may be infinite). We are concerned with explicit
finite subsets of $T. Such subsets will be represented by lists of elements of $T. In
such a list, the order of elements is meaningless.
Starting with a finite subset of $T (of type 'List($T)'), and a 'derivation' process of
type '$T -> List($T)', we want to compute the smallest subset of $T, containing our
initial subset, and closed by derivation.
The process is roughly to add to our subset all elements derivable from the elements of
our subset, and to repeat this until it does not yield new elements. Such a process is
called a 'saturation' process. Of course, there is no warranty in general that this
saturation terminates, and this point is left under the responsability of the
user. Nevertheless, it terminates if $T is finite, but this may still take a very long
time.
However, it may also be useful to have information attached to elements of $T. This
information is actually accounted for in the type $T itself, so that comparing two
elements of $T regardless of the attached information is performed by a test which may
not be equality. In some sens our actual elements are not in $T but in some quotient
of $T. When two elements compare, we will say that they are 'equivalent' (instead of
saying that they are 'equal'). Now, when a new element has been derived, and is
recognized to be equivalent to an already seen element, the information of the new
element and of the previous one must in general be 'gathered' (in some sens that you
define yourself).
To that end, we need only one function which is both able to recognized equivalent
elements and to gather informations. This function (named 'gather' below) is of type:
($T,$T) -> Maybe($T)
It returns 'failure' when its two operands are not equivalent, and if they are
equivalent, it returns 'success(v)', where 'v' is the same (equivalent) element as the
two operands, but with their informations gathered.
public define List($T)
saturate
(
List($T) initial_set,
$T -> List($T) derive,
($T,$T) -> Maybe($T) gather
).
Examples of use of 'saturate' may be found in 'tools/saturate_example.anubis'. More
sophisticated examples may be found in 'filtering/make_parser.anubis'.
--- That's all for the public part ! --------------------------------------------------
'Move' an element 'x' into a list 'l'. This means that if x gathers with an element of
'l', then the list is returned into which the element has been replaced by the
gathering. Otherwise, 'failure' is returned.
define Maybe(List($T))
move
(
List($T) l,
$T x,
($T,$T) -> Maybe($T) gather
) =
if l is
{
[ ] then failure,
[h . t] then if gather(h,x) is
{
failure then if move(t,x,gather) is
{
failure then failure,
success(u) then success([h . u])
},
success(y) then success([y . t])
}
}.
Given two lists 'where' and 'what', move all elements of 'what' who gather with
elements of 'where' (enriching them). Returns the new pair '(where,what)'.
define (List($T),List($T))
move
(
List($T) where,
List($T) what,
($T,$T) -> Maybe($T) gather
) =
if what is
{
[ ] then (where,[]),
[h . t] then if move(where,h,gather) is
{
failure then if move(where,t,gather) is (new_where,new_what) then
(new_where,[h . new_what]),
success(new_where) then move(new_where,t,gather)
}
}.
Saturating.
define List($T)
saturate
(
List($T) to_be_derived,
List($T) already_derived,
$T -> List($T) derive,
($T,$T) -> Maybe($T) gather
) =
if to_be_derived is
{
[ ] then already_derived,
[tbd1 . tbds] then
with new_elements = derive(tbd1),
if move([tbd1 . already_derived],new_elements,gather) is (already_derived1,new_elements1) then
if move(tbds,new_elements1,gather) is (to_be_derived1,new_elements2) then
saturate(append(to_be_derived1,new_elements2),
already_derived1,
derive,
gather)
}.
The interface.
public define List($T)
saturate
(
List($T) initial_set,
$T -> List($T) derive,
($T,$T) -> Maybe($T) gather
) =
saturate(initial_set,[],derive,gather).