Information Technology Reference
In-Depth Information
This is of course the scheme by which, for example, the merge-sort algo-
rithm can be composed from a merge function
g
, splitting functions
h
1
,
h
2
,and
operations
c
,
s
that handle the base case.
∀
G,lc,df
critical-pair-completion
[
G, lc, df
]
⇔
∀
F
(
G
[
F
]=
G
[
F,
pairs[
F
]])
∀
F
(
G
[
F,
]=
F
)
∀
F,g
1
,g
2
,p
G
[
F, g
1
,g
2
, p
]=
where
f
=
lc
[
g
1
,g
2
]
,h
1
=
trd
[
rd
[
f, g
1
]
,F
]
,h
2
=
trd
[
rd
[
f, g
2
]
,F
]
,
G
[
F, p
]
.
⇐ h
1
=
h
2
⇐
otherwise
G
Fdf
[
h
1
,h
2
]
, p
F
k
,df
[
h
1
,h
2
]
k
=1
,...,
|
F
|
This is the scheme by which, for example, the author's Grobner bases algo-
rithm can be composed from the function
lc
(“least common reducible”, i.e. the
least common multiple of the leading power products of two polynomials) and
the function
df
(“difference”, i.e. the polynomial difference in the polynomial
context). The algorithm scheme can be tried in all domains in which we have a
reduction function rd (whose iteration is called
trd
, “total reduction”) that re-
duces objects
f
w.r.t. to finite sets
F
of objects. The algorithm (scheme) starts
with producing all pairs of objects in
F
and then, for each pair
,checks
whether the total reduction of
lc
[
g
1
,g
2
] w.r.t.
g
1
and
g
2
yields identical results
h
1
and
h
2
, respectively. If this is not the case,
df
[
h
1
,h
2
] is added to
F
.
g
1
,g
2
6
Learning from Failed Reasoning
Learning from failed reasoning can be applied both in the case of proving propo-
sitions and in the case of synthesizing methods (algorithms). In this paper, we
will sketch the method only for the case of method (algorithm) synthesis.
Let us assume that we are working with some knowledge base K and we are
given some problem, e.g.
explicit-problem
[
A, P, Q
]
,
where the predicates
P
and
Q
are “known”, i.e. they occur in the knowledge
base
K
. For example,
P
and
Q
could be the unary predicate
is-finite-Grobner-
basis
and the binary predicate
generate-the-same-ideal
, respectively. (The exact
definitions of these predicates are assumed to be part of
K
. For details see [7]).
Then we can try out various algorithm schemes in our algorithm schemes library
L
. In the example, let us try out the general scheme
critical-pair-completion
, i.e.
let us assume
critical-pair-completion
[
A, lc, df
]
.
(It is an interesting, not yet undertaken, research subject to try out for this
problem systematically all algorithm schemes that are applicable in the context
Search WWH ::
Custom Search