[Agda] Why dependent type theory?
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Tue Mar 3 23:14:14 CET 2020
On 2020-03-03 22:43, Jason Gross wrote:
> I'm in the process of writing my thesis on proof assistant performance
> bottlenecks (with a focus on Coq), and there's a large class of
> performance bottlenecks that come from (mis)using the power of
> dependent types. So in writing the introduction, I want to provide
> some justification for the design decision of using dependent types,
> rather than, say, set theory or classical logic (as in, e.g.,
> Isabelle/HOL). And the only reasons I can come up with are "it's fun"
> and "lots of people do it"
>
> So I'm asking these mailing lists: why do we base proof assistants on
> dependent type theory? What are the trade-offs involved?
> I'm interested both in explanations and arguments given on list, as
> well as in references to papers that discuss these sorts of choices.
>
For example, mathematicians write:
"In any field F there is an inversion operation for a nonzero elements:
inv : F\{0} -> F
".
With dependent types, the type of inv is expressed as
(x : F) -> x /= 0# -> F
This type depends on the value x, and this value can change during some
computation.
And I do not know how to express as a type this mathematical notion.
There are many such examples.
Also dependent types are good for constructive proofs.
For example, consider a theorem
"For any prime number p there exists a prime q greater than p".
With dependent types, we prove a stronger statement:
"This provided below algorithm A takes any prime number p and returns a
prime q greater than p".
If one cannot invent a constructive proof, but can prove the thing in a
classical logic,
then one can add the postulate of excluded third and write a classical
proof in Agda.
Regards,
------
Sergei
More information about the Agda
mailing list