The computational content of abstract algebra and analysis

In this dissertation we discuss several forms of proof interpretation based on examples in algebra and analysis. Our main goal is the construction of algorithms or functions out of proofs - constructive proofs and classical proofs. At the beginning of this dissertation the constructive handling of Zorn's lemma in proofs of algebra plays a main role. We consider maximal objects and their approximations in various algebraic structures. The approximation is inspired by Gödel's functional interpretation and methods from proof mining. Proof mining is a branch of mathematical logic which analyses classical existence statements to get explicit bounds. We describe a recursive algorithm which constructs a sequence of approximations until they become close enough. This algorithm will be applied to Krull's lemma and its generalisation: the universal Krull-Lindenbaum lemma. In some case studies and applications like the theorem of Gauß-Joyal and Kronecker's theorem we show explicit uses of this algorithm. By considering Zariski's lemma we present how a manual construction of an algorithm from a constructive proof works. We formulate a constructive proof of Zariski's lemma, and use this proof as inspiration to formulate an algorithm and a computational interpretation of Zariski's lemma. Finally, we prove that the algorithm indeed fulfils the computational interpretation. As an outlook we sketch how this algorithm could be combined with our state-based algorithm from above which constructs approximations of maximal objects, to get an algorithm for Hilbert's Nullstellensatz. We then take a closer look at an example of an algorithm which is extracted out of a constructive proof by using a computer assistant. In our case we use the proof assistant Minlog. We use coinductively defined predicates to prove that the signed digit representation of real numbers is closed under limits of convergent sequences. From a formal proof in Minlog, the computer generates an algorithm, a soundness theorem and a proof of the soundness theorem corresponding to the convergence theorem out of our formalisation. The convergence theorem is applied to Heron's method to get an algorithm which computes the signed digit representation of the square root of a non-negative real number out of its signed digit representation. Here we use the programming language Haskell to display the computational content. As second application we show that the signed digit code is closed under multiplication and state the corresponding algorithm. This dissertation is concluded by an example of proof mining in analysis. We consider one convergence lemma with a classical proof, use techniques of proof mining to get a new lemma with a rate of convergence, and apply the new lemma to various fixed-point theorems for asymptotically weakly contractive maps and their variants. In the last step, beside extracting quantitative information - in our case rates of convergence - from proofs, we also discuss the usage of proof mining to generalise or combine theorems.