Hi, thanks for your further comments. But now I feel maybe it’s worth to attack the more difficult problem instead: porting the BNF_datatype [1] to HOL4. Once this is done, not only I can use finite maps directly in the datatype definition, but also I could easily have infinite sums (:num -> CCS) in the CCS datatype.
Since I’ve already done with my thesis project, I have no other urgent HOL-related projects in hands at all. Maybe it’s a good time for me to slow down, restarting from Category Theory, then Isabelle, finally maybe I’ll be strong enough to bring HOL4 with the same strong datatype package as currently in Isabelle. There’s another related concept called “nominal datatype”, I don’t know what is it, but it seems necessary for formalizing more powerful process algebra (pi-calculus, psi-calculus, etc.), I could investigate if it’s possible to have its feature merged into the BNF_datatype. Anyway, this is long-term plan, I don’t make any promise. And thanks so much for all the help I got from HOL community! Regards, Chun Tian [1] Traytel, D., Popescu, A.: Foundational, compositional (co) datatypes for higher-order logic: Category theory applied to theorem proving. 2012 27th Annual IEEE Symposium on Logic in Computer Science. 596–605 (2012). > Il giorno 29 ott 2017, alle ore 23:27, michael.norr...@data61.csiro.au ha > scritto: > > You would have to define every function in terms of “fix” and then come up > with a clause for the new constant using “Fix” as well (or prove a new > “axiom” for the type). You would also need to prove new induction and cases > theorems. But yes, this “cheap approach” might be doable. > > Michael > > On 28/10/17, 02:39, "Chun Tian" <binghe.l...@gmail.com> wrote: > > >> Il giorno 27 ott 2017, alle ore 17:35, Chun Tian <binghe.l...@gmail.com> ha >> scritto: >> >> Thanks for your comments. >> >> If I quotient [1] the original CCS datatype into another one, I could expect >> to have the a “fix” constructor with a finite map, right? >> >> On the the other side, what if I directly define another similar constant, >> say “Fix” in this form: >> >> |- Fix fm X = fix (alist_to_fmap ls) X > > Sorry, it should be: > > |- Fix fm X = fix (fmap_to_alist fm) X > >> >> And in all theorems I only use “Fix”. Is this possible (as a cheap solution) >> for resolving the “structural congruences” issue? >> >> Regards, >> >> Chun Tian >> >> [1] Homeier, P.V.: Higher Order Quotients in Higher Order Logic. >> preparation; draft available at http://www cis …. (1969). > > > > ------------------------------------------------------------------------------ > 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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
