Mutual (co)inductive relations?

12 views
Skip to first unread message

siva.som...@gmail.com

unread,
Jul 24, 2020, 3:14:01 PM7/24/20
to Abella
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

unread,
Jul 24, 2020, 5:16:37 PM7/24/20
to Abella
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

unread,
Jul 25, 2020, 7:25:54 PM7/25/20
to Abella
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
Reply all
Reply to author
Forward
0 new messages