[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] question about dependence operator in mmlquery

Hi Jesse,

the 'dependence' is generated by the sequence of instructions
(extended/admin mmlquery):

foreach constr operation dependence =
   # [ref or [firstnot|definiens|ref]];
foreach notat operation dependence = # ref;
foreach thdef operation dependence = # [ref or by ref];
foreach sch operation dependence = # [ref or by ref];
foreach dfs operation dependence = # ref;
foreach reg operation dependence = # [ref or by ref];

So, ENUMSET1:func 1 as constructor depends on
 ref:  HIDDEN:mode 1 -> set
and
 firstnot|definiens|ref: HIDDEN:mode 1
   HIDDEN:pred 1 -> =
   HIDDEN:pred 2 -> in
where firstnot (first notation) is ENUMSET1:funcnot 1
 and definiens of it is ENUMSET1:dfs 1:

  for b1 being set holds
         b1 in a4
      iff
         (b1 <> a1 & b1 <> a2 implies b1 = a3);

ENUMSET1:def 1 depends on all items above and additionally
on propositions referred to from the proof of correctness
and ENUMSET1:func 1 itself.

Such approach was good for my purposes but I may change it
for good reasons or add a new operation.

Regrads,
Grzegorz

Quoting Jesse Alama <alama@stanford.edu>:


I'm interested in fine-grained dependency analysis of proofs in mizar.
For that purpose I noticed (accidentally, it turns out) that mmlquery
implements a `dependence' operator.  For example:

mmlquery> dependence ENUMESET1:func 1;
QUERY: 'dependence ENUMSET1:func 1'
3 element(s)
HIDDEN:mode 1
HIDDEN:pred 1
HIDDEN:pred 2
mmlquery> dependence ENUMSET1:def 1;
QUERY: ' dependence ENUMSET1:def 1'
6 element(s)
ENUMSET1:func 1
HIDDEN:mode 1
HIDDEN:pred 1
HIDDEN:pred 2
TARSKI:def 2
XBOOLE_0:sch 3

This has been quite helpful for my work, but it leads to some unexpected
results.  The problem is that when I construct a dependency graph for my
recent proof of Euler's polyhedron formula, I use repeated calls to
mmlquery's dependency operator, and end up with the curious result that
the roots of the whole dependency graph are

ENUMSET1:func 1
ORDINAL1:attr 2
ARYTM 3:func 1
TARSKI:sch 1
TARSKI:th 7
TARSKI:th 2
TARSKI:func 3
STRUCT 0:struct 1
XBOOLE 0:func 3
TARSKI:func 2
XBOOLE 0:func 4
XBOOLE 0:func 2
TARSKI:pred 1
TARSKI:func 1
XBOOLE 0:func 1

I have thrown away HIDDEN:pred 1, HIDDEN:pred 2, and HIDDEN:mode 1 from
the dependency graph because I take those as just the input parameters
for the initial language; I count them as "improper" dependencies.

We recognize the axioms in TARSKI in the list, which should come as no
surprise; what is perhaps more curious is that items outside of TARSKI
are present, such as ENUMSET1:func 1.  After throwing away the
"improper" dependencies that come from HIDDEN) ENUMSET1:func 1 turns out
to be a root of the dependence tree because it has no proper
dependencies!

What I'd like to do is identify ENUMSET1:func 1 and its definition,
ENUMSET1:def 1, and stipulate that the dependencies of ENUMSET1:func 1
are just the dependencies of ENUMSET1:def 1.  I'm interested not so much
in the definiens of the functor itself, which seems to be what I get
when I query `dependence ENUMSET1:func 1'.  Rather, I'd like to focus on
the existence and uniqueness proofs for ENUMSET1:func 1.  As it stands,
that seems to be the meaning of `dependence ENUMSET1:def 1', but with an
additional twist: ENUMSET1:def 1 depends on ENUMSET1:func 1.

Does anyone have any idea how I might carry out that kind of analysis
using mmlquery (or any other tools, for that matter)?

Thanks,

Jesse

--
Jesse Alama (alama@stanford.edu)





--
-----------------------------------------------------------
Grzegorz Bancerek
e-mail: bancerek@mizar.org (bancerek@math.uwb.edu.pl)
http://mmlquery.mizar.org/~bancerek/
Dept. of Theoretical CS
Faculty of Computer Science      fax. +48 (85) 746-9057
Bialystok Technical University   tel. +48 (85) 746-9116
http://wi.pb.edu.pl