[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)