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
