Newest at the top
2025-03-30 05:09:35 +0200 | <EvanR> | isn't the result of Branch t1 t2 always "a tree different by exactly a single application of the Branch constructor" |
2025-03-30 05:08:00 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: well, I think we need the whole thing: 1. a natural number 2. designating a natural number and its succesor 3. such that fed to a function that indexes constructor applications, 4. produce a tree different by exactly a single application of the "Branch" constructor (if our tree datatype is defined by a "Node" and "Branch" constructor) |
2025-03-30 05:06:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-03-30 05:05:50 +0200 | <EvanR> | based |
2025-03-30 05:05:38 +0200 | <EvanR> | and there's only finitely many of them |
2025-03-30 05:05:14 +0200 | <EvanR> | alright so a step is a constructor |
2025-03-30 05:04:46 +0200 | haritz | (~hrtz@user/haritz) haritz |
2025-03-30 05:04:46 +0200 | haritz | (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) (Changing host) |
2025-03-30 05:04:44 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah in this case, only inductively defined trees |
2025-03-30 05:04:28 +0200 | <EvanR> | are you only allowing finite trees |
2025-03-30 05:04:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> replace "at most one application of the datatype constructor" by "exactly one application" |
2025-03-30 05:03:49 +0200 | <EvanR> | what |
2025-03-30 05:03:35 +0200 | <haskellbridge> | <thirdofmay18081814goya> (tentative definition) |
2025-03-30 05:03:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: a step is a natural number that designates a pair, given by a natural number and its successor, such that when fed into a function "Nat -> Tree Int", produce a tree that is at most different by a single application of the datatype constructor |
2025-03-30 05:02:57 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-03-30 05:02:55 +0200 | haritz | (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) |
2025-03-30 05:02:45 +0200 | haritz | (~hrtz@user/haritz) (Remote host closed the connection) |
2025-03-30 05:01:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-30 04:59:23 +0200 | <EvanR> | did I construct let xs = 1 : xs in xs in a finite number of steps, or is it even successfully constructed |
2025-03-30 04:58:15 +0200 | <monochrom> | A step is a finite number of substeps. >:) |
2025-03-30 04:57:16 +0200 | <EvanR> | what's a step |
2025-03-30 04:56:57 +0200 | <EvanR> | thirdofmay18081814goya, "any element of Tree Int can be constructed in a finite number of steps" ... |
2025-03-30 04:56:22 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
2025-03-30 04:50:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-03-30 04:43:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-30 04:37:48 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-03-30 04:35:13 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
2025-03-30 04:33:55 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
2025-03-30 04:33:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-03-30 04:28:43 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 245 seconds) |
2025-03-30 04:27:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-03-30 04:15:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-03-30 04:15:08 +0200 | <EvanR> | I will gratefully deposit 0x$1.00 ($2.56) to the account of the first person who finds and reports anything that remains technically, historically, typographically, or politically incorrect. -- knuth |
2025-03-30 04:13:30 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
2025-03-30 04:13:11 +0200 | <JuanDaugherty> | (and credit where credit due to Conway) |
2025-03-30 04:12:51 +0200 | <JuanDaugherty> | https://en.wikipedia.org/wiki/Surreal_number confirmed |
2025-03-30 04:11:44 +0200 | <JuanDaugherty> | issat knuth's? |
2025-03-30 04:07:23 +0200 | <EvanR> | data Surreal = Cut (Tree Surreal) (Tree Surreal) |
2025-03-30 04:05:47 +0200 | roconnor | (~quassel@rocq/roconnor) roconnor |
2025-03-30 04:05:35 +0200 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
2025-03-30 04:05:15 +0200 | roconnor | (~quassel@rocq/roconnor) (Ping timeout: 252 seconds) |
2025-03-30 04:05:04 +0200 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
2025-03-30 04:02:18 +0200 | <EvanR> | data Real = Rat Rat | Lim (Rat -> Real) |
2025-03-30 04:01:46 +0200 | <geekosaur> | I was going to say you got that backwards, but in hindsight I guess it depends on how you interpret that name |
2025-03-30 04:00:40 +0200 | <EvanR> | data Rat = Over { numer :: Int, denomMinusOne :: Nat } |
2025-03-30 03:59:51 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
2025-03-30 03:56:36 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out) |
2025-03-30 03:52:58 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f5684d81f92e812b9d0.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
2025-03-30 03:51:53 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
2025-03-30 03:51:50 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |