Newest at the top
| 2025-12-28 07:18:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-28 07:13:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 07:11:02 +0100 | <ski> | ah, okay |
| 2025-12-28 07:10:47 +0100 | <ski> | (there's not even a need for the branching to be finite, it could still be well-founded. although, possibly, in your case, you're only interested in finite branching) |
| 2025-12-28 07:10:16 +0100 | <iqubic> | Yeah. But in my case, I want you to always have strictly less moves as you go along. That's the main case I'm interested in exploring. |
| 2025-12-28 07:09:53 +0100 | <ski> | you could have the branching explode, and still have finite depth for every path |
| 2025-12-28 07:09:17 +0100 | <ski> | the important part is that each state is getting closer to a minimal element (a leaf, one which has zero successors), on each step |
| 2025-12-28 07:08:22 +0100 | <ski> | a tree that at each node at depth `n' has either zero or `n' branches of that node could still be well-founded |
| 2025-12-28 07:08:21 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2025-12-28 07:07:06 +0100 | <ski> | not necessarily |
| 2025-12-28 07:03:55 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-12-28 07:03:27 +0100 | <iqubic> | Basically, if you keep iterating nextMoves function, you should keep getting less and less options. |
| 2025-12-28 07:02:51 +0100 | <iqubic> | Or something like that. |
| 2025-12-28 07:02:39 +0100 | <iqubic> | forall a. let a' = nextMoves a in all [ length (nextMoves opt) < length a' | opt <- nextMoves a] |
| 2025-12-28 07:02:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-12-28 07:00:53 +0100 | <ski> | in terms of `nextMoves', instead of `forall y. y < x -> P y', we'd say `forall y. elem y (nextMoves x) = True -> P y'. iow, assuming that it holds for all the possible next states, it should be able to show it holds for the current state |
| 2025-12-28 06:59:14 +0100 | <iqubic> | Right I see. |
| 2025-12-28 06:58:38 +0100 | <ski> | for a strict order relation `<', a property like `forall P. (forall x. (forall y. y < x -> P y) -> P x) -> forall x. P x'. if we were talking about natural numbers, this would be called "strong induction" : you can prove a property `P' holds for all `x', if you can prove it holds for all `x', under the assumption it holds for all `y' that are strictly less than `x' |
| 2025-12-28 06:58:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 06:55:43 +0100 | <iqubic> | What do you mean by well-foundedness? |
| 2025-12-28 06:55:20 +0100 | <ski> | (iow, you don't need more than one operation, to be able to have a law) |
| 2025-12-28 06:55:01 +0100 | <ski> | in any case, even without an explicit order relation (computationally irrelevant or not), you should still be able to express a well-foundedness law for `nextMoves' |
| 2025-12-28 06:54:30 +0100 | <iqubic> | ski: Currently my planned API doesn't need a way to tell which states are smaller. |
| 2025-12-28 06:54:08 +0100 | <iqubic> | I agree. Because different games with completely different rules might want to use similar state representations. |
| 2025-12-28 06:53:45 +0100 | <ski> | (you could put the order relation as a second operation in the record .. but perhaps you have no use for it, at all, at run-time) |
| 2025-12-28 06:53:12 +0100 | <ski> | yep. the latter seems more reasonable |
| 2025-12-28 06:52:47 +0100 | <iqubic> | But my main question was "Do I model this as a typeclass with one function or a record of one function"? |
| 2025-12-28 06:52:30 +0100 | <ski> | (that is well-founded) |
| 2025-12-28 06:52:02 +0100 | <ski> | yea, some arbitrary partial order |
| 2025-12-28 06:51:33 +0100 | <iqubic> | ski: For some definition of "strictly less", yeah. |
| 2025-12-28 06:51:17 +0100 | <haskellbridge> | <slack1256> Data* |
| 2025-12-28 06:51:17 +0100 | <iqubic> | Basically, I've been reading the book "Winning Ways For Your Mathematical Plays" by Berlekamp, Guy, and Conway, and I want to implement some of these things in Haskell. |
| 2025-12-28 06:51:12 +0100 | <ski> | all the outputs of `nextMoves' are presumably strictly less than the input |
| 2025-12-28 06:51:06 +0100 | <haskellbridge> | <slack1256> Multiple implementations for that in no way related to the days structure to give an instance |
| 2025-12-28 06:49:33 +0100 | <ski> | some kind of well-founded order thing |
| 2025-12-28 06:49:23 +0100 | <iqubic> | Correct. I'm only interested in finite games here. |
| 2025-12-28 06:48:54 +0100 | <ski> | presumably iterating `nextMoves' is meant to lead to a tree where no path is infinite ? |
| 2025-12-28 06:47:42 +0100 | <haskellbridge> | <slack1256> Right, which is also a non obvious function |
| 2025-12-28 06:47:24 +0100 | <iqubic> | And I have no laws, because I have just the one function. |
| 2025-12-28 06:47:12 +0100 | <iqubic> | It's mainly just the "nextMoves" function that relates them. |
| 2025-12-28 06:46:56 +0100 | <iqubic> | Yeah, correct. |
| 2025-12-28 06:46:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-28 06:45:41 +0100 | <haskellbridge> | <slack1256> These combinatorial games are not related in anyway right? They just happen to implement a nextMoves function, the lack of laws pushes you to record of functions |
| 2025-12-28 06:45:16 +0100 | <iqubic> | BTW, Conway et al. call that version "prim", I think. |
| 2025-12-28 06:44:52 +0100 | <iqubic> | I can model this as with a state of [Int]. But if I want a similar game, but with the constraint of "after each move, the piles must all have a coprime number of objects", that's also a state of type "[Int]" but a different "nextMoves :: a -> [a]" function. |
| 2025-12-28 06:43:34 +0100 | <ski> | (unlike doing OO via existentials, where you'd open the record, apply an operation to the current state, and then rewrap new state with the operations again, every time) |
| 2025-12-28 06:43:03 +0100 | <iqubic> | In the basic game of "nim" you have a bunch of distinct piles, and each pile has a bunch of objects. Players take turns removing any amount of objects from a single pile. The winner is the player to make the last valid move. In other words, if you can't make a move, you lose. |
| 2025-12-28 06:42:45 +0100 | <ski> | you'd open the returned record in a scope, bringing the skolem into scope, and then use the operations directly. this is a way to do Abstract Data Types |
| 2025-12-28 06:42:16 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-28 06:41:29 +0100 | <haskellbridge> | <slack1256> I liked backpack... |