Email Gateway (Aug 19 2022 at 16:38): Email Gateway (Aug 19 2022 at 16:38):From: Joachim Breitner <breitner@kit.edu>
Hi,
I’m doing my first steps with coinductive data type, and I’m struggling
with primcorec (probably due to a lack of understanding of the syntactic
requirements and the usual ways to work around them).
I created a data type for possibly infinite labeled trees:
codatatype (lset: 'a) ltree = Node (lnext : "'a ⇒ 'a ltree option")
With help of Andreas¹ I managed to define an „or“ operation: A path in
the resulting tree is a path in either one or the other:
primcorec lor :: "'a ltree ⇒ 'a ltree ⇒ 'a ltree"
where "lnext (lor t1 t2) = (λ x.
case (lnext t1 x) of Some t1' ⇒ (case lnext t2 x of Some t2' ⇒ Some (lor t1' t2') | None ⇒ Some t1')
| None ⇒ lnext t2 x)"
Now I try to define an "and" operation: A path in the resulting tree is
an interleaving of paths in one or the other tree. I tried it like this:
primcorec land :: "'a ltree ⇒ 'a ltree ⇒ 'a ltree"
where "lnext (land t1 t2) = (λ x.
case (lnext t1 x) of Some t1' ⇒ (case lnext t2 x of Some t2' ⇒ Some (lor (land t1' t2) (land t1 t2')) | None ⇒ Some (land t1' t2))
| None ⇒ (case lnext t2 x of Some t2' ⇒ Some (land t1 t2') | None ⇒ None))"
but it does not like the recursion via lor and gives this error message:
primcorec error:
Type unification failed: Clash of types "_ + _" and "_ ltree"
Type error in application: incompatible operand type
Operator: lor :: 'a ltree ⇒ 'a ltree ⇒ 'a ltree
Operand: Inr (t1', t2) :: 'a ltree + 'a ltree × 'a ltree
It seems that primcorec likes definitions of the form
primcorec land :: "'a ltree ⇒ 'a ltree ⇒ 'a ltree"
where "lnext (land t1 t2) = map_option (λ (x,y). land x y) o (λ x. ...)
better, but I couldn’t figure out how to use that here, where in once
case I need to invoke land twice and pass the result to lor.
Can I rewrite the definition in a way that primcorec likes it?
Greetings,
Joachim
¹ http://stackoverflow.com/questions/26883229/invalid-map-function-when-defining-a-corecursive-tree
signature.asc
Email Gateway (Aug 19 2022 at 16:38):From: Dmitriy Traytel <traytel@in.tum.de>
Dear Joachim,
your land is not primitively corecursive. Primitive means that the
corecursive call appears directly or via a map function as an argument
the constructor, but without any other function in between. In your case
there is a function in between: lor.
In my Coinductive_Languages AFP entry I show how to circumvent the
syntactic criterion in an ad-hoc fashion. The Times-function from there
has exactly the flavour of your land. A more systematic approach is
described in an unpublished draft [1] (however no package is yet
available for this). If you decide to go the systematic route, we could
still provide some guidance through the material that is formalized in
the context of [1], and you might become a first tester of the
forthcoming package.
Hope that helps,
Dmitriy
[1] http://www21.in.tum.de/~traytel/papers/fouco/fouco.pdf
Last updated: May 06 2024 at 08:19 UTC