Proof assistants such as Agda can be used to assert properties about programs, such as "the double of a number is even". Interestingly, supercompilers can be used for the same purpose, creating typeless proofs. Even more interestingly, macro tree transducers can, too. My question is: what is the relationship between those? What does a dependently typed language have that makes it more powerful than other type systems as far as theorem proving goes, considering proofs can be done without types?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
I think you're confusing two things: dependently typed languages are convenient for specifying properties and giving proofs about functional programs. The techniques you mention are possible decision procedures for certain properties of functional programs.
The ability to specify program properties usually takes place within a logic. Dependent types are a kind of logic, when viewed through the propositions-as-types lens. The nice thing about this logic is that it is naturally suited to talk about functional programs, which also can be used as a proof language. But there are other logics as well capable of doing this, and some are not based on dependent types.
Supercompilation type proofs are essentially a way to prove that two functions are observationally equal i.e. send identical inputs to outputs. But the fact that a supercompiled function $\mathrm{S}(f)$ is observationally equal to $f$ is not obvious: it has to be proven. Usually this is done with pen and paper, but of course Agda could be used for such a purpose.
Some things to note:
Agda is sufficiently powerful to prove (almost) all the program equivalences you could be interested in. The drawback is that you have to supply the proof yourself.
The things that can be proven automatically using SC or transducers are nice, but they only cover a tiny percent of what people want to prove about their functional programs. In particular, these techniques will fail with any slightly complex property (say, always returning a prime number) and even expressing the desired property may be hard (e.g. always returning a prime number).
There are a number of decision procedures for functional programs which are well-studied and offer similar or additional power as the techniques you mention. In particular ACL2 has been around for quite some time and is (I hear) quite powerful for these kinds of things.
In theory, we could integrate these kinds of procedures to help the user produce a proof in a system like Agda or Coq. There are a number of technical and social reasons for which this hasn't happened yet. There's still hope though! Note also that Coq has a fair number of automated techniques already.
