Inhaltsbereich
Books and surveys
Papers
-
Constructive aspects of Riemann's permutation theorem for series,
with J. Berger, D.S. Bridges and H. Diener. Final version in Logic Journal
of the IGPL 2023. DOI: 10.1093/jigpal/jzad024.
The notions of permutable and weak-permutable convergence of a
series of real numbers are introduced. Classically, these two
notions are equivalent, and, by Riemann's two main theorems on the
convergence of series, a convergent series is permutably convergent
if and only if it is absolutely convergent. Working within
Bishop-style constructive mathematics, we prove that Ishihara's
principle BD-N implies that every permutably convergent series is
absolutely convergent. Since there are models of constructive
mathematics in which the Riemann permutation theorem for series
holds but BD-N does not, the best we can hope for as a partial
converse to our first theorem is that the absolute convergence of
series with a permutability property classically equivalent to that
of Riemann implies BD-N. We show that this is the case when the
property is weak-permutable convergence.
-
Lookahead analysis in exact real arithmetic with logical methods, with
Nils Köpp. Final version in in TCS 943 (2023), 171-186.
Program extraction from proofs can be used to obtain verified
algorithms in exact real arithmetic for e.g., the signed-digit code
representation. In Minlog this has been done in the past with the use
of certain coinductive predicates. In a next step we want to analyze
the lookahead of these extracted programs. Doing it by hand is quite
cumbersome, so instead we change our definitions. Instead of a
coinductive predicate we use an inductive predicate for the
representation of reals that already incorporates the lookahead. In
this way the lookahead becomes part of the specification which is
carried through all the proofs. In the end we extract programs for
computations on a signed-digit representation and we can just read off
the lookahead from the specification.
-
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.
-
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
See also the listing in
Google scholar
Last change
18. March 2024
