diff options
author | Son Ho | 2023-05-15 10:32:46 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | c6e9e51197833a8685c63e6c40d8eabf4e64c22d (patch) | |
tree | 257138e643515e09874f8d7cf6b2e7942622d258 /backends/hol4/divDefLib.sig | |
parent | 7801bca412767c8b71256ad480ae0e91d3a9392b (diff) |
Make minor modifications
Diffstat (limited to 'backends/hol4/divDefLib.sig')
-rw-r--r-- | backends/hol4/divDefLib.sig | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig index 51a09b9c..df879b4b 100644 --- a/backends/hol4/divDefLib.sig +++ b/backends/hol4/divDefLib.sig @@ -9,6 +9,32 @@ divDefExampleTheory. For examples of how to use DefiveDiv, see divDefLibExampleScript. + + Limitations: our encoding has limitations with regards to higher-order functions. More + precisely, the following definition wouldn't be accepted, because we don't know how + “MAP” would use ‘explore_tree’, meaning we can't prove the validity property required + by the fixed point upon defining ‘explore_tree’ and ‘explore_node’: + + {[ + Datatype tree: + | Leaf : int + | Node : tree list + + explore_tree (t : tree) : tree = + case t of + Leaf i => Leaf i + | Node ns => Node (explore_node ns) + + explore_node (ns : tree list) : tree list = + MAP explore_tree ns (* This is not supported *) + ]} + + *However*, our encoding does allow defining a function ‘f’ *then* giving it + as argument to a higher-order function such as ‘MAP’. + + Remark: "Partial recursive functions in higher-order logic", Alexander Krauss, + introduces an interesting approach by means of an inductive. It could be + interesting to try and compare. *) signature divDefLib = |