Mutual (co)inductive relations?

[siva.som...@gmail.com]

Hi all,

I was wondering whether it is possible to define mutual (co)inductive relations i.e. like this example with even' and odd' but one of the relations is CoDefine'd.

Thanks,

Siva

[Kaustuv Chaudhuri]

Abella doesn't support mixing inductive and co-inductive modes in the same mutually recursive definition block.

Can you explain why you need this feature with an actual example?

Kaustuv

[siva.som...@gmail.com]

Hi Kaustuv,

Sure! I have a grammar for types that I want to represent as a mixed inductive-coinductive type like this:

Kind ty type.

Type unit            ty.
Type foo ty -> ty -> ty.
Type bar ty -> ty -> ty.

Define is_ty : ty -> prop by
; is_ty unit
; is_ty (foo A B) := is_ty A /\ is_ty B
; is_ty (bar A B) := is_ty_co A /\ is_ty_co B
.

CoDefine is_ty_co : ty -> prop by
; is_coty A := is_ty A
.

(Not sure how to format code, unfortunately).

Siva