Newest at the top
| 2024-12-22 18:09:39 +0100 | toch | (toch@user/toch) toch |
| 2024-12-22 18:09:28 +0100 | sinbad | (~sinbad@user/sinbad) Sinbad |
| 2024-12-22 18:07:33 +0100 | toch | (toch@user/toch) (Ping timeout: 248 seconds) |
| 2024-12-22 18:07:02 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2024-12-22 18:06:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-22 18:01:40 +0100 | tnt2 | tnt1 |
| 2024-12-22 18:01:40 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2024-12-22 18:01:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 18:00:33 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-22 18:00:21 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-12-22 17:59:50 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-12-22 17:58:28 +0100 | <ski> | albet70 : btw, i literally did the "like it capture k1 inside f, then call g with k1, then capture g's rest as k2, it jumps to k1 with k2" thing, in Haskell, to do coroutines, to be able to jump back and forth between two parallel (and a priori independent) traversals of two data structures, combining their data "pointwise"/"coordinatewise"/"in lockstep" |
| 2024-12-22 17:57:02 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-12-22 17:56:19 +0100 | <ski> | albet70 : dunno whether it'd be reasonable with `async'. passing data (and not just the frozen control point) as "baton" back and forth between coroutines requires them to know about each other, or at least about the interface of the other(s), so would seem to assume synchronous communication |
| 2024-12-22 17:55:03 +0100 | tnt2 | tnt1 |
| 2024-12-22 17:55:03 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 2024-12-22 17:55:00 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-22 17:53:36 +0100 | <ski> | thirdofmay18081814goya : from what i've seen, it's more common for formalize modal logics in axiomatic / Hilbert-style (with possible axioms like `[] A |- A',`[] A |- [] [] A',`A |- [] <> A',`[] A |- <> A',`<> A |- [] <> A ',&c. depending on the particular modal logic in question that we're formalizing), rather than in a natural deduction, or in a sequent calculus (what i sketched above) style |
| 2024-12-22 17:51:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-12-22 17:50:48 +0100 | <albet70> | how to archive that with async? |
| 2024-12-22 17:50:38 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-12-22 17:50:25 +0100 | <albet70> | or say passing function inside context into another function |
| 2024-12-22 17:49:34 +0100 | <albet70> | ski , but that coroutine passing variable between two functions |
| 2024-12-22 17:46:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 17:45:51 +0100 | <ski> | albet70 : sounds like coroutines |
| 2024-12-22 17:45:37 +0100 | <haskellbridge> | <thirdofmay18081814goya> woah thank you very much for the extensive comments! I'm studying these |
| 2024-12-22 17:45:19 +0100 | toch | (toch@user/toch) toch |
| 2024-12-22 17:44:38 +0100 | <ski> | (or, if we want to restrict to single conclusions, just : if `[] Gamma , A |- <> B', then `[] Gamma , <> A |- <> B') |
| 2024-12-22 17:44:37 +0100 | toch | (toch@user/toch) (Quit: WeeChat 4.5.0) |
| 2024-12-22 17:42:45 +0100 | <ski> | and, symmetrically, we can have a rule that if `[] Gamma , A |- <> Delta', then `[] Gamma , <> A |- <> Delta' |
| 2024-12-22 17:40:35 +0100 | <ski> | left it means "and" roughly)) |
| 2024-12-22 17:40:29 +0100 | <ski> | more generally, one can have a rule that if `[] Gamma |- A' (where `Gamma' is a collection of hypotheses considered conjunctively, and `[] Gamma' means `[]' applied to each one of them, individually), then `[] Gamma |- [] A' (or even : if `[] Gamma |- A , <> Delta', then `[] Gamma |- [] A , <> Delta', where `Delta' is a collection taken disjunctively (`,' on the right of `|-' means "or" roughly, while to the |
| 2024-12-22 17:40:18 +0100 | tnt2 | tnt1 |
| 2024-12-22 17:40:17 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 2024-12-22 17:39:48 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-22 17:38:36 +0100 | gmg | (~user@user/gehmehgeh) (Ping timeout: 264 seconds) |
| 2024-12-22 17:38:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-22 17:37:34 +0100 | <ski> | necessarily, `A' still holds, so `B' is also still holds), and then we can derive `[] A |- [] B' (when `A' holds even necessarily, `B' will then also hold necessarily). first step is comonadic unit (`extract'). second step is comonadic "preservation" (`(<<=)', `(=>>)') |
| 2024-12-22 17:37:28 +0100 | <ski> | thirdofmay18081814goya : if `[]' represents "necessity" of some kind (alethic ("necessary"), temporal ("always","henceforth/hereafter","hitherto/heretofore"), epistemic ("is known by me"), doxastic ("is believed by me", deontic ("obligatory"), provability ("is provable in the formal system"), ..), then if we assume `A |- B' holds, then we can derive `[] A |- B' (under the stronger condition of `A' holding |
| 2024-12-22 17:33:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 17:32:15 +0100 | <ski> | (`return'). second step is monadic extension (`(=<<)', `(>>=)'/"bind") |
| 2024-12-22 17:31:23 +0100 | <ski> | we can derive `A |- <> B' (under the condition of `A', `B' holds, so `B' is possible), and then we can derive `<> A |- <> B' (should `A' hold only possibly, `B' will then still hold possibly). first step is monadic unit |
| 2024-12-22 17:31:17 +0100 | <ski> | thirdofmay18081814goya : if `<>' represents "possibility" of some kind (alethic ("possible"), temporal ("sometimes","eventually/later","earlier/before"), epistemic ("is consistent with my knowledge / might hold for all i know"), doxastic ("is consistent with my belief", deontic ("permissible"), provability ("is consistent with derivability in the formal system"), ..), then if we assume `A |- B' holds, then |
| 2024-12-22 17:25:19 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-12-22 17:25:07 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 252 seconds) |
| 2024-12-22 17:22:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-22 17:20:50 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) alecs |
| 2024-12-22 17:19:24 +0100 | roosterphant | (~roosterph@185.21.217.76) |
| 2024-12-22 17:19:12 +0100 | swistak | (~swistak@185.21.216.141) |
| 2024-12-22 17:19:01 +0100 | roosterphant_ | (~roosterph@185.21.217.76) (Remote host closed the connection) |