| 1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162 |
- Review 2
- > Cite a standard type checking algorithm.
- For instance,
- A. Abel, T. Coquand, "Untyped Algorithmic Equality for Martin-Löf’s Logical
- Framework (extended version)".
- > Theorem 1
- Indeed \Gamma and \Sigma are assumed to be correct as a premise to the
- statement. The precise formulation (for type checking) is:
- <\Sigma> \Gamma |- e ^ A ~> M ==> <\Sigma'> /\ \Gamma |-_\Sigma A type
- \implies \Sigma' extends \Sigma /\ \Gamma |-_{\Sigma'} M : A
- Here \Gamma |- \Sigma A type implies that \Gamma and \Sigma are well-formed.
- The statements for the other judgement forms are similar. To save space we cut
- all of the precise formulations, which made the statement unneccesarily
- unclear.
- > Theorem 2
- The premise \Gamma |-_\Sigma A type is missing. This is a typo.
- > On p.7 the rule in paragraph "Conversion rules"...
- The rule is correct. p takes arguments of types \Gamma and A_1 and returns a
- term of type A_2.
- > On p.8, the first rule has several typos...
- The rule is correct. The relationship between A and B is
- B[\bar M/\Delta] = A = B[\bar N/\Delta]
- which is guaranteed by the fact that h \bar{M} and h \bar{N} have type A (this
- invariant is stated on p.6 in the second paragraph). Consequently we don't need
- to check it. The choice of names for the type of h in the text is unfortunate
- and should match the type in the rule to avoid confusion.
- > Where do you use pattern unification?
- We only instantiate meta-variables if they are applied to distinct variables
- (last rule on p.8). This is the same restriction as in pattern unification.
- > Are you implying that a correct unification algorithm (returning a
- > substitution that does unify) could be too strong?
- We are not sure what you mean here. The main point of our algorithm is that
- substitutions are well-typed. Not all unification algorithms produce well-typed
- substitutions.
- > How are the types of terms unified before the terms are unified?
- This is ensured by the invariant (second paragraph on p.6) that all constraints
- are well-typed, i.e when we try to solve a constraint \Gamma |- M = N : A we
- know that \Gamma |- M : A and \Gamma |- N : A, and so the types unify
- trivially. The invariant is maintained by introducing guarded constants.
|
