[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: a term representing the extension of a type
Hi Jesse,
On Wed, 20 Dec 2006, Jesse Alama wrote:
Hi Josef,
Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
On Wed, 29 Nov 2006, Jesse Alama wrote:
Andrzej Trybulec <trybulec@math.uwb.edu.pl> writes:
you probably need in the Environment Declaration
registrations FRAENKEL;
Why?
Because the registrations in FRAENKEL ensure that the type Element of
Funcs(A,B) widens to the "type" Function. "Function" is actually just
syntactic sugar ("expandable mode") for attributes Function-like and
Relation-like
(http://mmlquery.mizar.org/mml/4.66.942/funct_1.html#NM1).
When you import the needed registrations from FRAENKEL, i.e.
registration let A, B be set;
cluster Funcs(A,B) -> functional;
end;
registration let P be functional set;
cluster -> Function-like Relation-like Element of P;
end;
the attribute "functional" will be automatically added to any
"Funcs(A,B)" term, and the attributes "Function-like" and
"Relation-like" will be automatically added to any term which already
has the "functional" attribute, making it a "Function" (needed for the
"." functor).
Thanks; I appreciate your help. It still seems that I'm missing
something, though.
In the MIZAR file in question the registerations directive is
registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, NAT_1, INT_1, VECTSP_1;
It's not easy to say precisely what the problem is not knowing the
contents of your 'constructors' directive as well. It's because some
registrations are not imported ('cut off' secretly, even if an article is
listed in 'registrations') if there are some constructors missing which
are neccessary to 'understand' the registration - the information of this
'cutting off' is stored in the '*.log' file, which not many users know
about, I'm affraid ;-) So, probably in your case, one of the needed
clusters needs some extra constructors. To check which constructors are
needed for any notion, you may use the 'constr' utility, say:
./constr -f 'text/myarticle' FRAENKEL:funcreg 1
or so (try constr without arguments to see the invocation synopsis).
Here's my definition of 1-chain of p:
definition let p be polyhedron;
mode 1-chain of p is Element of Funcs(edges(p),{0,1});
end;
Here's the problematic definition:
definition let p be polyhedron, c be 1-chain of p, v be vertex of p;
func ENumSet(p,c,v) -> Subset of {0,1} means
ex X being Subset of {0,1} st X = { aa(p,v,e) where e is edge of p : c.e = 1 } & it = sum(X);
::> *103
existence;
uniqueness;
end;
Error 103 is "Unknown functor". I'm pretty sure that the problem here
is that c does not have type `Function'. (Evidence:
definition let p be polyhedron, c be 1-chain of p, v be vertex of p;
func ENumSet(p,c,v) -> Subset of {0,1} means
ex X being Subset of {0,1} st X = { aa(p,v,e) where e is edge of p : (c qua Function).e = 1 } & it = sum(X);
::> *116
existence;
uniqueness;
end;
Error 116 is "Invalid `qua'".)
Here's what I think is happening. The term `Funcs(edges(p),{0,1})' has
type `functional' thanks to
registration let A, B be set;
cluster Funcs(A,B) -> functional;
end;
in FRAENKEL. Also, `Element of Funcs(edges(p),{0,1})' has type
`Function-like Relation-like Element of P', thanks to
registration let P be functional set;
cluster -> Function-like Relation-like Element of P;
end;
in FRAENKEL. (Does this statement say that any term that has type
Element of P, where P has type functional set, gets types
Function-like and Relation-like?) Finally, we have
definition
mode Function is Function-like Relation-like set;
end;
from FUNCT_1, which is in my definitions directive. (FUNCT_1 is also
in my registrations directive.)
Is this a correct reconstruction of what's happening?
What might account for the error that I'm getting?
Your reconstruction is correct - the only broken link may be a missing
constructor ;-)
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/
======================================================================