On 08/26/2011 01:08 PM, Makarius wrote:
On Thu, 25 Aug 2011, Andreas Schropp wrote:
Of course I am probably the only one that will ever care about these
things, so whatever.
I have always cared about that, starting about 1994 in my first
investigations what HOL actually is -- there are still various
misunderstandings in printed texts. And of course there is still no
fully formal theory of all the aspects that have been emphasized in
the variety of HOL implementations.
No offense: the last time we discussed these things
you were introducing local typedefs directly instead of expressing them
via global typedefs, which I told you is not exactly hard.
It looks like you are more concerned with an easy implementation,
leaving any matters of conservativity to me. I am not saying this is
bad, but every time my transformation gets harder, I am not
exactly feeling that "Makarius always cares about conservativity". ;D
Maybe you want to start a realistic formalization yourself?
This conservativity result that I am animating is a global theory
transformation featuring replacement of certain typedefs by
their representing sets, regarding them as soft types.
If someone is interested I would indeed write this up, but
given the complexity (I guess 3-4 pages of rule systems, without text)
I don't think we can hope for a realistic formalization.
BTW: Steven should get credit for seriously trying
conservativity of overloading at least. This helped to expose
the misconception, though he did not notice the problem.
Also my write-up of the Isabelle-Kernel is 8 pages (of rule systems,
without text!)
and still incomplete, so I don't think we will ever manage to prove
something
important about Isabelle. I am even being generous here, excluding e.g.
unification
which is part of the trusted code (for speed I guess) but generates
proof terms.
In my eyes, the only reason we can claim to satisfy the deBruijn
criterion is
that proof-checking is much easier in ZF. From an LCF POV we are not really
in game, because unification et al are trusted code.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
