I'm afraid your picture of the current state-of-play is entirely accurate.
I can add the following: - the tree type that lurks behind Harrison's datatype package already has countably infinite branching "for free". (IOW, that's where you have num on the left of the arrow.) In HOL4, our port of this code has this defined in src/datataype/ind_typeScript.sml. If you wanted infinite branching on a larger type (the reals say), this would be a bit fiddlier to set up, but the approach in John's paper would be slick. The problem would remain of needing to handle the function space functor in the SML code. Fundamentally, the datatype package's assumption is that all nested recursion happens through existing algebraic types. That assumption would have to be changed so that the recursions are assumed to happen through the equivalent of the LICS paper's bounded natural functors. - the inftree type is a distraction really; it can be used to help in a manual construction of a new type but it depends on lists, so isn't really a good basis for a foundational datatype package. - there is no ongoing development of anything on this front at the moment because there aren't enough hours in the day Michael On 4/12/20, 01:48, "Pablo Buiras" <bui...@kth.se> wrote: Hello everyone, I was wondering about the status of data type recursion on the right hand side of a function arrow in HOL4. For the sake of clarity, this would be to add support for a data type such as the following: test = A (num -> test) | B As far as I know this is currently not supported by the datatype package, and I am aware this issue has been raised a few times before [1,2] and is also an issue in the HOL4 GitHub repo [3]. As of 2015, it seems the most direct way of adding this feature was to implement the approach found in a LICS 2012 paper [4]. I was not able to find any new developments since 2015. Is this still a viable plan or has the situation changed in any way? Does anyone know if there are any ongoing efforts to implement this? Previously I found a paper by Harrison [5] in which he claims that it would be easy to extend his package to infinitely-branching trees, though I think this was never implemented. I found that there is a definition of potentially infinitely-branching trees in the HOL4 repository, under src/datatype/inftree, but it seems this is not used in the rest of the package. I know we could just use an alternative representation and/or manually construct the type we need, but this would be quite a hassle in the particular application we have in mind, as the development itself is exported from another tool. I’d be grateful for any other pointers you can provide. Thanks, Pablo References [1] https://sourceforge.net/p/hol/mailman/message/24442904/ [2] https://sourceforge.net/p/hol/mailman/hol-developers/thread/B678E335-C741-4F09-8803-187E00BCFD92%40nicta.com.au/#msg34282410 [3] https://github.com/HOL-Theorem-Prover/HOL/issues/266 [4] https://ieeexplore.ieee.org/document/6280479 [5] https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.115.1474&rep=rep1&type=pdf _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
