[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] reconsiderings
Hi,
On Sat, 8 Nov 2003, Adam Grabowski wrote:
> Another substantial change yet noticed by Freek is removing
> of unclusterability of attributes.
This is really very good, big thanks to Czeslaw Bylinski and others
involved. I have started to fix my articles, and many reconsiderings and
references to typing theorems can be cleanly removed by clusters.
Two large remaining sources of "trivial" reconsiderings are castings of
function applications (e.g. "f.x") into "Element of Range" and castings
of "x in X" into "Element of X".
As for the first, I know that "/." (FINSEQ_4:def 4) can be used instead,
but much more theorems are stated using ".", so usually one would need to
quote FINSEQ_4:def 4 and additionally its assumption (it is a permissive
definition), which may be even more irritating than the reconsidering.
We discussed a bit similar problems last year
(http://mizar.uwb.edu.pl/forum/archive/0210/msg00018.html), and it seems
to me that maybe the cleanest solution is the discussed introduction of
the default (fixed, chosen) objects for types, and changing FUNCT_1:def 4
into something like this:
definition let f,x;
func f.x -> Element of rng f means
:: FUNCT_1:def 4
[x,it] in f if x in dom f otherwise it = the Element of rng f;
end;
FINSEQ_4:def 4 can then easily become just a redefinition (if needed at
all).
As for the second "trivial reconsidering" problem, i.e. how to get
"Element of X" from "x in X" (or e.g. "Subset" from "c=") without
reconsidering, it might get better in many cases just by applying fixes
like the one above to the result types of functors.
Just one quite experimental idea bringing more mess into Mizar:
We might allow predicates to contribute result types too (no, not any
higher order logic :-). Something like:
definition let X,Y;
redefine pred X c= Y;
synonym X is Subset of Y;
end;
This is probably not a big problem (we have that for predicates and
attributes). The problem is how to use this in analyser, which could be
something like:
- such types are collected from the atomic statements in the proof (or
conjunctions)
- if an argument of a functor fails to have a correct type according to
the current rules, these "predicate" types are tried (so they would be
"weaker" in comparison with normal type rules, preserving compatibility)
Maybe this is only needed for "in" and "c=" - once we have "Element" or
"Subset", the type inclusion rules should take over - so it could rather
be some requirement or pragma, that could be switched on and off ( in some
articles it would be quite undesirable).
Generally, it seems to me that there could be some research about the
practical optimality of such type systems, e.g. counting the number of
reconsiderings and references to typing theorems, or overall number of
type rules needed to automate some mechanism, etc.
Josef Urban
FFrom owner-majordomo Thu Nov 13 02:40:07 2003
Received: from mizar.uwb.edu.pl (localhost [127.0.0.1])
by mizar.uwb.edu.pl (8.12.10/8.12.8) with ESMTP id hAD1e7cY002890
for <mizar-forum-outgoing@mizar.uwb.edu.pl>; Thu, 13 Nov 2003 02:40:07 +0100 (CET)
Received: (from majordom@localhost)
by mizar.uwb.edu.pl (8.12.10/8.12.8/Submit) id hAD1e6eT002889
for mizar-forum-outgoing; Thu, 13 Nov 2003 02:40:06 +0100 (CET)
X-Authentication-Warning: mizar.uwb.edu.pl: majordom set sender to owner-mizar-forum@mizar.uwb.edu.pl using -f
Received: from mailgate.uwb.edu.pl (mailgate.uwb.edu.pl [212.33.71.77])
by mizar.uwb.edu.pl (8.12.10/8.12.8) with ESMTP id hAD1e3cY002885
for <mizar-forum@mizar.uwb.edu.pl>; Thu, 13 Nov 2003 02:40:05 +0100 (CET)
Received: from ktilinux.ms.mff.cuni.cz (ktilinux.ms.mff.cuni.cz [195.113.17.207])
by mailgate.uwb.edu.pl (8.11.6p2-18092003/8.11.6) with ESMTP id hAD1nL406502
for <mizar-forum@mizar.uwb.edu.pl>; Thu, 13 Nov 2003 02:49:21 +0100
Received: from localhost (urban@localhost)
by ktilinux.ms.mff.cuni.cz (8.11.6/linuxconf) with ESMTP id hAD1koN23665
for <mizar-forum@mizar.uwb.edu.pl>; Thu, 13 Nov 2003 02:46:50 +0100
Date: Thu, 13 Nov 2003 02:46:50 +0100 (CET)
From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
To: <mizar-forum@mizar.uwb.edu.pl>
Subject: [mizar] weak types
Message-ID: <Pine.LNX.4.33.0311122307500.22277-100000@ktilinux.ms.mff.cuni.cz>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-RAVMilter-Version: 8.4.2(snapshot 20021217) (mailgate)
Sender: owner-mizar-forum@mizar.uwb.edu.pl
Precedence: bulk
Reply-To: mizar-forum@mizar.uwb.edu.pl
Hi,
would it be difficult to implement in Mizar types that do not have to be
inhabited?
Sometimes it is quite natural to work with something, which generally
does not have to exist (e.g. large cardinals). Even if the existence is
provable, the proof may be much harder than the rest of the theory, and
not an immediate concern of the author. Both happened to me several times,
and I would much prefer to have at least some of the normal type
mechanisms, than to handle such "weak" types always just as predicates,
having to quote the "typing" theorems explicitly all the time.
It seems to me that in the implementation, one would just have to remember
for such types, that "consider" cannot be used, and maybe fix some
other hard-wired stuff in checker and analyser. Or is there any deeper
reason for avoiding them?
Josef Urban