Newest at the top
| 2025-02-03 09:39:03 +0100 | <tomsmeding> | if it turns out that the logic language is not quite expressive enough to do what you want and you end up needing to work around that, I'm not sure the result will really be much simpler than a straight implementation in a regular (functional) language |
| 2025-02-03 09:38:12 +0100 | <tomsmeding> | if you can indeed express them very naturally in the logic language :) |
| 2025-02-03 09:38:11 +0100 | <kuribas> | Of course, it doesn't prove the underlying logic system correct, but I don't really care about that. |
| 2025-02-03 09:37:51 +0100 | <kuribas> | tomsmeding: I am just surprised, because it seems much easier to prove right than a full blown algorithm that includes logic variables and unification. |
| 2025-02-03 09:36:12 +0100 | <kuribas> | Maybe a simple scheme/clojure macro to make it look nicer. |
| 2025-02-03 09:35:57 +0100 | <kuribas> | tomsmeding: I want to write them as an inductive data family in idris, then use elaborator reflection to translate them automatically. |
| 2025-02-03 09:34:16 +0100 | CiaoSen | (~Jura@2a05:5800:26f:a800:ca4b:d6ff:fec1:99da) CiaoSen |
| 2025-02-03 09:32:57 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-02-03 09:31:37 +0100 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) |
| 2025-02-03 09:30:03 +0100 | <tomsmeding> | simple prolog rules without cut can be directly translated to TeX inference rules with nothing more than a few regexes, but I'm not sure about the other way round |
| 2025-02-03 09:27:55 +0100 | <kuribas> | Also, prolog doesn't have occurs check. |
| 2025-02-03 09:27:23 +0100 | dysthesis | (~dysthesis@user/dysthesis) (Remote host closed the connection) |
| 2025-02-03 09:24:24 +0100 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) (Ping timeout: 260 seconds) |
| 2025-02-03 09:23:19 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 2025-02-03 09:20:28 +0100 | <kuribas> | Maybe because it is inefficient? |
| 2025-02-03 09:20:22 +0100 | <kuribas> | It seems to me that inference rules lend themselves quite well towards logic programming, but I don't find a lot about this. |
| 2025-02-03 09:19:47 +0100 | <kuribas> | Is there any work on implementing type inference algorithms in prolog or logic languages (minikanren)? |
| 2025-02-03 09:18:41 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-03 09:05:04 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-02-03 09:04:27 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-02-03 09:04:01 +0100 | CiaoSen | (~Jura@2a05:5800:26f:a800:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 2025-02-03 09:02:30 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-02-03 09:01:39 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-02-03 09:00:03 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-02-03 08:57:11 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-03 08:47:37 +0100 | erdem | (~erdem@user/erdem) (Quit: ZNC 1.9.1 - https://znc.in) |
| 2025-02-03 08:46:29 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-02-03 08:42:45 +0100 | kuribas | (~user@ptr-17d51emyzmm4mq8sbfo.18120a2.ip6.access.telenet.be) kuribas |
| 2025-02-03 08:42:31 +0100 | kuribas | (~user@ptr-17d51emyzmm4mq8sbfo.18120a2.ip6.access.telenet.be) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2025-02-03 08:41:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-03 08:38:39 +0100 | erdem | (~erdem@user/erdem) erdem |
| 2025-02-03 08:36:11 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-02-03 08:36:08 +0100 | kuribas | (~user@ptr-17d51emyzmm4mq8sbfo.18120a2.ip6.access.telenet.be) kuribas |
| 2025-02-03 08:35:06 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-03 08:30:57 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-02-03 08:30:57 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-03 08:29:45 +0100 | misterfish | (~misterfis@22.1-12-147.kabelnoord.net) misterfish |
| 2025-02-03 08:24:39 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-03 08:14:17 +0100 | urdh | (~urdh@user/urdh) urdh |
| 2025-02-03 08:13:49 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-02-03 08:09:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-03 08:02:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-03 07:58:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-03 07:58:24 +0100 | chele | (~chele@user/chele) chele |
| 2025-02-03 07:55:56 +0100 | ft | (~ft@p3e9bcd97.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-02-03 07:52:29 +0100 | sabathan | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-02-03 07:50:37 +0100 | alp | (~alp@2001:861:8ca0:4940:c78a:20e1:b983:926e) |
| 2025-02-03 07:48:09 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-02-03 07:47:34 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-02-03 07:47:34 +0100 | sabathan | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Ping timeout: 244 seconds) |