 ## Papers

• Logic for exact real arithmetic, with Franziskus Wiesnet. In LMCS 17(2021), arXiv.org:1904.12763
Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.
• Program extraction from proofs: the fan theorem for uniformly coconvex bars. Final version in Mathesis Universalis and Proof Theory (eds. S. Centrone and P. Schuster), Synthese Library, 2019
Proofs can have computational content, and the most direct method to extract it is via a realizability interpretation in the form given by Kreisel. After a short introduction into the subject we present a recent case study on Brouwer's fan theorem for uniform coconvex bars. As an application we prove a constructive version of the Heine-Borel Theorem, for uniformly coconvex coverings.
• Tiered arithmetics, with Stan Wainer. Final version in G. Jäger and W. Sieg (eds.), Feferman on Foundations, Springer, 2017
In his paper "Logics for Termination and Correctness of Functional Programs, II. Logics of Strength PR" Feferman was concerned with the problem of how to guarantee the feasibility (or at least the subrecursive complexity) of functions definable in certain logical systems. His ideas have influenced much subsequent work, for instance the final chapter of [SchwichtenbergWainer12]. There, linear two-sorted systems LRT (a version of Gödel's T) and LRA (a corresponding arithmetical theory) of polynomial-time strength were introduced. Here we extend LRT and LRA in such a way that some forms of non-linearity are covered as well. This is important when one wants to deal on the proof level with particular algorithms, not only with the functions they compute. Examples are divide-and-conquer approaches as in treesort, and the first of two main sections here gives a detailed analysis of this. The second topic treated heads in a different direction, though again its roots lie in the final chapter of [SchwichtenbergWainer12]. Instead of just two sorts we consider transfinite ramified sequences of such sorts (or "tiers"). A hierarchy of infinitary arithmetical systems EA(I_alpha) is devised, being weak analogues of the iterated inductive definitions underpinning much of Feferman's work. Their strengths turn out to correspond to the levels of the extended Grzegorczyk or Fast-Growing hierarchy. A "pointwise" concept of transfinite induction provides an ordinal measure of strength, but it is a weak (essentially finitistic) notion, related to the Slow-Growing hierarchy.
• Logic for Gray-code computation, with U. Berger, K. Miyamoto and H. Tsuiki. Final version in D. Probst and P. Schuster (eds), Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter, 2016
Gray-code is a well-known binary number system where neighboring values differ in one digit only. Tsuiki (2002) has introduced Gray code to the field of real number computation. He assigns to each number a unique 1bot-sequence, i.e., an infinite sequence of -1, 1, bot containing at most one copy of bot (meaning undefinedness). In this paper we take a logical and constructive approach to study real number computation based on Gray-code. Instead of Tsuiki's indeterministic multihead Type-2 machine, we use pre-Gray code, which is a representation of Gray-code as a sequence of constructors, to avoid the difficulty due to bot which prevents sequential access to a stream. We extract real number algorithms from proofs in an appropriate formal theory involving inductive and coinductive definitions. Examples are algorithms transforming pre-Gray code into signed digit code of real numbers, and conversely, the average for pre-Gray code and a translation of finite segments of pre-Gray code into its normal form. These examples are formalized in the proof assistant Minlog.
• Higman's Lemma and its computational content, with M. Seisenberger and F. Wiesnet. Final version in R. Kahle, T. Strahm, and T. Studer (eds), Advances in Proof Theory, Birkhäuser, 2016.
Higman's Lemma is a fascinating result in infinite combinatorics, with manyfold applications in logic and computer science. It has been proven several times using different formulations and methods. The aim of this paper is to look at Higman's Lemma from a computational and comparative point of view. We give a proof of Higman's Lemma that uses the same combinatorial idea as Nash-Williams' indirect proof using the so-called minimal bad sequence argument, but which is constructive. For the case of a two letter alphabet such a proof was given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary well-quasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of Gödel's system T) expressing its computational content.
• Embedding classical in minimal implicational logic, with H. Ishihara. Final version in Mathematical Logic Quarterly 63, 2016.
Consider the problem which set V of propositional variables suffices to prove intuitionistically A from stability (not not P -> P) for all P in V provided A is provable classically. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula ((Q -> P) -> Q) -> Q. It is an easy consequence of the result above that adding a single instance of the Peirce formula suffices to move from classical to intuitionistic derivability. Finally we consider the question whether one could do the same for minimal logic. Given a classical derivation of a propositional formula not involving falsum, which instances of the Peirce formula suffice as additional premises to ensure derivability in minimal logic? We define a set of such Peirce formulas, and show that in general an unbounded number of them is necessary.
• Program extraction from nested definitions, with K. Miyamoto and F. Nordvall Forsberg. In Proceedings ITP 2013.
Minlog is a proof assistant which automatically extracts computational content in an extension of Gödel's T from formalized proofs. We report on extending Minlog to deal with predicates defined using a particular combination of induction and coinduction, via so-called nested definitions. In order to increase the efficiency of the extracted programs, we have also implemented a feature to translate terms into Haskell programs. To illustrate our theory and implementation, a formalisation of a theory of uniformly continuous functions due to Berger is presented.
• Viewing lambda-terms through Maps, with M. Sato, R. Pollack and T. Sakurai. Final version in Indagationes Mathematicae 24, 2013.
In this paper we introduce the notion of map, which is a notation for occurrence of a symbol in syntactic expressions such as formulas or lambda-terms. We use binary trees over 0 and 1 as maps, but some well-formedness conditions are required. We develop a representation of lambda terms using maps. The representation is concrete (inductively definable in HOL or Constructive Type Theory) and canonical (one representative per lambda-term). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic lambda-terms and de Bruijn nameless terms. These proofs are mechanically checked in Isabelle/HOL and Minlog respectively. The map representation has good properties. Substitution does not require adjustment of binding information: neither alpha-conversion of the body being substituted into, nor de Bruijn lifting of the term being implanted. We have a natural proof of the substitution lemma of lambda calculus that requires no fresh names, or index manipulation. Using the notion of map we study conventional raw lambda syntax. E.g. we give, and prove correct, a decision procedure for alpha-equivalence of raw lambda terms that does not require fresh names. We conclude with a definition of beta-reduction of map terms, some discussion on the limitations of our current work, and suggestions for future work.
• Constructive aspects of Riemann's permutation theorem for series, with J. Berger, D.S. Bridges and H. Diener. Draft (February 2012).
• Program extraction in exact real arithmetic, with K. Miyamoto. Final version in MSCS 25, 2015.
The importance of an abstract approach to a computation theory over general data types has been stressed by John Tucker in many of his papers. Ulrich Berger and Monika Seisenberger recently elaborated the idea for extraction out of proofs involving (only) abstract reals. They considered a proof involving coinduction of the proposition that any two reals in [-1,1] have their average in the same interval, and informally extract a Haskell program from this proof, which works with stream representations of reals. Here we formalize the proof, and machine-extract its computational content using the Minlog proof assistant. This required an extension of this system to also take coinduction into account.
• A bound for Dickson's lemma, with J. Berger. Final version in LMCS, 2016
We consider the following special case of Dickson's lemma: for any two functions f,g on the natural numbers there are two numbers i,j with i less than j such that both f and g weakly increase on them, i.e., f_i \le f_j and g_i \le g_j. By a combinatorial argument (due to the first author) a simple bound for such i,j is constructed. The combinatorics is based on the finite pigeon hole principle and results in a certain descent lemma. From the descent lemma one can prove Dickson's lemma, then guess what the bound might be, and verify it by an appropriate proof. We also extract (via realizability) a bound from (a formalization of) our proof of the descent lemma.
• Minimal from classical proofs, with C. Senjak. Final version in APAL 164, 2013.
Let A be a formula without implications, and Gamma consist of formulas containing disjunction and falsity only negatively and implication only positively. Orevkov (1968) and Nadathur (2000) proved that classical derivability of A from Gamma implies intuitionistic derivability, by a transformation of derivations in sequent calculi. We give a new proof of this result (for minimal rather than intuitionistic logic), where the input data are natural deduction proofs in long normal form (given as proof terms via the Curry-Howard correspondence) involving stability axioms for relations; the proof gives a quadratic algorithm to remove the stability axioms. This can be of interest for computational uses of classical proofs. Keywords: Minimal logic, stability axioms, Glivenko-style theorems, Orevkov, intuitionistic logic.
• Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras, with U. Berger, K. Miyamoto and M. Seisenberger. (In: A. Corradini et al., eds, CALCO-Tools 2011, LNCS 6859, 393-399)
Minlog is an interactive system which implements proof-theoretic methods and applies them to verification and program extraction. We give an overview of Minlog and demonstrate how it can be used to exploit the computational content in (co)algebraic proofs and to develop correct and efficient programs. We illustrate this by means of two examples: one about parsing, the other about exact real numbers in signed digit representation.
• Towards a formal theory of computability, with S. Huber and B. Karadais (In: R. Schindler, ed, Ways of Proof Theory: Festschrift for W. Pohlers, 2010)
We sketch a constructive formal theory TCF+ of computable functionals, based on the partial continuous functionals as their intendend domain. Such a task had long ago been started by Dana Scott (1969, 1993), under the well-known abbreviation LCF (logic of computable functionals). The present approach differs from Scott's in two aspects. (i) The intended semantical domains for the base types are non-flat free algebras, given by their constructors, where the latter are injective and have disjoint ranges; both properties do not hold in the flat case. (ii) TCF+ has the facility to argue not only about the functionals themselves, but also about their finite approximations. In this setting we give an informal proof (based on Berger 1993) of Kreisel's density theorem, and an adaption of Plotkin's definability theorem. We then show that both proofs can be formalized in TCF+.
• Decorating proofs, with D. Ratiu (In: S. Feferman and W. Sieg, eds, Mints Festschrift, 2010)
The programs synthesized from proofs are guaranteed to be correct, however at the cost of sometimes introducing irrelevant computations, as a consequence of the fact that the extracted code faithfully reflects the proof. In this paper we extend the work of Ulrich Berger (1993), which introduces the concept of ''non-computational universal quantifiers'', and propose an algorithm by which we identify at the proof level the components - quantified variables, as well as premises of implications - that are computationally irrelevant and mark them as such. We illustrate the benefits of this (optimal) decorating algorithm in some case studies and present the results obtained with the proof assistant Minlog.
• Content in proofs of list reversal (Marktoberdorf '07)
Ulrich Berger (2005) observed that the well-known linear list reversal algorithm can be obtained as the computational content of a weak (or ''classical'') existence proof. The necessary tools are a refinement of the Dragalin/Friedman A-translation, and uniform (or ''non-computational'') quantifiers. Both tools are implemented in the Minlog proof assistant, in addition to the more standard realizability interpretation. The aim of the paper is to give an introduction into the theory underlying these tools, and to explain their usage in Minlog, using list reversal as a running example.
• Dialectica Interpretation of Well-Founded Induction. (Final version in Mathematical Logic Quarterly 54, 2008)
From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well-founded recursion can be used to Dialectica interpret well-founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an algorithm close to Euclid's.
• Realizability interpretation of proofs in constructive analysis. (Final version in ToCS, 2008)
We prove constructively (in the style of Bishop) that every monotone continuous function with a uniform modulus of increase has a continuous inverse. The proof is formalized, and a realizing term extracted. It turns out that even in the logical term language - a version of Gödel's T - evaluation is reasonably efficient.
• New Developments in Proofs and Computations. (Final version in New Computational Paradigms (B. Cooper, B. Löwe, A. Sorbi, eds.))
• Machine Extraction of the Normalization-by-Evaluation Algorithm from a Normalization Proof, with Dominik Schlenker (Marktoberdorf '05)
• Inverting monotone continuous functions in constructive analysis, (Proc. CiE 2006, Swansea)
• Program extraction in constructive analysis. (Final version in S. Lindström et al., eds, Logicism, Intuitionism, and Formalism - What has become of them?)
We sketch a development of constructive analysis in Bishop's style, with special emphasis on low type-level witnesses (using separability of the reals). The goal is to set up things in such a way that realistically executable programs can be extracted from proofs. This is carried out for (1) the Intermediate Value Theorem and (2) the existence of a continuous inverse to a monotonically increasing continuous function. Using the Minlog proof assistant, the proofs leading to the Intermediate Value Theorem are formalized and realizing terms extracted. It turns out that evaluating these terms is a reasonably fast algorithm to compute, say, approximations of the square root of 2.
• Recursion on the partial continuous functionals, (Proc. LC 2005, Athens)
We describe a constructive theory of computable functionals, based on the partial continuous functionals as their intendend domain. Such a task had long ago been started by Dana Scott (1969) under the well-known abbreviation LCF. However, the prime example of such a theory, Per Martin-Löf's type theory in its present form deals with total (structural recursive) functionals only. An early attempt of Martin-Löf (1983) to give a domain theoretic interpretation of his type theory has not even been published, probably because it was felt that a more general approach - such as formal topology - would be more appropriate. In the paper we try to make a fresh start, and do full justice to the fundamental notion of computability in finite types, with the partial continuous functionals as underlying domains. The total ones then appear as a dense subset, and seem to be best treated in this way.
• A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis. (Final version in J. of Universal Computer Science 11, 2005)
From results of Ishihara it is known that the weak (that is, binary) form of König's lemma (WKL) implies Brouwer's fan theorem (Fan). Moreover, Berger and Ishihara [MLQ 2005] have shown that a weakened form WKL! of WKL, where as an additional hypothesis it is required that in an effective sense infinite paths are unique, is equivalent to Fan. The proof that WKL! implies Fan is done explicitly. The other direction (Fan implies WKL!) is far less directly proved; the emphasis is rather to provide a fair number of equivalents to Fan, and to do the proofs economically by giving a circle of implications. Here we give a direct construction. Moreover, we go one step further and formalize the equivalence proof (in the Minlog proof assistant). Since the statements of both Fan and WKL! have computational content, we can automatically extract terms from the two proofs. It turns out that these terms express in a rather perspicuous way the informal constructions.
• Program extraction from normalization proofs, with U. Berger, S. Berghofer and P. Letouzey (Final version in Studia Logica 82, 2006)
This paper describes formalizations of Tait's normalization proof for the simply typed lambda-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-bt-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.
• Proof search in minimal logic (AISC, 2004)
• Constructive Analysis with Witnesses (Marktoberdorf '03)
• Constructive Solutions of Continuous Equations, with P. Schuster (Russell Volume, 2004)
• An arithmetic for polynomial-time computation (Final version in TCS 357, 2006)
We define a restriction LHA of Heyting arithmetic HA with the property that all extracted programs are feasible. The restrictions consist in linearity and ramification requirements.
• An arithmetic for non-size-increasing polynomial-time computation, with K. Aehlig, U. Berger and M. Hofmann (Final version in TCS 318, 2004)
• Feasible computation with higher types, with S. Bellantoni (Marktoberdorf '01)
We restrict recursion in finite types so as to characterize the polynomial time computable functions. The restrictions are obtained by enriching the type structure with the formation of ordinary and linear arrow types and abstraction terms. It turns out that we need two sorts of typed variables: complete and incomplete ones.
• Linear Ramified Higher Type Recursion and Parallel Computation, with K. Aehlig, J. Johannsen and S. Terwijn (PTCS Volume LNCS 2183, 2001)
• Refined Program Extraction from Classical Proofs, with U. Berger and W. Buchholz (Final version in Annals of Pure and Applied Logic 114, 2002)
It is well known that it is undecidable in general whether a given program meets its specification. In contrast, it can be checked easily by a machine whether a formal proof is correct, and from a constructive proof one can automatically extract a corresponding program, which by its very construction is correct as well. This - at least in principle - opens a way to produce correct software, e.g. for safety-critical applications. Moreover, programs obtained from proofs are ''commented'' in a rather extreme sense. Therefore it is easy to maintain them, and also to adapt them to particular situations. We will concentrate on the question of classical versus constructive proofs. It is known that any classical proof of a specification of the form forall x exists y B with B quantifier-free can be transformed into a constructive proof of the same formula. However, when it comes to extraction of a program from a proof obtained in this way, one easily ends up with a mess. Therefore, some refinements of the standard transformation are necessary. In this paper we develop a refined method of extracting reasonable and sometimes unexpected programs from classical proofs. We also generalize previously known results since B in forall x exists y B no longer needs to be quantifier-free, but only has to belong to the strictly larger class of ''goal formulas''. Furthermore we allow unproven lemmas D in the proof of forall x exists y B, where D is a ''definite'' formula.
• Beweise und Programme. Anmerkungen zu Heytings Formalisierung der intuitionistischen Logik (Ber. Abh. Berlin Brand. Akad. Wiss 8, 2000)
• A syntactical analysis of non-size-increasing polynomial time computation, with K. Aehlig (LICS'2000) ( Journal version, in ACM ToCL)
• Refined Program Extraction from Classical Proofs: Some Case Studies, (Marktoberdorf '99)
We make use of a refined method of extracting programs from classical proofs [Berger, Buchholz and Schwichtenberg 2002]. Its use is demonstrated with two rather detailed case studies. Specifically, we extract programs from classical proofs of the existence of (i) integer square roots, and (ii) integer coefficients to linearly combine the greatest common divisor of two numbers from these numbers.
• Term rewriting for normalization by evaluation, with U. Berger and M. Eberl (Final version in Information and Computation 183, 2003)
We extend normalization by evaluation (first presented in [Berger and Schwichtenberg 1991]) from the pure typed lambda-calculus to general higher type term rewriting systems and prove its correctness w.r.t. a domain-theoretic model. We distinguish between computational rules and proper rewrite rules. The former is a rather restricted class of rules, which, however, allows for a more efficient implementation
• Higher Type Recursion, Ramification and Polynomial Time, with S. Bellantoni and K-H. Niggl (Final version in Annals of Pure and Applied Logic 104, 2000).
• Normalization by evaluation, with U. Berger and M. Eberl (NADA Volume LNCS 1546, 1998)
• Proof theory at work: Program development in the Minlog system , with H. Benl, U. Berger, M. Seisenberger and W. Zuber (Automated Deduction, W. Bibel and P.H. Schmitt, eds., Vol. II, Kluwer 1998)
• Formal correctness proofs of functional programs: Dijkstra's algorithm, a case study , with H. Benl (Marktoberdorf '97))
• Termination of permutative conversions in intuitionistic Gentzen calculi (Final version in TCS 212, 1999)
• Monotone majorizable functionals (Final version in Studia Logica 62, 1999)
• The Warshall Algorithm and Dickson's Lemma: Two examples of realistic program extraction, with U. Berger and M. Seisenberger (Final version in Journal of Automated Reasoning 26, 2001)
• Programmentwicklung durch Beweistransformation: Das Maximalsegmentproblem (Bayer. Akad., 12/96)
• Finite notations for infinite terms (Final version in Annals of Pure and Applied Logic 94, 1998)
• From higher order terms to circuits, with K. Stroetmann (ICLMPS Florenz '95)
• The greatest common divisor: a case study for program extraction from classical proofs (also in dvi or pdf -format), with U. Berger (Turin '95)
Yiannis Moschovakis suggested the following example of a classical existence proof with a quantifier-free kernel which does not obviously contain an algorithm: the gcd of two natural numbers is a linear combination of the two. Here we treat that example as a case study for program extraction from classical proofs. We apply Harvey Friedman's A-translation followed by a modified realizability interpretation to extract a program from this proof. However, to obtain a reasonable program it is essential to use a refinement of the A-translation. This refinement makes it possible that not all atoms in the proof are A-translated, but only those with a "critical" relation symbol. In our example only the divisibility relation is critical.
• Proofs, Lambda Terms and Control Operators (Marktoberdorf '95)
• Strict Functionals for Termination Proofs, with J. van de Pol (TLCA '95)
• Program Extraction from Classical Proofs , with U. Berger (LCC '94)
• Ordinal Bounds for Programs, with A. Wainer (Feasible Math '94)
• Density and choice for total continuous functionals (Kreisel '93)
• Program development by proof transformation, with U. Berger (Marktoberdorf '93)
• Minimal from Classical Proofs (CSL '91)
• Minimal Logic for Computable Functions (Marktoberdorf '91)
• Proofs as Programs (Leeds '90)
Suppose a formal proof of (all x)(ex y) Spec(x,y) is given, where Spec(x,y) is an atomic formula expressing some specification for natural numbers x, y. For any particular number n we then obtain a formal proof of (ex y) Spec(n,y). Now the proof-theoretic normalization procedure yields another proof of (ex y) Spec(n,y) which is in normal form. In particular, it does not use induction axioms any more, and it also does not contain non-evaluated terms. Hence we can read off, linearly in the size of the normal proof, an instance m for y such that Spec(n,m) holds. In this way a formal proof can be seen as a program, and the central part in implementing this programming language consists in an implementation of the proof-theoretic normalization procedure. It is not the prime purpose of the paper to discuss this implementation. Rather, we want to explore the theoretical possibilities and limitations of a programming language based on formal proofs. The notion of proof is taken here in a quite basic sense: the formal language is supposed to talk about algebraic data structures (i.e. free algebras), and structural recursion as well as structural induction is allowed. Hence we discuss systems of the strength of ordinary arithmetic. We will measure the strength of our proofs/programs in terms of the so-called slow growing hierarchy G_alpha introduced by Wainer and studied by Girard. We will give a new proof of the following result of Kreisel and (Girard 1981): Any function defined by a proof of (all x)(ex y)Spec (x,y) is bounded by a function G_alpha of the hierarchy with alpha below the Bachmann-Howard ordinal, and conversely that for any such G_alpha there is an atomic formula Spec_alpha (x,y) such that G_alpha(n) below the least m with Spec_alpha(n,m), and (all x)(ex y) Spec_alpha(x,y) is provable, and hence for any proof of this fact the function computed by that proof (considered as a program) grows at least as fast as G_alpha. On the more technical side, our work builds heavily on earlier work of Buchholz (1987) and Arai (1989). In particular, the material in Sections 1-3 on trees, tree notations and the slow growing hierarchy is taken from Buchholz. Also, the omega^+-Rule below is derived from (a special case of) the Omega-Rule in (Buchholz 1987) (or more precisely of its "slow-growing" variant in (Arai 1989)), which in turn is based on earlier work of Howard (1972). The new twist here is that we make use of a technique of Howard (1980) to measure the complexity of a (finite) term/proof by (transfinite) trees; for this to go through it is essential to use a natural deduction system and not a Tait calculus as in (Buchholz 1987) or (Buchholz and Wainer 1987). More precisely, we inductively define what it means for a (finite) term/proof involving recursion/induction constants to be SDH-generated (for Sanchis-Diller-Howard) with measure alpha (a transfinite tree) and rank m. One clause of this inductive definition is called omega^+-rule and introduces uncountable trees. In this setup it is easy to provide relatively perspicious and complete proofs of the relations mentioned above between the slow growing hierarchy and the functions computed by proofs/programs in arithmetical systems.
• An upper bound for reduction sequences in the typed lambda-calculus (Final version in Arch. Math. Logic 30, 1991)
• Normalization (Marktoberdorf '89)
• Primitive Recursion on the Partial Continuous Functionals (Bauer-Kolloquium '89)
There is also a List of publications