Logs: liberachat/#haskell
| 2021-05-31 15:02:12 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-05-31 15:02:14 | cheater1__ | is now known as cheater |
| 2021-05-31 15:02:16 | <jmcarthur> | Maybe even negative reals if that happens to work out nicely, but it's not a requirement. |
| 2021-05-31 15:02:39 | × | Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-05-31 15:05:05 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 2021-05-31 15:06:07 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) |
| 2021-05-31 15:06:56 | → | aditya joins (~aditya@106.212.79.20) |
| 2021-05-31 15:06:58 | → | Shaeto joins (~Shaeto@94.25.234.55) |
| 2021-05-31 15:08:12 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 2021-05-31 15:09:40 | × | nschoe quits (~quassel@178.251.84.79) (Remote host closed the connection) |
| 2021-05-31 15:09:55 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 2021-05-31 15:11:06 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:7549:f26f:981e:10ae) (Ping timeout: 264 seconds) |
| 2021-05-31 15:12:54 | → | nschoe joins (~quassel@178.251.84.79) |
| 2021-05-31 15:12:59 | → | chomwitt joins (~Pitsikoko@athedsl-20549.home.otenet.gr) |
| 2021-05-31 15:13:52 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 2021-05-31 15:14:17 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-31 15:16:16 | × | Shaeto quits (~Shaeto@94.25.234.55) (Quit: WeeChat 3.1) |
| 2021-05-31 15:16:35 | → | atwm joins (~andrew@178.197.235.239) |
| 2021-05-31 15:18:33 | × | sh9 quits (~sh9@softbank060116136158.bbtec.net) (Quit: WeeChat 3.0.1) |
| 2021-05-31 15:21:48 | × | nschoe quits (~quassel@178.251.84.79) (Ping timeout: 244 seconds) |
| 2021-05-31 15:22:35 | → | nschoe joins (~quassel@178.251.84.79) |
| 2021-05-31 15:23:12 | × | aditya quits (~aditya@106.212.79.20) (Read error: Connection reset by peer) |
| 2021-05-31 15:23:15 | <jmcarthur> | I think this stackoverflow question is basically about what I'm looking for https://mathoverflow.net/questions/208412/what-are-some-examples-of-non-commutative-mathbbq-monoids-and-or-mathbbr |
| 2021-05-31 15:23:44 | → | Shaeto joins (~Shaeto@94.25.234.55) |
| 2021-05-31 15:24:59 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-05-31 15:25:56 | → | lbseale_ joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 2021-05-31 15:26:19 | <opqdonut> | mmmmh... mathbbq |
| 2021-05-31 15:26:41 | × | dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 264 seconds) |
| 2021-05-31 15:27:01 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 2021-05-31 15:27:46 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 15:27:51 | × | atwm quits (~andrew@178.197.235.239) (Quit: WeeChat 3.1) |
| 2021-05-31 15:28:49 | × | sifu quits (~marek@219.244.200.146.dyn.plus.net) (Remote host closed the connection) |
| 2021-05-31 15:29:06 | × | lbseale quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Ping timeout: 264 seconds) |
| 2021-05-31 15:29:31 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-05-31 15:30:35 | × | argento quits (~argent0@168.227.96.53) (Ping timeout: 265 seconds) |
| 2021-05-31 15:31:01 | → | xkapastel joins (uid17782@id-17782.tinside.irccloud.com) |
| 2021-05-31 15:31:34 | × | brandonh quits (~brandonh@151.38.202.252) (Quit: brandonh) |
| 2021-05-31 15:32:05 | × | nschoe quits (~quassel@178.251.84.79) (Ping timeout: 264 seconds) |
| 2021-05-31 15:32:15 | → | nschoe joins (~quassel@2a04:cec0:118b:9ec7:c878:346:7ebb:d0f1) |
| 2021-05-31 15:32:40 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 2021-05-31 15:32:51 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 268 seconds) |
| 2021-05-31 15:33:26 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 2021-05-31 15:33:46 | → | pe200012_ joins (~pe200012@120.236.162.14) |
| 2021-05-31 15:33:46 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:7d39:eb90:ba7d:df66) (Ping timeout: 264 seconds) |
| 2021-05-31 15:33:54 | × | pe200012 quits (~pe200012@218.107.17.245) (Ping timeout: 264 seconds) |
| 2021-05-31 15:35:11 | → | imdoor joins (~imdoor@balticom-142-78-50.balticom.lv) |
| 2021-05-31 15:35:12 | × | rahguzar quits (~rahguzar@212.189.140.214) (Quit: Connection closed) |
| 2021-05-31 15:35:18 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-05-31 15:35:35 | → | rahguzar joins (~rahguzar@212.189.140.214) |
| 2021-05-31 15:36:18 | → | lbseale joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 2021-05-31 15:36:33 | × | lbseale_ quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Ping timeout: 268 seconds) |
| 2021-05-31 15:39:54 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 264 seconds) |
| 2021-05-31 15:40:28 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 15:41:20 | × | boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Quit: Gorn... bye...) |
| 2021-05-31 15:41:29 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 268 seconds) |
| 2021-05-31 15:41:54 | → | chddr joins (~Thunderbi@31.148.23.125) |
| 2021-05-31 15:42:21 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 2021-05-31 15:44:10 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 2021-05-31 15:44:14 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) |
| 2021-05-31 15:44:33 | × | poljar1 quits (~poljar@78-2-43-255.adsl.net.t-com.hr) (Remote host closed the connection) |
| 2021-05-31 15:44:48 | → | bor0 joins (~boro@77.28.64.72) |
| 2021-05-31 15:44:57 | → | poljar1 joins (~poljar@78-2-43-255.adsl.net.t-com.hr) |
| 2021-05-31 15:45:18 | × | sondre quits (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) (Ping timeout: 264 seconds) |
| 2021-05-31 15:45:29 | × | imdoor quits (~imdoor@balticom-142-78-50.balticom.lv) (Quit: imdoor) |
| 2021-05-31 15:48:17 | → | boioioing joins (~boioioing@cpe-76-84-141-127.neb.res.rr.com) |
| 2021-05-31 15:48:47 | <bor0> | Hi. I have a sort of mathematical question, but it has to do with my implementation of a number theory in Haskell. Suppose we have a formula `A = B` and a rule that converts `x = y` to `S x = S y`. Now, applying this rule to `A = B` makes sense, we get as output `S A = S B`. But, what about applying rules to subformulas? Are there any restrictions? E.g. applying `S x = S y` to `A = B` within `A = B /\ C = D`. My system is currently broken in that it can convert |
| 2021-05-31 15:48:47 | <bor0> | a formula from `A=B /\ Exists B:(B=C)` to `A=B /\ B=C`, so likely I'm missing some restriction around bound variables or something. Happy to elaborate further on the question! |
| 2021-05-31 15:49:05 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:3866:f955:de69:46b2) (Ping timeout: 272 seconds) |
| 2021-05-31 15:49:51 | × | rahguzar quits (~rahguzar@212.189.140.214) (Quit: Connection closed) |
| 2021-05-31 15:49:59 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-05-31 15:50:14 | <river> | > what about applying rules to subformulas? Are there any restrictions? |
| 2021-05-31 15:50:15 | <lambdabot> | <hint>:1:70: error: |
| 2021-05-31 15:50:15 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
| 2021-05-31 15:50:31 | → | rahguzar joins (~rahguzar@212.189.140.214) |
| 2021-05-31 15:50:34 | × | Shaeto quits (~Shaeto@94.25.234.55) (Quit: WeeChat 3.1) |
| 2021-05-31 15:50:39 | <river> | a subformula can be defined as a context with a hole |
| 2021-05-31 15:50:54 | <river> | and if x = y then C[x] = C[y] |
| 2021-05-31 15:51:01 | <river> | so you can rewrite in subformulas |
| 2021-05-31 15:51:18 | → | Shaeto joins (~Shaeto@94.25.234.55) |
| 2021-05-31 15:51:40 | <tomsmeding> | are you asking how to do rewriting in general in terms with bound variables? |
| 2021-05-31 15:51:46 | <bor0> | Yes! |
| 2021-05-31 15:51:56 | <tomsmeding> | anything more specific would require knowledge about how you're representing things :p |
| 2021-05-31 15:52:03 | <ski> | yes |
| 2021-05-31 15:52:18 | <tomsmeding> | is this perhaps a case where you want capture-avoiding substitution? (that might be a good web-search term) |
| 2021-05-31 15:52:51 | <bor0> | It's all in https://github.com/bor0/hoare-imp/blob/master/src, though I don't expect anyone to go through the 500 LoC to just answer my question :) |
| 2021-05-31 15:52:55 | <tomsmeding> | i.e. if you're substituting a variable x with an expression E, then you are not allowed to substitute under a binder that binds x |
| 2021-05-31 15:53:00 | <ski> | bor0 : how is it elimianting the existential, in that example ? |
| 2021-05-31 15:53:43 | <bor0> | Hey ski! Basically it's the Path traversal function, if you recall. Right now it just ignores quantifiers https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L66-L67 and I am sure that's the error |
| 2021-05-31 15:54:02 | → | sondre joins (~sondrelun@eduroam-193-157-203-145.wlan.uio.no) |
| 2021-05-31 15:54:36 | <bor0> | Thanks, tomsmeding. That's helpful, I'll dig more into that |
| 2021-05-31 15:54:40 | <tomsmeding> | what does FOL stand for? |
| 2021-05-31 15:54:49 | <bor0> | "First-Order Logic" |
| 2021-05-31 15:54:58 | <tomsmeding> | oh right |
| 2021-05-31 15:54:59 | <ski> | you could have a rule that says that if `phi0' implies `phi1', and `psi0' implies `psi1', then `phi0 /\ psi0' implies `phi1 /\ psi1' |
| 2021-05-31 15:55:33 | <ski> | (and ditto for other connectives) |
| 2021-05-31 15:56:33 | <bor0> | So from GEB there was this restriction which kinda patched another similar issue - https://github.com/bor0/hoare-imp/blob/master/src/TNT.hs#L219. This is why I'm suspecting around bound variables. What you suggested might work, though it'd probably require a bigger refactor.. |
| 2021-05-31 15:57:14 | × | boioioing quits (~boioioing@cpe-76-84-141-127.neb.res.rr.com) (Quit: Gorn... bye...) |
| 2021-05-31 15:57:52 | → | ku joins (~ku@2601:280:c780:7ea0:a15d:a611:c59d:5265) |
| 2021-05-31 15:57:59 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-31 15:58:04 | <tomsmeding> | bor0: can you give an example call of that function applyFOLRule that goes wrong? |
All times are in UTC.