3 ms·

the empty bunch (unit for `,`) is usually[0] spelled null. I don't recall that Hehner goes as far as topology (his bunches behave in a boolean manner, so the e

the empty bunch (unit for `,`) is usually[0] spelled null. I don't recall that Hehner goes as far as topology (his bunches behave in a boolean manner, so the elementary bunches must all be clopen; going beyond his windowless[1] functions was my inspiration for attempting Junk) so he doesn't have any affordance for open/closed. [0] 名可名也，非一名也。I sometimes wonder why Dijkstra footnoted that if it were allowed in his guarded command notation, nullary if fi would be abort and do od, skip — but it's not allowed. It can't be a desire for uniqueness, because there are too many other different ways to write abort and skip. (although it would have been convenient were it to have been possible to syntactically distinguish skip from arbitrary code) [1] after spending years on Junk, I can very well appreciate why, even if he'd thought further, he chose to stop where he did for the book. That said, every few years he seems to manage to narrow the difference between lists and contiguous N->element functions a little more. (and at the moment I am not convinced that it's possible to make more than a pragmatic decision to declare a particular partial order to be the <= at a given datatype, but I am convinced that it's helpful to declare the existence of a [clerical] total order over all datatypes — which leads to annoying subtleties with equality)

gsf_emergency 2y ago
Thanks. It just felt like being unable to spell out the empty bunch should be as interesting as the nonexistence of bunches o' bunches. I've heard from the students of RLC that quotient types are potentially useful** so should I wait to find out from you when those subtleties turn out to be less annoying or schlep on my current path till I bump up against bumpkin-type*-related annoyances not entirely of my own making ? *Sum & product types,I'm either always told not to worry about them, or be asked to pay attention in a way that I think I probably shouldn't ** itswise.. for bits-schlepping often end up needing more marketing than it's worth, imex
- 082349872349872 2y ago
  Re: quotient types, I believe so, even bitswise... but it's exactly the projection forgetting all that stuff that's in the same class as zero that's easier mathematically than computationally. (guess I should see what Lean does here) incidentally, rummaging by way of Hagino and Charity leads to Burstall87: http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-LFCS-87-25.pdf http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-L... (what Burstall has written as ind case is what we'd currently call fold) in particular, 5. Equational data types (cut down by eq's <== quotients) which has the interesting observation: > Notice that the initial algebra gives rise to an induction principle and to use this we have to invent a suitable predicate to prove by induction. This comes from the 'no junk' property of the initial algebra. The 'no confusion' property gives rise to inequations, and here to do proofs we have to invent a suitable discriminant function. There is some pleasant feeling of duality here.
  - gsf_emergency 2y ago
    So there's already pleasance?? Sorry, can't add anything substantive, but the following might save some time? https://proofassistants.stackexchange.com/questions/908/what-exactly-is-setoid-hell/927#927 https://proofassistants.stackexchange.com/questions/908/what... https://eprints.illc.uva.nl/id/document/12673 https://eprints.illc.uva.nl/id/document/12673
    - 082349872349872 2y ago
      many thanks! "Observational Equality: Now for Good" led me to "Observational Equality, Now!" which is a little easier for the layman to read without developing a headache: "Observational Equality: Ow!"
      - gsf_emergency 2y ago
        Heh I'm surprised (as in your fencing related dicta) that you got back on the trail.. what was the link chain?? Edit: if I told you this was the most layman paper I could find on my secondary (mostly killer-mode) ikigai, could you maybe deduce what the problem statement (aka MVP, to use some old country lingo) is, and even find a more appropriate paper for a layman? https://ems.press/content/serial-article-files/48098 https://ems.press/content/serial-article-files/48098
        082349872349872 2y ago
        hmm. I'd remembered it was short (3 hops?) from 42470111 but now I'm not seeing how I first got to TT^Obs from either of those starting points... cubic diracs are well out of my ken — even normal square ones are. are casimir elements and spins somewhere in the correct general direction? (otherwise the cubic doesn't make sense to me, as I don't think jerk normally enters physically motivated diffy-qs?)
        gsf_emergency 2y ago
        If by spins you mean Cliff(Lie) then you got the 2 swords* I'm quite intrigued that enwiki hasn't vibed about that, but it has produced a lagniappe: P81 The shaggy steed of physics: mathematical beauty in the physical world Casimir elements, heh, it's why my Erdos number is lower than expected.. * or is it a pitchfork? also vibing currently that the hypernormal distrust models that appear simpler than their own, while the weird have the opposite inclination. Holding in mind that dynamic between YeGoblyneQueene & g***n as a fine example of the ur academic conflict which I believe Taleb was trying to direct attention to

gsf_emergency 2y ago

Thanks. It just felt like being unable to spell out the empty bunch should be as interesting as the nonexistence of bunches o' bunches. I've heard from the students of RLC that quotient types are potentially useful** so should I wait to find out from you when those subtleties turn out to be less annoying or schlep on my current path till I bump up against bumpkin-type*-related annoyances not entirely of my own making ? *Sum & product types,I'm either always told not to worry about them, or be asked to pay attention in a way that I think I probably shouldn't ** itswise.. for bits-schlepping often end up needing more marketing than it's worth, imex

082349872349872 2y ago
Re: quotient types, I believe so, even bitswise... but it's exactly the projection forgetting all that stuff that's in the same class as zero that's easier mathematically than computationally. (guess I should see what Lean does here) incidentally, rummaging by way of Hagino and Charity leads to Burstall87: http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-LFCS-87-25.pdf http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-L... (what Burstall has written as ind case is what we'd currently call fold) in particular, 5. Equational data types (cut down by eq's <== quotients) which has the interesting observation: > Notice that the initial algebra gives rise to an induction principle and to use this we have to invent a suitable predicate to prove by induction. This comes from the 'no junk' property of the initial algebra. The 'no confusion' property gives rise to inequations, and here to do proofs we have to invent a suitable discriminant function. There is some pleasant feeling of duality here.
- gsf_emergency 2y ago
  So there's already pleasance?? Sorry, can't add anything substantive, but the following might save some time? https://proofassistants.stackexchange.com/questions/908/what-exactly-is-setoid-hell/927#927 https://proofassistants.stackexchange.com/questions/908/what... https://eprints.illc.uva.nl/id/document/12673 https://eprints.illc.uva.nl/id/document/12673
  - 082349872349872 2y ago
    many thanks! "Observational Equality: Now for Good" led me to "Observational Equality, Now!" which is a little easier for the layman to read without developing a headache: "Observational Equality: Ow!"
    - gsf_emergency 2y ago
      Heh I'm surprised (as in your fencing related dicta) that you got back on the trail.. what was the link chain?? Edit: if I told you this was the most layman paper I could find on my secondary (mostly killer-mode) ikigai, could you maybe deduce what the problem statement (aka MVP, to use some old country lingo) is, and even find a more appropriate paper for a layman? https://ems.press/content/serial-article-files/48098 https://ems.press/content/serial-article-files/48098
      - 082349872349872 2y ago
        hmm. I'd remembered it was short (3 hops?) from 42470111 but now I'm not seeing how I first got to TT^Obs from either of those starting points... cubic diracs are well out of my ken — even normal square ones are. are casimir elements and spins somewhere in the correct general direction? (otherwise the cubic doesn't make sense to me, as I don't think jerk normally enters physically motivated diffy-qs?)
        gsf_emergency 2y ago
        If by spins you mean Cliff(Lie) then you got the 2 swords* I'm quite intrigued that enwiki hasn't vibed about that, but it has produced a lagniappe: P81 The shaggy steed of physics: mathematical beauty in the physical world Casimir elements, heh, it's why my Erdos number is lower than expected.. * or is it a pitchfork? also vibing currently that the hypernormal distrust models that appear simpler than their own, while the weird have the opposite inclination. Holding in mind that dynamic between YeGoblyneQueene & g***n as a fine example of the ur academic conflict which I believe Taleb was trying to direct attention to