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.

I'm not quite sure whether these conform to the emergent behavior of the
sample implementation, but I vaguely recall checking that this conforms
back in february of this year, when I sent my initial comments.

The document is a mishmash of mathematical conventions, scheme
conventions, and notation thought up on the spot.  I hope this does not
inhibit legibility too much.

Kind regards,
Jakob Wuhrer