We thank the referees for their useful comments and suggestions.
Reviews A, C, and D express concerns about the novelty of the work, and D specifically asks if the categorical semantics is novel. We believe our semantics is indeed novel: as review A notes, there are no prior extensions of the Rydeheard and Burstall proof to pattern unification. This is because none of the prior semantics for metavariables (eg, Hamana[1], Fiore and Hur[2], and Hsu et al[3]) are suitable for this purpose: they all permit interpreting general metavariables with full substitutions as arguments, rather than only pattern metavariables, which take only a disjoint set of variables as arguments. As a result, the "fatter" models lack the universal properties needed to generalise Rydeheard and Burstall's proof. Furthermore, the notion of signature we introduce is also novel, and is general enough to let us derive several unification algorithms not previously found in the literature, including pattern unification for terms in ordered logic. See our response to review D for more details.
Review D also expresses concern that our notion of arity is only a list of variables, and does not keep track of type information. Fortunately, this is not the case: as review A notes, our notion of arity is typed, and metavariable arities carry enough type information to rule out type-incorrect uses of metavariables. We give a detailed explanation of this below, and will perhaps switch our example in section 2 from untyped to typed lambda calculus, to make this clear.
Reviews B and D also ask about support for equations. Our core notion of signature does not contain equations in it (since general E-unification is undecidable), and so by default it does unification modulo alpha-equivalence. (Eg, we cannot do unification modulo the structural congruence of pi-calculus.) However, in the specific case of typed lambda calculus, we can do better, since there is a GB-signature capturing the normal (and neutral) forms, which lets us lift to pattern unification modulo beta-eta. We sketch the (essentially standard) details below.
In the following, we list the main changes we plan to implement in the final version, and provide detailed answers to the questions of the referees.
[1] Free S-Monoids: A Higher-Order Syntax with Metavariables. Hamana, APLAS 2004
[2] Second-Order Equational Logic. Fiore, Hur, CSL 2010
[3] A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types. Hu, Pientka, Schöpp, ACM TOCL 2022
- Reorder the figures and fix formatting problems
- Introduce some of the GB-signature examples from section 7 immediately after the definition of GB-signature, in particular simply-typed lambda calculus (from section 7.2 currently)
- Expand the related work to compare with the approach based on contextual modal type theory and other semantics of metavariables
- Add the example of normalised syntax of simply-typed lambda calculus to explain how we can accommodate lambda-calculus modulo beta/eta.
We give detailed answers to the questions in each of the reviews below.
I would have liked to see a more in-depth comparison to the many other notions of abstract binding signature that have been developed over the years, several of which are cited. Why couldn't you adapt one of those?
Most existing formalisations of binding signature support general metavariables (ie, metavariables can be instantiated with substitutions containing arbitrary terms). This is too strong to model pattern unification, and our goal was rather to identify the features of a syntax with metavariables satisfying the pattern restriction, which led us to the notion of GB-signatures.
Can you clarify exactly which aspects of the paper are novel,
See our answer to the first concern of review D below.
is there anything novel in Section 2.1
The specific example lambda-calculus as treated in Section 2.1 is not new, except for minor features such as the treatment of failure, as noted by Review B. Section 2.1 is intended to present the pattern unification algorithm in a way that fits into our generic framework. We will make this more explicit in the final version.
could you instead consider the entire category of substitutions, of which the renamings form a subcategory?
It is unclear how to define the category of substitutions for a syntax generated by an arbitrary GB-signature.
I was constantly expecting unification modulo β-equivalence to appear
See our answer to the third concern of review D below.
for the specific case of proving termination of unification, would it be possible to adapt McBride's elegant expression of unification in a structurally recursive manner?
We initially tried to apply McBride's technique in a Coq formalisation, but couldn't make it work due to the limitations of Coq's pattern matching and termination checking. It would indeed be interesting to prove termination of our algorithm in Agda using the McBride style, but we have not yet tried to do so.
l.493, l.591: The text is careful to specify "small category" but the Agda definitions use level- polymorphism to support arbitrarily large universes. As far as I can tell no use is made of this, so might it not be simpler to use small concrete Set levels (i.e. Set, with Set₁ where required)?
If the reviewers prefer, we are ready to apply the change. We don't have a strong opinion on this matter: being a small category could also be interpreted as being small with respect to some universe.
This review highlights four major areas of concern, and two specific examples:
1. The novelty of the contribution
This concern observes that the pattern unification algorithm is not especially novel, and asks if the ideas in our categorical semantics also exist in the literature.
We agree that the core steps of our algorithm are essentially the same as in other papers: the pattern unification algorithm is the same, regardless of the details of how it is presented.
However, our semantics for metavariables does differ in a critical way
from prior semantics of metavariables (such as that of Hsu et al, as
well as those Fiore's and Hamana's). Those models permit interpreting
general metavariables -- i.e., a metavariable can be instantiated
with a full substitution of arbitrary terms. A consequence of this is
that they contain the semantic analogues of problems outside the
pattern fragment, such as M x x ?= N x x. Since problems like this
do not have most general unifiers, the more general categories in the
literature correspondingly do not always have suitable equalisers.
However, the pattern fragment is much more restrictive: a metavariable can only be instantiated with a disjoint collection of free variables, ensuring that mgu's can be found (if they exist). Our semantics has been engineered so that it can only interpret metavariable instantiations in the pattern fragment, and cannot interpret full metavariable instantiations.
This restriction gives our model much stronger properties, enabling us to characterise each part of the pattern unification algorithm in terms of universal properties. This lets us extend Rydeheard and Burstall's proof to the pattern case. No prior semantics can be used for this purpose.
2. Are arities just vectors of variables without type information? How can this possibly extend to dependent types?
This concern is whether our notion of arity is too limited, as a vector of variables without type information.
Our notion of arity is not limited to a vector of variables without type information. As review A notes, in section 7 we give examples which show that our notion of arity includes the sorts of the inputs and the output of the result. As a result, we are performing unification on intrinsically well-sorted terms, and our correctness theorem ensures that the result of unification is always a well-typed substitution whose application results in well-typed terms.
For example, the instance of our unification algorithm for System F will never confuse type and term variables, nor will it produce ill-typed terms or substitutions. Likewise, the example of ordered unification will never produce substitutions which require exchange or any other structural rule.
As we say in the paper, extending our approach to fully dependently-sorted theories is future work. However, the fact that our approach works for System F (which permits a light dependency on types) makes us hopeful.
3. Can our approach handle equations such as beta/eta-laws?
This concern asks whether our algorithm supports unification modulo equational laws like the β- and η-laws of the lambda calculus.
Our algorithm is generic over a notion of signature, and so does not "know" anything about the lambda calculus. Since our definition of GB-signature does not carry an equational theory with it, the core algorithm works only on terms modulo α-equivalence, and works the same regardless of the signature, whether λ-calculus, π-calculus, or anything else.
However, in the specific case of the lambda calculus, every typed lambda term has a normal form, and furthermore, the syntax of the normal forms can be specified by a GB-signature. As a result, we can do unification modulo βη by lowering the metavariables, pre-normalising the terms and doing unification on normal forms, along the lines of Vezzosi and Abel[1]. (This is also similar to the approach of Abel and Pientka.) In the final version of the paper, we will give this as an extended example.
[1] A Categorical Perspective on Pattern Unification, Vezzosi-Abel, RISC-Linz 2014
4. Motivation -- is LF-style unification already enough?
This concern asks if pattern unification for LF-style type theories can already be used to emulate our results with a suitable choice of LF signature. The answer to this question is no, it cannot. In fact, LF signatures and GB-signatures are strictly incomparable in power.
LF-style signatures already handle type dependency (which is future work for us), but there are also GB-signatures which cannot be encoded with an LF signature. For example, GB-signatures allow us to express pattern unification for ordered lambda terms. This is (to our knowledge) completely novel -- even Schack-Nielsen and Schürman's pattern unification algorithm for linear types assumes the admissibility of exchange.
5. The two concrete problems
Review D asked about two specific problems.
The problem in the review M:(A); y:A |- M[y] = \x. c x y is not a
valid input to our unification algorithm, because it is
ill-sorted. The M metavariable needs a return sort to have a
well-formed arity. If we choose the base sort B, then M:(A) → B,
and M[y] is of type B. But \x. c x y would have function
type, and we would be mistakenly trying to unify terms of different
sorts.
In regards to the question about the problem M:0 ; 1 |- M() 1 = 1,
when the problem is corrected to give the proper typed arity to the
metavariable, this should succeed when the unification problem is
specified via the normal-form signature after lowering and normalistion,
and fail in the general theory of lambda terms modulo alpha-equivalence.