[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Re: a term representing the extension of a type
Hi Adam,
Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
> 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).
Thanks! When I ran this utility, I got the following:
$ constr -f mizar/text/polyform.miz FRAENKEL:funcreg 1
Required Constructors Directives, Mizar Ver. 7.8.03 (Darwin/FPC)
Copyright (c) 1990-2006 Association of Mizar Users
Constructors for FRAENKEL:funcreg 1 (with respect to mizar/text/polyform)
FRAENKEL
Once I added FRAENKEL to my the constructors directive, the error went
away.
By the way, what does `FRAENKEL:funcreg 1' mean? And what does the
invocation of constr on my file with the library reference
`FRAENKEL:funcreg 1' mean? (Sorry for asking such a basic question.
I'm fraid I don't know of any source of documentation, apart from the
people on this list, where I could look for an answer to my question.)
>> 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 ;-)
You're absolutely right -- thanks for your help! It has been a
harrowing expereience trying to debug this tiny error; I'm glad a
solution has been found.
Warm regards,
Jesse
--
Jesse Alama (alama@stanford.edu)
*393: Incorrect beginning of a reasoning item