Re: Urelements?
Jesse Alama <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
I don't know exactly how the checker works, so this may be out of line, but here is one simple idea that doesn't even use heuristics. One could try a breadth-first approach to expansion: first don't do any definitional expansion, and try running the inference through the checker. If that fails, uniformly expand once anything that could be expanded, and retry the inference with a bigger premise set. And so forth. That's how SAD, for example, handles definitions. This preserves the complete/exhaustive property of the checker. This would probably not deliver the big speedups that Artur finds when expansion is switched off, but it might help nonetheless. And with this approach, one needn't to introduce a new primitive type. Jesse Josef Urban <[email protected]> writes: > Calling the basic object of set theory an "element" and preventing its > automated typing as "set" feels foundationally inventive. > > It seems that you want additional ad-hoc type/definitional-expansion > machinery for some particular sets. I would not do it ad-hoc for two > kinds of objects, but rather have a standard mechanism that allows to > mark a definition as something that should not be automatically > expanded by default (or in an environment). We faced a similar > situation some time ago with quaternions, and that had nothing to do > with foundations - just with having proper mechanisms for "knowledge > expansion". > > Josef > > 2012/3/12 <[email protected]>: >> Let me make one thing clear: >> >> we do not propose to chang the foundations of MML. The chang eis rather >> related to type handling. >> >> The (quite old/brand new) TARSKI:1 will be >> >> for x being element holds x is set >> >> >> It now obvious that 2 is a set, I mean >> >> 2 is set; >> >> is accepted without any references. In new approach it will need >> justification: >> >> 2 is set by TARSKI:1; >> >> I used many times (and it must be revised) >> >> 1-sorted(#1, ... #) >> >> for 1-element 1-sorted. I even wanted to do a revision :-). With new >> approach >> one must write >> >> 1-sorted(#{0}, ...#) >> >> that means the same and it less tricky. >> >> Regards, >> Andrzej >> >> >> >> > -- Jesse Alama http://centria.di.fct.unl.pt/~alama/