2
$\begingroup$

In extensional type theory, identity types are lifted to the definitional equality mechanism, this lead to a bunch of problems, and I imagine that's why they are not very popular. My question is if we extend identity type to depend on some other solver, where both sides of the equation are asked for this mechanism whether they are equal or not, we also consider the reflection rule, hence if the mechanism agrees they are equal, then they are lifted also to be definitional equality. This mechanism could be an SMT solver, for instance.

For all "mechanisms", this type of system is non-decidable or non-consistent? Is there any type of system that uses an ad-hoc identity type or some similar approach?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Do you mean when I finished a proof and send it to someone else, their computer may reject the proof because of non-determinism? $\endgroup$
    – Trebor ♦
    Jul 15 at 3:04
  • $\begingroup$ It could happen if the mechanism is not deterministic, but this same mechanism could also be another type checker, so it depends on what source of truth you choose. $\endgroup$
    – Tiago Campos
    Jul 15 at 17:05

2 Answers 2

Reset to default
3
$\begingroup$

I know of several works that have examined the idea of using some non-trivial decision procedure to implement conversion in a dependent type theory:

Coq Modulo Theory, by Pierre-Yves Strub.

This allows parametrizing the conversion algorithm by an arbitrary(ish) decidable theory.

Programming up to Congruence by Stephanie Weirich and Vilhelm Sjöberg, arguably a less general framework but with better type-inference properties, I think.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ That is what I was looking for, thank you. $\endgroup$
    – Tiago Campos
    Jul 23 at 3:15
2
$\begingroup$

Your idea to use heuristics and tactics to solve problems in type theory is good, and is massively used, not just for equality checking but also for all sorts of other things.

But you are trying to put it in the wrong place. It does not belong to the underlying theoretical formalism (type theory), but to the operational part of a proof assistant (tactics, vernacular, meta-language, etc.)

The job of type theory is to be the mathematical bedrock on top of which we build a proof assistant. It is not there to help solve problems, but as a standard of mathematical correctness, guaranteeing objective and verifiable expression of mathematical statements, constructions and proofs.

Imagine a situation in which we implemented a proof assistant by inserting in its kernel (the core that everyone trusts to do its job correctly and reliably) some external tool $T$, such as a SAT solver or an automated theorem prover, and declared that whatever the tool $T$ says is the holy mathematical truth (inference rules are precisely that). Suddenly all of our formalized mathematics is subject to bugs in $T$, which is presumably a much much larger piece of software than the kernel of a proof assistant. If someone fixes a bug in $T$, or upgrades $T$ so that it works better, does that mean mathematics changed and there are now new mathematical truths, while the old ones are possibly false? What if $T$ works differently on your computer than mine (because it runs concurrently on many cores and I have more core than you), do we live in different worlds of mathematics? This situation is untenable.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Assuming T as a source of truth could not be seen as good to formalize general mathematics. But if one trusts T, and wants to extend its power for the sake of expressivity, that person is only inverting the arrow of source tool <-> type checker dependencies. Instead of using a type checker as a source of truth and having to deal with proof re-constructions between these tools, we could use a type checker as a plugin of T. $\endgroup$
    – Tiago Campos
    Jul 15 at 17:01
  • $\begingroup$ Of course, the type checker can not lead to triviality, that's why I think if someone went to this approach, they need to be careful what inference rules they choose for their ad-hoc type system. Also, T could also be another type checker, for example. Just wondering if someone already tried this path. $\endgroup$
    – Tiago Campos
    Jul 15 at 17:01
  • $\begingroup$ You know what we would get if we went down your road? Mathematica. It can compute a whole lot of things, and is mostly correct, but nobody knows what it does or what its expression mean. $\endgroup$
    – Andrej Bauer
    Jul 15 at 21:23
  • $\begingroup$ Someone (possibly your good self) reminded me that there is not just one "type theory" to rule them all. How do you reconcile that with having type theory as the bedrock on which a proof assist sits? $\endgroup$
    – Bruce Adams
    Jul 17 at 19:37
  • 1
    $\begingroup$ By being more careful with articles: A type theory is a bedrock of a mathematics. I am not saying there is holy truth codified by the type theory, but that the role of type theory to express whatever foundation one wants to have. $\endgroup$
    – Andrej Bauer
    Jul 17 at 20:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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