32 ms·

Simplified but care-full application of notation: "no empty bunches"? And (,much less care-fully maybe a little machinationally,) what do you call the op that m

Simplified but care-full application of notation: "no empty bunches"? And (,much less care-fully maybe a little machinationally,) what do you call the op that maps bunches to open sets and sets to closed sets? 空即是合，束不可空 (expectedly trad) Somehow.. Hehner could be better rendered in Classical..

082349872349872 2y ago
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

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