Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [coinduction]

The tag has no usage guidance.

2
votes
1answer
55 views

Does co-inductive and co-recursive types also have their recursors?

I'm new to type theory, and recently read introductory materials where dependent type are discussed. One of my friend asked me, "Those dependent types are having recursors & 'inductors'(dependent ...
0
votes
1answer
16 views

Bisimulations: Proof that the following LTS are not bisimilar

I have the two LTS (labeled transition system) as seen in the following picture: And the book is telling me that between those two LTS, their $1$ and $1'$ are non-bisimilar. So I tried to get a ...
5
votes
0answers
61 views

Is the set finite words over an alphabet a final coalgebra*?

I am studying what coinduction is. In particular, I am reading that coinductive datatypes can be defined as elements of a final coalgebra for a given polynomial endofunctor on $\tt Set$. I've seen ...
1
vote
0answers
91 views

Typing rules of coinductive types?

Are there typing rules for specific coinductive types such as conat or stream, or even in general the M-types?
8
votes
0answers
122 views

Is extensionality for coinductive datatypes consistent with Coq's logic?

Given a coinductive datatype, one can usually (always?) define a bisimulation as the smallest equivalence relation over it. I would like to add an axiom stating that if two members of the type are ...
63
votes
2answers
6k views

What is coinduction?

I've heard of (structural) induction. It allows you to build up finite structures from smaller ones and gives you proof principles for reasoning about such structures. The idea is clear enough. But ...