[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: puzzling errors
On Mon, 12 Mar 2007, Jesse Alama wrote:
Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
On Sun, 11 Mar 2007, Jesse Alama wrote:
In the article I'm working on, the formula
bounding-0-circuit-space(p) is Subspace of 0-circuit-space(p)
is flagged with *101 ("Unknown mode") underneath the use of Subspace.
At the stage where this formula occurs in my article, the term
bounding-0-circuit-space is just a VectSpStr over F2 (the field {0,1}
with the usual operations). I'm trying to establish that it has type
VectSp of F2 by proving and then appealing to
for G being Field,
U being VectSp of G,
X being non empty Subset of the carrier of U,
f being BinOp of X,
l being Function of [:the carrier of G,X:],X,
z being Element of X
st f = (the add of U)||X &
l = (the lmult of U)|[:the carrier of G,X:] &
z = the Zero of U
holds VectSpStr (# X, f, z, l #) is Subspace of U;
What surprises me is that this formula is flagged only with *4; it is
not flagged with *101. That suggests that the last formula
VectSpStr (# X, f, z, l #) is Subspace of U
is well-formed (in the sense that the use of Subspace there isn't
flagged with *101). Why is my theorem about Subspaces not flagged
with *101 but my claim about bounding-0-circuit-space(p) is flagged
with that error?
I guess the term '0-circuit-space(p)' is the culprit here - it seems its
type doesn't widen to 'Vectsp of F', where F is some field.
You're right -- it turns out that 0-circuit-space(p) didn't have the
right type. But there's a little twist in this story.
Indeed, it's a twist - I remember I've already tried to answer it before
;-)
I proved earlier in my article that the term 0-circuit-space(p) has
type VectSp of F2, and F2 has type Field. But what's required for
formulas of the form
X is Subspace of Y
is that Y has type
(*) non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF
where GF has type
non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr.
(This comes from VECTSP_4.) I have a registration
(**) registration let p be polyhedron;
cluster 0-circuit-space(p) -> VectSp of F2;
coherence by <some theorem>;
end;
So 0-circuit-space(p) has type VectSp of F2. But, to my surprise, it
didn't automatically get the adjectives in (*).
No, it doesn't register anything - please remember that term registrations
like this one do not register types for the term specified, only
attributes. The registration in general has the form:
cluster <term> -> adj_1 adj_2 ... adj_n [<type>];
where the optional <type> means only that if <term> already widens to that
<type>, the adjectives adj_1 etc are registered for the <term>.
In your case the list of attributes is just empty, so the registration
does nothing! It seems this new syntax extension which allows to include
types in registrations is very misleading, as people tend to confuse it
with redefinitions.
By adding a new registration
(***) registration let p be polyhedron;
cluster 0-circuit-space(p) -> non empty Abelian add-associative right_zeroed right_complementable VectSp-like;
coherence by <some theorem>;
end;
Yes, this registration is OK
the *101 error I described goes away. This surprises me because the
mode VectSp of F is expandable; I thought that any term of type VectSp
of F automatically got all the adjectives in (*). This is reinforced
by the failure of the coherence of registration (***) to go through
when I omit the reference to <some theorem>, even though (**) occurs
before (***). Is this a feature or a bug?
So you can see it's a feature, although a misleading one ;-)
Best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================