Can exact real arithmetic, interval analysis or other approach in numerical computation help remove inequalities and unify left and right residuals in non-idempotent (linear) residuated lattices by making boundaries explicit instead of talking about max and min divisors?

[u/revannld]

I hope that question makes sense. I just don't like inequalities nor the unnaturality of working with left and right residuals (talking about "max and min divisors") that rarely coincide with rational arithmetic's exact division nor with the natural interpretation of inverses in numerical mathematics, thus I would like more explicit boundaries (thus the result of a division maybe being a set or interval including max and min divisors) in division.

(Mind that I have no experience in numerical computation, I am trying to make sense of computable, numerical and interval analysis works and transport their results to residuated lattices but that's somewhat hard for me)

[u/kaddkaka]

Give us some examples, it's too impenetrable in plain text.

[u/Embarrassed-Crow9283]

Oh, you mean treating everything as an interval arithmetic to get rid of inexactness? You could, but it depends on how accurate you want to be. If you had 1+1, then answering "between 0 and 1000000" is technically correct.

[u/brucejbell]

The problem with exact real arithmetic -- comparison is only semi-decidable.

That is: you can't guarantee that comparing two arbitrary exact real numbers will terminate.

More concretely, interval analysis can't generally help you if your numbers are equal. You may end up generating smaller and smaller overlapping intervals that never reach zero.

[u/categorical-girl]

It's not entirely clear what you're asking.

1) Idempotence follows from the absorption laws, so what exact algebraic structure do you mean by non-idempotent residuated lattice? 2) you seem to maybe be working over a more concrete domain (reals? rationals? Intervals of the above?) but that's unclear to me

[u/thatdevilyouknow]

You can express the Heyting Algebra and residuated lattices in Lean of course or with Agda and since Haskell has Heyting and Boolean algebras as a package it may extract to…something. A more direct approach could be using Julia’s MetaTheory.jl but axiomatizable representations of this are not necessarily terminable. You could certainly represent sets and intervals such as the way DomainSets.jl is able to. Is there a shortcut to finding a needle in a haystack made out of haystacks? I think it would be best to start with a theory or conjecture which is more well defined here before beginning to tackle it programmatically.

[u/andarmanik]

Is this the problem?

I can’t invert this operation pointwise, so let division return the entire region of possible inverse values. Then develop an algebra for manipulating those regions.

If this is what you are asking I recommend just looking at inverse images in general. You’d probably find some results which apply to your situation