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

[mizar] question about dependence operator in mmlquery



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)