Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 25 26 27 28 29 30 31 32 33 34 35 .. 5022
— 502,152 events total
2020-09-17 16:03:38 <carter> they are sortah matching pair eliminiators
2020-09-17 16:03:39 <ski> i have been pondering a pet example, converse of induction on naturals
2020-09-17 16:03:57 <carter> wait, PAR is the multiplicative one
2020-09-17 16:03:59 <carter> ddrr
2020-09-17 16:04:05 <carter> & is the mult product
2020-09-17 16:04:09 <carter> PAr is the XOR of proofs
2020-09-17 16:04:30 <ski> XOR ?
2020-09-17 16:04:40 <carter> yes
2020-09-17 16:04:47 <carter> multiplicative disjunction is constructive xor
2020-09-17 16:04:47 <ski> in which sense ?
2020-09-17 16:04:54 × gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 256 seconds)
2020-09-17 16:05:02 <carter> like a real number is zero XOR some signed nonzero distance from zero
2020-09-17 16:05:10 <carter> proving one rules out the other
2020-09-17 16:05:13 → Neuromancer joins (~Neuromanc@unaffiliated/neuromancer)
2020-09-17 16:05:15 <carter> or disproving one implies the other
2020-09-17 16:05:31 <carter> lets you be more explicit about mutally exclusive facts
2020-09-17 16:05:38 <carter> which IS COOL
2020-09-17 16:05:45 <ski> how about `x >= 0 \/ x =< 0', disproving one gives you information for proving the other ?
2020-09-17 16:05:48 <dumptruckman> Is it normal to have a data type with only a single value constructor or is there some better construct for this?
2020-09-17 16:05:58 <carter> ski: :P
2020-09-17 16:06:01 <ski> or `p | a*b => p | a \/ p | b', `p' a prime
2020-09-17 16:06:19 <ski> (the usual proof starts with "Assume not `p | a'.")
2020-09-17 16:06:27 → gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net)
2020-09-17 16:06:41 <carter> ski i think your example isn't quite sound unless you have a != zero assumption
2020-09-17 16:06:42 <dumptruckman> Once again trying to use Haskell to better understand a problem in Java. However, I'm attempting to learn more about the type system this time.
2020-09-17 16:06:49 <monochrom> But x>=0 together with x >= 0 \/ x =< 0 does not give you any information about x=<0
2020-09-17 16:07:16 <carter> though x > 0 | x <=0 does thave the onely one is true at the same time
2020-09-17 16:07:27 <carter> ski: you need to have something where the XOR of the propreties is true
2020-09-17 16:07:33 <carter> Never the ANd
2020-09-17 16:07:42 <carter> monochrom: how're you?
2020-09-17 16:07:44 <monochrom> dumptruckman: It is normal.
2020-09-17 16:07:55 <ski> dumptruckman : sometimes `newtype' is preferable
2020-09-17 16:08:22 <ski> carter : i don't see why
2020-09-17 16:08:36 <ski> carter : `a != zero', for the prime example ?
2020-09-17 16:09:07 <carter> ski: your lack of parens confused me
2020-09-17 16:09:09 <ski> monochrom : the idea was that refuting one would give you information about the other
2020-09-17 16:09:19 <carter> *proves the other*
2020-09-17 16:09:40 <carter> so par is actually a really good model for bijections
2020-09-17 16:09:53 <carter> because negation could just be producer/consumer polarity
2020-09-17 16:10:01 <carter> in certain models of the logic
2020-09-17 16:10:11 × urdh quits (~urdh@unaffiliated/urdh) (Ping timeout: 240 seconds)
2020-09-17 16:10:19 → heatsink joins (~heatsink@2600:1700:bef1:5e10:b0dc:6c54:247b:ece)
2020-09-17 16:11:08 <carter> (gcd(a,b)==1, AND `p' a prime AND p | a*b ) => (p | a) xor (p | b'),
2020-09-17 16:11:16 <carter> ski: tweaks it
2020-09-17 16:11:25 <carter> *fixed it
2020-09-17 16:11:33 <carter> that would you be the property using par
2020-09-17 16:11:40 <dolio> I think the `A ∨ B` version would probably not be linear.
2020-09-17 16:11:57 <dolio> You can only do that argument linearly with par.
2020-09-17 16:12:08 <carter> dolio: yeah, the formal modelling this way is still useful sans linearity
2020-09-17 16:12:19 <carter> linearity is just how you derive the logic and dualities first
2020-09-17 16:12:25 <carter> or at least thats my perspective
2020-09-17 16:12:26 <carter> idk
2020-09-17 16:12:27 <dolio> Because for additive disjunction you'd be dropping a proof in the case you don't need it.
2020-09-17 16:12:27 × aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Quit: Free ZNC ~ Powered by LunarBNC: https://LunarBNC.net)
2020-09-17 16:12:31 <carter> yup
2020-09-17 16:12:38 <carter> dolio: sum?
2020-09-17 16:12:42 <dolio> Right.
2020-09-17 16:12:45 → aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net)
2020-09-17 16:13:08 <carter> yeah,
2020-09-17 16:13:10 × aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Client Quit)
2020-09-17 16:13:17 <dolio> Also `P \par Q` has aspects where they "can't both be true".
2020-09-17 16:13:24 <carter> dolio: oh?
2020-09-17 16:13:31 <carter> i mean, yes
2020-09-17 16:13:34 <carter> err
2020-09-17 16:13:39 <carter> dolio: example / explaborate?
2020-09-17 16:13:47 <carter> have i been wrong for years, AGAIN :)
2020-09-17 16:14:03 → aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net)
2020-09-17 16:14:29 <carter> either way i'm happy to continue chatting about this with folks
2020-09-17 16:14:29 → urdh joins (~urdh@unaffiliated/urdh)
2020-09-17 16:14:29 <dolio> Well, that's what you'd expect from xor.
2020-09-17 16:14:33 <carter> oh yeah
2020-09-17 16:14:42 <ski> carter : yea .. except that one wants to be able to refer to primality, often, without having to make sure / know that the two factors are coprime
2020-09-17 16:14:45 <carter> if both are true or both are false, xor is fal
2020-09-17 16:14:52 × DavidEichmann quits (~david@43.240.198.146.dyn.plus.net) (Remote host closed the connection)
2020-09-17 16:15:00 → DavidEichmann joins (~david@43.240.198.146.dyn.plus.net)
2020-09-17 16:15:03 <carter> ski: absolutely, i'm just showing
2020-09-17 16:15:12 × aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Client Quit)
2020-09-17 16:15:22 → cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net)
2020-09-17 16:15:48 <carter> dolio: you mean that/
2020-09-17 16:15:55 <dolio> carter: I don't have examples because I'm still not good at thinking about par.
2020-09-17 16:16:00 <carter> dolio: i was presupposing you have a proof of a xor b
2020-09-17 16:16:12 <carter> dolio: you can def prove a xor b false
2020-09-17 16:16:17 <ski> carter : anyway, i'm not convinced it should model `xor' in some sense. (and i didn't follow the "so par is actually a really good model for bijections" bit, either)
2020-09-17 16:16:33 <carter> ski: depends on your model of it
2020-09-17 16:16:34 <dolio> Yeah, proving both would be a way to prove a xor b false.
2020-09-17 16:16:40 <carter> yup
2020-09-17 16:16:42 <carter> exactly
2020-09-17 16:16:50 <carter> or disproving both
2020-09-17 16:16:59 <carter> ski: i'm aboslutely happy to help explain more
2020-09-17 16:16:59 <ski> usually, with boolean logic, biimplication would be `xnor', not `xor'
2020-09-17 16:17:16 <ski> (maybe that's not what you meant by "bijections", though)
2020-09-17 16:17:23 <carter> ski: for the relational model, negation could just be the direction that info flows
2020-09-17 16:17:30 <carter> *for bijections
2020-09-17 16:17:37 <carter> not a consumes an a
2020-09-17 16:17:41 <carter> a produces an a
2020-09-17 16:18:03 <carter> i think of A `par` B as ==== (not a -> b) & (not b -> a)
2020-09-17 16:18:24 <ski> yes, but that image would admit overlap
2020-09-17 16:18:25 <carter> & === multiplicative conj where you *choose which* field you get
2020-09-17 16:18:40 <carter> all the session type falvored stuff dropps the symmetries
2020-09-17 16:18:44 <ski> that would be additive conj.
←Prev  Next→
Page 1 .. 25 26 27 28 29 30 31 32 33 34 35 .. 5022

All times are in UTC.