Information Technology Reference
In-Depth Information
R
Lemma 1 (Permutations of a regular expression).
Given that Perms
(
)
returns all
R
permutations of the sub-expressions of a regular expression
such that any sub-
R
1
and
R
2
can be reordered using
R
1
R
2
≡R
2
R
1
and
R
1
|R
2
≡R
2
|R
1
,it
expressions
holds that
∃
p
∈
Perms
(
s
)
.
match(
p
,R
)
↔∃
p
∈
Perms
(
s
)
.∃
r
∈
Perms
(
R
)
.
match(
p
,
r
)
Lemma 2 (Regex decomposition).
Decomposed strings match sub-expressions, that
is,
∈ Σ
∗
.
∀
s
match(
s
,R
1
R
2
)
→∃
p
1
p
2
=
s
.
match(
p
1
,R
1
)
∧
match(
p
2
,R
2
)
, and
∈ Σ
∗
.
∀
s
match(
s
,R
1
|R
2
)
→
match(
s
,R
1
)
∨
match(
s
,R
2
)
Proof (Evaluation
Match).
Every basic constraint, constraint vector and DCE can
be reconstructed into a regular expression, as follows:
→
a
n
(
a
m
1
a
m
2
a
m
k
)
∗
Rec(
{
m
1
,
m
2
,...,
m
k
}
n
·
a
)
=
...
Rec(
{C
1
,C
2
,...,C
k
}
)
=
Rec(
C
1
) Rec(
C
2
)
...
Rec(
C
k
)
Rec(
C
1
∨
C
2
∨...∨
C
k
)
=
Rec(
C
1
)
|
Rec(
C
2
)
| ...|
Rec(
C
k
)
If
˙
#
s
Σ
, then one can rebuild a string
a
#
a
b
#
b
z
#
i
,for
C
is a DCE which holds for
↓
...
a
with a frequency
equal to its value in the aggregated input. Given the definition of Rec(), it follows
that
,
b
...
z
∈ Σ
, that will contain a symbol for each element in
Σ
,
Rec(
˙
Perms
(
a
#
a
b
#
b
z
#
i
)
∃
p
∈
...
.
match(
p
C
)). By using Lemma 1, the fact that
Perms
(
s
), and by substituting
˙
Perms
(
a
#
a
b
#
b
z
#
i
)
...
=
C
with
C
Σ
(
R
), the statement to be
proven can be reformulated as:
∃
p
∈
Perms
(
s
)
.
match(
p
,
Rec(
C
Σ
(
R
)))
→∃
p
∈
Perms
(
s
)
.∃
r
∈
Perms
(
R
)
.
match(
p
,
r
)
ff
The relation will be demonstrated through case analysis on the di
erent forms of
regular expressions. Given that Lemma 2 holds, it is su
cient to show that the operators
hold on the basic elements of regular expressions and then induce on the length of the
regular expression.
R
C
Σ
(
R
)
Rec(
C
Σ
(
R
))
a
n
b
m
a
n
b
m
{∅
n
·
a
,∅
m
·
b
}
∈
Perms
(
R
)
a
n
b
m
a
n
b
m
|
{∅
n
·
a
,∅
0
·
b
}∨{∅
0
·
a
,∅
m
·
b
}
|
∈
Perms
(
R
)
a
n
∗
a
0
a
n
∗
{{
}
0
·
a
}
∈
n
Perms
(
R
)
a
n
∗
b
m
∗
(
a
n
|
b
m
)
∗
{{
}
0
·
a
,{
}
0
·
b
}
R
n
m
Matches
for permutation of
s
(
a
n
∗
b
m
∗
)
k
a
n
∗
b
m
∗
|
{{
}
0
·
a
,{
}
0
·
b
}
R
n
m
Matches
for permutation of
s
Proof (Match
C
Σ
() is evaluated in two phases, first trans-
forming the input into an initial constraint expression (Definition 7), and then iteratively
reducing the expression into a DCE. The initial transformation simply changes the op-
erators into those of the constraint-expression domain, whilst replacing alphabetic sym-
bols into basic constraints. It is evident that
→
Evaluation).
Recall that
∈ Σ
∗
. ∀
a
n
)
∀
a
∈ Σ.
s
n
∈ N.
match(
s
,
↔
eval
↓
#
s
Σ
∅
n
·
a
), since the LHS will only be true for sequences of
a
s of length
n
,which
also holds for the RHS. The task is thus to demonstrate that expressions obtained by
reductions using
(
will also evaluate to true. This is done via case analysis on the
operators, as follows:
