Newest at the top
2025-02-26 11:57:52 +0100 | <tomsmeding> | Athas: it switches to taping in C, instead of in haskell |
2025-02-26 11:57:36 +0100 | <Athas> | tomsmeding: I do use Numeric.AD.Double, but what does +ffi do? |
2025-02-26 11:57:04 +0100 | <lambdabot> | Consider it noted. |
2025-02-26 11:57:04 +0100 | <tomsmeding> | @tell Athas You may get better performance with 'ad' if you use Numeric.AD.Double _and_ enable the +ffi flag |
2025-02-26 11:50:23 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f8044b147bcd5cee5e7.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
2025-02-26 11:48:10 +0100 | xff0x | (~xff0x@2405:6580:b080:900:17f4:b7d4:84ba:3a30) |
2025-02-26 11:40:09 +0100 | merijn | (~merijn@77.242.116.146) merijn |
2025-02-26 11:39:03 +0100 | <ncf> | cheater: it's just a pair of functions. all functions are total unless stated otherwise, in mathematics |
2025-02-26 11:36:54 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
2025-02-26 11:23:28 +0100 | hattckory | (~hattckory@149.102.242.103) |
2025-02-26 11:20:24 +0100 | acidsys | (~crameleon@openSUSE/member/crameleon) crameleon |
2025-02-26 11:19:46 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
2025-02-26 11:14:57 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-26 11:14:06 +0100 | ski | (~ski@remote11.chalmers.se) |
2025-02-26 11:12:40 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f8044b147bcd5cee5e7.dip0.t-ipconnect.de) acidjnk |
2025-02-26 11:10:40 +0100 | <ames> | it ranges from subtly incorrect and extra verbose to complete and utter bullshit |
2025-02-26 11:10:29 +0100 | ski | (~ski@remote11.chalmers.se) (Ping timeout: 248 seconds) |
2025-02-26 11:09:54 +0100 | <ames> | just don't listen to nlab when it comes to type theory |
2025-02-26 11:09:10 +0100 | <tomsmeding> | I'd personally expect that as soon as that bouncing has any kind of _property_ (it converges, or you end up where you started, ...) then it _does_ have a name |
2025-02-26 11:06:18 +0100 | <cheater> | even smoothly so |
2025-02-26 11:06:11 +0100 | <cheater> | and can be continuated |
2025-02-26 11:05:47 +0100 | <cheater> | and a topology |
2025-02-26 11:05:44 +0100 | <cheater> | it can easily create congruences, for example |
2025-02-26 11:04:59 +0100 | <cheater> | anyways i think the idea of being able to bounce back and forth an infinite amount of times is pretty interesting |
2025-02-26 11:04:44 +0100 | <cheater> | you don't know about ncatlab? |
2025-02-26 11:04:00 +0100 | acidsys | (~crameleon@openSUSE/member/crameleon) (Ping timeout: 244 seconds) |
2025-02-26 11:02:38 +0100 | <[exa]> | oh that's a nice site. |
2025-02-26 11:01:12 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f8044b147bcd5cee5e7.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
2025-02-26 11:00:22 +0100 | bilegeek | (~bilegeek@2600:1008:b06e:701b:8c92:bcff:3789:c22c) (Quit: Leaving) |
2025-02-26 10:59:08 +0100 | <tomsmeding> | https://ncatlab.org/nlab/show/concept+with+an+attitude |
2025-02-26 10:59:04 +0100 | <Leary> | I'm still not sure what the original statement is supposed to be. f and g are partial functions with opposite co/domains and the property that each is total on the other's range? |
2025-02-26 10:58:01 +0100 | <[exa]> | anyway yeah, I'd say the original definiton would need a bit more of a spirit to it to actually spawn a useful name |
2025-02-26 10:57:26 +0100 | <[exa]> | ah well okay in math that could cause issues, I see |
2025-02-26 10:57:24 +0100 | <tomsmeding> | but if you already have the types of f and g, there's nothing more to specify! |
2025-02-26 10:57:10 +0100 | <[exa]> | f.f doesn't type |
2025-02-26 10:56:17 +0100 | <tomsmeding> | if it's just "f . g", then it's weaker; if you also include "f . f", then it's stronger |
2025-02-26 10:55:59 +0100 | <tomsmeding> | depends on what compositions you mean when you say "compositions of f and g" |
2025-02-26 10:55:55 +0100 | <[exa]> | so I'd say it's the same |
2025-02-26 10:55:40 +0100 | <[exa]> | the totality of the composition implies exactly the domain-is-a-superset property that was requested, and I just run it in both directions |
2025-02-26 10:54:41 +0100 | <tomsmeding> | that's not quite the same statement, is it? |
2025-02-26 10:54:37 +0100 | <cheater> | i don't like puzzle definitions |
2025-02-26 10:54:20 +0100 | <[exa]> | cheater: you can just say that compositions of f and g are total |
2025-02-26 10:52:11 +0100 | <cheater> | that sounds like something out of control theory. |
2025-02-26 10:51:20 +0100 | merijn | (~merijn@77.242.116.146) merijn |
2025-02-26 10:51:04 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 272 seconds) |
2025-02-26 10:49:13 +0100 | <tomsmeding> | you can call it a "back-and-forth" |
2025-02-26 10:48:39 +0100 | <cheater> | if no such thing is described then i shall coin that as a speculative function pair (or tuple for a more complex graph) |
2025-02-26 10:47:02 +0100 | tromp | (~textual@2a02:a210:cba:8500:b949:287e:6bbd:873b) |
2025-02-26 10:46:18 +0100 | <cheater> | no, they have no such property as stated |
2025-02-26 10:45:55 +0100 | <cheater> | i think that's interesting enough. |