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

[Peter Wang]

On Fri, 10 May 2024 15:19:11 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> On 2024-05-10 14:45 +10:00 AEST, "Peter Wang" <novalazy at gmail.com> wrote:
> >> @@ -7828,6 +7828,12 @@ However, variables which are in the range of a functional dependency
> >>  need not appear in the signature,
> >>  since it is known that their bindings will be determined
> >>  from the bindings of the variables in the domain.
> >> + at c XXX What about a class with two fundeps: A -> B, and B -> A.
> >> + at c Both A and B are in the range of a fundep.
> >> + at c The above text seems to imply that it is ok for *neither* to appear
> >> + at c in the signature.
> >> + at c Should we replace "since it is known that their bindings will be determined"
> >> + at c with "provided that their bindings are determined"?
> >>  
> > 
> > How about:
> > 
> >     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 does not need appear in the signature *if* the variables
> >     in the domain of that functional dependency do appear in the
> >     signature.
> 
> I don't think that is quite right. Given functional dependencies
> A->B and B->C, it is ok for only A to appear in the signature.
> C does not have to appear there, even though B is not in the signature either,
> because B is nevertheless determined by a type var, A, that *is* in the
> signature.

You're right.

> 
> We need to avoid being both too strict (ruling out the chained application of
> more than one fundep, even though it is allowed, as with the {A->B, B->C} example
> above) and too loose (allowing circular reasoning of the form "assuming
> we know A, we can prove we know A", as with the {A->B, B->A} example
> in the original text). It is difficult to thread the needle between these two issues.
> I can't think of a way to do that using simple and short text, because I think
> that what we need to describe is forward chaining: starting with a given set of type vars
> from the signature, and adding to that set  by applying fundeps *whose domain
> is already in that set*.

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 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 :)

Peter