=Paper=
{{Paper
|id=Vol-2240/paper3
|storemode=property
|title=Automated Comparative Study of Some Generalized Rough Approximations
|pdfUrl=https://ceur-ws.org/Vol-2240/paper3.pdf
|volume=Vol-2240
|authors=Adam Grabowski
|dblpUrl=https://dblp.org/rec/conf/csp/Grabowski18
}}
==Automated Comparative Study of Some Generalized Rough Approximations==
https://ceur-ws.org/Vol-2240/paper3.pdf
Automated Comparative Study of Some
Generalized Rough Approximations
(Extended Abstract)
Adam Grabowski
Institute of Informatics, University of Bialystok
Konstantego Ciolkowskiego 1M, 15-245 Bialystok, Poland
adam@math.uwb.edu.pl
Abstract. The paper contains some remarks on building automated
counterpart of the research presented during one of the previous CS&P
workshops by A. Gomolińska. My main objective was the formal (and
machine-checked) proof of Theorem 4.1 from her paper “A Comparative
Study of Some Generalized Rough Approximations”, hence the title of
the present paper is by no means accidental.
Keywords: rough approximation, formalization of mathematics, Mizar
Mathematical Library
1 Motivation
During Concurrency Specification & Programming International Workshop in
2001 Anna Gomolińska presented a draft of her paper on the generalization of
rough approximation operators. Essentially, the idea behind the research was to
collect some standard properties of rough approximations and to cut off some
ordinary properties of binary relations to get – a little bit in the spirit of reverse
mathematics – a catalogue of equivalences between relations’ properties and cor-
responding formulas for rough sets. The final – revised and updated – version
of the research appeared eventually in Fundamenta Informaticae under the ti-
tle A Comparative Study of Some Generalized Rough Approximations [2] and
contained also a brief review of various rough approximations, not necessarily
classical ones.
During that time, I was also interested in computer-supported formalization
of rough sets and I claimed that the paper could be a quite interesting testbed
for my studies on the use of proof-assistants to support mathematicians in their
work. Just to be a little more explicit, the system which was considered by me
was Mizar, equipped with first order logic language and Tarski-Grothendieck set
theory as a underlying set theory.
After a deeper study at that time, I decided to abandon the formalization
work as it looked too much different from the one I followed as described in
[5]. In the aproach chosen by Gomolińska, rough inclusion function κ and two
uncertainty mappings – I and τ were quite fundamental at the very first first
sight.
2 Approximations according to Gomolińska
Gomolińska started with – quite general – uncertainty map I from non-empty
universe U into its powerset. Potentially, no additional assumptions at the be-
ginning are made, with the exception of a kind of reflexivity – that any object
u from the universe is an element of I(u).
Theorem 4.1 is the core of the first part. We aimed at the full formalization
of this item, so we quote it here using original notation from [2].
Theorem 4.1 For any sets x, y ⊆ U , objects u, w ∈ U , and i = 0, 1, it
holds that:
a) f0d ≤ id ≤ f0 .
b) f1d ≤ id ≤ f1 .
c) f0 (x) is definable.
d) ∀u ∈ f1 (x).κ(I(u), x) > 0.
e) ∀u ∈ f1d (x).κ(I(u), x) = 1.
f) If τ (u) = τ (w), then u ∈ f0 (x) iff w ∈ f0 (x); and similarly for f0d .
g) If I(u) = I(w), then u ∈ f1 (x) iff w ∈ f1 (x); and similarly for f1d .
h) fi (∅) = ∅ and fi (U ) = U ; and similarly for fid .
i) fi and fid are monotone.
j) fi (x ∪ y) = fi (x) ∪ fi (y).
k) fid (x ∪ y) ⊇ fid (x) ∪ fid (y).
l) fi (x ∩ y) ⊆ fi (x) ∩ fi (y).
m) fid (x ∩ y) = fid (x) ∩ fid (y).
The approach is significantly different than those of W. Zhu [11] (but Zhu’s
paper was published later), where the starting point is – at least in my opinion
– more natural. Moreover, in the second part of the paper under discussion the
catalogue of various rough approximation operators is given (which is outside
Zhu’s research area).
3 Mizar State of the Art
In our formal approach to rough approximations, our choice was to have indis-
cernibility relation ρ defined as a binary relation on a non-empty universe U .
Essentially then, this corresponds to an abstract relational structure
R = hU, ρi
with all properties credited to the internal relation of R.
At the very beginning, we do not assume any of standard properties of ap-
proximations (or tolerances) added to the type of ρ, although we introduce two
basic Mizar types, called Approximation_Space and Tolerance_Space, to have
them available in the Mizar Mathematical Library. More thorough discussion on
this development is given in [4].
Faithfully following Gomolińska, we should be aware of the fact that we have
A = hU, I, κi
as a formal approximation space. I had some doubts if I should mention κ at all
– rough inclusion function as in the classical approach the membership function
was considered. Also ρ as indiscernibility relation was rather preferred over the
uncertainty mapping. My convincement was stronger after the formalization of
Zhu’s paper on correspondence between properties of binary relations and of
rough sets.
In the literature [11] the authors skip over the theory of less known properties
of binary relations (or at least treat them as widely known), and I was also in a
dead point as the – contrary to the notion of serial or mediate which could be
claimed as mathematical folklore – positive or negative alliance relations were
really unknown for me.
Even if in considered paper standard lower approximation operator is defined
as (10)
LOW (x) = {u ∈ U : κ(I(u), x) = 1},
happily its immediate consequence is available as (12):
LOW (x) = {u ∈ U : I(u) ⊆ x}.
Then we could be sure the function κ will not be needed at the moment.
4 Generalizing Functions
Gomolińska claimed the following name space for approximations operators (18):
f0 (x) = {u ∈ U : τ (u) ∩ x 6= ∅}
f1 (x) = {u ∈ U : I(u) ∩ x 6= ∅}
with corresponding f0d and f1d .
Then we can think on the following definition for τ
definition
let R be non empty RelStr;
let tau be Function of the carrier of R, bool the carrier of R;
func f_0 R -> map of R means
for x being Subset of R holds
it.x = { u where u is Element of R : tau.u meets x };
end;
and similar, for uncertainty mapping I. Hence, it is quite straightforward to see
that the common variable in both definitions is just arbitrary function (with
proper domain and codomain), let us call it f , and then it is quite natural to
use instead of the above formulation something like
definition
let R be non empty RelStr;
let f be Function of the carrier of R, bool the carrier of R;
func ff_0 f -> map of R means
for x being Subset of R holds
it.x = { u where u is Element of R : f.u meets x };
end;
and then to use
definition
let R be non empty RelStr;
func f_0 R -> map of R equals
ff_0 tau R;
func f_1 R -> map of R equals
ff_0 UncertaintyMap R;
end;
For a reader not very much acquainted with the Mizar system it is not very
cryptic, but the use of a keyword equals turns automatic treatment of equalities
on and then more reasonings can be justified automatically.
Furthermore, we have just a single – more general – theorem expressing (f)
and (g) at the same time, instead of two:
theorem :: ROUGHS_5:31 :: 4.1 f) Flip
for u,w being Element of R,
x being Subset of R st
f.u = f.w holds
u in (Flip ff_0 f).x iff w in (Flip ff_0 f).x;
It can be noted at the first sight, that there is nothing on approximation
operators there – we can think on quite general property of mappings as R is
only non-empty relational structure.
The Mizar functor Flip f, which is the formal counterpart of f d is defined
accordingly as
definition let X be set;
let f be Function of bool X, bool X;
func Flip f -> Function of bool X, bool X means
for x being Subset of X holds
it.x = (f.x‘)‘;
end;
Obviously, no approximations are needed here, either.
5 Attributes
In our Mizar approach, U P P and LOW operators from [2] are classical upper
and lower approximation operators, respectively. Theorem 3.1 from [2] lists them
all, but it could be mentioned in this point, that all these – more or less standard –
properties were already formulated and proved formally in Mizar script available
in MML under identifier ROUGHS_1 as a direct reflection of Pawlak’s paper [7].
In our study of fuzzy implications, we developed some techniques (Mizar
schemes) which could decrease the number of technical steps in defining func-
tions.
It should be pointed out that if we start with the uncertainty mapping rather
than with indiscernibility relation, the core property is
∀u∈U u ∈ f (u),
which is essentially the formula (1) in [2].
To have faithful formal representation is the above, we introduced the new
Mizar attribute
definition :: property (1) p. 105
let R be non empty set;
let I be Function of R, bool R;
attr I is map-reflexive means
:: ROUGHS_5:def 1
for u being Element of R holds u in I.u;
end;
As we already mentioned before, our core idea was to start with an approxi-
mation space hU, ρi, where U is non-empty universe and ρ is an indiscernibility
relation defined on U . All rough operators, membership and uncertainty func-
tions, and also rough inclusions, could be defined based within this framework.
The proper choice of the formal background is especially important, because
in the Mizar Mathematical Library, all statements should be proven based on
classical logic and/or already proven lemmas.
In this paper, as a rule we do not quote correctness conditions (as they are
needed also for definitions), although definitions should also obey the rule of the
necessary justification. Even if sometimes of quite technical character, the proof
is needed and the example of that is given below. We formulate a bunch of handy
Mizar schemes which make this activity a little bit less painful for the user.
definition
let R be non empty set;
func singleton R -> Function of R, bool R means
:: ROUGHS_5:def 2
for x being Element of R holds it.x = {x};
existence
proof
deffunc U(object) = {$1};
A1: now
let x be Element of R;
{x} c= R;
hence U(x) in bool R;
end;
thus ex f being Function of R, bool R st
for x being Element of R holds f.x = U(x)
from FUNCT_2:sch 8(A1);
end;
uniqueness; ::: here the proof is not quoted
end;
Why this definition was really needed? Essentially, to use the Mizar type
(and adjectives are important constructors for types) one should prove its non-
emptiness, i.e., to construct at least one example of an object possessing this
property, to show the usefulness of the attribute.
registration
let R be non empty set;
cluster singleton R -> map-reflexive;
end;
Another handy use of adjectives is given below:
registration
let R, f;
cluster ff_0 f -> c=-monotone;
end;
This allows to obtain automatically the proof of Theorem 4.1(i) as follows:
registration
let R be non empty RelStr; :: i)
cluster f_0 R -> c=-monotone;
cluster f_1 R -> c=-monotone;
end;
6 Conclusions and Further Work
Obviously, building proper formal framework for further work is crucial. Having
said that, we can build the rest of functions defined in [2]: f2 , . . . , f9 , having
ten mappings altogether. This allows for the possibility of automated reasoning
on these operators, which could be made in the nearest future, as well as the
reasoning on the – temporarily abandoned – rough inclusion function κ.
Even is this extended abstract is only a draft of the formal work done, the
complete formalization (just accepted for inclusion into the Mizar Mathematical
Library) is available at
http://mizar.uwb.edu.pl/library/roughsets/
Using 1386 lines of Mizar code (44 kilobytes) and formulating 7 definitions
and proving 53 theorems we completed the first part of formalization work of
Gomolińska’s paper [2]. The roughs_5.abs file contains the abstract for the
development while roughs_5.miz is the complete source file.
References
1. Bryniarski E.: Formal conception of rough sets, Fundamenta Informaticae, 27(2/3),
109–136 (1996)
2. Gomolińska A.: A comparative study of some generalized rough approximations,
Fundamenta Informaticae, 51, 103–119 (2002)
3. Grabowski A.: Mechanizing complemented lattices within Mizar system. Journal
of Automated Reasoning, 55:211–221 (2015)
4. Grabowski A.: Efficient rough set theory merging, Fundamenta Informaticae,
135(4), 371–385 (2014)
5. Grabowski A.: Automated discovery of properties of rough sets, Fundamenta In-
formaticae, 128(1–2), 65–79 (2013)
6. Järvinen J.: Lattice theory for rough sets, Transactions on Rough Sets VI, LNCS
(LNAI) 4374, 400–498 (2007)
7. Pawlak, Z.: Rough Sets: Theoretical Aspects of Reasoning about Data, Kluwer,
Dordrecht (1991). doi: 10.1007/978-94-011-3534-4
8. Rasiowa H. and Sikorski R.: The Mathematics of Metamathematics. Polish Scien-
tific Publishers (1970)
9. Skowron A., Stepaniuk J.: Tolerance approximation spaces, Fundamenta Informat-
icae, 27(2–3), pp. 245–253 (1996). doi: 10.3233/FI-1996-272311
10. Wiedijk F.: Formal proof – getting started, Notices of the American Mathematical
Society, 55(11), 1408–1414 (2008)
11. Zhu W.: Generalized rough sets based on relations, Information Sciences, 177(22),
pp. 4997–5011 (2007). doi: 10.1016/j.ins.2007.05.037