[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] puzzling error *109
Hi Jesse,
On Tue, 20 Feb 2007, Jesse Alama wrote:
I'm trying to redefine the operator * (composition of relations and
functions) for functions having certain specific types. One example
is the case of an enumeration, which I define as follows:
definition let X be finite set;
mode enumeration of X -> FinSequence of X means
len it = card X & rng it = X;
end;
Then I want to say the following, but I get an error:
definition let p be polyhedron,
f be enumeration of vertices(p),
P be Permutation of Seg V(p);
redefine func f*P -> enumeration of vertices(p);
::> *109
coherence;
end;
Error 109 is "Invalid order of arguments of redefined constructor". I
don't see what order I'm getting wrong, since the types of both the
left and right argument of * are the same (namely, Relation). What
might be going on here?
With this definition you redefine the '*' operator for relations since
Mizar allows to redefine only original constructors. And although in your
redefinition you're using the "functional" notation of '*' (reverse order
of arguments as compared with relations - the misterious and highly
confusing synonym just after FUNCT_1:19 in 'funct_1.abs' ;-)))), it still
means the composition of relations, so in fact it's P*f in terms of
relations. So the "real" order of arguments (loci) listed in this
redefinition should match the order used in RELATION:def 8 - 'P' should go
before 'f'.
I hope this doesn't sound like complete nonsense ;-) As I said, many
people have got confused by the consequences of function/relation notation
of '*' already.
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/
======================================================================