Talk:Coinduction

Untitled

This page has a serious problem: it is only useful to someone who already understands the concept very well. If you don't understand the concept, it is not going to help along the path to understanding. The function of an encyclopedia is to act as introductory material for the uninitiated, not to act as a terse reference for those who already know a topic. The page needs to be enriched with clearer definitions aimed at someone who does not already understand the topic, and examples to allow people to concretize their comprehension. --Pmetzger (talk) 15:59, 18 October 2011 (UTC)

It's on my to do list, but this is a very tricky subject. Many tutorials have been written on the subject, even these are aimed at mathematically mature computer scientists and then still difficult to follow. It will take considerable effort to write a good article on this subject. —Ruud 12:11, 20 October 2011 (UTC)

The thing with explanations is: If one can’t explain it to a freshman, then one hasn’t actually understood the subject.

Usualy this is because most classical education focusses on memorization without questioning, because the teachers themselves haven’t understood anything either. … Which is why the Feynmann method is so important.

So don’t best yourself; you probably suffer from the same problem, and need to first truly understand it yourself. Until then, there is nothing you can do. Except maybe find somebody who can explain it properly himself. — 109.42.178.124 (talk) 13:10, 10 October 2023 (UTC)

I agree with Pmetzger. Here is what I run into, this might help. The trouble starts in the second sentence for me, which says this:

"Coinduction is the mathematical dual to structural induction. [...]"

What is a "mathematical dual"? "dual" gets me into a whole new thing, category theory. And then "structural induction" gets me into another whole new thing.

Hope this helps.

Melizg (talk) 21:57, 13 August 2014 (UTC)

Theorem Provers

I guess there is more to say to co-datatypes and co-induction. I find:

"Coinductive methods are becoming widespread in computer science. In proof assistants such as Agda, Coq, and Matita, codatatypes and coinduction are intrinsic to the logical calculus. [...] Codatatypes and corecursion have long been missing features in proof assistants based on higher-order logic. Isabelle’s new (co)datatype definitional package finally addresses this deficiency, while generalizing and modularizing the support for datatypes."

Truly Modular (Co)datatypes for Isabelle/HOL
http://www21.in.tum.de/~traytel/papers/itp14-codata_impl/codata_impl.pdf

Jan Burse (talk) 00:43, 30 November 2014 (UTC)

The actual definition is missing

Coinduction is a mathematical proof principle. Its the categorical inverse of induction. The article should start with that, because its basically as simple as induction. THen give a simple proof by coinduction. THen go to implications and use cases. — Preceding unsigned comment added by 141.45.12.231 (talk) 23:04, 5 October 2018 (UTC)

Major Additions (September 2022)

Hey guys, I just added a lot of material to the article trying to address some of the concerns I saw on this talk page. The biggest issue in my opinion was that the page was essentially worthless to a non-expert (and probably not that helpful to an expert). So my main goal was to make the page USEFUL in some way. I did not edit the introduction at all, although it probably should be updated to better reflect some of the actual content. I may have violated some wikipedia guidelines, did some poor formatting, incorrectly cited something, or added/elided some important information or figures. If anyone has any serious concerns about my edits that can't be solved by making simple corrections, please let me know. Nathan.s.chappell (talk) 10:42, 1 September 2022 (UTC)

Typesetting

$\bot \times \bot \times ...=\bot \times \bot \times ...\times \bot \times \bot \times ...$

$\bot \times \bot \times \cdots =\bot \times \bot \times \cdots \times \bot \times \bot \times \cdots$

I encountered the first line above, with `...`, and changed it to the second, with `\cdots`. The difference is not only that the dots look different, but also the horizontal spacing between ${\textstyle \bot }$ and ${\textstyle \times }$ is different. TeX was deliberately designed that way from the outset for obvious reasons, but it seems those reasons are appallingly alien to 99% of its users. ok, Maybe 98%. Michael Hardy (talk) 15:09, 30 May 2023 (UTC)

Utterly useless description

I’m a very experienced programmer, write maily Haskell, yet the introductory section explains absolutely nothing. Is states"' a lot. But the author(s) clearly confuse(s) memorization for understanding. (A common problem in US education). … When even I can read the whole section and get nothing from it … then the article fails, and needs to be replaced by something actually useful. — 109.42.178.124 (talk) 13:05, 10 October 2023 (UTC)

I tend to agree. I wrote most of the stuff after the intro, but the intro was weird to me. It has a lot of links and "buzzwords." If you think it's appropriate I will try to rewrite the intro at some point. Any other opinions or comments would be appreciated. Nathan.s.chappell (talk) 21:49, 22 July 2024 (UTC)

I concur too. The article mixes "computer science" with logical and set-theoretical arguments. It may make sense to separate the way all this is formulated here. Mixing "mechanical" computer pseudo-science with Logic and Math give an impression of them having equal rights. Vlad Patryshev (talk) 10:10, 23 September 2024 (UTC)

Categorical Interpretation/Explanation?

I got a feeling that all this is pretty much formalizable/explainable via adjoint functors and limits. Existence of fixpoints is ensured by preserving limits (or colimits, respectively). What do you think?

Vlad Patryshev (talk) 10:10, 23 September 2024 (UTC)