Newest at the top
| 2024-10-07 06:26:33 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: totally ordered tree is just N |
| 2024-10-07 06:26:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:25:48 +0200 | <haskellbridge> | <Bowuigi> Not sure why can the trees be infinitely wide if the relation is a total order with a minimum element |
| 2024-10-07 06:25:43 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah wellordered trees are less structured than wellfounded trees, only the latter must have finite chains |
| 2024-10-07 06:24:13 +0200 | <haskellbridge> | <thirdofmay18081814goya> i'm not 100% how this translates to wellfoundedness |
| 2024-10-07 06:23:59 +0200 | <haskellbridge> | <thirdofmay18081814goya> uh i meant wellfounded |
| 2024-10-07 06:23:04 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-10-07 06:22:19 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) (Quit: Client closed) |
| 2024-10-07 06:22:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> so it works for induction but i'm trying to get at computable traversal |
| 2024-10-07 06:21:46 +0200 | <haskellbridge> | <Bowuigi> Oh yeah forgot about that |
| 2024-10-07 06:21:13 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 06:20:56 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: hm issue is well-ordered trees can have infinite branches |
| 2024-10-07 06:15:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-10-07 06:15:21 +0200 | <haskellbridge> | <Bowuigi> M types are the coinductive (thus possibly infinite) ones |
| 2024-10-07 06:12:54 +0200 | <haskellbridge> | <Bowuigi> Inducting in the direction of the least element of course, like induction on the natural numbers |
| 2024-10-07 06:12:34 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) |
| 2024-10-07 06:12:13 +0200 | <haskellbridge> | <Bowuigi> Every well ordered set has a least element and thus induction over the well order always terminates (assuming strong normalization outside of the W types) |
| 2024-10-07 06:10:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:10:29 +0200 | <haskellbridge> | <Bowuigi> I mean, they represent well orders constructively |
| 2024-10-07 06:08:40 +0200 | <haskellbridge> | <Bowuigi> According to https://ncatlab.org/nlab/show/W-type every W type should be traversable in a finite number of steps |
| 2024-10-07 05:59:37 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-10-07 05:59:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-10-07 05:56:25 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's a restriction on w-types that would get us all w-types that are traversable in a finite number of operations? |
| 2024-10-07 05:54:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:51:24 +0200 | synchromesh | (~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) synchromesh |
| 2024-10-07 05:46:46 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 05:46:16 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2024-10-07 05:43:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 05:38:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:27:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-10-07 05:23:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:22:41 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-07 05:19:23 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-07 05:12:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 05:08:45 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) ZLima12 |
| 2024-10-07 05:08:39 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-07 05:07:55 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) () |
| 2024-10-07 05:07:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:07:19 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-07 05:04:19 +0200 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-10-07 05:00:46 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 2024-10-07 04:56:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 04:52:07 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-10-07 04:52:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:41:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-10-07 04:36:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:35:09 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 04:32:47 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Read error: Connection timed out) |
| 2024-10-07 04:29:14 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-07 04:25:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |