Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unification structure #59

Open
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

herbelin
Copy link
Member

This CEP is about organizing knowledge about the (evarconv) unification algorithm of Coq in the hope to draw directions for the future.

It is a rather extensive first draft but at the same time a rather naive one. A lot should be done to make it even more comprehensive, collecting experiences and contributions of everyone.

Rendered here

A reflexive unification problem induces constraints on the possible definitions of `?e`: once `?e` is defined, it may generate new unification problems between terms of the instances that contain existential variables.

A reflexive unification problem can be simplified as follows:
- Variables of the context whose instances in the substitution are provably incompatible (e.g. because corresponding to distinct head normal forms) can be removed from the context.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This optimization seems unsound?
Consider x : nat |- ?e : nat and the pair of unification problems |- ?e@{x:=O} == ?e@{x:=S O} and x : nat |- ?e@{x:=x} == match x with O => O | S _ => O end. The only valid solution of this is ?e := match x with O => O | S _ => O end, which refers to x.
And in fact Coq fails to solve such a problem:

Check let e := (fun x => ?[e]) in
      eq_refl : (e O, e) = (e (S O), fun x => match x with O => O | S _ => O end).
(* Error:
In environment
e := fun _ : nat => ?e : nat -> nat
The term "eq_refl" has type "(e 0, e) = (e 0, e)" while it is expected to have type
 "(e 0, e) = (e 1, fun x : nat => match x with
                                  | 0 | _ => 0
                                  end)" (cannot instantiate "?e" because "x" is not in its scope).
*)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reported as coq/coq#15110

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're right, this should be distinct neutral, i.e. blocking on a variable, head normal forms. Current code is indeed wrong and should be modified.


A reflexive unification problem can be simplified as follows:
- Variables of the context whose instances in the substitution are provably incompatible (e.g. because corresponding to distinct head normal forms) can be removed from the context.
- If both instances are free of existential variables, the problem can be dropped since its resolution will eventually only create equations between convertible existential-variables-free terms.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I understand this one. Is conversion run again after unification completes? How do you get convertibility constraints? Also, this seems overly optimistic, consider x : nat |- ?e : nat and |- ?f : nat and the pair of unification problems |- ?e@{x:=O} == ?e@{x:=S O} and x : nat |- ?e@{x:=x} == match x with O => O | S _ => ?f end. We must instantiate ?e with match x with O => O | S _ => ?f end, and only after this substitution do we get |- O == ?f out of the first unification problem, which it seems would have been dropped according to this rule.

It seems that Coq can solve this problem, though?

Check let e := (fun x => ?[e]) in
      let f := ?[f] in
      eq_refl : (e, e O) = (fun x => match x with O => O | S _ => f end, e (S O)).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems I meant "If both instances are pointwise existential-variable-free compatible terms". So, with your previous remark, it should be "If both instances are pointwise existential-variable-free compatible neutral terms".

Your example works because e := fun x => match x with O => O is solved first. If you invert the order of unification problems:

Check let e := (fun x => ?[e]) in
      let f := ?[f] in
      eq_refl : (e O, e) = (e (S O), fun x => match x with O => O | S _ => f end).

it fails.

## Simplification of atomic unification problems

An atomic unification problem can be simplified as follows:
- Variables of the context of the existential variables that are bound to terms mentioning variables of the context of the equations in non-erasable position in only one of the two instances can be restricted since there would be no way to make these terms match a subterm of the instance of the other existential variables; otherwise said, both existential variables can be restricted on the (well-typed closure of the) subsets of their context which intersect.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does "non-erasable position" mean? What does "restricted" mean?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If I'm understanding correctly, this again seems incorrect for the same reason as above. We might have consider x : nat |- ?e : bool and x : nat |- ?e' : bool and the triple of unification problems x, y : nat |- ?e@{x:=S x} == ?e'@{x:=S y} and x : nat |- ?e@{x:=x} == match x with O => true | S _ => false end and x : nat |- ?e@{x:=x} == match x with O => true | S _ => false end. We must instantiate ?e and e' both with match x with O => true | S _ => false end.

Check let e := (fun x => ?[e]) in
      let e' := (fun x => ?[e']) in
      fun x y => eq_refl
                 : (e (S x), e, e') =
                   (e' (S y), (fun x => match x with O => true | S _ => false end),
                    (fun x => match x with O => true | S _ => false end)).
(* Error:
In environment
e := fun x : nat => match x with
                    | 0 => true
                    | S _ => false
                    end : nat -> bool
e' := fun _ : nat => false : nat -> bool
x : nat
y : nat
The term "eq_refl" has type "(e (S x), e, e') = (e (S x), e, e')" while it is expected to have type
 "(e (S x), e, e') =
  (e' (S y), fun x : nat => match x with
                            | 0 => true
                            | S _ => false
                            end, fun x : nat => match x with
                                                | 0 => true
                                                | S _ => false
                                                end)" (cannot unify "e'" and
"fun x : nat => match x with
                | 0 => true
                | S _ => false
                end").
*)

text/unification.md Outdated Show resolved Hide resolved
text/unification.md Outdated Show resolved Hide resolved
text/unification.md Outdated Show resolved Hide resolved
*Higher order pattern unification* (see Miller 1991 and Pfenning 1991) is a special case of simple unification problem when the substitution is made only of distinct variables. In this case, there is a single solution obtained by projecting the unique possible variable or imitating if not a variable.

Pattern unification has various refinements (see e.g. Libal and Miller 2016) such as:
- expecting distinct variables only among the variables that actually occur in the term to match
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that this can cause the pattern solution to be incorrect if there are other variables in the context which are assigned to terms which are headed by a constructor, because we may choose whether or not to match on them. (Consider x, y : bool |- ?e and x : bool |- ?e@{x:=x,y:=true} == x, we can solve this with either x or with if y then x else _, and the latter may be manded by a future unification problem.)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be formulated clearly. It is among the variables, so the presence of true makes that it is not a pattern (see the Option.List.map in Evarsolve.is_unification_pattern_evar; the restriction to actual dependencies in get_actual_deps comes after).


Pattern unification has various refinements (see e.g. Libal and Miller 2016) such as:
- expecting distinct variables only among the variables that actually occur in the term to match
- identifying arguments that are irrefutable patterns over variables at their leaves (e.g. `(x,(y,z))` with those variables (i.e. a form of curryfication) (see PR [#14798](https://github.com/coq/coq/pull/14798))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is only guaranteed to generate a good solution either (a) in the presence of eta conversion for the record type, or (b) when no subterm of the constructor tree, other than the leaves, occurs in the RHS. e.g., x, y, z |- ?e@{x:=(x,(y,z))} == (y,z) can be solved with either snd x or (fst (snd x), snd (snd x)).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right.

Comment on lines +114 to +115
- Second-order unification heuristics: e.g. to resolve `?P t =?= u` by selecting a number of occurrences of subterms unifiable to `t` in `u` (see `Evarconv.second_order_matching`). Such a heuristic is central to any form of reasoning by induction. As far as I can recap, it is currently used in Coq only for tactics.
- One issue is to recognize subterms: we can assume `t` free of existential variables and reason modulo convertibility, or we can reason using syntactic equality, or syntactic equality discarding non-essential, i.e. reinferable arguments (i.e., morally the implicit arguments).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this should be subsumed by introducing constructors of types with eta. That is, if we have ?P t =?= u, we can always instantiate ?P with fun x => ?Q, turning the application into a substitution. And if we have fst ?x =?= u (or match ?x with pair x y => Q end =?= u) and primitive projections / eta are turned on, it should always be safe to instantiate ?x with (?a, ?b) (though we probably want to run canonical structures first, and we maybe want to make sure that u doesn't reduce to something that structurally matches such a projection/match, because otherwise we may forget information that we want to remember for first-order heuristics)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I see this is mentioned below


- Second-order unification heuristics: e.g. to resolve `?P t =?= u` by selecting a number of occurrences of subterms unifiable to `t` in `u` (see `Evarconv.second_order_matching`). Such a heuristic is central to any form of reasoning by induction. As far as I can recap, it is currently used in Coq only for tactics.
- One issue is to recognize subterms: we can assume `t` free of existential variables and reason modulo convertibility, or we can reason using syntactic equality, or syntactic equality discarding non-essential, i.e. reinferable arguments (i.e., morally the implicit arguments).
- Another issue is that typing constraints induce equivalence classes of subterms that have to be abstracted altogether.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does this mean? Or what's an example?

- Systematically eta-reduce the solutions to existential variables (with all kinds of eta). On one side, this seems to be the natural expectation. On the other side, this would avoid caring about whether it might be dommageable to eta-expand this or that solution in the unification algorithm.
- Give an order between constants which would allow to predict which side to reduce in `E[c] =?= E'[c]`.
- Keep constants unfolding to fixpoints folded so as to concentrate on the essential and reduce the size of expressions, including in evaluation contexts (i.e. stacks).
- Do more aggressive restrictions of contexts (e.g. Sozeau and Ziliani seem to take the downwards well-typed closure of restrictions while Coq takes the upwards well-typed closure - knowing that taking the closure by dependency requires in theory to take care of erasable occurrences)?
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the difference between downwards and upwards here? (Or what's an example?)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By downwards I mean the largest well-formed context which exclude the forbidden variables. By upwards, I mean the smallest well-formed context which include the allowed variables.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmmm, it seems that upwards is more powerful unless we have reduced enough that no further occurrences of forbidden variables can be erased by reduction. Consider T : Type, f : T -> Type, x : T |- ?e : Type, and the pair of problems A, B : Type, f : bool -> Type, x : bool |- ?e@{T:=(fun _ => bool) A,f:=f,x:=x} == ?e@{T:=(fun _ => bool) B,f:=f,x:=x} and f : bool -> Type, x : bool |- ?e@{T:=bool,f:=f,x:=x} == f x. IIUC, upwards closure would keep T, while downwards would remove it? (Do you have an example not involving reduction where they differ where upwards closure does better than downwards closure?)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But maybe this is what you meant by "erasable"?

herbelin and others added 2 commits November 3, 2021 12:47
Co-authored-by: Jason Gross <jasongross9@gmail.com>
Co-authored-by: Jason Gross <jasongross9@gmail.com>
Copy link
Member Author

@herbelin herbelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot for the review! I'll answer the remaining questions when I'll have more time.

A reflexive unification problem induces constraints on the possible definitions of `?e`: once `?e` is defined, it may generate new unification problems between terms of the instances that contain existential variables.

A reflexive unification problem can be simplified as follows:
- Variables of the context whose instances in the substitution are provably incompatible (e.g. because corresponding to distinct head normal forms) can be removed from the context.
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're right, this should be distinct neutral, i.e. blocking on a variable, head normal forms. Current code is indeed wrong and should be modified.


A reflexive unification problem can be simplified as follows:
- Variables of the context whose instances in the substitution are provably incompatible (e.g. because corresponding to distinct head normal forms) can be removed from the context.
- If both instances are free of existential variables, the problem can be dropped since its resolution will eventually only create equations between convertible existential-variables-free terms.
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems I meant "If both instances are pointwise existential-variable-free compatible terms". So, with your previous remark, it should be "If both instances are pointwise existential-variable-free compatible neutral terms".

Your example works because e := fun x => match x with O => O is solved first. If you invert the order of unification problems:

Check let e := (fun x => ?[e]) in
      let f := ?[f] in
      eq_refl : (e O, e) = (e (S O), fun x => match x with O => O | S _ => f end).

it fails.

*Higher order pattern unification* (see Miller 1991 and Pfenning 1991) is a special case of simple unification problem when the substitution is made only of distinct variables. In this case, there is a single solution obtained by projecting the unique possible variable or imitating if not a variable.

Pattern unification has various refinements (see e.g. Libal and Miller 2016) such as:
- expecting distinct variables only among the variables that actually occur in the term to match
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be formulated clearly. It is among the variables, so the presence of true makes that it is not a pattern (see the Option.List.map in Evarsolve.is_unification_pattern_evar; the restriction to actual dependencies in get_actual_deps comes after).


Pattern unification has various refinements (see e.g. Libal and Miller 2016) such as:
- expecting distinct variables only among the variables that actually occur in the term to match
- identifying arguments that are irrefutable patterns over variables at their leaves (e.g. `(x,(y,z))` with those variables (i.e. a form of curryfication) (see PR [#14798](https://github.com/coq/coq/pull/14798))
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right.

- Systematically eta-reduce the solutions to existential variables (with all kinds of eta). On one side, this seems to be the natural expectation. On the other side, this would avoid caring about whether it might be dommageable to eta-expand this or that solution in the unification algorithm.
- Give an order between constants which would allow to predict which side to reduce in `E[c] =?= E'[c]`.
- Keep constants unfolding to fixpoints folded so as to concentrate on the essential and reduce the size of expressions, including in evaluation contexts (i.e. stacks).
- Do more aggressive restrictions of contexts (e.g. Sozeau and Ziliani seem to take the downwards well-typed closure of restrictions while Coq takes the upwards well-typed closure - knowing that taking the closure by dependency requires in theory to take care of erasable occurrences)?
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By downwards I mean the largest well-formed context which exclude the forbidden variables. By upwards, I mean the smallest well-formed context which include the allowed variables.

- Give an order between constants which would allow to predict which side to reduce in `E[c] =?= E'[c]`.
- Keep constants unfolding to fixpoints folded so as to concentrate on the essential and reduce the size of expressions, including in evaluation contexts (i.e. stacks).
- Do more aggressive restrictions of contexts (e.g. Sozeau and Ziliani seem to take the downwards well-typed closure of restrictions while Coq takes the upwards well-typed closure - knowing that taking the closure by dependency requires in theory to take care of erasable occurrences)?
- Filters need to be better understood: why not to directly restrict the context more often?
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a performance optimization?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants