Logs: liberachat/#haskell
| 2021-05-31 15:58:19 | × | ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Max SendQ exceeded) |
| 2021-05-31 15:58:45 | × | prite quits (~pritam@user/pritambaral) (Ping timeout: 268 seconds) |
| 2021-05-31 15:58:52 | → | ku joins (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) |
| 2021-05-31 15:58:55 | <tomsmeding> | to me it kind of looks like applyFOLRule in itself is quite fine, but it lays some restrictions on what Paths are fine |
| 2021-05-31 15:59:05 | <bor0> | Sure: it's in https://github.com/bor0/hoare-imp/commit/d891212a5f7cbf26483f8051fab57e36ab6641f2 |
| 2021-05-31 15:59:37 | → | brandonh joins (~brandonh@151.38.151.222) |
| 2021-05-31 15:59:41 | <bor0> | Though, e.g. `applyFOLRule [GoLeft] ruleAddS (A = B /\ C = D)` (pseudo-code) works fine - S A = S B /\ C = D |
| 2021-05-31 15:59:53 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection) |
| 2021-05-31 15:59:56 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 2021-05-31 16:00:08 | → | Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 2021-05-31 16:00:40 | <bor0> | So basically `applyFOLRule` within `applyFOLRule` easily exploits it |
| 2021-05-31 16:00:53 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 2021-05-31 16:01:11 | → | schuelermine joins (~anselmsch@ip5b409cba.dynamic.kabel-deutschland.de) |
| 2021-05-31 16:01:12 | <bor0> | Or maybe the problem is `applyFOLRule` within `applyFOLRule` on the _same_ formula... |
| 2021-05-31 16:02:00 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 265 seconds) |
| 2021-05-31 16:02:04 | ← | boioioing parts (~boioioing@cpe-76-84-141-127.neb.res.rr.com) () |
| 2021-05-31 16:02:23 | × | hyiltiz quits (~quassel@31.220.5.250) (Ping timeout: 252 seconds) |
| 2021-05-31 16:02:24 | <tomsmeding> | bor0: what does it even mean to have a path [GoLeft,GoRight] for a formula that has only one And? |
| 2021-05-31 16:02:34 | → | hyiltiz joins (~quassel@31.220.5.250) |
| 2021-05-31 16:03:21 | <bor0> | Here's the full definition of it: https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L61-L76. In this case, it will just apply the function at the "bottom" |
| 2021-05-31 16:03:39 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2021-05-31 16:04:00 | <tomsmeding> | that sounds like a convenience laxness that you'd not want in a logic system |
| 2021-05-31 16:04:10 | <tomsmeding> | but maybe that's me :) |
| 2021-05-31 16:04:47 | <bor0> | Yeah, I should make that stricter and make it return either an error or a proof like others |
| 2021-05-31 16:05:30 | × | ku quits (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) (Remote host closed the connection) |
| 2021-05-31 16:05:56 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 2021-05-31 16:05:59 | → | ku joins (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) |
| 2021-05-31 16:06:08 | × | dpl quits (~dpl@77-121-78-163.chn.volia.net) (Remote host closed the connection) |
| 2021-05-31 16:06:09 | × | xkapastel quits (uid17782@id-17782.tinside.irccloud.com) (Quit: .) |
| 2021-05-31 16:06:29 | → | dpl joins (~dpl@77-121-78-163.chn.volia.net) |
| 2021-05-31 16:06:39 | → | prite joins (~pritam@user/pritambaral) |
| 2021-05-31 16:06:49 | <tomsmeding> | yeah so in terms of logic, what's going wrong there is that you have a proof prfAeqB that claims A=B, and you're applying that under an 'exists B' binder |
| 2021-05-31 16:06:58 | <tomsmeding> | which of course defines a different B |
| 2021-05-31 16:07:16 | × | schuelermine quits (~anselmsch@ip5b409cba.dynamic.kabel-deutschland.de) (Quit: WeeChat 3.1) |
| 2021-05-31 16:07:53 | <tomsmeding> | one different way to approach this might be to adopt a convention that bound variables never shadow a free variable |
| 2021-05-31 16:07:55 | × | favonia quits (~favonia@user/favonia) (Quit: The Lounge - https://thelounge.chat) |
| 2021-05-31 16:08:45 | × | zebrag quits (~chris@user/zebrag) (Remote host closed the connection) |
| 2021-05-31 16:09:01 | <tomsmeding> | I believe that's called the Barendregt convention, but I may be mistaken |
| 2021-05-31 16:09:22 | <tomsmeding> | as long as you always ensure that this is the case, you can rewrite freely and you'll never shadow anything |
| 2021-05-31 16:09:30 | → | Ariakenom joins (~Ariakenom@2001:9b1:efb:fc00:84c1:f198:927e:8e8c) |
| 2021-05-31 16:09:51 | <tomsmeding> | but I'm not sure if that's practical to achieve in your system |
| 2021-05-31 16:10:53 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 244 seconds) |
| 2021-05-31 16:10:56 | <tomsmeding> | bor0: this function that gets passed to applyFOLRule, does that really need to be a full Haskell function? Could it perhaps also be some kind of expression with a hole? |
| 2021-05-31 16:11:23 | <bor0> | It's a full Haskell function, but limited to rule*. E.g. https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L255 |
| 2021-05-31 16:11:24 | × | cheater quits (~Username@user/cheater) (Ping timeout: 244 seconds) |
| 2021-05-31 16:11:46 | <tomsmeding> | if you could inspect that "function" inside applyFOLRule, then when you descend below a binder, you could check whether the bound variable name exists anywhere within the function, and if so, first rename the binder to something fresh |
| 2021-05-31 16:11:59 | <tomsmeding> | but you can't look inside a Haskell function, so you can't currently do that |
| 2021-05-31 16:12:03 | → | cheater joins (~Username@user/cheater) |
| 2021-05-31 16:12:10 | → | Bartosz joins (~textual@24.35.90.211) |
| 2021-05-31 16:12:34 | <bor0> | I'm okay to just error on it e.g. like https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L237. But I am unsure about the condition on which to error... |
| 2021-05-31 16:12:40 | <tomsmeding> | will the output of that function always be a single equality? |
| 2021-05-31 16:13:10 | <bor0> | well you can applyFOLRule ruleSymmetry within A=B/\B=C/\D=E to get A=C/\D=E |
| 2021-05-31 16:13:17 | <bor0> | This is the case where it works :) |
| 2021-05-31 16:13:26 | <tomsmeding> | the condition is that the function f itself, without its parameter, contains a reference to a variable with the same name as the binder you're descending under in applyFOLRule |
| 2021-05-31 16:13:38 | <tomsmeding> | but you can't currently check that criterion because Haskell function |
| 2021-05-31 16:14:10 | <tomsmeding> | bor0: but then the output of 'f' (here ruleSymmetry) will still be a single equality, right? |
| 2021-05-31 16:14:41 | <tomsmeding> | oh wait no it's more general |
| 2021-05-31 16:15:32 | <tomsmeding> | bor0: am I at least kind of clear in what I mean when I say that f does or doesn't contain a reference to a variable? :p |
| 2021-05-31 16:17:14 | <tomsmeding> | in the example from that commit, you're descending under a binder that binds B, but the function f is basically (\expr -> rewrite B to A in expr) |
| 2021-05-31 16:17:41 | × | chddr quits (~Thunderbi@31.148.23.125) (Ping timeout: 264 seconds) |
| 2021-05-31 16:17:48 | <tomsmeding> | so f mentions the free B, but the binder now shadows that B, hence the wrong answer |
| 2021-05-31 16:18:14 | <bor0> | Yeah, right now `f` does not have any knowledge about variables. :) |
| 2021-05-31 16:18:23 | <bor0> | It's just getting blindly applied |
| 2021-05-31 16:19:29 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 2021-05-31 16:19:44 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2021-05-31 16:20:02 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 2021-05-31 16:20:09 | × | jess quits (~jess@libera/staff/jess) () |
| 2021-05-31 16:20:24 | → | jess joins (~jess@libera/staff/jess) |
| 2021-05-31 16:20:35 | → | o1lo01ol1o joins (~o1lo01ol1@cpe-74-72-45-166.nyc.res.rr.com) |
| 2021-05-31 16:21:50 | <tomsmeding> | I wonder how much of your code would still work if your applyFOLRule gets reduced to taking a variable name A, an expression F, and an expression E, where it replaces all free occurrences of A with F in E |
| 2021-05-31 16:22:18 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 2021-05-31 16:22:54 | <tomsmeding> | that's a well-understood function where you can easily check, when going under a binder for B in E, whether A=B (and if so, stop recursing), or if B is free in F (and if so, first rename the binder of B to a fresh variable, and then continue recursing) |
| 2021-05-31 16:23:01 | <tomsmeding> | that's capture-avoiding substitution |
| 2021-05-31 16:23:12 | <tomsmeding> | but it only works if you can inspect A and F |
| 2021-05-31 16:24:13 | <tomsmeding> | alternative: use "partial De Bruijn" indices, which is a name I just thought up |
| 2021-05-31 16:24:31 | <tomsmeding> | represent free variables like you do now, but use De Bruijn indices for all bound variables |
| 2021-05-31 16:24:43 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 265 seconds) |
| 2021-05-31 16:24:52 | <tomsmeding> | then you kind of automatically have to adhere to the Barendregt convention |
| 2021-05-31 16:25:08 | <bor0> | Hey! I was working on this example and just when I was about to paste it I saw that you are actually hosting the pastebin, lol! <3 |
| 2021-05-31 16:25:20 | coot | is now known as the-coot |
| 2021-05-31 16:25:30 | <tomsmeding> | working with De Bruijn indices does make some things quite a bit more difficult, but those are exactly the points where you should watch out with shadowing anyway :p |
| 2021-05-31 16:25:33 | <bor0> | https://paste.tomsmeding.com/2MU96uol this is an answer to "but then the output of 'f' (here ruleSymmetry) will still be a single equality, right?" |
| 2021-05-31 16:25:37 | <tomsmeding> | bor0: :) |
| 2021-05-31 16:26:51 | <bor0> | I am okay with even a simpler solution - don't do any variable replacement, just crash when the programmer tries to prove something using it |
| 2021-05-31 16:26:57 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 2021-05-31 16:27:17 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-31 16:27:22 | <tomsmeding> | but then you still have to detect the problem! |
| 2021-05-31 16:27:28 | <tomsmeding> | and you need the same things for that |
| 2021-05-31 16:27:43 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 272 seconds) |
| 2021-05-31 16:28:21 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 272 seconds) |
| 2021-05-31 16:29:04 | <tomsmeding> | bor0: ok right good example, you really use the generality of a full Haskell function |
| 2021-05-31 16:29:10 | <bor0> | I had similar problem with `ruleGeneralize`. The way I solved it was to accept a list of variables (in the premise): https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L219-L225 |
| 2021-05-31 16:29:37 | × | rahguzar quits (~rahguzar@212.189.140.214) (Ping timeout: 272 seconds) |
| 2021-05-31 16:29:38 | <bor0> | When we are not in a fantasy (within implication really) this is how we use it: https://github.com/bor0/hoare-imp/blob/fdb70a94a7e49ddff4e12c4096996f9c619a204c/examples/ExampleTNT2.hs#L118. When we are in a fantasy, we have to pass the premise `(Just premise)`. https://github.com/bor0/hoare-imp/blob/fdb70a94a7e49ddff4e12c4096996f9c619a204c/examples/ExampleTNT2.hs#L129 |
| 2021-05-31 16:30:11 | <ski> | (why the `fromRight's in the example ?) |
| 2021-05-31 16:30:42 | × | nschoe quits (~quassel@2a04:cec0:118b:9ec7:c878:346:7ebb:d0f1) (Remote host closed the connection) |
| 2021-05-31 16:30:58 | <bor0> | It's a dirty hack to avoid nested `whenRight`s https://github.com/bor0/hoare-imp/blob/master/src/Common.hs#L6-L12 |
| 2021-05-31 16:31:56 | → | nschoe joins (~quassel@2a04:cec0:118b:9ec7:45a:fcee:e159:4f31) |
| 2021-05-31 16:32:21 | <tomsmeding> | I'm not sure how to solve your problem in a nice way tbh; what I would do, probably, is encode the axioms of my logic in a data type instead of Haskell functions, and work with that |
| 2021-05-31 16:32:32 | <tomsmeding> | hence ensuring you can always inspect everything |
All times are in UTC.