Adds unary disjoint relation

[bsaul]

This PR adds the relation between two predicates expressing disjointness.

I am not at all wedded to the _#_ notation.

See the discussion on the Agda Zulip for more background.

[bsaul]

Before I fix the build errors (due to overloaded # symbol), I'll wait till we've settled on notation.

[jamesmckinna]

What about \perp/⊥ instead? (not \bot BTW, but indistinguishable in many fonts, alas...)

[bsaul]

That's Ok by me. That said, I already find some of the symbols used in Relation.Unary to be difficult to distinguish.

[JacquesCarette]

paging in @WolframKahl who might also have a suggestion.

[JacquesCarette]

Because \bot and \perp are so hard to distinguish, I'm not pro. I think using the same symbol as apartness makes sense.

[bsaul]

I just pushed a version using \perp, so folks can look at it.

[jamesmckinna]

Actually, at least in github, I find I can distinguish it from \bot.
FWIW, I think I'd rather have a distinct symbol than need to have hiding directives/qualified imports for the sake of reusing _#_...

[bsaul]

Another option is to be more verbose as in _IsDisjointFrom_.

[jamesmckinna]

Perhaps, 'ideally', use of a 'fat \perp' might be best, but I don't think we can shoehorn that into the agda-input-mode...?

[JacquesCarette]

that would be nice (fat perp)

[jamesmckinna]

(in lieu of my (now deleted) comment, I took the liberty of adding the link myself to your OP... hope that's OK)

[bsaul]

(I took the liberty of adding the link myself to your OP... hope that's OK)

Of course, thanks!

[jamesmckinna]

cf. #2594 ... Can you also add some properties of these relations? Or other extensions, eg.:

• prove Symmetric _⊥_, Symmetric _≬_
• lift _⊥_ to Relation.Binary.Definitions (and even: Relation.Nullary?), and redefine Irreflexive using it?
• redefine relational composition using _≬_? (there may be dependency issues in trying to do this; partly because of the Nullary/Unary/Binary distinction, and partly because neither of Unary nor Nullary split off distinct Definitions modules...)
• ...

All of these strictly go outside the scope of what you have so far, but might also give life to the new definitions.

You also alluded to how they are part of your basic toolkit when developing in Agda, so what's a specimen client application/deployment context which might also be generally useful as an addition to the library?

[bsaul]

Can you also add some properties of these relations?

Yes, will do. Those are good suggestions.

[bsaul]

You also alluded to how they are part of your basic toolkit when developing in Agda, so what's a specimen client application/deployment context which might also be generally useful as an addition to the library?

I'm working on formalizing parts probability/statistics/causal inference wherein disjoint "events" or sets are sometimes a precondition in a theorem, e.g. Pearl's definition of d-separation.

[jamesmckinna]

You also alluded to how they are part of your basic toolkit when developing in Agda, so what's a specimen client application/deployment context which might also be generally useful as an addition to the library?

I'm working on formalizing parts probability/statistics/causal inference wherein disjoint "events" or sets are sometimes a precondition in a theorem, e.g. Pearl's definition of d-separation.

Nice! But not sure quite how in scope (yet) that might be for stdlib. Still the two concepts introduced are familiar to me from constructive approaches to (the foundations of) probability, cf. eg. Jan van Plato's book from some years ago now...

[bsaul]

Nice! But not sure quite how in scope (yet) that might be for stdlib.

I wouldn't expect most of what I'm noodling on to be in scope for stdlib -- I'm just trying to upstream things that might be.

[bsaul]

cf. eg. Jan van Plato's book from some years ago now...

Thanks for the reference -- looks quite interesting.

[bsaul]

• prove Symmetric _⊥_, Symmetric _≬_

Done in f77d38b

[bsaul]

• lift _⊥_ to Relation.Binary.Definitions? and redefine Irreflexive using it?

Trying to import Relation.Unary into Relation.Binary.Defintions introduces a cyclic dependency, so I suspect there would be a bit of refactoring to make this happen.

[jamesmckinna]

Thanks very much for the PR, it looks in good shape for merging once the CHANGELOG is fixed.

I'm happy with \perp as the symbol, but I'll leave it to the other maintainers to rule on this.

[WolframKahl]

On Tue, Feb 25, 2025 at 05:20:24PM -0800, Jacques Carette wrote: that would be nice (fat perp)

Fat perp is apparently not on offer by Unicode, but see: https://www.fileformat.info/info/unicode/char/search.htm?q=perp&han=Y https://www.fileformat.info/info/unicode/char/search.htm?q=tack&han=Y

[jamesmckinna]

In favour of \perp:

• easy to type
• mildly distinct visually from \bot
• definitely distinct visually/lexically from _#_

In favour of _#_

• semantically it is an apartness
• ... what else?

Regarding @WolframKahl 's links to Unicode, I wonder if perhaps we should make every module preamble comment include the new (infix/mixfix) symbols introduced with their character encodings (emacs and Unicode?), as 'self-documentation', rather than trying to build a big lookup table in style-guide?

[JacquesCarette]

I wonder if perhaps we should make every module preamble comment include the new (infix/mixfix) symbols introduced with their character encodings (emacs and Unicode?), as 'self-documentation', rather than trying to build a big lookup table in style-guide?

That seems like a good idea.

[bsaul]

I wonder if perhaps we should make every module preamble comment include the new (infix/mixfix) symbols introduced with their character encodings (emacs and Unicode?), as 'self-documentation', rather than trying to build a big lookup table in style-guide?

That seems like a good idea.

Agreed.

[WolframKahl]

On Wed, Feb 26, 2025 at 03:58:22AM -0800, jamesmckinna wrote: In favour of `\perp`: * [...] * mildly distinct visually from `\bot`

With my current fonts, I can see that when they are side-by-side, but I wouldn't be able to distinguish individual occurrences. I'd therefore argue against using both symbols in Agda.

[jamesmckinna]

On Wed, Feb 26, 2025 at 03:58:22AM -0800, jamesmckinna wrote: In favour of \perp: * [...] * mildly distinct visually from \bot
With my current fonts, I can see that when they are side-by-side, but I wouldn't be able to distinguish individual occurrences. I'd therefore argue against using both symbols in Agda.

Hmm... that's a shame, I think. I'd maybe try to influence things further by adding

• \perp as a definition is lifting/proxying for the underlying appeal to \bot, so 'it makes sense' (?) to use cognate symbols
• plus any additional cognitive reinforcement arising from documenting the symbology sur place

But I'd better stop beating this particular donkey now.

[MatthewDaggitt]

I have no strong opinions on the choice of symbol. We use quite a lot of close cognates in the library already, but I can understand the urge not to add more.