Hi Andrei,
It should be noted that Coquand wrote this already in 1986, basically arguing
that HOL is consistent because it allows only "a (weak) form of polymorphism",
see section 6.1 "Predicative polymorphism" in [Coquand, 1986] available online
at
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3153 (p. 10)
https://hal.inria.fr/inria-00076023/document (p. 9)
Impredicativity is prevented by a stratification of types to "Type" and
"Type_1".
Andrews' logic Q [Andrews, 1965] extends Q0 to a transfinite type theory
capable of expressing cardinals, as intended in your presentation at
http://andreipopescu.uk/slides/ITP2014-card-slides.pdf
In Q, a similar stratification exists implicitly by the use of different
quantifiers,
see the last paragraph of section 1 of my former post
https://sourceforge.net/p/hol/mailman/message/35280731/
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html
Tom in Extended HOL [Melham, 1993b] doesn't take into account [Coquand, 1986],
but obviously because he inherits the implicit stratification from Q [Andrews,
1965]
by restricting lambda to bind regular variables only and by restricting the
universal quantifier (as primitive symbol) to bind type variables only, as in
Q, see
http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf (p. 7)
However, in all cases above, types are a separate syntactic category
and a matter of the meta-language rather than the formal language itself.
In R0, types are terms of type tau, hence their logic is integrated into the
object language,
similar to the integration of propositions if one proceeds from first-order
logic
(where terms and propositions are two separate syntactic categories)
to higher-order logic (where propositions are terms of type bool).
Therefore in R0 dependencies between the types are part of and expressible
in the formal language itself, and not only a matter of the meta-language,
and no stratification is required.
As the dependencies are preserved in the object language, I do not
object to impredicativity (self-reference) in general, as argued at
http://doi.org/10.4444/100.3 (p. 11)
Library references (ISBN etc.) for [Coquand, 1986] are also available at
http://lics.siglog.org/archive/1986/Coquand-AnAnalysisofGirards.html
http://dblp.org/rec/conf/lics/Coquand86
http://dblp.dagstuhl.de/db/conf/lics/lics86.html
Best regards,
Ken
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100
> Am 24.07.2017 um 14:07 schrieb Andrei Popescu <a.pope...@mdx.ac.uk>:
>
> Hi Chun,
>
> >> Thank you very much for letting me know this great paper.
>
> I am happy you find it helpful. Incidentally, this construction is not only
> more general, but also much simpler than the traditional one: Roughly, one
> just takes the product ofall algebras of the desired functor (in a suitably
> bounded fashion), which immediately gets weak initiality (meaning there
> exists at least one morphism to any other algebra -- here, of course, the
> cartesian projection), and then one takes its smallest subalgebra by a
> straightforward inductive construction -- the latter ensures uniqueness of
> the morphism, hence initiality.
>
> As a historical note: John Reynolds had performed a similar construction back
> in 1984, for a particular functor, in his famous "polymorphism is not set
> theoretic," and 10 years later Coquand adapted it to show that HOL cannot be
> extended with _impredicative_ polymorphism. My ITP 2014 slides discuss the
> high level ideas of the construction, as a bounded adaptation of the
> Reynolds-Coquand one:
>
> http://andreipopescu.uk/slides/ITP2014-card-slides.pdf
>
> Note also that Jan Rutten presents the dual of this construction for
> coalgebras (yielding what we call coinductive datatypes) in his standard
> monograph:
> https://fldit-www.cs.uni-dortmund.de/~peter/Rutten/UniversalCoalgebra.pdf
>
> >> If I managed to understand your method, instead of creating my datatype
> >> manually, I have more willing to try to implement it in HOL4 (as extension
> >> to the Datatype command), with the existing implementation in Isabelle/HOL
> >> referenced.
>
> This will probably be a lot of work, and require serious HOL4 expertise.
> Obviously, I am one of the people who finds such efforts trustworthy. :-)
> Besides allowing flexeble and compositional datatypes, they offer the
> infrastructure for expressive (co)recursion
> (http://andreipopescu.uk/pdf/ICFP2015.pdf
> http://andreipopescu.uk/pdf/amico.pdf), which is also useful for process
> algebra. But be warned they would be a serious detour from your specific
> process algebra research.
>
> Best regards,
>
> Andrei
>
>
> > Il giorno 21 lug 2017, alle ore 23:58, Andrei Popescu <a.pope...@mdx.ac.uk>
> > ha scritto:
> >
> > Hi Chun,
> >
> > That paper by Melham is important pioneering work, but will be of little
> > help to you since it only shows how to construct non-permutative datatypes,
> > like lists and ordered trees. The following paper
> >
> > http://andreipopescu.uk/pdf/LICS2012.pdf
> >
> > shows how to construct in HOL (inductive or coinductive) types of a more
> > general kind, which include, e.g., those that recurse through
> > bounded-cardinality powersets -- like the one you need.
> >
> > Best wishes,
> >
> > Andrei
> >
> >
> > Message: 1
> > Date: Fri, 14 Jul 2017 08:47:38 +0200
> > From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> > To: Michael Norrish <michael.norr...@data61.csiro.au>
> > Cc: hol-info@lists.sourceforge.net
> > Subject: Re: [Hol-info] [ExternalEmail] Re: On the use of new_axiom()
> > in formal projects
> > Message-ID: <730f82c8-3234-454a-bf19-5354a927a...@gmail.com>
> > Content-Type: text/plain; charset="utf-8"
> >
> > Hi Michael,
> >
> > Great, thanks! Then I guess the only remain issue in my project is to
> > define this datatype by hand. I?ll make a deeper reading in Tom Melham?s
> > paper [1] and see how such job can be done. If there're other relevant
> > materials, please let me know (at least the title).
> >
> > Regards,
> >
> > Chun Tian
> >
> > [1] Melham, Tom. Automating recursive type definitions in higher order
> > logic. 1989.
> >
> > > Il giorno 14 lug 2017, alle ore 08:24, <michael.norr...@data61.csiro.au>
> > > <michael.norr...@data61.csiro.au> ha scritto:
> > >
> > > Note further that a type where you have
> > >
> > > Datatype?CCS = C1 ? | C2 .. | SUM (num -> CCS)?;
> > >
> > > does not fall foul of cardinality problems. (You can recurse to the
> > > right of a function arrow as above, but not to the left, as would happen
> > > in SUM (CCS -> bool).)
> > >
> > > So, when I wrote ?you just can?t have infinite sums?, I was over-stating.
> > > If you see num -> CCS as enough of an infinite sum, then you?re OK. (And
> > > you could certainly also have ?SUM : ('a ordinal -> CCS) -> CCS?.)
> > >
> > > Unfortunately, HOL4?s Datatype principle doesn?t allow the definition
> > > above as I?ve written it, but such types can be defined by hand with
> > > sufficient patience.
> > >
> > > Michael
> > >
> > > On 14/7/17, 14:47, "michael.norr...@data61.csiro.au"
> > > <michael.norr...@data61.csiro.au> wrote:
> > >
> > > You just can?t have infinite sums inside the existing type for the
> > > cardinality reasons. But there?s no reason why you couldn?t have a type
> > > that featured infinite sums over a base type that didn?t itself include
> > > infinite sums.
> > >
> > > Something like
> > >
> > > Datatype`CCS = ? existing def ? (* with or without finite/binary
> > > sums *)`
> > >
> > > Datatype`bigCCS = SUM (num -> CCS)`
> > >
> > > Depending on the degree of branching you want, you might replace the
> > > num above with something else. Indeed, you could replace it with ?a
> > > ordinal.
> > >
> > > Michael
> > >
> > > On 14/7/17, 04:15, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
> > >
> > > Hi Ramana,
> > >
> > > Thanks for explanation and hints. Now it?s clear to me that, I
> > > *must* remove the new_axiom() from the project, even if this means I have
> > > to bring some ?ugly? solutions.
> > >
> > > Now I see ord_RECURSION is a universal tool for defining recursive
> > > functions on ordinals, for this part I have no doubts any more. But my
> > > datatype is discrete, no order, no accumulation, currently I can?t see a
> > > function (lf :?a ordinal -> ?b set -> ?b) which can be supplied to
> > > ord_RECURSION ..
> > >
> > > Currently I?m trying to something else in the datatype, and I have
> > > to replay all theorems in the project to see the side effects. Meanwhile
> > > I would like to hear from other HOL users for possible solutions on the
> > > infinite sum problem which looks quite a common need ..
> > >
> > > Regards,
> > >
> > > Chun
> > >
> > >> Il giorno 13 lug 2017, alle ore 14:35, Ramana Kumar
> > >> <ramana.ku...@cl.cam.ac.uk> ha scritto:
> > >>
> > >> Some very quick answers. Others will probably go into more detail.
> > >>
> > >> 1. If you use new_axiom, it becomes your responsibility to ensure that
> > >> your axiom is consistent. If it is not consistent, the principle of
> > >> explosion makes any subsequent formalisation vacuous. (If you don't use
> > >> new_axiom, it can be shown that any formalisation is consistent as long
> > >> as set theory is consistent.)
> > >>
> > >> 2. Yes. But you should probably detail why you claim that the axiom is
> > >> consistent and that you wrote it down correctly. It also makes it less
> > >> appealing for others to build on your work subsequently.
> > >>
> > >> 3. Yes. Prove the existence of functions defined on ordinals, specialise
> > >> that existence theorem with your desired definition, then use
> > >> new_specification. Maybe the required theorem exists already? Does
> > >> ord_RECURSION do it? See how ordADD is defined. (I haven't looked at
> > >> this in detail.)
> > >>
> > >> On 13 July 2017 at 21:10, Chun Tian (binghe) <binghe.l...@gmail.com>
> > >> wrote:
> > >> Hi,
> > >>
> > >> (Thank you for your patience for reading this long mail with the
> > >> question at the end)
> > >>
> > >> Recently I kept working on the formal proof of an important (and
> > >> elegant) theorem in CCS, in which the proof requires the construction of
> > >> a recursive function defined on ordinals (returning infinite sums of CCS
> > >> processes). Here is the informal definition:
> > >>
> > >> 1. Klop a 0o := nil
> > >> 2. Klop a (ordSUC n) := Klop a n + (prefix a (Klop a n))
> > >> 3. islimit n ==>
> > >> Klop a n := SUM (Klop a m) for all ordinals m < n
> > >>
> > >> (here the "+" operator is overloaded, it's the "sum" of an custom
> > >> datatype (CCS) defined by HOL's Define command. "prefix" is another
> > >> operator, both are 2-ary)
> > >>
> > >> I think it's a well-defined function, because the ordinal arguments
> > >> strictly becomes smaller in each recursive call. But I don't know how to
> > >> formall prove it, and of course HOL's Define package doesn't support
> > >> ordinals at all.
> > >>
> > >> On the other side, my datatype doesn't support infinite sums at all, and
> > >> it seems no hope for me to successfully defined it, after Michael has
> > >> replied my easier email and explained the cardinality issues for such
> > >> nested types.
> > >>
> > >> So I got two issues here: 1) no way to define infinite sums, 2) no way
> > >> to define resursive functions on ordinals. But I found a "solution" to
> > >> bypass both issues: instead of trying to express infinite sums, I turn
> > >> to focus on the behavior of the infinite sums and define the behavior
> > >> directly as an axiom. In CCS, if a process p transits to p', then p + q
> > >> + ... (infinite other process) still transit to p'. Thus I wrote the
> > >> following "cases" theorem (which looks quite like the 3rd return values
> > >> by Hol_reln) talking about a new constant "Klop"
> > >>
> > >> val _ = new_constant ("Klop", ``:'b Label -> 'c ordinal -> ('a, 'b)
> > >> CCS``);
> > >>
> > >> |- (!a. Klop a 0o = nil) ?
> > >> (!a n u E.
> > >> Klop a n? --u-> E <==>
> > >> u = label a ? E = Klop a n ? Klop a n --u-> E) ?
> > >> !a n u E.
> > >> islimit n ==> (Klop a n --u-> E <==> !m. m < n ? Klop a m --u-> E)
> > >>
> > >> I used new_axiom() to make above definion accepted by HOL. I don't know
> > >> how to "prove" it, don't even know what to prove, because it's just a
> > >> definition on a new logical constant (acts as a black-box function),
> > >> while it's behaviour is exactly the same as if I have infinite sums in
> > >> my datatype and HOL has the ability to define recursive function on
> > >> ordinals.
> > >>
> > >> From now on, I need no other axioms at all. Then I can prove the
> > >> following "rules" theorems which looks like the first return value of
> > >> Hol_reln:
> > >>
> > >> |- (!a n. Klop a n? --label a-> Klop a n) ?
> > >> !a n m u E. islimit n ? m < n ? Klop a m --u-> E ==> Klop a n --u-> E
> > >>
> > >> Then I can use transfinite inductino to prove a lot of other properties
> > >> of the function ``Klop a``. And with a lot of work, finally I have
> > >> proved the following elegant theorem in Concurrent Theory:
> > >>
> > >> Thm. (Coarsest congruence contained in weak equivalence)
> > >> |- !g h. g ?? h <==> !r. g + r ? h + r
> > >>
> > >> ("??" is observation congruence, or rooted weak bisimulation
> > >> equivalence. "?" is weak bisimulation equivalence)
> > >>
> > >> Every lemma or proof step corresponds to the original paper [1] with
> > >> improvements or simplification. And if you let me to write down the
> > >> informal proof (from the formal proof) using strict Math notations and
> > >> theorems from related theories, I have full confidence to convince
> > >> people that it's a correct proof.
> > >>
> > >> But I do have used new_axiom() in my proof script. My questions:
> > >>
> > >> 1. What's the risk for a new_axiom() used on a new constant to break the
> > >> consistency of entire HOL Logic?
> > >> 2. With new_axiom() used, can I still claim that, I have correctly
> > >> formalized the proof of that theorem?
> > >> 3. (optionall) is there any hope to prevent using new_axiom() in my case?
> > >>
> > >> Best regards,
> > >>
> > >> Chun Tian
> > >>
> > >> [1] van Glabbeek, Rob J. "A characterisation of weak bisimulation
> > >> congruence." Lecture notes in computer science 3838 (2005): 26.
> > >>
> > >> --
> > >> Chun Tian (binghe)
> > >> University of Bologna (Italy)
> > >>
> > >>
> > >> ------------------------------------------------------------------------------
> > >> 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
> hol-info Info Page - SourceForge
> lists.sourceforge.net
> hol-info is for general discussions about the HOL system, and for relevant
> announcements (of system updates, and also of conferences that the moderators
> feel will be ...
>
> > >>
> > >>
> > >
> > >
> > >
> > >
> > > ------------------------------------------------------------------------------
> > > 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
> hol-info Info Page - SourceForge
> lists.sourceforge.net
> hol-info is for general discussions about the HOL system, and for relevant
> announcements (of system updates, and also of conferences that the moderators
> feel will be ...
>
> > hol-info Info Page - SourceForge
> > lists.sourceforge.net
> > hol-info is for general discussions about the HOL system, and for relevant
> > announcements (of system updates, and also of conferences that the
> > moderators feel will be ...
> >
> >
> > >
> > >
> > > ------------------------------------------------------------------------------
> > > 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
> hol-info Info Page - SourceForge
> lists.sourceforge.net
> hol-info is for general discussions about the HOL system, and for relevant
> announcements (of system updates, and also of conferences that the moderators
> feel will be ...
>
> > hol-info Info Page - SourceForge
> > lists.sourceforge.net
> > hol-info is for general discussions about the HOL system, and for relevant
> > announcements (of system updates, and also of conferences that the
> > moderators feel will be ...
> >
> >
> >
> > -------------- next part --------------
> > A non-text attachment was scrubbed...
> > Name: signature.asc
> > Type: application/pgp-signature
> > Size: 203 bytes
> > Desc: 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
> >
> > ------------------------------
> >
> > Subject: Digest Footer
> >
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> hol-info Info Page - SourceForge
> lists.sourceforge.net
> hol-info is for general discussions about the HOL system, and for relevant
> announcements (of system updates, and also of conferences that the moderators
> feel will be ...
>
> > hol-info Info Page - SourceForge
> > lists.sourceforge.net
> > hol-info is for general discussions about the HOL system, and for relevant
> > announcements (of system updates, and also of conferences that the
> > moderators feel will be ...
> >
> >
> >
> >
> > ------------------------------
> >
> > End of hol-info Digest, Vol 134, Issue 24
> > *****************************************
>
> ------------------------------------------------------------------------------
> 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
