Skip to content

[ draft ] add Galois connections and residuated lattices. #1760

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from

Conversation

sstucki
Copy link
Contributor

@sstucki sstucki commented May 3, 2022

This PR is not ready to be merged. I think the contents are useful, but there are some problems with the organization of the code (what goes into which module etc.) and I need some help/feedback to address these. In particular:

  1. I don't know where the definition and properties of Galois connections should go. They involve both relations/orders and (monotone) functions, so maybe Relation.Binary? If so, where exactly? For now, I put them under Function.

  2. Currently, the definition of Galois connection and their properties are in the same file. Following the rest of the stdlib, the properties should probably go into a separate file, but I'm not sure where (depends on point 1).

  3. There are definitions for (right-)residuated pomonoids and (right-)residuated semilattices. I put them all in the same file, in the Algebra.Ordered hierarchy, but maybe the semilattices should go into Relation.Binary.Lattice hierarchy?

  4. Residuated structures and bundles currently live in the same file. To be consistent with the library, these should be split, but I'm not sure where the resulting modules should live (depends on point 3).

  5. The definitions of the residuated structures are biased in several ways:

    • only right-residuated cases are covered explicitly, the left-residuated ones are represented by flipping the operation;
    • for the semilattices, only the join-version is covered, the meet-version is dual;
    • only the multiplication is assumed to be monotone, and only in its first argument, all other monotonicity properties can be derived.

    In theory, this is sufficient, but it may be nicer to have unbiased versions for symmetry. But I don't know how much symmetry is enough symmetry and where to put the biased versions, etc. (This all depends on points 3 and 4).

  6. Finally, there are properties of the residuated structures, in separate modules, but these may be in the wrong place too (depends on 3).

@MatthewDaggitt
Copy link
Contributor

@sstucki reviewing this PR has triggered a shift in my thinking about the design of the library. All of your questions result from there being no natural place to put this stuff. In #1763 I've just proposed creating a new top-level Order module which I think would solve all of these problems you've listed.

Given that, can we wait to see how the discussion around the proposal plays out?

@sstucki
Copy link
Contributor Author

sstucki commented May 5, 2022

Given that, can we wait to see how the discussion around the proposal plays out?

Absolutely. I am not in a rush with this one. I think the contents are useful, so I decided to share them, but I fully expect this one to require a lot of work and discussion before it can be merged (including work on loosely related issues). So please prioritize whatever else you deem useful.

@JacquesCarette
Copy link
Contributor

Good stuff! Also: all my comments are already preemptively raised in the PR description.

Opinions:

  1. I think Function is a horrible place for the definition of Galois connection. The new Order (if that comes to pass) would be way better.
  2. I have the same feeling about 'symmetry'. It's annoying to have to duplicate things, but I think it's even more annoying as a user to work with something that's biased "the wrong way" for one's application.

@jamesmckinna
Copy link
Contributor

Suggest taking this out of v2.0, at least until a resolution (how, exactly?) of #1763 ?

@MatthewDaggitt
Copy link
Contributor

Closing. See discussion #1759 for details.

@MatthewDaggitt MatthewDaggitt removed this from the v2.0 milestone Oct 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
addition library-design status: won't-merge Decided against merging the PR in.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants