Newest at the top
| 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... |
| 2025-12-28 06:41:16 +0100 | rekahsoft | (~rekahsoft@70.51.99.245) rekahsoft |
| 2025-12-28 06:41:11 +0100 | <iqubic> | Yeah, I get what you mean. |
| 2025-12-28 06:40:46 +0100 | <ski> | btw, sometimes it makes sense to make a function from a record-of-operations, to another (possibly existential) record-of-operations. this being one way to do something similar to the parameterized modules in the module system of the MLs (SML,OCaml) (cf. Backpack) |
| 2025-12-28 06:40:43 +0100 | rekahsoft | (~rekahsoft@70.51.99.245) (Remote host closed the connection) |
| 2025-12-28 06:39:28 +0100 | <ski> | yea, sounds like record of operations is more sensible, then |
| 2025-12-28 06:39:17 +0100 | <iqubic> | Essentially, I'm trying to model simple combinatorial games like "nim" where I can write a function like "nextMoves :: a -> [a]", but then I realized that different games might have the type for the state variable. |