[m-rev.] for post-commit review: check for terms containing distinct vars in one place

[Zoltan Somogyi]

On 2024-05-10 17:09 +10:00 AEST, "Peter Wang" <novalazy at gmail.com> wrote:
> I'll give it another go:
> 
>     Without any functional dependencies, all variables in constraints
>     must appear in the signature of the predicate or function being
>     declared.
>     However, a variable that appears in the range of a functional
>     dependency FD does not need to appear in the signature *if*
>     each variable in the domain of FD satisfies one of these conditions:
> 
>     - the variable in the domain of FD appears in the signature; or
> 
>     - the variable in the domain of FD appears in the range of a
>       functional dependency FD2, and the variables in the domain of FD2
>       in turn satisfy these conditions.

I think that's definitely better, but still not quite enough, because "satisfy these
conditions" is too vague, and can be read incorrectly as well as correctly.
The incorrect reading I am thinking of is the "A->B, B->A is ok" viewpoint.

I would preface your text with something along the lines of "There must exist
an ordering of the fundeps into FD1, FD2 etc such that ...."; and reword the above
*somehow* to get across the idea that for the domain of FDn, we can apply the
second rule *only* using fundeps FDm where m > n (or m < n, it does not matter
which way the numbers go, as long as they go in only one direction).

>> I thought we can describe things using dags, along the lines of
>> 
>> (1) every fundep with N type vars in its domain and M in its range defines N*M directed edges.
>> with each one pointing from a var in the domain to one in the range, and (2) every var that
>> is not in the signature must be reachable from the vars that are in the signature.
>> 
>> But I can't come up with a correctness argument for this description, because I have the
>> nagging feeling that treating a fundep such as P,Q->R as two *independent* edges,
>> P->R and Q->R, loses significant information. In reality, fundeps are not really
>> collections of edges, they are *hyperedges*. But if we use that terminology, we lose
>> at least 95% of our audience.
> 
> You've lost me :)

That is OK; I knew I would :-)

Zoltan.