14
$\begingroup$

Formal proofs in proof systems that avoid the law of the excluded middle and certain other principles can be automatically converted into algorithms.

What useful new algorithms have been produced by this?

For an algorithm to be useful, it doesn't need to be particularly efficient, but should be at least efficient enough to be run on an existing computer. It's not necessary that the algorithm be something that couldn't have been discovered without the constructive proof, but one should at least assume a better algorithm wasn't already known. The function being computed need not have real-life value, as long as it's something a mathematician or computer scientist might want to know.

$\endgroup$
2
  • $\begingroup$ A folklore: The reducibility candidate proof of normalization provides a normalization by evaluation algorithm. This is confirmed on a wide range of type theories. $\endgroup$
    – Trebor
    Mar 20 at 5:22
  • $\begingroup$ This is a really great question! $\endgroup$
    – Jason Rute
    Mar 20 at 13:12

4 Answers 4

5
$\begingroup$

The logic group in Munich has worked on program extraction in the past decades. Most notably, they extracted a program computing the transitive closure of a relation from a graph-theoretic proof and a normalization-by-evaluation algorithm from a proof of normalization. This line of worked has been continued in Swansea recent years, see for instance this paper on monadic parsing. (An aside: A focus of the group in Munich was also extraction of programs from classical proofs, following Kreisel's conviction that many classical proofs require only slight adjustments to evince computational content).

I wouldn't call the Brunerie number an algorithm, as it merely demonstrates the usefulness of a proof system with canonical forms. Usually, for a proof $f$ to be considered an algorithm, it needs to inhabit a type of the following form: $$f : \Pi_{x:A}\Sigma_{y:B(x)}P(x,y)$$

A term $x:A$ can be read as input to the algorithm and $y : B(x)$ as the output of the algorithm. The type $P(x,y)$ encodes the postcondition of the algorithm, i.e., what properties the output should satisfy. Consider the following simple Agda proof (using builtin Nat, Equality and Sigma):

extractDouble : (x : Nat) → Σ Nat (λ y → y ≡ x + x)
extractDouble zero = zero , refl
extractDouble (suc x) = suc (x + suc x) , refl

Thereby extractDouble acts as a proof that for any natural number there exists its doubling, and as an algorithm which explicitly computes this doubling. For instance, the normal form of extractDouble 5 is 10 , refl, so 10 is the result of our algorithm and refl the proof term witnessing that our program has worked correctly.

$\endgroup$
3
  • $\begingroup$ I guess I specified that a better algorithm shouldn't already exist, but I didn't consider the case where the algorithm produced is identical to an already existing algorithm, as it is in your first couple examples. I don't think this counts - the point is to get a new algorithm. I agree that such work can be a proof of concept for obtaining new algorithms in the future, though. $\endgroup$
    – Will Sawin
    Mar 21 at 11:45
  • $\begingroup$ I didn't read your question carefully enough -- you're right, these examples didn't give new algorithms. I doubt that there are cases when a constructive proof yielded a 'new' algorithm however: A misconception of program extraction is that algorithms 'magically fall out' of a formalization. Rather, it's hard work to make a constructive proof work, and at this point the mathematician will already have a deep understanding of the algorithmic problem at hand. $\endgroup$ Mar 21 at 11:59
  • $\begingroup$ (1) I edited the question to add the word "new" to clarify things (assuming the algorithm has to be new is at least a reasonable interpretation of the original, if not the most reasonable interpretation) so you didn't miss it. (2) It's still possible to win the game, if what you say is correct, by refusing to convert your deep understanding into an algorithm until your constructive proof is done, as long as no one else has already obtained the same understanding and algorithm. $\endgroup$
    – Will Sawin
    Mar 21 at 13:02
4
$\begingroup$

Cubical type theory, or any constructive interpretation of HoTT implies the computability of various aspects of algebraic topology. That means, you can encode concepts of homotopy theory into $\lambda$-terms, and use computers to do what only mathematicians could do before. In particular, it shows lots of boolean values, natural numbers, integers or functions of numbers you may find in homotopy theory textbooks/papers can be computed by certain Turing machines.

Brunerie number is an example, as is already mentioned. One should notice that, it is a special case of Whitehead product, which is an operation defined on homotopy groups for any types, and the so-called Brunerie number is all about using a natural number (instead of abstract terms) to encode the Whitehead product $[\iota,\iota]$ of 2-sphere's identity element with itself. People talk about the number more often because it is the one related to $\pi_4(S^3)$. Every Whitehead product could be computed in this way if you are able to make such an encoding. So it satisfies the criterion of @Maximilian Doré, I suppose:)

Unfortunately, it only guarantees the existence of algorithms for homotopy-theoretic computation, or one would say it provides a universal algorithm through normalization. Whatever, up to now it is far from being efficient enough to be run on an existing computer... But I have confidence that someone will find the way out eventually.

The point is, general results about computability are very rare in homotopy theory before constructive HoTT is invented. I only heard about one general theory, the spaces with effective homology, and based on that people built the Kenzo program. It can be used to compute Eilenberg-Moore spectral sequences, the homology of loop spaces and homotopy groups of spheres. Impressive, indeed, but not all-around. I'm not sure if it can compute the Whitehead product. Kenzo can run on your laptop. However, things like cubical type theory could recover all these achievements and much more, at least in theory.

$\endgroup$
3
  • $\begingroup$ Kenzo is 30+ years old, and certainly there were papers on computing various topological invariants of "tame" spaces, e.g. semialgebraic sets, long before HoTT. $\endgroup$ Mar 21 at 15:43
  • $\begingroup$ Yeah, but they base everything on homology and it's not clear how a general topological invariant/operation can be computed. On the other hand, constructive HoTT is more or less a programming language with spaces as basic data structures. It allows you to use anything, like the isomorphism provide by Blakers-Massey theorem, as intermediate steps in your program. $\endgroup$ Mar 21 at 16:00
  • $\begingroup$ But here's new result about spaces with effective homotopy that seems suitable to general homotopy computations. I'm not familiar with these works so I couldn't say much. $\endgroup$ Mar 21 at 16:04
4
$\begingroup$

In structural proof theory, a nice example of an algorithm arising from a constructive proof is the technique of hereditary substitution.

In 1995, Frank Pfenning wrote a paper, Structural Cut Elimination, in which he gave a proof of cut-admissibility for several sequent calculi whose termination metric was structural on the size of the cut formula and the derivation trees being cut against each other.

In 2003, Kevin Watkins and his collaborators observed that if you gave a proof term assignment to the sequent calculus, then Pfenning's cut admissibility proof gives rise to a normalisation procedure for the lambda calculus, which they named hereditary substitution.

(Robin Adams invented essentially the same algorithm in his 2004 PhD thesis on logical frameworks, though AFAICT he was not thinking in terms of the constructive content of cut-elimination proofs, but was rather thinking about adequacy proofs for representing logical systems.)

$\endgroup$
1
$\begingroup$

I don’t think you can exactly call that a useful algorithm, but being able to actually compute with the proof that there exists an $n$ such that $\pi_4(S^3)$ is isomorphic to $\mathbb{Z}/n\mathbb{Z}$ and witness it is 2 (as homotopy theorists have known for a long time) has been a driving problem towards implementations of homotopy and cubical type theories. You can find more references about this by looking around for the "Brunerie number" (the first proof in HoTT of that isomorphism is due to Guillaume Brunerie, so 2 has been jokingly renamed in this honour).

$\endgroup$
1
  • $\begingroup$ Yes, for this to count by my rules, we would need (1) Brunerie's thesis to not include a paper HoTT proof that $n=2$, so that the question "What is $\pi_4(S^3)$ in a given $\infty$-topos" not have the known answer "output $2$ regardless of the topos", and (2) the algorithm to have actually been run. (In fact, this example is why I added the first condition.) $\endgroup$
    – Will Sawin
    Mar 21 at 11:41

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.