Rose Tree Mutual Recursion Termination
When trying implement a Rose Tree type data structure:
type node 't =
| Leaf 't
| Internal (List.list Int.int) (Seq.seq (node 't))
gives the error "Constructor Internal2 contains a non strictly positive occurrence of type node2 't", which seems to be cause by Seq.seq 't
being an opaque type which is assumed invariant over 't
. I think it should be sound for seq.Seq
to be covariant as it could be implemented with a List.list 't
or a (int, (int -> 't))
both of which are covariant.
Even if Seq.seq
was covariant it would still be difficult/(maybe impossible) to prove termination for functions using this definition as Why3 functions don't seem to have a way of ensuring that there result is less than there input in the structural well founded order. For example:
type node 't =
| Leaf 't
| Internal (List.list (node 't))
let rec function node_sum (self : node Int.int) : Int.int =
match (self) with
| Leaf x -> x
| Internal nodes -> list_sum nodes
end
with function list_sum (nodes : List.list (node Int.int)) : Int.int =
match (nodes) with
| Nil -> 0
| Cons first rest -> (node_sum first) + (list_sum rest)
end
use list.Length
use list.Nth
use option.Option
type node 't =
| Leaf 't
| Internal (List.list (node 't))
let rec function node_last (self : node 't) : Option.option 't =
match (self) with
| Leaf x -> Option.Some x
| Internal nodes -> list_last nodes
end
with function list_last (nodes : List.list (node 't)) : Option.option 't =
match(Nth.nth ((Length.length nodes) - 1) nodes) with
| Option.Some x -> node_last x
| Option.None -> Option.None
end
in the first example Why3 is able prove termination, but the second example it isn't since Nth.nth
isn't known to return a structural sub-part of the list.
This also makes it difficult to prove termination for map based rose-trees, eg. Why3 also can't prove termination for:
let rec function node_sum (self : node Int.int) : Int.int =
match (self) with
| Leaf x -> x
| Internal keys nodes -> list_sum keys nodes
end
with function list_sum (keys : List.list Int.int) (nodes : Map.map Int.int (node Int.int)) : Int.int =
match (keys) with
| Nil -> 0
| Cons first rest -> (node_sum (Map.get nodes first)) + (list_sum rest nodes)
end