-1
$\begingroup$

A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom: $$\forall p, (p(T) \wedge p(F)) = \forall x, p(x) $$ HM can easily infer that $p$ has type Bool -> Bool and $x$ has type Bool.

But IIUC, theorems don't always prove the most general interpretation of a proposition. For example, say that I prove $T = T$ and $F = F$, and use these with the above axiom to prove $$\forall x, x = x$$

In this case, the proof assistant must explicitly keep track of the fact that $x$ had type Bool, right? Without this extra information, the type system would infer that $x$ could be any arbitrary $\alpha$, even though we've only proved the $x : $ Bool case. (I know that equality should probably be reflexive in every type, but one shouldn't be able to prove this for all types from just checking $T$ and $F$).

How do existing proof assistants combat this issue? How much "extra" type information do they need to track to avoid accidentally "over-generalizing"?* Is this a phenomenon which has been encountered/documented in existing proof assistants (whether they use HM or more complex dependent type systems)?

* I initially believed that you could resolve this issue by just tracking the types of all bound variables, but this doesn't seem to work: Suppose in our theory we define the predicate $\mathrm{reflexive}(f) = \forall x, f(x, x)$, then we can use the above theorem to prove $\mathrm{reflexive}(=)$. This proposition has no bound variables, but again we must somehow keep track of the fact that it has only been proven for equality over type Bool.

$\endgroup$
5
  • $\begingroup$ It is unclear how you intend to use such a proof assistant (I take it you have in mind HOL-style proof assistants) to get from $T = T$ to $F = F$. I suggest that you either provide an actual example, or a more detailed description of what you have in mind, or choose a better example. The one you have is double unfortunate for being both true and blatantly polymorphic. $\endgroup$ Mar 24 '21 at 13:31
  • $\begingroup$ To be precise, the murky part of your question is "and use these with the above axiom to prove". What exactly do you tell the proof assistant when you "use" $T = T$"? $\endgroup$ Mar 24 '21 at 13:32
  • $\begingroup$ I'm not sure of the exact HOL-style syntax. But from $T = T$ and $F = F$ you can prove $(T = T) \wedge (F = F)$, which is beta equivalent to $(\lambda y, y = y)(T) \wedge (\lambda y, y = y)(F)$. Therefore you can apply the axiom to get $\forall x, (\lambda y, y = y)(x)$ which beta-reduces to the theorem. $\endgroup$ Mar 24 '21 at 13:45
  • $\begingroup$ A better example of an theorem which is "obviously wrong when over-generalized" would be: $\forall f \forall x, f(x) = f(f(f(x)))$. The proof assistant must track that $x$ has type Bool to remain sound, even though $x$ could have a more general inferred type. $\endgroup$ Mar 24 '21 at 13:47
  • $\begingroup$ I see. Well, there is no problem. As soon as you use your axiom, it will force $x$ in $\forall x, x = x$ to get type $\mathtt{bool}$. $\endgroup$ Mar 24 '21 at 15:23
0
$\begingroup$

Generally, HM type inference should be a part of the I/O interface, far away from the inference kernel. This constraint will drive your design to ensure that this won't be a problem. In your $\mathrm{reflexive}$ example, there are two polymorphic constants at play:

$$\mathrm{reflexive} : (\alpha \to \alpha \to \mathrm{bool}) \to \mathrm{bool}$$ $$(=) : \alpha \to \alpha \to \mathrm{bool}$$

You should remember the type used to instantiate any polymorphic constants in your theorems. This solves your problem.

In general, most HOL systems I'm aware of identify constants and variables by their (name, type) pair in the kernel. That is, $x_{bool}$ and $x_{nat}$ are different variables, but when they both occur in the same context, the parsing and printing logic are allowed to complain. This is a nice way to think about the logic...

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.