Re: [isabelle] primcorec error: Type unification failed



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

On 12.11.2014 13:38, Joachim Breitner wrote:
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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.