Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [coinduction]

The tag has no usage guidance.

9 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
12 votes
0 answers

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

Given a coinductive datatype, one can usually (always?) define a bisimulation as the largest equivalence relation over it. I would like to add an axiom stating that if two members of the type are ...
Jannis Limperg's user avatar
5 votes
0 answers

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 ...
Damaru's user avatar
  • 51
2 votes
0 answers

How to prove by coinduction?

Previously, I've asked a question about coinduction. That gave me a lot of useful high-level insights on what coinduction provides, and what are the usefulness of coinductive proofs. This question is ...
Russell's user avatar
  • 153
2 votes
0 answers

"Practical coinduction" over $\mathbb N_\infty$?

I've just finished reading the paper Practical Coinduction by Kozen and Silva. What is the difference between induction over $\mathbb N$ and coinduction over $\mathbb N_\infty$? From the paper, it ...
wlad's user avatar
  • 489
2 votes
0 answers

Understanding Isabelle's implementation of coinduction

I'm studying how coinduction was encoded in Isabelle. At page 7 of the attached document, the author describes how some datatypes can be encoded as initial algebras. Here is one example: Finite lists ...
user1868607's user avatar
  • 2,194
2 votes
0 answers

How can one flip a stream using corecursion

Following is the definition of codata stream: codata Stream where hd : Stream −> A tl : Stream −> Stream For simplicity I assume I have just a ...
Imago's user avatar
  • 425
1 vote
0 answers

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?
盛安安's user avatar
  • 944
0 votes
1 answer

Definition of semantics of coinductive type

It is relatively easy to construct an object in set/class theory which has properties of any of the following: dependent sum, dependent product, W-types. E.g. Dependent sum of a family F is just the ...
georgy_dunaev's user avatar
0 votes
0 answers

Can you make the following "coinductive" proof precise?

Question: I have a proof which overwhelmingly feels like it's a proof "by coinduction." Unfortunately I can't coinduct my way out of a paper bag, so I don't know if this actually works. I ...
Siddharth's user avatar
  • 131