Logs: freenode/#haskell
| 2021-05-02 16:13:33 | × | xelxebar quits (~xelxebar@gateway/tor-sasl/xelxebar) (Ping timeout: 240 seconds) |
| 2021-05-02 16:13:37 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 2021-05-02 16:13:44 | → | xelxebar_ joins (~xelxebar@gateway/tor-sasl/xelxebar) |
| 2021-05-02 16:13:46 | × | jgt quits (~jgt@85.105.142.226) (Ping timeout: 240 seconds) |
| 2021-05-02 16:16:04 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-05-02 16:16:21 | × | Pickchea quits (~private@unaffiliated/pickchea) (Ping timeout: 260 seconds) |
| 2021-05-02 16:16:39 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:a182:9232:ec83:3157) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-02 16:18:26 | → | bitmapper joins (uid464869@gateway/web/irccloud.com/x-knwieyhblwaofvow) |
| 2021-05-02 16:19:12 | → | nbloomf joins (~nbloomf@76.217.43.73) |
| 2021-05-02 16:20:10 | → | geekosaur joins (930099da@rrcs-147-0-153-218.central.biz.rr.com) |
| 2021-05-02 16:20:59 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 252 seconds) |
| 2021-05-02 16:21:08 | → | wonko7 joins (~wonko7@62.115.229.50) |
| 2021-05-02 16:21:49 | → | Athas joins (athas@2a01:7c8:aaac:1cf:744:f358:5346:deb7) |
| 2021-05-02 16:32:24 | → | juuandyy joins (~juuandyy@90.106.228.121) |
| 2021-05-02 16:32:28 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 2021-05-02 16:32:30 | → | asicia joins (~asdfasdfa@86.100.110.212) |
| 2021-05-02 16:34:06 | × | malumore quits (~malumore@151.62.120.164) (Ping timeout: 240 seconds) |
| 2021-05-02 16:36:04 | → | usr25 joins (~usr25@unaffiliated/usr25) |
| 2021-05-02 16:36:42 | <asicia> | Can someone explain this part: https://youtu.be/uykHCg2VUjc?t=1575 where he says that we can assume the induction hypothesis? He later uses that assumption to switch statements in the equality, but how is that proving anything? |
| 2021-05-02 16:40:02 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 2021-05-02 16:41:14 | → | jao joins (~jao@pdpc/supporter/professional/jao) |
| 2021-05-02 16:41:33 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-05-02 16:44:06 | × | DTZUZU_ quits (~DTZUZO@207.81.119.43) (Ping timeout: 240 seconds) |
| 2021-05-02 16:44:08 | → | jgt joins (~jgt@85.105.142.226) |
| 2021-05-02 16:45:23 | <monochrom> | Have you done induction proofs in other contexts? No difference here. |
| 2021-05-02 16:46:18 | → | NieDzejkob joins (~quassel@195.149.98.3) |
| 2021-05-02 16:47:22 | <monochrom> | And at that specific point, he is just starting the inductive case by carefully writing down what to prove in the inductive case. |
| 2021-05-02 16:48:06 | × | ddellacosta quits (~ddellacos@86.106.143.200) (Ping timeout: 240 seconds) |
| 2021-05-02 16:48:08 | <monochrom> | But the assumption is the equation before the ⇒. |
| 2021-05-02 16:48:35 | → | ADG1089 joins (~aditya@223.226.237.158) |
| 2021-05-02 16:48:56 | <asicia> | i have not done any induction proofs before, so i am a bit confused as to why can assume that hypothesis |
| 2021-05-02 16:49:52 | <asicia> | i kind of thought the base case should be used in the steps proving the inductive case |
| 2021-05-02 16:50:03 | → | constrixor joins (~chargen@D964062A.static.ziggozakelijk.nl) |
| 2021-05-02 16:50:46 | <pavonia> | Is there a Haskell type that discriminates between a positive and negative NaN? |
| 2021-05-02 16:53:08 | × | ADG1089 quits (~aditya@223.226.237.158) (Read error: Connection reset by peer) |
| 2021-05-02 16:53:43 | <monochrom> | I think the first 10 minutes is a rough sketch why induction is valid. |
| 2021-05-02 16:53:54 | <monochrom> | I mean I would give the same rough sketch too. |
| 2021-05-02 16:54:31 | <monochrom> | There is a way to rigorously prove that induction is valid, but it's pure math rather than programming. |
| 2021-05-02 16:56:10 | <asicia> | so by "we can assume" he means that it should be proven, but we will just skip that part for the sake of explaning the rough sketch? |
| 2021-05-02 16:56:29 | × | jgt quits (~jgt@85.105.142.226) (Ping timeout: 246 seconds) |
| 2021-05-02 16:56:45 | <monochrom> | Huh, which "we can assume"? |
| 2021-05-02 16:57:14 | <asicia> | the very first sentence |
| 2021-05-02 16:57:24 | <asicia> | in the link i provided |
| 2021-05-02 16:57:31 | <monochrom> | Then no. |
| 2021-05-02 16:57:32 | → | tvn joins (~tvn@217.146.82.202) |
| 2021-05-02 16:57:46 | <asicia> | so what is that assumption based on? |
| 2021-05-02 16:58:20 | <monochrom> | We can assume P(n). We can assume "add n Zero = n". |
| 2021-05-02 16:58:52 | <monochrom> | When proving "X ⇒ Y", we assume X and under it prove Y. |
| 2021-05-02 17:00:03 | <asicia> | but there is no statement with Zero in the inductive case proof |
| 2021-05-02 17:00:27 | <monochrom> | That's fine. |
| 2021-05-02 17:00:51 | <monochrom> | Not the job of the inductive case to worry about P(Zero). |
| 2021-05-02 17:01:37 | <monochrom> | How about this: |
| 2021-05-02 17:02:59 | <monochrom> | Are you mixing up eg "for every day D, (if I receive a gold coin on day D, then I will receive a gold coin on day D+1)" with "if (for every day D, I receive a gold coin on day D) then (for every day D, I will receive a gold coin on day D+1)"? |
| 2021-05-02 17:03:13 | <monochrom> | The inductive case is the former, not the latter. |
| 2021-05-02 17:03:35 | <monochrom> | The latter doesn't prove anything. |
| 2021-05-02 17:04:30 | <monochrom> | A child saved an injured bird. The bird turned out to be a fairy, and offered to grant two wishes to the child. |
| 2021-05-02 17:04:46 | <monochrom> | The child's 1st wish was "I wish to receive a gold coin today". |
| 2021-05-02 17:05:17 | <monochrom> | 2nd wish was "I wish that: for every day, if I receive a gold coin on that day, then I will receive a gold coin on the next day" |
| 2021-05-02 17:05:18 | × | landonf quits (landonf@mac68k.info) (Excess Flood) |
| 2021-05-02 17:05:37 | → | v01d4lph4 joins (~v01d4lph4@171.48.62.25) |
| 2021-05-02 17:05:45 | hackage | css-selectors 0.4.0.0 - Parsing, rendering and manipulating css selectors in Haskell. https://hackage.haskell.org/package/css-selectors-0.4.0.0 (wvanonsem90) |
| 2021-05-02 17:05:49 | <monochrom> | Why didn't the child simply use one wish to say "I wish to receive a gold coin everyday, starting from today"? |
| 2021-05-02 17:05:58 | → | Lowl3v3l joins (~Lowl3v3l@dslb-002-207-103-026.002.207.pools.vodafone-ip.de) |
| 2021-05-02 17:06:04 | <monochrom> | Because this is a fairy tale for induction. >:) |
| 2021-05-02 17:06:07 | → | landonf joins (landonf@mac68k.info) |
| 2021-05-02 17:06:33 | × | juliagoda quits (~juliagoda@2a02:a31a:e13a:eb00:758f:d455:b475:46e4) (Quit: Leaving) |
| 2021-05-02 17:08:31 | × | sw1nn quits (~sw1nn@2a00:23c7:622f:2c00:b279:c6ef:9497:e6fa) (Ping timeout: 260 seconds) |
| 2021-05-02 17:08:45 | → | ADG1089 joins (~aditya@223.226.237.158) |
| 2021-05-02 17:09:18 | <asicia> | i guess i will need to learn some more about induction, as it still confuses me why the proof does not step by step convert the left side of equation to the right side one |
| 2021-05-02 17:09:48 | <asicia> | but just takes a shortcut when the statements looks like the one in the hypothesis and switches the left side with the right side |
| 2021-05-02 17:10:25 | <monochrom> | That may be an entirely different issue. |
| 2021-05-02 17:12:33 | <hrnz> | pavonia: Double. |
| 2021-05-02 17:13:33 | <monochrom> | Huh, from 26:34 to 30:00 he was doing from left side to right side. |
| 2021-05-02 17:14:39 | <monochrom> | Except at the darkest minute, as usual, it is not clear how to do the hardest step unless you take hints from working backwards. |
| 2021-05-02 17:14:57 | → | mav1 joins (~mav@ip-88-152-11-191.hsi03.unitymediagroup.de) |
| 2021-05-02 17:16:08 | → | ddellacosta joins (~ddellacos@86.106.143.83) |
| 2021-05-02 17:16:43 | <asicia> | at 27:45~ he rebrackets the statement, but we are trying to prove that part, how can he use this in the proof? |
| 2021-05-02 17:17:12 | <DigitalKiwi> | that's the proof by induction part |
| 2021-05-02 17:17:14 | <monochrom> | That's using the induction hypothesis "add x (add x y) = add (add x y) z" |
| 2021-05-02 17:17:37 | <monochrom> | the "P(x)" |
| 2021-05-02 17:18:05 | <pavonia> | hrnz: And how do you create those values? |
| 2021-05-02 17:18:19 | <monochrom> | At this point, no one is trying to prove "add x (add x y) = add (add x y) z" |
| 2021-05-02 17:18:35 | <hrnz> | 0*(8/0) :: Double and 0*(-8/0) :: Double :> |
| 2021-05-02 17:18:39 | <monochrom> | Everyone is only trying to prove "add (Succ x) (add x y) = add (add (Succ x) y) z" |
| 2021-05-02 17:18:53 | <monochrom> | Remember the gold coins? |
| 2021-05-02 17:19:28 | <asicia> | but why is it legal to use that assumption in that step of the proof to rebracket the statement |
| 2021-05-02 17:19:31 | <monochrom> | No one is either assuming nor proving "every day I get a coin". |
| 2021-05-02 17:19:36 | × | ADG1089 quits (~aditya@223.226.237.158) (Quit: Konversation terminated!) |
| 2021-05-02 17:19:59 | <pavonia> | > (0*(8/0) :: Double, 0*(-8/0) :: Double) |
| 2021-05-02 17:20:01 | <lambdabot> | (NaN,NaN) |
| 2021-05-02 17:20:03 | <monochrom> | Everyone is just assuming "if on a particular day D, I get a coin", then what will happen on day D+1. |
| 2021-05-02 17:20:17 | × | ddellacosta quits (~ddellacos@86.106.143.83) (Ping timeout: 246 seconds) |
| 2021-05-02 17:20:35 | <pavonia> | > (0*(8/0) :: Double) == (0*(-8/0) :: Double) |
| 2021-05-02 17:20:35 | → | chimera joins (~chimera@168-182-134-95.pool.ukrtel.net) |
| 2021-05-02 17:20:37 | <lambdabot> | False |
| 2021-05-02 17:20:47 | <pavonia> | Awesome |
| 2021-05-02 17:20:49 | → | sw1nn joins (~sw1nn@2a00:23c7:622f:2c00:cbb9:38e5:9364:df1e) |
| 2021-05-02 17:21:15 | <monochrom> | Because the inductive case proves "for all x, (if P(x), then P(Succ x)" |
| 2021-05-02 17:22:13 | <monochrom> | So you begin with "Let an arbitrary x be given, it's an unknown to me, but it's called 'x'" |
| 2021-05-02 17:22:34 | <monochrom> | So now you need to prove "if P(x) then P(Succ x)" under that x. |
All times are in UTC.