Looking for a mathy term/theory: invertible operator, functional dependency
We say a function is 'invertible' if given its result we can derive the argument. The corresponding binary relation is 'injective'.
What's the terminology/theory for an operation of two arguments/a ternary relation such that given its result and one of the arguments we can derive the other? For example Addition: given the sum and one addend, we can infer the other.
This is kinda in the same ball park as Functional Dependencies: Appendix A's relation PLUS could have 3 FD's: {X, Y} -> {Z}, {X, Z} -> {Y}, {Y, Z} -> {X}. But I'm more thinking a situation where there's an algorithm to get from left to right across the arrow. Database FD's are not in general algorithmic: given SNO, PNO in relation SP, there's no algorithm to calculate Qty, we just have to go look it up. (Also the answer might be different at different times in the life of the database.)
And database FD's are not in general injective-like in the sense I'm looking for: a given SNO, Qty doesn't determine PNO.
For example, in a Boolean (actually, Heyting) algebra the implication is the right adjoint to meet (p 15-16) In an ordered ring, the division is adjoint to multiplication.
I have made some progress in that field since out last exchange. In database theory relational division (AKA set join) is adjoined to natural join. What kind of relational division? There are several versions, which are closely related to the concept of generalized quantifiers in logic. Set join partitions input relations into disjoint sets of tuples, and partitioning is exactly what is needed to express functional dependency.
From the set join perspective to express functional dependency we need either "no more than one", or "exactly one" quantifier. And here is the formal algebraic definition:
r < ((R00 ^ (y /1 x)) v r) /1 ((y^R00) v r) <-> FD(r,x,y).
I have found it via computerized expression search in QBQL, but on afterthought its validity is obvious. The expression
(R00 ^ (y /1 x)) v r
is projection of r onto the attribute set which is the symmetric difference of the x and y. Any other set join operation here would suffice. Next,
(y^R00) v r
is the projection of r onto y. Then, the final "exactly one" set join is comparing the result with the original relation. Here is a couple of examples illustrating this idea:
r=[p q r]
0 a 0
0 a 1
1 c 0
1 c 1
2 a 0
;
Here FD(r,[p],[q]) is valid, but FD(r,[q],[p]) is not. Consider the first case:
x = [p];
y = [q];
Then,
(R00 ^ (y /1 x)) v r = [p q]
0 a
1 c
2 a
;
is the projection of r onto [p q]. Next:
(y^R00) v r = [q]
a
c
;
((R00 ^ (y /1 x)) v r) /1 ((y^R00) v r) = [p]
0
1
2
;
The partial lattice order (which by abuse of notation I denoted by irreflexive symbol) there holds.
On the other hand, take
x = [q];
y = [p];
(R00 ^ (y /1 x)) v r = [p q]
0 a
1 c
2 a
;
(y^R00) v r = [p]
0
1
2
;
((R00 ^ (y /1 x)) v r) /1 ((y^R00) v r) = [q]
c
;
The partial order there fails, as expected.
P.S. I should have made a proper exposition of these ideas in a paper, but my axiomatization for the /1 operation is not complete yet.