question about dependence operator in mmlquery

[Jesse Alama]

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@...)

[Josef Urban]

Hi Jesse,

On Sat, 3 May 2008, Jesse Alama wrote:

> I'm interested in fine-grained dependency analysis of proofs in mizar.
...
> 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)?

You can use XPath/XQuery directly on the XML form of articles (perhaps
after running through addabsrefs.xsl). E.g.

Existence//Ref

will collect references inside an Existence block, see Mizar.html for the
xml description, and e.g
http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl for a
Perl example

Josef

[Jesse Alama]

Hi Josef,

Josef Urban <urban@...> writes:

> Hi Jesse,
>
> On Sat, 3 May 2008, Jesse Alama wrote:
>
>> I'm interested in fine-grained dependency analysis of proofs in mizar.
> ...
>> 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)?
>
> You can use XPath/XQuery directly on the XML form of articles (perhaps
> after running through addabsrefs.xsl). E.g.
>
> Existence//Ref
>
> will collect references inside an Existence block, see Mizar.html for
> the xml description, and e.g
> http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl
> for a Perl example

I'm afraid I'm a bit of a neophyte when it comes to XPath/XQuery.  Can
you say a bit more about how I can use to collect, for example, all
references within a theorem?  (Also, I find Mizar.html a bit too
cryptic; from an outsider's perspective, it seems to be a inexplicable.)

Perhaps those who work on MMLQuery can explain just what the dependence
operator means.

Thanks,

Jesse

--
Jesse Alama (alama@...)

[Josef Urban]

Hi Jesse,

On Sun, 4 May 2008, Jesse Alama wrote:

> Josef Urban <urban@...> writes:
>> On Sat, 3 May 2008, Jesse Alama wrote:
>>
>>> I'm interested in fine-grained dependency analysis of proofs in mizar.
>> ...
>>> 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)?
>>
>> You can use XPath/XQuery directly on the XML form of articles (perhaps
>> after running through addabsrefs.xsl). E.g.
>>
>> Existence//Ref
>>
>> will collect references inside an Existence block, see Mizar.html for
>> the xml description, and e.g
>> http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl
>> for a Perl example
>
> I'm afraid I'm a bit of a neophyte when it comes to XPath/XQuery.  Can
> you say a bit more about how I can use to collect, for example, all
> references within a theorem?

say for ABCMIZ:1 the following XPath expression can be used

//JustifiedTheorem[@aid="ABCMIZ_0" and @nr="1"]//Ref

> (Also, I find Mizar.html a bit too
> cryptic; from an outsider's perspective, it seems to be a inexplicable.)

I don't say the documentation of the XML format is perfect. It probably
requires some knowledge about how Mizar works, though some parts could be
quite easy to understand. Also it is quite new, and I am probably the only
regular user so far. But certainly, I can extend the documentation if
there is enough interest and feedback. Also, it may really be quite
low-level for immediate query usage by outsiders, it is more intended as
an API for easy building of nice interfaces like MML Query, collecting
and transforming a lot of data from MML, etc.

Josef

[Grzegorz Bancerek]

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@...>:

> 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@...)
>

--
-----------------------------------------------------------
Grzegorz Bancerek
e-mail: bancerek@... (bancerek@...)
http://mmlquery.mizar.org/~bancerek/
Dept. of Theoretical CS
Faculty of Computer Science      fax. [phone]
Bialystok Technical University   tel. [phone]
http://wi.pb.edu.pl