Function converse

Source
pub fn converse<K: ArrayKind>(
    r: &IndexedCoproduct<K, FiniteFunction<K>>,
) -> IndexedCoproduct<K, FiniteFunction<K>>
where K::Type<K::I>: NaturalArray<K>,
Expand description

Compute the converse of an IndexedCoproduct thought of as a “multirelation”.

An IndexedCoproduct c : Σ_{x ∈ X} s(x) → Q can equivalently be thought of as c : X → Q*, i.e. a mapping from X to finite lists of elements in Q.

Such a list defines a (multi-)relation as the multiset of pairs

R = { ( x, f(x)_i ) | x ∈ X, i ∈ len(f(x)) }

This function computes the converse of that relation as an indexed coproduct converse(c) : Q → X*, or more precisely converse(c) : Σ_{q ∈ Q} s(q) → X.

NOTE: An indexed coproduct does not uniquely represent a ‘multirelation’, since order of the elements matters. The result of this function is only unique up to permutation of the sublists.