On 23 Nov 2022, at 15:40, Jakob Wuhrer <jakob.wuh...@gmail.com> wrote:
> Hi, > > Daphne Preston-Kendal <d...@nonceword.org> writes: >> On 19 Nov 2022, at 01:35, Shiro Kawai <shiro.ka...@gmail.com> wrote: >>> That part is resolved by the replies to my post. Sensible base cases can >>> be defined, and it makes sense to have them taking zero arguments. >> >> Can you formally define them and show that they are a correct base >> case, in the sense of being of null effect if appended to the end of >> another arguments list? I can observe how the sample implementation >> behaves (emergently) when given no comparator arguments, but I’m still >> far from certain that they’re correct in a compositional sense. > > I have made an attempt at providing a formal definition for a ``zero'' > comparator and a ``one'' comparator along with some rudimentary proofs > showing that they are neutral elements for ~make-sum-comparator~ and > ~make-product-comparator~, respectively. I've attached both a pdf > document and org source code for said document, containing some > definitions and proofs. Wow, thanks so much for this detailed analysis! The only problem (and it’s a real nitpick) is the hash function of comparator-one. Since it is implementation-defined how a product comparator combines the hash values of each of the comparators it is given, there’s no guarantee that 0 will truly be of null effect. Possible resolutions: 1. ignore the problem – the hash value will still be stable even if it isn’t guaranteed to be exactly same as a comparator without comparator-one mixed in 2. actually define how hash values in a product comparator are combined 3. simply require that a hash value of 0 from one of the comparators is ignored and has no effect on the output value Daphne
