Hi Chun Tian,
I don't know much about rich(er) type systems, and I'm not well
acquainted with Coq, but I'd say that what can be done in Isabelle or
HOL should be possible also in richer type systems.
Regarding modelling of a proof, the context of what I said is
describing, in HOL or Isabelle, a proof system for some logic, and
describing proofs in that proof system.
This is to be contrasted with an approach which I believe may be
available in constructive logic systems, which is to do a proof in (say)
Coq, then from that proof, to obtain a function which implements that
proof, so in a sense you are getting an object representing the proof.
But I may be talking nonsense here, so you need the comments of someone
more familiar with Coq or similar systems
Cheers,
Jeremy
On 06/10/17 05:38, Chun Tian (binghe) wrote:
Hi Jeremy,
I have a relevant question: one time we talked about the differences between Coq and
HOL (thread title: "Difficulties when migrating proof scripts from Coq”), and
you said:
"There's a distinction between an inductively defined set (in Isabelle or
HOL) and a datatype, though they can look similar. I don't know which
corresponds better to your Coq code
You can model a proof by a proof tree "object" by using a datatype
definition - then you have something of which you can define functions
to give, eg, its' height, number of rule applications, etc.”
Is the ability for theorem provers to do reasoning directly on “proofs” (or can
we say “proofs” are 1st-class objects?) also a consequence of “rich” type
systems?
Regards,
Chun Tian
Il giorno 05 ott 2017, alle ore 18:53, Jeremy Dawson <jeremy.daw...@anu.edu.au>
ha scritto:
Hi Mario,
Slightly off-topic, I had experience with the type system of HOL-Omega (system
F, if I recall the terminology right, not dependent types, so my experience may
not be very relevant)
My dominant recollection is the difficulty of getting the system to do the
right type inference, and getting terms to typecheck. I was forever working
out where I needed to put in type annotations. Quite frustrating after my
experience with regular HOL, and Isabelle.
It led me to conclude that the systems offering automatic inference of a principal type
really occupy a "sweet spot", ie the best compromise between ease of use and
expressive power.
Cheers,
Jeremy Dawson
On 06/10/17 03:46, Mario Castelán Castro wrote:
On 04/10/17 20:09, Ramana Kumar wrote:
Perhaps it would make more sense to ask people who are using rich type
systems what their motivations are :)
(On this list it's probably mostly people who are satisfied with simple
type theory.)
Yes, you are right. I wrote to this list because I am interesting in the
opinion of informed “outsiders”, not only “insiders”, so to speak.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
