Skip to main content

Questions tagged [coinduction]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
1 answer
50 views

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
26 views

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
1 vote
1 answer
49 views

(Co)-induction, fixpoints and inference systems

I'm learning about induction and co-induction. From what I know, given a set of judgments $U$ and an inference system $\Phi \subseteq \wp(U) \times U$, where $(\left\{ h_1,\dots,h_n \right\}, c) \in \...
dalz's user avatar
  • 13
2 votes
0 answers
89 views

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
1 vote
2 answers
72 views

"Largest set" in coinductive definitions

In several explanations of coinductive definitions (for example, in the answers to What is coinduction?), we're told that while an inductive definition gives us the smallest set with a specified set ...
N. Virgo's user avatar
  • 976
9 votes
3 answers
1k views

Can a total programming language be Turing-complete?

I've seen two answers to this: Wikipedia says no: These restrictions mean that total functional programming is not Turing-complete. And the Wikipedia article cites D.A. Turner as the coiner of "...
Max Heiber's user avatar
3 votes
1 answer
285 views

When can the coinduction hypothesis be used?

We can use the induction hypothesis when we are proving a property for a structure that is well-ordered. I am aware that there is a proof for this. When it comes to coinduction, I'm confused. One of ...
Russell's user avatar
  • 153
3 votes
1 answer
179 views

Coinduction in mathematical analysis?

Coinduction is a logical principle that is somehow dual to induction. I'm struggling to understand it. Are there any interesting examples of coinduction in analysis? A few examples seem like they ...
wlad's user avatar
  • 489
2 votes
0 answers
85 views

"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
72 views

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
5 votes
1 answer
370 views

How to write a coterminating, effectful program?

[Using Idris for code examples and terminology, but the question is not about Idris per se] In a post titled A Neighborhood of Infinity, @sigfpe argues that "the kind of open-ended loop we see in ...
Kazark's user avatar
  • 253
5 votes
1 answer
194 views

Proving with co-induction principles

I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the ...
0xd34df00d's user avatar
3 votes
1 answer
332 views

Definition of M-type in type theory

According to nLab, M-types are the dual of W-types. What are the introduction and elimination rules for M-types? Edit: For example, the formation/introduction/elimination rules for W-types are: $$\...
Andrew Cann's user avatar
2 votes
0 answers
46 views

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
2 votes
1 answer
151 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 ...
Bell Fox's user avatar
0 votes
1 answer
151 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 ...
Sudix's user avatar
  • 709
5 votes
0 answers
102 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 ...
Damaru's user avatar
  • 51
1 vote
0 answers
116 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?
盛安安's user avatar
  • 944
12 votes
0 answers
282 views

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
80 votes
2 answers
13k 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 ...
Dave Clarke's user avatar
  • 20.2k