Timeline for "Largest set" in coinductive definitions
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 14, 2022 at 19:45 | comment | added | Dan Doel | The point here is that for elements to be 'of the form $σ:s$,' means not just that there is any old function of type $\mathcal{E} → Σ×\mathcal{E}$. The point is to characterize it in such a way that bisimilarity coincides with set theoretic equality. For examples like this, some amount of encoding is going to be necessary unless non-well-founded sets are allowed. But the point is to be considering sets of traces, not carrier sets of any algebra. | |
| Oct 14, 2022 at 7:53 | comment | added | N. Virgo | Actually this doesn't make sense, does it? The unique map into the final coalgebra can be many-to-one, so the final one doesn't have to be the largest one at all. I think this idea of "largest set" might actually just be wrong. | |
| Oct 14, 2022 at 5:56 | history | edited | N. Virgo | CC BY-SA 4.0 |
added 92 characters in body
|
| Oct 14, 2022 at 5:32 | history | answered | N. Virgo | CC BY-SA 4.0 |