On 23 Nov 2022, at 15:40, Jakob Wuhrer <xxxxxx@gmail.com> wrote:

> Hi,
>
> Daphne Preston-Kendal <xxxxxx@nonceword.org> writes:
>> On 19 Nov 2022, at 01:35, Shiro Kawai <xxxxxx@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