[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Re: Mizar 7.8.04 MML 4.80.962


Hi,

On Sun, 25 Mar 2007, Adam Grabowski wrote:


 Let me briefly summarize the changes in the hottest official
distribution of the Mizar system:

- The basic change in the Mizar sources which enforced
 the revision is that local definitions (objects introduced
 mainly by the "set" construct) are prohibited now in the
 exportable items. This was used extensively in the SCM series,
 unfortunately, due to the change the readability of these
 articles is much smaller.
There is no technical reason to forbid "set", "deffunc", and "defpred" which are (recursively) clean of local constants introduced by "(re)consider". That means, the existing exportable items can remain as they are, if the implementation does the additional "cleanness" check.
For me the main issue is presentation of exportable items: An article can use a lot of "local stuff" for convenience, but it seems reasonable to have the "global stuff" (i.e. exportable items) use only the "global language". Otherwise the general advantages of scoping and abstraction are gone (i.e., instead of just reading a theorem, you need to browse through the whole article, etc.). If naive expansion of the local definitions makes the exportable items unreadable, then perhaps some of the local definitions (which make the item "locally readable") should be made global? I.e., use normal function definition (via "equals") instead of a long "set" and "deffunc"?
Anyway, I agree that readability is one of Mizar's strengths, and we should try to preserve it. There has been so much time since this issue came up, and it's hard to understand why we should suddenly hurry to take a quick & dirty solution with side-effects that will be hard to revert. 


- There is no agreement which approach is better: (let me describe
 this based on the definition of a group) - to define the unity
 of a group as the selector of the underlying structure possessing
 the appropriate properties (the latter via "attribute" definition),
 or to introduce it by an adjective without any additional selector.
 The earlier approach is represented by "well-unital" adjective (and
 the unity is denoted by 1.F for a field F), the latter - by
 "unital" one (1_F). The change, done by Andrzej Trybulec consisted
 mainly in replacing "unital" with "well-unital" and "1." with "1_"
 (for "well-unital" these are equivalent notions). I am not sure if
 it's right because as I remember some five years ago we did exactly
 the opposite - but the "identify" construction wasn't available those
 days.


:-) "Experience, Not Only Doctrine", a.k.a. "Brownian Motion"

Best,
Josef