Contents

Acknowledgements. The Minlog system has been under development since around 1990. My sincere thanks go to the many contributors: Holger Benl (Dijkstra algorithm, inductive data types), Ulrich Berger (very many contributions), Michael Bopp (program development by proof transformation), Wilfried Buchholz (translation of classical proof into intuitionistic ones), Laura Crosilla (tutorial), Matthias Eberl (normalization by evaluation), Dan Hernest (functional interpretation), Felix Joachimski (many contributions, in particular translation of classical proofs into intuitionistic ones, producing Tex output, documentation), Ralph Matthes (documentation), Karl-Heinz Niggl (program development by proof transformation), Jaco van de Pol (experiments concerning monotone functionals), Martin Ruckert (many contributions, in particular the MPC tool), Robert Stärk (alpha equivalence), Monika Seisenberger (many contributions, including inductive definitions and translation of classical proofs into intuitionistic ones), Klaus Weich (proof search, the Fibonacci numbers example), Wolfgang Zuber (documentation).

1. Introduction

• Proofs are treated as first class objects: they can be normalized and then used for reading off an instance if the proven formula is existential, or changed for program development by proof transformation.
• To keep control over the complexity of extracted programs, we follow Kreisel’s proposal and aim at a theory with a strong language and weak existence axioms. It should be conservative over (a fragment of) arithmetic.
• Minlog is based on minimal rather than classical or intuitionistic logic. This more general setting makes it possible to implement program extraction from classical proofs, via a refined A-translation (cf. [3]).
• Constants are intended to denote computable functionals. Since their (mathematically correct) domains are the Scott-Ershov partial continuous functionals, this is the intended range of the quantifiers.
• Variables carry (simple) types, with free algebras as base types. The latter need not be finitary (so we allow e.g. countably branching trees), and can be simultaneously generated. Type parameters (ML style) are allowed, but we keep the theory predicative and disallow type quantification.
• To simplify equational reasoning, the system identifies terms with the same normal form. A rich collection of rewrite rules is provided, which can be extended by the user. Decidable predicates are implemented via boolean valued functions, hence the rewrite mechanism applies to them as well.

We now describe in more details some of these features.

1.1. Simultaneous free algebras. A free algebra is given by constructors, for instance zero and successor for the natural numbers. We want to treat other data types as well, like lists and binary trees. When dealing with inductively defined sets, it will also be useful to explicitely refer to the generation tree. Such trees are quite often countably branching, and hence we allow infinitary free algebras from the outset.

The freeness of the constructors is expressed by requiring that their ranges are disjoint and that they are injective. Moreover, we view the free algebra as a domain and require that its bottom element is not in the range of the constructors. Hence the constructors are total and non-strict. For the notion of totality cf. [12, Chapter 8.3].

In our intended semantics we do not require that every semantic object is the denotation of a closed term, not even for finitary algebras. One reason is that for normalization by evaluation (cf. [4]) we want to allow term families in our semantics.

To make a free algebra into a domain and still have the constructors injective and with disjoint ranges, we model e.g. the natural numbers as shown in Figure 1.

Notice that for more complex algebras we usually need many more “infinite” elements; this is a consequence of the closure of domains under suprema. To make dealing with such complex structures less annoying, we will normally restrict attention to the total elements of a domain, in this case – as expected – the elements labelled 0, S0, S(S0) etc.

1.2. Partial continuous functionals. As already mentioned, the (mathematically correct) domains of computable functionals have been identified by Scott and Ershov as the partial continuous functionals; cf. [12]. Since we want to deal with computable functionals in our theory, we consider it as mandatory to accommodate their domains. This is also true if one is interested in total functionals only; they have to be treated as particular partial continuous functionals. We will make use of predicate constants Total_ρ with the total functionals of type ρ as the intended meaning. To make formal arguments with quantifiers relativized to total objects more managable, we use a special sort of variables intended to range over such objects only. For example, n0,n1,n2,…,m0,… range over total natural numbers, and nˆ0,nˆ1,nˆ2,… are general variables. This amounts to an abbreviation of

	∀.Totalρ() → A	by	∀xA,
	∃.Totalρ() ∧ A	by	∃xA.

1.3. Primitive recursion, computable functionals. The elimination constants corresponding to the constructors are called primitive recursion operators ℛ. They are described in detail in Section 4. In this setup, every closed term reduces to a numeral.

However, we shall also use constants for rather arbitrary computable functionals, and axiomatize them according to their intended meaning by means of rewrite rules. An example is the general fixed point operator fix, which is axiomatized by fixF = F(fixF). Clearly then it cannot be true any more that every closed term reduces to a numeral. We may have non-terminating terms, but this just means that not always it is a good idea to try to normalize a term.

An important consequence of admitting non-terminating terms is that our notion of proof is not decidable: when checking e.g. whether two terms are equal we may run into a non-terminating computation. But we still have semi-decidability of proofs, i.e., an algorithm to check the correctness of a proof that can only give correct results, but may not terminate. In practice this is sufficient.

To avoid this somewhat unpleasant undecidability phenomenon, we may also view our proofs as abbreviated forms of full proofs, with certain equality arguments left implicit. If some information sufficient to recover the full proof (e.g. for each node a bound on the number of rewrite steps needed to verify it) is stored as part of the proof, then we retain decidability of proofs.

1.4. Decidable predicates, axioms for predicates. As already mentioned, decidable predicates are viewed via boolean valued functions, hence the rewrite mechanism applies to them as well.

Equality is decidable for finitary algebras only; infinitary algebras are to be treated similarly to arrow types. For infinitary algebras (extensional) equality is a predicate constant, with appropriate axioms. In a finitary algebra equality is a (recursively defined) program constant. Similarly, existence (or totality) is a decidable predicate for finitary algebras, and given by predicate constants Total_ρ for infinitary algebras as well as composed types. The axioms are listed in Subsection 8.2 of Section 8.

1.5. Minimal logic, proof transformation. For generalities about minimal logic cf. [13]. A concise description of the theory behind the present implementation can be found in “Minimal Logic for Computable Functions” which is available on the Minlog page www.minlog-system.de.

1.6. Comparison with Coq and Isabelle.

The Isabelle/HOL system of Paulson and Nipkow has its roots in Church’s theory of simple types and Hilbert’s Epsilon calculus. It is an inherently classical system; however, since many proofs in fact use constructive arguments, in is conceivable that program extraction can be done there as well. This has been explored by Berghofer in his thesis [6].

Compared with the Minlog system, the following points are of interest.

• The fact that in Coq a formula is just a map into the type Prop (and in Isabelle into the type bool) can be used to define such a function by what is called strong elimination, say by f(tt) := A and f(ff) := B with fixed formulas A and B. The problem is that then it is impossible to assign an ordinary type (say in the sense of ML) to a proof. It is not clear how this problem for program extraction can be avoided (in a clean way) for both Coq and Isabelle. In Minlog it does not exist due to the separation of terms and formulas.
• The impredicativity (in the sense of quantification over predicate variables) built into Coq and Isabelle has as a consequence that extracted programs need to abstract over type variables, which is not allowed in program languages of the ML family. Therefore one can only allow outer universal quantification over type and predicate variables in proofs to be used for program extraction; this is done in the Minlog system from the outset. However, many uses of quantification over predicate variables (like defining the logical connectives apart from → and ∀) can be achieved by means of inductively defined predicates. This feature is available in all three systems.
• The distinction between properties with and without computational content seems to be crucial for a reasonable program extraction environment; this feature is available in all three systems. However, it also seems to be necessary to distinguish between universal quantifiers with and without computational content, as in Berger’s [2]. At present this feature is availble in the Minlog system only.
• Coq has records, whose fields may contain proofs and may depend on earlier fields. This can be useful, but does not seem to be really essential. If desired, in Minlog one can use products for this purpose; however, proof objects have to be introduced explicitely via assumptions.
• Minlog’s automated proof search search tool is based on Miller’s [10]; it produces proofs in minimal logic. In addition, Coq has many strong tactics, for instance Omega for quantifier free Presburger arithmetic, Arith for proving simple arithmetic properties and Ring for proving consequences of the ring axioms. Similar tactics exist in Isabelle. These tactics tend to produce rather long proofs, which is due to the fact that equality arguments are carried out explicitely. This is avoided in Minlog by relativizing every proof to a set of rewrite rules, and identifyling terms and formulas with the same normal form w.r.t. these rules.
• In Isabelle as well as in Minlog the extracted programs are provided as terms within the language, and a soundness proof can be generated automatically. For Coq (and similarly for Nuprl) such a feature could at present only be achived by means of some form of reflection.

2. Types, with simultaneous free algebras as base types

We have type constants atomic, existential, prop and nulltype. They will be used to assign types to formulas. E.g. ∀nn = 0 receives the type nat → atomic, and ∀n,m∃k n + m = k receives the type nat → nat → existential. The type prop is used for predicate variables, e.g. R of arity nat,nat -> prop. Types of formulas will be necessary for normalization by evaluation of proof terms. The type nulltype will be useful when assigning to a formula the type of a program to be extracted from a proof of this formula. Types not involving the types atomic, existential, prop and nulltype are called object types.

Type variable names are alpha,beta…; alpha is provided by default. To have infinitely many type variables available, we allow appended indices: alpha1,alpha2,alpha3… will be type variables. The only type constants are atomic,existential,prop and nulltype.

2.1. Generalitites for substitutions, type substitutions.

Composition ϑσ of two substitutions

We shall have occasion to use these general substitution procedures for the following kinds of substitutions

The following substitutions will make sense for a

In particular, for type substitutions tsubst we have

2.2. Simultaneous free algebras as base types. We allow the formation of inductively generated types μ, where = α₁,…,α_n is a list of distinct type variables, and is a list of “constructor types” whose argument types contain α₁,…,α_n in strictly positive positions only.

For instance, μα(α,α → α) is the type of natural numbers; here the list (α,α → α) stands for two generation principles: α for “there is a natural number” (the number 0), and α → α for “for every natural number there is another one” (its successor).

Let an infinite supply of type variables α,β be given. Let = (α_j)_j=1,…,m be a list of distinct type variables. Types ρ,σ,τ,μ,ν ∈ Types and constructor types κ ∈ KT() are defined inductively as follows.

	(n ≥ 0)
	(n ≥ 1, j = 1,…,m)

To add and remove names for type variables, we use

To introduce simultaneous free algebras we use

An example is

This simultaneously introduces the two free algebras labtree and labtlist, both finitary, whose constructors are LabLeaf, LabBranch, LabEmpty and LabTcons (written as an infix pair operator, hence right associative). The constructors are introduced as “self-evaluating” constants; they play a special role in our semantics for normalization by evaluation.

In case there are no parameters we use add-algs, and in case there is no need for a simultaneous definition we use add-alg or add-param-alg.

For already introduced algebras we need constructors and accessors

We require that there is at least one nullary constructor in every free algebra; hence, it has a “canonical inhabitant”. For arbitrary types this need not be the case, but occasionally (e.g. for general logical problems, like to prove the drinker formula) it is useful. Therefore

which returns the canonical inhabitant; it is an error to apply this procedure to a non-inhabited type. We do allow non-inhabited types to be able to implement some aspects of [7, 1]

To remove names for algebras we use

Examples. Standard examples for finitary free algebras are the type nat of unary natural numbers, and the type btree of binary trees. The domain ℐ_nat of unary natural numbers is defined (as in [4]) as a solution to a domain equation.

We always provide the finitary free algebra unit consisting of exactly one element, and boole of booleans; objects of the latter type are (cf. loc. cit.) true, false and families of terms of this type, and in addition the bottom object of type boole.

Tests:

We also need constructors and accessors for arrow types

Implementation. Type variables are implemented as lists:

3. Variables

In most cases we need to argue about existing (i.e. total) objects only. For the notion of totality we have to refer to [12, Chapter 8.3]; particularly relevant here is exercise 8.5.7. To make formal arguments with quantifiers relativized to total objects more managable, we use a special sort of variables intended to range over such objects only. For example, n0,n1,n2,…,m0,… range over total natural numbers, and nˆ0,nˆ1,nˆ2,… are general variables. We say that the degree of totality for the former is 1, and for the latter 0.

n,m for variables of type nat), we use

We need a constructor, accessors and tests for variables.

For convenience we have the function

Using the empty string as the name, we can create so called numerated variables. We further require that we can test whether a given variable belongs to those special ones, and that from every numerated variable we can compute its index:

with inverses var-to-type, numerated-var-to-index and var-to-t-deg.

Although these functions look like an ad hoc extension of the interface that is convenient for normalization by evaluation, there is also a deeper background: these functions can be seen as the “computational content” of the well-known phrase “we assume that there are infinitely many variables of every type”. Giving a constructive proof for this statement would require to give infinitely many examples of variables for every type. This of course can only be done by specifying a function (for every type) that enumerates these examples. To make the specification finite we require the examples to be given in a uniform way, i.e. by a function of two arguments. To make sure that all these examples are in fact different, we would have to require make-var to be injective. Instead, we require (classically equivalent) make-var to be a bijection on its image, as again, this can be turned into a computational statement by requiring that a witness (i.e. an inverse function) is given.

Finally, as often the exact knowledge of infinitely many variables of every type is not needed we require that, either by using the above functions or by some other form of definition, functions

Occasionally we may want to create a new variable with the same name (and degree of totality) as a given one. This is useful e.g. for bound renaming. Therefore we supply

Implementation. Variables are implemented as lists:

4. Constants

• constructors, kind constr,
• constants with user defined rules (also called program(mable) constant, or pconst), kind pconst,
• constants whose rules are fixed, kind fixed-rules.

The latter are built into the system: recursion operators for arbitrary algebras, equality and existence operators for finitary algebras, and existence elimination. They are typed in parametrized form, with the actual type (or formula) given by a type (or type and formula) substitution that is also part of the constant. For instance, equality is typed by α → α → boole and a type substitution αρ. This is done for clarity (and brevity, e.g. for large ρ in the example above), since one should think of the type of a constant in this way.

For constructors and for constants with fixed rules, by efficiency reasons we want to keep the object denoted by the constant (as needed for normalization by evaluation) as part of it. It depends on the type of the constant, hence must be updated in a given proof whenever the type changes by a type substitution.

4.1. Rewrite and computation rules for program constants.

There a more general approach was used: one may enter into components of products. Then instead of one arity one needs several “type informations” → σ with a list of types, 0’s and 1’s indicating the left or right part of a product type. For example, if c is of type τ → (τ → τ → τ) × (τ → τ), then the rules cy0xxa and cy1b are admitted, and c comes with the type informations (τ,0,τ,τ → τ) → τ and (τ,1) → (τ → τ). – However, for simplicity we only deal with a single arity here.

Given a set of rewrite rules, we want to treat some rules - which we call computation rules - in a different, more efficient way. The idea is that a computation rule can be understood as a description of a computation in a suitable semantical model, provided the syntactic constructors correspond to semantic ones in the model, whereas the other rules describe syntactic transformations.

In order to define what we mean by computation rules, we need the notion of a constructor pattern. These are special terms defined inductively as follows.

• Every variable is a constructor pattern.
• If c is a constructor and P₁,…,P_n are constructor patterns (or projection markers 0 or 1), such that c is of ground type, then c is a constructor pattern.

From the given set of rewrite rules we choose a subset Comp with the following properties.

• If cQ ∈ Comp, then P₁,…,P_n are constructor patterns or projection markers.
• The rules are left-linear, i.e. if cQ ∈ Comp, then every variable in c occurs only once in c.
• The rules are non-overlapping, i.e. for different rules cM and cN in Comp the left hand sides c and c are non-unifiable.

We write c_compQ to indicate that the rule is in Comp. All other rules will be called (proper) rewrite rules, written c_rewK.

In our reduction strategy computation rules will always be applied first, and since they are non-overlapping, this part of the reduction is unique. However, since we allowed almost arbitrary rewrite rules, it may happen that in case no computation rule applies a term may be rewritten by different rules Comp. In order to obtain a deterministic procedure we then select the first applicable rewrite rule (This is a slight simplification of [4], where special functions sel_c were used for this purpose).

4.2. Recursion over simultaneous free algebras.

,

For convenience in our later treatment of proofs (when we want to normalize a proof by (1) translating it into a term, (2) normalizing this term and (3) translating the normal term back into a proof), we also allow all-formulas ∀x₁^μ₁A₁,…,∀x_k^μ_kA_k instead of arrow-types: they are treated as μ₁ → τ(A₁), ..., μ_k → τ(A_k) with τ(A_j) the type of A_j.

Recall the definition of types and constructor types in Section 2, and the examples given there. In order to define the type of the recursion operators w.r.t.  = μ and result types , we first define for

the step type

δi, := →	( 1 → μj1) →→ (n → μjn) →
	(1 → τj1) →→ (n → τjn) → τj.

,

We will often write ℛ_j^, for ℛ_μj^,, and omit the upper indices , when they are clear from the context. In case of a non-simultaneous free algebra, i.e. of type μα (κ), for ℛ_μ^μ,τ we normally write ℛ_μ^τ.

A simple example for simultaneous free algebras is

The constructors are

	(const Rec δ1 → δ2 → δ3 → δ4 → tree → α1
	(α1τ1,α2τ2))
with
	δ1 := α1,
	δ2 := tlist → α2 → α1,
	δ3 := α2,
	δ4 := tree → tlist → α1 → α2 → α2.

For the external representation (i.e. display) we use the shorter notation

As already mentioned, it is also possible that the object constant Rec comes with formulas instead of types, as the assumption constant Ind below. This is due to our desire not to duplicate code when normalizing proofs, but rather translate the proof into a term first, normalize the term and then translate back into a proof. For the last step we must have the original formulas of the induction operator available.

To see a concrete example, let us recursively define addition +: tree → tree → tree and ⊕: tlist → tree → tlist. The recursion equations to be satisfied are

+	:= ℛtree: tree → tree → tree,
⊕	:= ℛtlist: tlist → tree → tlist.

To explain the conversion relation, it will be useful to employ the following notation. Let = μ,

and consider constri. Then we write P = N1P ,…,NmP for the parameter arguments N1ρ1,…,Nmρm and R = N1R,…,NnR for the recursive arguments Nm+11→μj1,…,Nm+nn→μjn, and nR for the number n of recursive arguments.

We define a conversion relation _ρ between terms of type ρ by

(λxM)N	M[x:=N]	(1)
λx.Mx	M if xFV(M), M not an abstraction	(2)
(ℛj,)μj→τj (constri)	M i(ℛj 1,) ∘ N 1R…(ℛ jn,) ∘ N nR	(3)

,

,

4.3. Internal representation of constants. Every object constant has the internal representation

	(const Compose (α→β)→(β→γ)→α→γ (αρ,βσ,γτ) ...)
	(const Eq α → α → boole (αfinalg) ...)
	(const E α → boole (αfinalg…))
	(const Ex-Elim ∃xαP(x) → (∀xα.P(x) → Q) → Q
	(ατ,P(α){zτ ∣ A},Q{ ∣ B }) ...)

Constructor, accessors and tests for all kinds of constants:

From these we can define

A constructor is a special constant with no rules. We maintain an association list CONSTRUCTORS assigning to every name of a constructor an association list associating with every type substitution (restricted to the type parameters) the corresponding instance of the constructor. We provide

For given algebras one can display the associated constructors with their types by calling

We also need procedures recovering information from the string denoting a program constant (via PROGRAM-CONSTANTS):

One can display the program constants together with their current computation and rewrite rules by calling

To add and remove program constants we use

To add and remove computation and rewrite rules we have

To generate our constants with fixed rules we use

Similarly to arrow-types-to-rec-const we also define the procedure all-formulas-to-rec-const. It will be used in to achieve normalization of proofs via translating them in terms.

[Noch einfügen: arrow-types-to-cases-const und zur Behandlung von Beweisen all-formulas-to-cases-const]

5. Predicate variables and constants

5.1. Predicate variables.

Predicate variable names are provided in the form of an association list, which assigns to the names their arities. By default we have the predicate variable bot of arity (arity), called (logical) falsity. It is viewed as a predicate variable rather than a predicate constant, since (when translating a classical proof into a constructive one) we want to substitute for bot.

Often we will argue about Harrop formulas only, i.e. formulas without computational content. For convenience we use a special sort of predicate variables intended to range over comprehension terms with Harrop formulas only. For example, P0,P1,P2,…,Q0,… range over comprehension terms with Harrop formulas, and Pˆ0,Pˆ1,Pˆ2,… are general predicate variables. We say that Harrop degree for the former is 1, and for the latter 0.

We need constructors and accessors for arities

We can test whether a string is a name for a predicate variable, and if so compute its associated arity:

To add and remove names for predicate variables of a given arity (e.g. Q for predicate variables of arity nat), we use

We need a constructor, accessors and tests for predicate variables.

For convenience we have the function

It is guaranteed that parsing a displayed predicate variable reproduces the predicate variable; the converse need not be the case (we may want to convert it into some canonical form).

5.2. Predicate constants.

Notice that a predicate constant does not change its name under a type substitution; this is in contrast to predicate (and other) variables. Notice also that the parser can infer from the arguments the types ρ₁…ρ_n to be substituted for the type variables in the uninstantiated arity of P.

To add and remove names for predicate constants of a given arity, we use

5.3. Inductively defined predicate constants.

More precisely, we allow the formation of inductively generated predicates μ, where = (X_j)_j=1,…,N is a list of distinct predicate variables, and = (K_i)_i=1,…,k is a list of constructor formulas (or “clauses”) containing X₁,…,X_N in strictly positive positions only.

To introduce inductively defined predicates we use

An example is

This simultaneously introduces the two inductively defined predicate constants Ev and Od, by the clauses given. The presence of an algebra name after the arity (here algEv and algOd) indicates that this inductively defined predicate constant is to have computational content. Then all clauses with this constant in the conclusion must provide a constructor name (here InitEv, GenEv, InitOd, GenOd). If the constant is to have no computational content, then all its clauses must be invariant (under realizability, a.k.a. “negative”).

Here are some further examples of inductively defined predicates:

6. Terms and objects

The if-construct distinguishes cases according to the outer constructor form; the simplest example (for the type boole) is if-then-else. Here we do not want to evaluate all arguments right away, but rather evaluate the test argument first and depending on the result evaluate at most one of the other arguments. This phenomenon is well known in functional languages; e.g. in Scheme the if-construct is called a special form as opposed to an operator. In accordance with this terminology we also call our if-construct a special form. It will be given a special treatment in nbe-term-to-object.

Usually it will be the case that every closed term of an sfa ground type reduces via the computation rules to a constructor term, i.e. a closed term built from constructors only. However, we do not require this.

We have constructors, accessors and tests for variables

It is convenient to have more general application constructors and accessors available, where application takes arbitrary many arguments and works for ordinary application as well as for component formation.

Moreover we need

6.1. Normalization. We need an operation which transforms a term into its normal form w.r.t. the given computation and rewrite rules. Here we base our treatment on normalization by evaluation introduced in [5], and extended to arbitrary computation and rewrite rules in [4].

For normalization by evaluation we need semantical objects. For an arbitrary ground type every term family of that type is an object. For an sfa ground type, in addition the constructors have semantical counterparts. The freeness of the constructors is expressed by requiring that their ranges are disjoint and that they are injective. Moreover, we view the free algebra as a domain and require that its bottom element is not in the range of the constructors. Hence the constructors are total and non-strict. Then by applying nbe-reflect followed by nbe-reify we can normalize every term, where normalization refers to the computation as well as the rewrite rules.

An object consists of a semantical value and a type.

where delayed-constr is a procedure of zero arguments which evaluates to this very same constructor. This is necessary to avoid having a cycle (for nullary constructors, and only for those).

The interpretation of the program constants requires some auxiliary functions (cf. [4]):

The if-form needs a special treatment. In particular, for a full normalization of terms (including permutative conversions), we define a preprocessing step that η expands the alternatives of all if-terms. The result contains if-terms with ground type alternatives only.

6.2. Substitution. Recall the generalities on substitutions in Section 2.1.

We define simultaneous substitution for type and object variables in a term, via tsubst and subst. It is assumed that subst only affects those vars whose type is not changed by tsubst.

In the abstraction case of the recursive definition, the abstracted variable may need to be renamed. However, its type can be affected by tsubst. Then the renaming cannot be made part of subst, because the condition above would be violated. Therefore we carry along a procedure renaming variables, which remembers the renaming of variables done so far.

Display functions for substitutions are

7. Formulas and comprehension terms

• (atom r) with a term r of type boole,
• (predicate a r1 ... rn) with a predicate variable or constant a and terms r1 ...rn.

Formulas are built from prime formulas by

• implication (imp formula1 formula2)
• conjunction (and formula1 formula2)
• tensor (tensor formula1 formula2)
• all quantification (all x formula)
• existential quantification (ex x formula)
• all quantification (allnc x formula) without computational content
• existential quantification (exnc x formula) without computational content

Moreover we have classical existential quantification in an arithmetical and a logical form:

Formulas can be unfolded in the sense that the all classical existential quantifiers are replaced according to their definiton. Inversely a formula can be folded in the sense that classical existential quantifiers are introduced wherever possible.

Comprehension terms have the form (cterm vars formula). Note that formula may contain further free variables.

Tests:

We need constructors and accessors for prime formulas

It is also useful to have some general procedures working for arbitrary quantified formulas. We provide

To fold and unfold formulas we have

Morever we need

Constructors, accessors and a test for comprehension terms are

Normalization of formulas is done with

To check equality of formulas we use

Display functions for formulas and comprehension terms are

We can define simultaneous substitution for type, object and predicate variables in a formula, via tsubst, subst and psubst. It is assumed that subst only affects those variables whose type is not changed by tsubst, and that psubst only affects those predicate variables whose arity is not changed by tsubst.

In the quantifier case of the recursive definition, the abstracted variable may need to be renamed. However, its type can be affected by tsubst. Then the renaming cannot be made part of subst, because then the condition above would be violated. Therefore we carry along a procedure rename renaming variables, which remembers the renaming of variables done so far.

We will also need formula substitution to compute the formula of an assumption constant. However, there (type and) predicate variables are (implicitely) considered to be bound. Therefore, we also have to carry along a procedure prename renaming predicate variables, which remembers the renaming of predicate variables done so far.

Display functions for predicate substitutions are

8. Assumption variables and constants

8.1. Assumption variables. Assumption variables are for proofs what variables are for terms. The main difference, however, is that assumption variables have formulas as types, and that formulas may contain free variables. Therefore we must be careful when substituting terms for variables in assumption variables. Our solution (as in Matthes’ thesis [9]) is to consider an assumption variable as a pair of a (typefree) identifier and a formula, and to take equality of assumption variables to mean that both components are equal. Rather than using symbols as identifiers we prefer to use numbers (i.e. indices). However, sometimes it is useful to provide an optional string as name for display purposes.

We need a constructor, accessors and tests for assumption variables.

An assumption constant appears in a proof, as an axiom, a theorem or a global assumption. Its formula is given as an “uninstantiated formula”, where only type and predicate variables can occur freely; these are considered to be bound in the assumption constant. In the proof the bound type variables are implicitely instantiated by types, and the bound predicate variables by comprehension terms (the arity of a comprehension term is the type-instantiated arity of the corresponding predicate variable). Since we do not have type and predicate quantification in formulas, the assumption constant contains these parts left implicit in the proof: tsubst and pinst (which will become a psubst, once the arities of predicate variables are type-instantiated with tsubst).

So we have assumption constants of the following kinds:

• axioms,
• theorems, and
• global assumptions.

To normalize a proof we will first translate it into a term, then normalize the term and finally translate the normal term back into a proof. To make this work, in case of axioms we pass to the term appropriate formulas: all-formulas for induction, an existential formula for existence introduction, and an existential formula together with a conclusion for existence elimination. During normalization of the term these formulas are passed along. When the normal form is reached, we have to translate back into a proof. Then these formulas are used to reconstruct the axiom in question.

Internally, the formula of an assumption constant is split into an uninstantiated formula where only type and predicate variables can occur freely, and a substitution for at most these type and predicate variables. The formula assumed by the constant is the result of carrying out this substitution in the uninstantiated formula. Note that free variables may again occur in the assumed formula. For example, assumption constants axiomatizing the existential quantifier will internally have the form

	(aconst Ex-Intro ∀α.() →∃α() (ατ,(α){ τ ∣ A}))
	(aconst Ex-Elim ∃α() → (∀α.() →) →
	(ατ,(α){ τ ∣ A},{ ∣ B }))

Interface for general assumption constants. To avoid duplication of code it is useful to formulate some procedures generally for arbitrary assumption constants, i.e. for all of the forms listed above.

8.2. Axiom constants.

=(0,0)	≈ tt
=(0,S) ≈ =(S,0)	≈ ff	e(0)	≈ tt
=(S1,S2)	≈ =(1,2)	e(S)	≈ e()
=(bbnat,) ≈ =(,bbnat)	≈ bb	e(bbnat)	≈ bb
=(∞nat,) ≈ =(,∞nat)	≈ bb	e(∞nat)	≈ bb

	T		Truth-Axiom
	≈		Eq-Refl
	1 ≈2 →2 ≈1		Eq-Symm
	1 ≈2 →2 ≈3 →1 ≈3		Eq-Trans
	∀ 1 ≈ 2 → 1 ≈ 2		Eq-Ext
	1 ≈2 →(1) →(2)		Eq-Compat
	Totalρ→σ( ) ↔∀.Totalρ() → Totalσ( )		Total
	Totalρ(c)		Constr-Total
	Total(c) → Total(i)		Constr-Total-Args
and for every finitary algebra, e.g. nat
	1 ≈2 → E(1) →1 = 2		Eq-to-=-1-nat
	1 ≈2 → E(2) →1 = 2		Eq-to-=-2-nat
	1 = 2 →1 ≈2		=-to-Eq-nat
	1 = 2 → E(1)		=-to-E-1-nat
	1 = 2 → E(2)		=-to-E-2-nat
	Total() → E()		Total-to-E-nat
	E() → Total()		E-to-Total-nat