Algorithms obtained through constructive formalization

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.)

Answer 4

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).