Weak Functional Dependencies in Higher-Order Datamodels

We present an axiomatisation for weak functional dependencies, i.e. disjunctions of functional dependencies, in the presence of several constructors for complex values. These constructors are the tuple constructor, the set-constructor, an optionality constructor, and a union constructor. The theory is smooth and rather uniform, if the union-constructor is absent. Its presence, however, complicates all results and proofs significantly. The reason for this is that the union-constructor comes alomg with non-trivial restructuring rules. In particular, if the union-constructor is absent, a subset of the rules is complete for the implication of ordinary functional dependencies, but this does not hold, if the union constructor is present.