xxMinlog reference manual

MINLOG REFERENCE MANUAL

Date:xJanuary 17, 2007.

ContentsxxAcknowledgementsx1.xxIntroductionxxx1.1.xxSimultaneous free algebrasxxx1.2.xxPartial continuous functionalsxxx1.3.xxPrimitive recursion, computable functionalsxxx1.4.xxDecidable predicates, axioms for predicatesxxx1.5.xxMinimal logic, proof transformationxxx1.6.xxComparison with Coq and Isabellex2.xxTypes, with simultaneous free algebras as base typesxxx2.1.xxGeneralitites for substitutions, type substitutionsxxx2.2.xxSimultaneous free algebras as base typesx3.xxVariablesx4.xxConstantsxxx4.1.xxRewrite and computation rules for program constantsxxx4.2.xxRecursion over simultaneous free algebrasxxx4.3.xxInternal representation of constantsx5.xxPredicate variables and constantsxxx5.1.xxPredicate variablesxxx5.2.xxPredicate constantsxxx5.3.xxInductively defined predicate constantsx6.xxTerms and objectsxxx6.1.xxNormalizationxxx6.2.xxSubstitutionx7.xxFormulas and comprehension termsx8.xxAssumption variables and constantsxxx8.1.xxAssumption variablesxxx8.2.xxAxiom constantsxxx8.3.xxTheoremsxxx8.4.xxGlobal assumptionsx9.xxProofsxxx9.1.xxConstructors and accessorsxxx9.2.xxNormalizationxxx9.3.xxSubstitutionxxx9.4.xxDisplayxxx9.5.xxClassical logicx10.xxInteractive theorem proving with partial proofsxxx10.1.xxPartial proofsxxx10.2.xxInteractive theorem provingx11.xxSearchx12.xxComputational content of classical proofsx13.xxExtracted termsx14.xxReading formulas in external formxxx14.1.xxLexical analysisxxx14.2.xxParsingReferencesIndex

0 Contents

[next] [tail] [up]

Contents

ContentsxxAcknowledgementsx1.xxIntroductionxxx1.1.xxSimultaneous free algebrasxxx1.2.xxPartial continuous functionalsxxx1.3.xxPrimitive recursion, computable functionalsxxx1.4.xxDecidable predicates, axioms for predicatesxxx1.5.xxMinimal logic, proof transformationxxx1.6.xxComparison with Coq and Isabellex2.xxTypes, with simultaneous free algebras as base typesxxx2.1.xxGeneralitites for substitutions, type substitutionsxxx2.2.xxSimultaneous free algebras as base typesx3.xxVariablesx4.xxConstantsxxx4.1.xxRewrite and computation rules for program constantsxxx4.2.xxRecursion over simultaneous free algebrasxxx4.3.xxInternal representation of constantsx5.xxPredicate variables and constantsxxx5.1.xxPredicate variablesxxx5.2.xxPredicate constantsxxx5.3.xxInductively defined predicate constantsx6.xxTerms and objectsxxx6.1.xxNormalizationxxx6.2.xxSubstitutionx7.xxFormulas and comprehension termsx8.xxAssumption variables and constantsxxx8.1.xxAssumption variablesxxx8.2.xxAxiom constantsxxx8.3.xxTheoremsxxx8.4.xxGlobal assumptionsx9.xxProofsxxx9.1.xxConstructors and accessorsxxx9.2.xxNormalizationxxx9.3.xxSubstitutionxxx9.4.xxDisplayxxx9.5.xxClassical logicx10.xxInteractive theorem proving with partial proofsxxx10.1.xxPartial proofsxxx10.2.xxInteractive theorem provingx11.xxSearchx12.xxComputational content of classical proofsx13.xxExtracted termsx14.xxReading formulas in external formxxx14.1.xxLexical analysisxxx14.2.xxParsingReferencesIndex

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

[next] [front] [up]

1 Introduction

[next] [prev] [prev-tail] [tail] [up]

1. Introduction

Intro Minlog is intended to reason about computable functionals, using minimal logic. It is an interactive prover with the following features.

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.x[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.xcountably 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.x[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.x[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.xthe natural numbers as shown in Figurex1.

PICT [figure: •; ⊥; •; 0; •; S⊥; •; S0; •; S(S⊥); •; S(S0); •; S(S(S⊥)); •; S(S(S0)); .; .; .; •; ∞] Figurex1: The domain of natural numbers

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.x[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, x, m0, x range over total natural numbers, and n^0, n^1, n^2, x are general variables. This amounts to an abbreviation of

∀x̂.Total_{ρ}(x̂) → A  by  ∀xA,
∃x̂.Total_{ρ}(x̂) ∧ A  by  ∃xA.

1.3. Primitive recursion, computable functionals.

The elimination constants corresponding to the constructors are called primitive recursion operators R. 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.xwhether 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.xfor 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 Sectionx8.

1.5. Minimal logic, proof transformation.

For generalities about minimal logic cf.x[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.

SS:Coq Coq (cf.xcoq.inria.fr) has evolved from a calculus of constructions defined by Huet and Coquand. It is a constructive, but impredicative system based on type theory. More recently it has been extended by Paulin-Mohring to also include inductively defined predicates. Program extraction from proofs has been implemented by Paulin-Mohring, Filliatre and Letouzey, in the sense that Ocaml programs are extracted from proofs.

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

[next] [prev] [prev-tail] [front] [up]

2 Types, with simultaneous free algebras as base types

[next] [prev] [prev-tail] [tail] [up]

2. Types, with simultaneous free algebras as base types

S:Types Generally we consider typed theories only. Types are built from type variables and type constants by algebra type formation (alg ρ_{1}xρ_{n}), arrow type formation ρ → σ and product type formation ρ × σ (and possibly other type constructors).

We have type constants atomic, existential, prop and nulltype. They will be used to assign types to formulas. E.g.x∀n n = 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.xR 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, betax; alpha is provided by default. To have infinitely many type variables available, we allow appended indices: alpha1, alpha2, alpha3x will be type variables. The only type constants are

atomic, existential, prop and nulltype.

2.1. Generalitites for substitutions, type substitutions.

SS:GenSubst Generally, a substitution is a list ((x_{1}xt_{1})x(x_{n}xt_{n})) of lists of length two, with distinct variables x_{i} and such that for each i, x_{i} is different from t_{i}. It is understood as simultaneous substitution. The default equality is equal?; however, in the versions ending with -wrt (for “with respect to”) one can provide special notions of equality. To construct substitutions we have

             (make-substitution args vals)
             (make-substitution-wrt arg-val-equal?xargs vals)
             (make-subst arg val)
             (make-subst-wrt arg-val-equal?xarg val)
             empty-subst

Accessing a substitution is done via the usual access operations for association list: assoc and assoc-wrt. We also provide

(restrict-substitution-wrt subst test?)
(restrict-substitution-to-args subst args)
(substitution-equal?xsubst1 subst2)
(substitution-equal-wrt?xarg-equal?xval-equal?xsubst1 subst2)
(subst-item-equal-wrt?xarg-equal?xval-equal?xitem1 item2)
(consistent-substitutions-wrt?
    arg-equal?xval-equal?xsubst1 subst2)

Composition ϑσ of two substitutions

\begin{aligned}ϑ & = ((x_{1}xs_{1})x(x_{m}xs_{m})), \\ σ & = ((y_{1}xt_{1})x(y_{n}xt_{n})) \end{aligned}

is defined as follows. In the list ((x_{1}xs_{1}σ)x(x_{m}xs_{m}σ)x(y_{1}xt_{1})x(y_{n}xt_{n})) remove all bindings (x_{i}xs_{i}σ) with s_{i}σ = x_{i}, and also all bindings (y_{j}xt_{j}) with y_{j} ∈ {x_{1}, x, x_{n}}. It is easy to see that composition is associative, with the empty substitution as unit. We provide

   (compose-substitutions-wrtx substitution-proc arg-equal?

                                  arg-val-equal?xsubst1 subst2)

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

. for  called domain equality arg-val-equality type variables  tsubst  equal?         equal? object variables  osubst  equal?         var-term-equal? predicate variables psubst  equal?         pvar-cterm-equal? assumption variables asubst  avar=?         avar-proof-equal?

The following substitutions will make sense for a

.  type  tsubst term  tsubst and osubst formula tsubst and osubst and psubst proof tsubst and osubst and psubst and asubst

In particular, for type substitutions tsubst we have

                     (type-substitute type tsubst)
                     (type-subst type tvar type1)
                     (compose-t-substitutions tsubst1 tsubst2)

A display function for type substitutions is

                               (display-t-substitution tsubst)

2.2. Simultaneous free algebras as base types.

We allow the formation of inductively generated types μα⃗ κ⃗, where α⃗ = α_{1}, x, α_{n} is a list of distinct type variables, and κ⃗ is a list of “constructor types” whose argument types contain α_{1}, x, α_{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,x,m} be a list of distinct type variables. Types ρ, σ, τ, μ, ν ∈ Types and constructor types κ ∈ KT(α⃗) are defined inductively as follows.

\frac{ρ⃗, σ⃗_{1}, …, σ⃗_{n} ∈ Types}{ρ⃗ → (σ⃗_{1} → α_{j_{1}}) → ⋯ → (σ⃗_{n} → α_{j_{n}}) → α_{j} ∈ KT(α⃗)} (n ≥ 0)
\frac{κ_{1}, …, κ_{n} ∈ KT(α⃗)}{(μα⃗ (κ_{1}, …, κ_{n}))_{j} ∈ Types} (n ≥ 1, j = 1, x, m)  \frac{ρ, σ ∈ Types}{ρ → σ ∈ Types}

Here ρ⃗ is short for a list ρ_{1}, x, ρ_{k} (k ≥ 0) of types and ρ⃗ → σ means ρ_{1} → ⋯ → ρ_{k} → σ, associated to the right. We shall use μ, ν for types of the form (μα⃗ (κ_{1}, x, κ_{n}))_{j} only, and for types τ⃗ = (τ_{j})_{j=1,x,m} and a constructor type κ = ρ⃗ → (σ⃗_{1} → α_{j_{1}}) → ⋯ → (σ⃗_{n} → α_{j_{n}}) → α_{j} ∈ KT(α⃗) let

. κ[τ⃗] := ρ⃗ → (σ⃗_{1} → τ_{j_{1}}) → ⋯ → (σ⃗_{n} → τ_{j_{n}}) → τ_{j}.

Examples.

unit  := μα α,
boole  := μα (α, α),
nat  := μα (α, α → α),
ytensor(α_{1})(α_{2})  := μα.α_{1} → α_{2} → α,
ypair(α_{1})(α_{2})  := μα.(unit → α_{1}) → (unit → α_{2}) → unit → α,
yplus(α_{1})(α_{2})  := μα.(α_{1} → α, α_{2} → α),
list(α_{1})  := μα (α, α_{1} → α → α),
(tree, tlist)  := μ(α, β) (α, β → α, β, α → β → β),
btree  := μα (α, α → α → α),
O  := μα (α, α → α, (nat → α) → α),
T_{0}  := nat,
T_{n+1}  := μα (α, (T_{n} → α) → α).

Note that we could have defined our primitive ρ × σ by μα.ρ → σ → α. However, this may lead to complex terms when it comes to extract programs from proofs. Therefore we stick to using ρ × σ as a primitive.

To add and remove names for type variables, we use

                       (add-tvar-name name1 ...)
                       (remove-tvar-name name1 ...)

We need a constructor, accessors and a test for type variables.

(make-tvar index name)  constructor
(tvar-to-index tvar)  accessor
(tvar-to-name tvar)  accessor

(tvar?xx).

To generate new type variables we use

                   (new-tvar type)

To introduce simultaneous free algebras we use

. add-algebras-with-parameters, abbreviated add-param-algs .

An example is

(add-param-algs
xxx(listx"labtree"x"labtlist")x'alg-typeopx2
xxx'("LabLeaf"x"alpha1=>labtree")
xxx'("LabBranch"x"labtlist=>alpha2=>labtree")
xxx'("LabEmpty"x"labtlist")
xxx'("LabTcons"x"labtree=>labtlist=>labtlist"xpairscheme-op))

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

                     (make-alg name type1 ...)
                     (alg-form-to-name alg)
                     (alg-form-to-types alg)
                     (alg-name-to-simalg-names alg-name)
                     (alg-name-to-token-types alg-name)
                     (alg-name-to-typed-constr-names alg-name)
                     (alg-name-to-tvars alg-name)
                     (alg-name-to-arity alg-name)

We also provide the tests

(alg-form?xx)  incomplete test
(alg?xx)  complete test

                                (finalg?xtype)  incomplete test
                                (ground-type?xx)  incomplete test

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.xfor general logical problems, like to prove the drinker formula) it is useful. Therefore

                               (make-inhabited type term1 ...)

marks the optional term as the canonical inhabitant if it is provided, and otherwise creates a new constant of that type, which is taken to be the canonical inhabitant. We also have

.  (type-to-canonical-inhabitant type),

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,x1]

To remove names for algebras we use

                                   (remove-alg-name name1 ...)

Examples. Standard examples for finitary free algebras are the type nat of unary natural numbers, and the type btree of binary trees. The domain Inat 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.xloc.xcit.)xtrue, false and families of terms of this type, and in addition the bottom object of

type boole.

Tests:

(arrow-form?xtype)
(star-form?xtype)
(object-type?xtype)

We also need constructors and accessors for arrow types

(make-arrow arg-type val-type)  constructor
(arrow-form-to-arg-type arrow-type)  accessor
(arrow-form-to-val-type arrow-type)  accessor

and star types

(make-star type1 type2)  constructor
(star-form-to-left-type star-type)  accessor
(star-form-to-right-type star-type)  accessor.

For convenience we also have

(mk-arrow type1 ...xtype)

(arrow-form-to-arg-types type <n>)  all (first n) argument types
(arrow-form-to-final-val-type type)  type of final value.

To check and to display a type we have

(type?xx)
(type-to-string type).

Implementation. Type variables are implemented as lists:

.  (tvar index name).

3 Variables

[next] [prev] [prev-tail] [tail] [up]

3. Variables

Variables A variable of an object type is interpreted by a continuous functional (object) of that type. We use the word “variable” and not “program variable”, since continuous functionals are not necessarily computable. For readable in- and output, and also for ease in parsing, we may reserve certain strings as names for variables of a given type, e.g.xn, m for variables of type nat. Then also n0, n1, n2, x, m0, x can be used for the same purpose.

In most cases we need to argue about existing (i.e.xtotal) 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, x, m0, x range over total natural numbers, and n^0, n^1, n^2, x 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

                              (add-var-name name1 ...xtype)
                              (remove-var-name name1 ...xtype)
                              (default-var-name type).

The first variable name added for any given type becomes the default variable name. If the system creates new variables of this type, they will carry that name. For complex types it sometimes is necessary to talk about variables of a certain type without using a specific name. In this case one can use the empty string to create a so called numerated variable (see below). The parser is able to produce this kind of canonical variables from type expressions.

We need a constructor, accessors and tests for variables.

               (make-var type index t-deg name)  constructor
               (var-to-type var)  accessor
               (var-to-index var)  accessor
               (var-to-t-deg var)  accessor
               (var-to-name var)  accessor

(var-form?xx)  incomplete test
(var?xx).  complete test

It is guaranteed that equal? is a valid test for equality of variables. Moreover, it is guaranteed that parsing a displayed variable reproduces the variable; the converse need not be the case (we may want to convert it into some canonical form).

For convenience we have the function

                         (mk-var type <index> <t-deg> <name>).

The type is a required argument; however, the remaining arguments are optional. The default for the name string is the value returned by

                                       (default-var-name type)

If there is no default name, a numerated variable is created. The default for the totality is “total”.

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:

                       (numerated-var?xvar)
                       (numerated-var-to-index numerated-var).

It is guaranteed that make-var used with the empty name string is a bijection

. Types × ℕ × TDegs → NumVars

 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.xby 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.xan 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

                                (type-to-new-var type)
                                (type-to-new-partial-var type)

are defined that return a (total or partial) variable of the requested type, different from all variables that have ever been returned by any of the specified functions so far.

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.xfor bound renaming. Therefore we supply

                                         (var-to-new-var var).

Implementation. Variables are implemented as lists:

.  (var type index t-deg name).

4 Constants

[next] [prev] [prev-tail] [tail] [up]

4. Constants

Pconst Every constant (or more precisely, object constant) has a type and denotes a computable (hence continuous) functional of that type. We have the following three kinds of 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.xfor 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.

SS:RewCompRules For every program constant c^{ρ} we assume that some rewrite rules of the form cK⃗ ↦N are given, where FV(N) ⊆ FV(K⃗) and cK⃗, N have the same type (not necessarily a ground type). Moreover, for any two rules cK⃗ ↦N and cK⃗′ ↦N′ we require that K⃗ and K⃗′ are of the same length, called the arity of c. The rules are divided into computation rules and proper rewrite rules. They must satisfy the requirements listed in [4]. 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.

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 cy0xx ↦a and cy1 ↦b 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_{1}, x, P_{n} are constructor patterns (or projection markers 0 or 1), such that cP⃗ is of ground type, then cP⃗ is a constructor pattern.

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

If cP⃗ ↦Q ∈ Comp, then P_{1}, x, P_{n} are constructor patterns or projection markers.

The rules are left-linear, i.e.xif cP⃗ ↦Q ∈ Comp, then every variable in cP⃗ occurs only once in cP⃗.

The rules are non-overlapping, i.e.xfor different rules cK⃗ ↦M and cL⃗ ↦N in Comp the left hand sides cK⃗ and cL⃗ are non-unifiable.

We write cM⃗ ↦_{comp}Q to indicate that the rule is in Comp. All other rules will be

called (proper) rewrite rules, written cM⃗ ↦_{rew}K.

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.

SS:RecSFA We now explain what we mean by recursion over simultaneous free algebras. The inductive structure of the types μ⃗ = μα⃗ κ⃗ corresponds to two sorts of constants. With the constructors constr_{i}^{μ⃗}: κ_{i}[μ⃗] we can construct elements of a type μ_{j}, and with the recursion operators R_{μ_{j}}^{μ⃗,τ⃗} we can construct mappings from μ_{j} to τ_{j} by recursion on the structure of μ⃗. So in

(Rec arrow-types), arrow-types is a list μ_{1} → τ_{1}, x, μ_{k} → τ_{k}. Here

μ_{1}, x, μ_{k} are the algebras defined simultaneously and τ_{1}, x, τ_{k} are the result types.

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_{1}^{μ_{1}}A_{1}, x, ∀x_{k}^{μ_{k}}A_{k} instead of arrow-types: they are treated as μ_{1} → τ(A_{1}), …, μ_{k} → τ(A_{k}) with τ(A_{j}) the type of A_{j}.

Recall the definition of types and constructor types in Sectionx2, and the examples given there. In order to define the type of the recursion operators w.r.t.xμ⃗ = μα⃗ κ⃗ and result types τ⃗, we first define for

. κ_{i} = ρ⃗ → (σ⃗_{1} → α_{j_{1}}) → ⋯ → (σ⃗_{n} → α_{j_{n}}) → α_{j} ∈ KT(α⃗)

the step type

\begin{aligned}δ_{i}^{μ⃗,τ⃗} := ρ⃗ → & (σ⃗_{1} → μ_{j_{1}}) → ⋯ → (σ⃗_{n} → μ_{j_{n}}) → \\ & (σ⃗_{1} → τ_{j_{1}}) → ⋯ → (σ⃗_{n} → τ_{j_{n}}) → τ_{j}. \end{aligned}

Here ρ⃗, (σ⃗_{1} → μ_{j_{1}}), x, (σ⃗_{n} → μ_{j_{n}}) correspond to the components of the object of type μ_{j} under consideration, and (σ⃗_{1} → τ_{j_{1}}), x, (σ⃗_{n} → τ_{j_{n}}) to the previously defined values. The recursion operator R_{μ_{j}}^{μ⃗,τ⃗} has type . R_{μ_{j}}^{μ⃗,τ⃗}: δ_{1}^{μ⃗,τ⃗} → ⋯ → δ_{k}^{μ⃗,τ⃗} → μ_{j} → τ_{j}.

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

A simple example for simultaneous free algebras is

. (tree, tlist) := μ(α, β) (α, β → α, β, α → β → β).

The constructors are

Leaf^{tree} := constr_{1}^{(tree,tlist)},
Branch^{tlist→tree} := constr_{2}^{(tree,tlist)},
Empty^{tlist} := constr_{3}^{(tree,tlist)},
Tcons^{tree→tlist→tlist} := constr_{4}^{(tree,tlist)}.

An example for a recursion constant is

(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}.

Here the fact that we deal with a simultaneous recursion (over tree and tlist), and that we define a constant of type tree → x, can all be inferred from what is given: the type tree → x is right there, and for tlist we can look up the simultaneously defined algebras.

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

. (Rec tree → τ_{1} tlist → τ_{2}).

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

+ Leaf  = λaa,
+ (Branch bs)  = λa.Branch(⊕ bs a),
⊕ Empty  = λa Empty,
⊕ (Tcons b bs)  = λa.Tcons(+ b a)(⊕ bs a).

We define + and ⊕ by means of the recursion operators R_{tree} and R_{tlist} with result types

τ_{1}  := tree → tree,
τ_{2}  := tree → tlist.

The step terms are

M_{1}  := λaa,
M_{2}  := λbsλg^{τ_{2}}λa.Branch(g a),
M_{3}  := λa Empty,
M_{4}  := λbλbsλf^{τ_{1}}λg^{τ_{2}}λa.Tcons(f a)(g a).

Then

+  := R_{tree}M⃗: tree → tree → tree,
⊕  := R_{tlist}M⃗: tlist → tree → tlist.

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

. κ_{i} = ρ_{1} → ⋯ → ρ_{m} → (σ⃗_{1} → α_{j_{1}}) → ⋯ → (σ⃗_{n} → α_{j_{n}}) → α_{j} ∈ KT(α⃗),

and consider constr_{i}^{μ⃗}N⃗. Then we write N⃗^{P} = N_{1}^{P} , x, N_{m}^{P} for the parameter arguments N_{1}^{ρ_{1}}, x, N_{m}^{ρ_{m}} and N⃗^{R} = N_{1}^{R}, x, N_{n}^{R} for the recursive arguments N_{m+1}^{σ⃗_{1}→μ_{j_{1}}} , x, N_{m+n}^{σ⃗_{n}→μ_{jn}}, and n^{R} 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 (2)  ↦M if x ∉FV(M), M not an abstraction
(R_{j}^{μ⃗,τ⃗} M⃗)^{μ_{j}→τ_{j}}(constr_{i}^{μ⃗}N⃗) ↦M_{i}N⃗ ((R_{j_{1}}^{μ⃗,τ⃗} M⃗) ∘ N_{1}^{R})x ((R_{j_{n}}^{μ⃗,τ⃗} M⃗) ∘ N_{n}^{R}) (3)

Here we have written R_{j}^{μ⃗,τ⃗} for R_{μ_{j}}^{μ⃗,τ⃗}, and ∘ means composition.

4.3. Internal representation of constants.

Every object constant has the internal representation

(constx  object-or-arity name uninst-type-or-formula subst

t-deg token-type arrow-types-or-repro-formulas),

where subst may have type, object and assumption variables in its domain. The type of the constant is the result of carrying out this substitution in uninst-type-or-formula (if this is a type; otherwise first substitute and then convert the formula into a type); free type variables may again occur in this type. Note that a formula will occur if name is Ex-Intro or Ex-Elim, and may occur if it is Rec. Examples for object constants are

(const Compose (α→β)→(β→γ)→α→γ (α ↦ρ, β ↦σ, γ ↦τ) ...)

    (const Eq α → α → boole (α ↦finalg) ...)
    (const E α → boole (α ↦finalgx))

(const Ex-Elim ∃x^{α}P (x) → (∀x^{α}.P (x) → Q) → Q

(α ↦τ, P^{(α)} ↦{ z^{τ} | A }, Q ↦{ | B }) ...)

object-or-arity is an object if this object cannot be changed, e.g.xby allowing user defined rules for the constant; otherwise, the associated object needs to be updated whenever a new rule is added, and we have the arity of those rules instead. The rules are of crucial importance for the correctness of a proof, and should not be invisibly buried in the denoted object taken as part of the constant (hence of any term involving it). Therefore we keep the rules of a program constant and also its denoted objects (depending on type substitutions) at a central place, a global variable PROGRAM-CONSTANTS which assigns to every name of such a constant the constant itself (with uninstantiated type), the rules presently chosen for it and also its denoted objects (as association list with type substitutions as keys). When a new rule has been added, the new objects for the program constant are computed, and the new list to be associated with the program constant is written in PROGRAM-CONSTANTS instead. All information on a program constant exept its denoted object and its computation and rewrite rules (i.e.xits type, degree of totality, arity and token type) is stable and hence can be kept as part of it. The token type can be either const (i.e.xconstant written as application) or one of: postfix-op,

prefix-op, binding-op, add-op, mul-op, rel-op, and-op, or-op, imp-op and
pair-op.

Constructor, accessors and tests for all kinds of constants:

(make-const obj-or-arity name kind uninst-type tsubst
  t-deg token-type . arrow-types-or-repro-formulas)
(const-to-object-or-arity const)
(const-to-name const)
(const-to-kind const)
(const-to-uninst-type const)
(const-to-tsubst const)
(const-to-t-deg const)
(const-to-token-type const)
(const-to-arrow-types-or-repro-formulas const)
(const?xx)
(const=?xx y)

The type substitution tsubst must be restricted to the type variables in

uninst-type. arrow-types-or-repro-formulas are only present for the Rec

constants. They are needed for the reproduction case.

From these we can define

                                        (const-to-type const)
                                        (const-to-tvars const)

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

                (constr-name? string)
                (constr-name-to-constr name <tsubst>)
                (constr-name-and-tsubst-to-constr name tsubst),

where in (constr-name-to-constr name <tsubst>), name is a string or else of

the form (Ex-Intro formula). If the optional tsubst is not present, the empty substitution is used.

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

          (display-constructors alg-name1 ...).

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

(pconst-name-to-pconst name)
(pconst-name-to-comprules name)
(pconst-name-to-rewrules name)
(pconst-name-to-inst-objs name)
(pconst-name-and-tsubst-to-object name tsubst)
(pconst-name-to-object name).

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

                         (display-program-constants name1 ...).

To add and remove program constants we use

                       (add-program-constant name type <rest>)
                       (remove-program-constant symbol);

rest consists of an initial segment of the following list: t-deg (default 0), token-type (default const) and arity (default maximal number of argument types).

To add and remove computation and rewrite rules we have

(add-computation-rule lhs rhs)
(add-rewrite-rule lhs rhs)
(remove-computation-rules-for lhs)
(remove-rewrite-rules-for lhs).

To generate our constants with fixed rules we use

(finalg-to-=-const finalg)  equality
(finalg-to-e-const finalg)  existence
(arrow-types-to-rec-const .xarrow-types)  recursion

(ex-formula-and-concl-to-ex-elim-const
ex-formula concl)

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 einfxgen: arrow-types-to-cases-const und zur Behandlung von

Beweisen all-formulas-to-cases-const]

5 Predicate variables and constants

[next] [prev] [prev-tail] [tail] [up]

5. Predicate variables and constants

S:Psyms

5.1. Predicate variables.

SS:PredVars A predicate variable of arity ρ_{1}, x, ρ_{n} is a placeholder for a formula A with distinguished (different) variables x_{1}, x, x_{n} of types ρ_{1}, x, ρ_{n}. Such an entity is called a comprehension term, written { x_{1}, x, x_{n} | A }.

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.xformulas 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, x, Q0, x range over comprehension terms with Harrop formulas, and P^0, P^1, P^2, x 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

                                        (make-arity type1 ...)
                                        (arity-to-types arity)

To display an arity we have

.  (arity-to-string arity)

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

                                (pvar-name?xstring)
                                (pvar-name-to-arity pvar-name)

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

                               (add-pvar-name name1 ...xarity)
                               (remove-pvar-name name1 ...)

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

(make-pvar arity index h-deg name)  constructor
(pvar-to-arity pvar)  accessor
(pvar-to-index pvar)  accessor
(pvar-to-h-deg pvar)  accessor
(pvar-to-name pvar)  accessor

(pvar?xx)
(equal-pvars?xpvar1 pvar2)

For convenience we have the function

       (mk-pvar arity <index> <h-deg> <name>)

The arity is a required argument; the remaining arguments are optional. The default for index is −1, for h-deg is 1 (i.e.xHarrop-formula) and for name it is

given by (default-pvar-name arity).

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.

SS:PredConsts We also allow predicate constants. The general reason for having them is that we need predicates to be axiomatized, e.g.xEqual and Total (which are not placeholders for formulas). Prime formulas built from predicate constants do not give rise to extracted terms, and cannot be substituted for.

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 ρ_{1}xρ_{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

                          (add-predconst-name name1 ...xarity)
                          (remove-predconst-name name1 ...)

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

(make-predconst uninst-arity tsubst index name)  constructor
(predconst-to-uninst-arity predconst)  accessor
(predconst-to-tsubst predconst)  accessor
(predconst-to-index predconst)  accessor
(predconst-to-name predconst)  accessor

(predconst?xx)

Moreover we need

                  (predconst-name? name)
                  (predconst-name-to-arity predconst-name).
                  (predconst-to-string predconst).

5.3. Inductively defined predicate constants.

SS:IDPredConsts As we have seen, type variables allow for a general treatment of inductively generated types μα⃗ κ⃗. Similarly, we can use predicate variables to inductively generate predicates μX⃗ K⃗.

More precisely, we allow the formation of inductively generated predicates μX⃗ K⃗, where X⃗ = (X_{j})_{j=1,x,N} is a list of distinct predicate variables, and K⃗ = (K_{i})_{i=1,x,k} is a list of constructor formulas (or “clauses”) containing X_{1}, x, X_{N} in strictly positive positions only.

To introduce inductively defined predicates we use

.  add-ids.

An example is

(add-idsx(listx(listx"Ev"x(make-arityx(pyx"nat"))x"algEv")
xxxxxxxxxxxxxxxx(listx"Od"x(make-arityx(pyx"nat"))x"algOd"))
xxxxxxxxxx'("Evx0"x"InitEv")
xxxxxxxxxx'("allncxn.Odxnx->xEv(n+1)"x"GenEv")
xxxxxxxxxx'("Odx1"x"InitOd")
xxxxxxxxxx'("allncxn.Evxnx->xOd(n+1)"x"GenOd"))

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.x“negative”).

Here are some further examples of inductively defined predicates:

(add-ids
xxx(listx(listx"Even"x(make-arityx(pyx"nat"))x"algEven"))
xxx'("Evenx0"x"InitEven")
xxx'("allncxn.Evenxnx->xEven(n+2)"x"GenEven"))
x
x(add-ids
xxx(listx(listx"Acc"x(make-arityx(pyx"nat"))x"algAcc"))
xxx'("allncxn.(allxm.m<nx->xAccxm)x->xAccxn"x"GenAccSup"))
x
x(add-idsx(listx(listx"OrID"x(make-arity)x"algOrID"))
xxxxxxxxxx'("P^1x->xOrID"x"InlOrID")
xxxxxxxxxx'("P^2x->xOrID"x"InrOrID"))
x
x(add-ids
xxx(listx(listx"EqID"x(make-arityx(pyx"alpha")x(pyx"alpha"))
xxxxxxxxxxxxxxx"algEqID"))
xxx'("allncxx^xEqIDxx^xx^"x"GenEqID"))
x
x(add-idsx(listx(listx"ExID"x(make-arity)x"algExID"))
xxxxxxxxxx'("allncxx^.Q^xx^x->xExID"x"GenExID"))
x
x(add-ids
xxx(listx(listx"FalsityID"x(make-arity)x"algFalsityID")))

6 Terms and objects

[next] [prev] [prev-tail] [tail] [up]

6. Terms and objects

Terms Terms are built from (typed) variables and constants by abstraction, application, pairing, formation of left and right components (i.e.xprojections) and the if-construct.

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.xin 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.xa closed term built from constructors only. However, we do not require this.

We have constructors, accessors and tests for variables

                     (make-term-in-var-form var)  constructor
                     (term-in-var-form-to-var term)  accessor,
                     (term-in-var-form?xterm)  test,

for constants

(make-term-in-const-form const)  constructor
(term-in-const-form-to-const term)  accessor
(term-in-const-form?xterm)  test,

for abstractions

(make-term-in-abst-form var term)  constructor
(term-in-abst-form-to-var term)  accessor
(term-in-abst-form-to-kernel term)  accessor
(term-in-abst-form?xterm)  test,

for applications

(make-term-in-app-form term1 term2)  constructor
(term-in-app-form-to-op term)  accessor
(term-in-app-form-to-arg term)  accessor
(term-in-app-form?xterm)  test,

for pairs

(make-term-in-pair-form term1 term2)  constructor
(term-in-pair-form-to-left term)  accessor
(term-in-pair-form-to-right term)  accessor
(term-in-pair-form?xterm)  test,

for the left and right component of a pair

(make-term-in-lcomp-form term)  constructor
(make-term-in-rcomp-form term)  constructor
(term-in-lcomp-form-to-kernel term)  accessor
(term-in-rcomp-form-to-kernel term)  accessor
(term-in-lcomp-form?xterm)  test
(term-in-rcomp-form?xterm)  test

and for if-constructs

(make-term-in-if-form test alts .xrest)  constructor
(term-in-if-form-to-test term)  accessor
(term-in-if-form-to-alts term)  accessor
(term-in-if-form-to-rest term)  accessor
(term-in-if-form?xterm)  test.

where in make-term-in-if-form, rest is either empty or an all-formula.

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.

               (mk-term-in-app-form term term1 ...)  constructor
               (term-in-app-form-to-final-op term)  accessor
               (term-in-app-form-to-args term)  accessor,

Also for abstraction it is convenient to have a more general constructor taking arbitrary many variables to be abstracted one after the other

                          (mk-term-in-abst-form var1 ...xterm).

We also allow vector notation for recursion (cf.xJoachimski and Matthes [8]).

Moreover we need

                                       (term?xx)
                                       (term=?xterm1 term2)
                                       (terms=?xterms1 terms2)
                                       (term-to-type term)
                                       (term-to-free term)
                                       (term-to-bound term)
                                       (term-to-t-deg term)
                                       (synt-total?xterm)
                                       (term-to-string term).

6.1. Normalization.

We need an operation which transforms a term into its normal form w.r.t.xthe 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.

                       (nbe-make-object type value)  constructor
                       (nbe-object-to-type object)  accessor
                       (nbe-object-to-value object)  accessor
                       (nbe-object?xx)  test.

To work with objects, we need

                       (nbe-object-apply function-obj arg-obj)

Again it is convenient to have a more general application operation available, which takes arbitrary many arguments and works for ordinary application as well as for component formation. We also need an operation composing two unary function objects.

              (nbe-object-app function-obj arg-obj1 ...)
              (nbe-object-compose function-obj1 function-obj2)

For ground type values we need constructors, accessors and tests. To make constructors “self-evaluating”, a constructor value has the form

.  (constr-value name objs delayed-constr),

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

                 (nbe-make-constr-value name objs)  constructor
                 (nbe-constr-value-to-name value)  accessor
                 (nbe-constr-value-to-args value)  accessor
                 (nbe-constr-value-to-constr value)  accessor
                 (nbe-constr-value?xvalue)  test
                 (nbe-fam-value?xvalue)  test.

The essential function which “animates” the program constants according to the given computation and rewrite rules is

                     (nbe-pconst-and-tsubst-and-rules-to-object
                        pconstxtsubstxcomprulesxrewrules)

Using it we can the define an evaluation function, which assigns to a term and an environment a semantical object:

                 (nbe-term-to-object term bindings)  evaluation.

Here bindings is an association list assigning objects of the same type to variables. In case a variable is not assigned anything in bindings, by default we assign the constant term family of this variable, which always is an object of the correct type.

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

(nbe-constructor-pattern?xterm)  test
(nbe-inst?xconstr-pattern obj)  test
(nbe-genargs constr-pattern obj)  generalized arguments

(nbe-extract termfam)  extracts a term from a family

(nbe-match pattern term)

Then we can define

                               (nbe-reify object)  reification
                               (nbe-reflect term)  reflection

and by means of these

                        (nbe-normalize-term term)  normalization,

abbreviated nt.

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

                       (term-substitute term tosubst)
                       (term-subst term arg val)
                       (compose-o-substitutions subst1 subst2)

The o in compose-o-substitutions indicates that we substitute for object variables. However, since this is the most common form of substitution, we also

write compose-substitutions instead.

Display functions for substitutions are

                                (display-substitution subst)
                                (substitution-to-string subst)

7 Formulas and comprehension terms

[next] [prev] [prev-tail] [tail] [up]

7. Formulas and comprehension terms S:Formulas A prime formula can have the form

(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:

                     (exca (x1...) formula)  arithmetical version
                     (excl (x1 ...) formula)  logical version.

Here we allow that the quantified variable is formed without ^, i.e.xranges over total objects only.

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:

(atom-form?xformula)
(predicate-form?xformula)
(prime-form?xformula)
(imp-form?xformula)
(and-form?xformula)
(tensor-form?xformula)
(all-form?xformula)
(ex-form?xformula)
(allnc-form?xformula)
(exnc-form?xformula)
(exca-form?xformula)
(excl-form?xformula)

and also

(quant-prime-form?xformula)
(quant-free?xformula).

We need constructors and accessors for prime formulas

        (make-atomic-formula boolean-term)
        (make-predicate-formula predicate term1 ...)
        atom-form-to-kernel
        predicate-form-to-predicate
        predicate-form-to-args.

We also have constructors for special atomic formulas

(make-eq term1 term2)  constructor for equalities
(make-= term1 term2)  constructor for equalities on finalgs
(make-total term)  constructor for totalities
(make-e term)  constructor for existence on finalgs

truth
falsity
falsity-log.

We need constructors and accessors for implications

               (make-imp premise conclusion)  constructor
               (imp-form-to-premise imp-formula)  accessor
               (imp-form-to-conclusion imp-formula)  accessor,

conjunctions

                    (make-and formula1 formula2)  constructor
                    (and-form-to-left and-formula)  accessor
                    (and-form-to-right and-formula)  accessor,

tensors

(make-tensor formula1 formula2)  constructor
(tensor-form-to-left tensor-formula)  accessor
(tensor-form-to-right tensor-formula)  accessor,

universally quantified formulas

     (make-all var formula)  constructor
     (all-form-to-var all-formula)  accessor
     (all-form-to-kernel all-formula)  accessor,

existentially quantified formulas

(make-ex var formula)  constructor
(ex-form-to-var ex-formula)  accessor
(ex-form-to-kernel ex-formula)  accessor,

universally quantified formulas without computational content

(make-allnc var formula)  constructor
(allnc-form-to-var allnc-formula)  accessor
(allnc-form-to-kernel allnc-formula)  accessor,

existentially quantified formulas without computational content

(make-exnc var formula)  constructor
(exnc-form-to-var exnc-formula)  accessor
(exnc-form-to-kernel exnc-formula)  accessor,

existentially quantified formulas in the sense of classical arithmetic

(make-exca var formula)  constructor
(exca-form-to-var exca-formula)  accessor
(exca-form-to-kernel exca-formula)  accessor,

existentially quantified formulas in the sense of classical logic

                (make-excl var formula)  constructor
                (excl-form-to-var excl-formula)  accessor
                (excl-form-to-kernel excl-formula)  accessor.

For convenience we also have as generalized constructors

(mk-imp formula formula1 ...)  implication
(mk-neg formula1 ...)  negation
(mk-neg-log formula1 ...)  logical negation
(mk-and formula formula1 ...)  conjunction
(mk-tensor formula formula1 ...) tensor
(mk-all var1 ...xformula)  all-formula
(mk-ex var1 ...xformula)  ex-formula
(mk-allnc var1 ...xformula)  allnc-formula
(mk-exnc var1 ...xformula)  exnc-formula

(mk-exca var1 ...xformula)  classical ex-formula (arithmetical)
(mk-excl var1 ...xformula)  classical ex-formula (logical)

and as generalized accessors

           (imp-form-to-premises-and-final-conclusion formula)
           (tensor-form-to-parts formula)
           (all-form-to-vars-and-final-kernel formula)
           (ex-form-to-vars-and-final-kernel formula)

and similarly for exca-forms and excl-forms. Occasionally it is convenient to have

 (imp-form-to-premises formula <n>)  all (first n) premises

 (imp-form-to-final-conclusion formula <n>)

where the latter computes the final conclusion (conclusion after removing the first n premises) of the formula.

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

(make-quant-formula quant var1 ...xkernel)  constructor
(quant-form-to-quant quant-form)  accessor
(quant-form-to-vars quant-form)  accessor
(quant-form-to-kernel quant-form)  accessor
(quant-form?xx)  test.

and for convenience also

.  (mk-quant quant var1 ... formula).

To fold and unfold formulas we have

                             (fold-formula formula)
                             (unfold-formula formula).

To test equality of formulas up to normalization and α-equality we use

(classical-formula=?xformula1 formula2)
(formula=?xformula1 formula2),

where in the first procedure we unfold before comparing. Morever we need

(formula-to-freexformula),
(nbe-formula-to-typexformula),
(formula-to-prime-subformulasxformula),

Constructors, accessors and a test for comprehension terms are

(make-cterm var1 ...xformula)  constructor
(cterm-to-vars cterm)  accessor
(cterm-to-formula cterm)  accessor
(cterm?xx)  test.

Moreover we need

(cterm-to-free cterm)
(cterm=?xx)
(classical-cterm=?xx)
(fold-cterm cterm)
(unfold-cterm cterm).

Normalization of formulas is done with

                      (normalize-formula formula)  normalization,

abbreviated nf.

To check equality of formulas we use

                       (classical-formula=? formula1 formula2)
                       (formula=? formula1 formula2)

where the former unfolds the classical existential quantifiers and normalizes all subterms in its formulas.

Display functions for formulas and comprehension terms are

                                   (formula-to-string formula)
                                   (cterm-to-string cterm).

The former is abbreviated nf.

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.

                         (formula-substitute formula topsubst)
                         (formula-subst formula arg val)
                         (cterm-substitute cterm topsubst)
                         (cterm-subst cterm arg val)

Display functions for predicate substitutions are

(display-p-substitution psubst)
(p-substitution-to-string psubst)

8 Assumption variables and constants

[next] [prev] [prev-tail] [tail] [up]

8. Assumption variables and constants

S:AssumptionVarConst

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

                     (make-avar formula index name)  constructor
                     (avar-to-formula avar)  accessor
                     (avar-to-index avar)  accessor
                     (avar-to-name avar)  accessor
                     (avar?xx)  test
                     (avar=?xavar1 avar2)  test.

For convenience we have the function

                              (mk-avar formula <index> <name>)

The formula is a required argument; however, the remaining arguments are optional. The default for the name string is u. We also require that a function

                                 (formula-to-new-avar formula)

is defined that returns an assumption variable of the requested formula different from all assumption variables that have ever been returned by any of the specified functions so far.

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 ∀x̂^{α}.P̂(x̂) → ∃x̂^{α}P̂(x̂) (α ↦τ, P̂^{(α)} ↦{ ẑ^{τ} | A }))
(aconst Ex-Elim ∃x̂^{α}P̂(x̂) → (∀x̂^{α}.P̂(x̂) → Q̂) → Q̂
(α ↦τ, P̂^{(α)} ↦{ ẑ^{τ} | A }, Q̂ ↦{ | 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.xfor all of the forms listed above.

(make-aconst name kind uninst-formula tpsubst

    repro-formula1 ...)  constructor
(aconst-to-name aconst)  accessor
(aconst-to-kind aconst)  accessor
(aconst-to-uninst-formula aconst)  accessor
(aconst-to-tpsubst aconst)  accessor
(aconst-to-repro-formulas aconst)  accessor
(aconst?xx)  test.

To construct the formula associated with an aconst, it is useful to separate the instantiated formula from the variables to be generalized. The latter can be obtained as free variables in inst-formula. We therefore provide

                               (aconst-to-inst-formula aconst)
                               (aconst-to-formula aconst)

We also provide

                                (aconst? aconst)
                                (aconst=?xaconst1 aconst2)
                                (aconst-without-rules?xaconst)
                                (aconst-to-stringxaconst)

8.2. Axiom constants.

SS:AxiomConst We use the natural numbers as a prototypical finitary algebra; recall Figurex1. Assume that n, p are variables of type nat, boole. Let ≈ denote the equality relation in the model. Recall the domain of type boole, consisting of tt, ff and the bottom element bb. The boolean valued functions equality = _{nat}: nat → nat → boole and existence (definedness, totality) e_{nat}: nat → boole need to be continuous. So we have

=(0, 0)  ≈ tt
=(0, Sn̂) ≈ =(Sn̂, 0)  ≈ ff  e(0)  ≈ tt
=(Sn̂_{1}, Sn̂_{2})  ≈ =(n̂_{1}, n̂_{2})  e(Sn̂)  ≈ e(n̂)
=(bb_{nat}, n̂) ≈ =(n̂, bb_{nat})  ≈ bb  e(bb_{nat})  ≈ bb
=(∞_{nat}, n̂) ≈ =(n̂, ∞_{nat})  ≈ bb  e(∞_{nat})  ≈ bb

Write T, F for atom(tt), atom(ff), r = s for atom(=(r, s)) and E(r) for atom(e(r)). We stipulate as axioms

T  Truth-Axiom
x̂ ≈ x̂  Eq-Refl

x̂_{1} ≈ x̂_{2} → x̂_{2} ≈ x̂_{1}  Eq-Symm
x̂_{1} ≈ x̂_{2} → x̂_{2} ≈ x̂_{3} → x̂_{1} ≈ x̂_{3}  Eq-Trans
∀x̂f̂_{1}x̂ ≈ f̂_{2}x̂ → f̂_{1} ≈ f̂_{2}  Eq-Ext
x̂_{1} ≈ x̂_{2} → P̂(x̂_{1}) → P̂(x̂_{2})  Eq-Compat
Total_{ρ→σ}(f̂) ↔ ∀x̂.Total_{ρ}(x̂) → Total_{σ}(f̂x̂)  Total

Total_{ρ}(c)  Constr-Total

Total(cx̂) → Total(x̂_{i})  Constr-Total-Args

and for every finitary algebra, e.g.xnat

n̂_{1} ≈ n̂_{2} → E(n̂_{1}) → n̂_{1} = n̂_{2}  Eq-to-=-1-nat
n̂_{1} ≈ n̂_{2} → E(n̂_{2}) → n̂_{1} = n̂_{2}  Eq-to-=-2-nat

n̂_{1} = n̂_{2} → n̂_{1} ≈ n̂_{2}  =-to-Eq-nat
n̂_{1} = n̂_{2} → E(n̂_{1})  =-to-E-1-nat
n̂_{1} = n̂_{2} → E(n̂_{2})  =-to-E-2-nat
Total(n̂) → E(n̂)  Total-to-E-nat
E(n̂) → Total(n̂)  E-to-Total-nat

Here c is a constructor. Notice that in Total(cx̂) → Total(x̂_{i}), the type of (cx̂) need not be a finitary algebra, and hence x̂_{i} may have a function type.

Remark. (E(n̂_{1}) → n̂_{1} = n̂_{2}) → (E(n̂_{2}) → n̂_{1} = n̂_{2}) → n̂_{1} ≈ n̂_{2} is not valid in our intended model (see Figurex1), since we have two distinct undefined objects bb_{nat} and ∞_{nat}.

We abbreviate

∀x̂.Total_{ρ}(x̂) → A  by  ∀xA,
∃x̂.Total_{ρ}(x̂) ∧ A  by  ∃xA.

Formally, these abbreviations appear as axioms

∀xP̂(x) → ∀x̂.Total(x̂) → P̂(x̂)  All-AllPartial
(∀x̂.Total(x̂) → P̂(x̂)) → ∀xP̂(x)  AllPartial-All
∃xP̂(x) → ∃x̂.Total(x̂) ∧ P̂(x̂)  Ex-ExPartial
(∃x̂.Total(x̂) ∧ P̂(x̂)) → ∃xP̂(x)  ExPartial-Ex

and for every finitary algebra, e.g.xnat

∀nP̂(n) → ∀n̂.E(n̂) → P̂(n̂)  All-AllPartial-nat
(∃n̂.E(n̂) ∧ P̂(n̂)) → ∃nP̂(n)  ExPartial-Ex-nat

Notice that AllPartial-All-nat i.e.x(∀n̂.E(n̂) → P̂(n̂)) → ∀nP̂(n) is provable (since E(n) ↦T). Similarly, Ex-ExPartial-nat, i.e.x∃nP̂(n) → ∃n̂.E(n̂) ∧ P̂(n̂) is provable.

Finally we have axioms for the existential quantifier

∀x̂^{α}.P̂(x̂) → ∃x̂^{α}P̂(x̂)  Ex-Intro
∃x̂^{α}P̂(x̂) → (∀x̂^{α}.P̂(x̂) → Q̂) → Q̂  Ex-Elim

The assumption constants corresponding to these axioms are

truth-aconst  for Truth-Axiom
eq-refl-aconst  for Eq-Refl
eq-symm-aconst  for Eq-Symm
eq-trans-aconst  for Eq-Trans
ext-aconst  for Eq-Ext
eq-compat-aconst  for Eq-Compat
total-aconst  for Total
(finalg-to-eq-to-=-1-aconst finalg)  for Eq-to-=-1
(finalg-to-eq-to-=-2-aconst finalg)  for Eq-to-=-2
(finalg-to-=-to-eq-aconst finalg)  for =-to-Eq
(finalg-to-=-to-e-1-aconst finalg)  for =-to-E-1
(finalg-to-=-to-e-2-aconst finalg)  for =-to-E-2
(finalg-to-total-to-e-aconst finalg)  for Total-to-E
(finalg-to-e-to-total-aconst finalg)  for E-to-Total
all-allpartial-aconst  for All-AllPartial
allpartial-all-aconst  for AllPartial-All
ex-expartial-aconst  for Ex-ExPartial
expartial-ex-aconst  for ExPartial-Ex
(finalg-to-all-allpartial-aconst finalg)  for All-AllPartial
(finalg-to-expartial-ex-aconst finalg)  for ExPartial-Ex

We now spell out what precisely we mean by induction over simultaneous free algebras μ⃗ = μα⃗ κ⃗, with goal formulas ∀x_{j}^{μ_{j}} P̂_{j}(x_{j}). For the constructor type . κ_{i} = ρ⃗ → (σ⃗_{1} → α_{j_{1}}) → ⋯ → (σ⃗_{n} → α_{j_{n}}) → α_{j} ∈ KT(α⃗) we have the step formula

D_{i} := ∀y_{1}^{ρ_{1}}, x, y_{m}^{ρ_{m}}, y_{m+1}^{σ⃗_{1}→μ_{j_{1}}} , x, y_{m+n}^{σ⃗_{n}→μ_{jn}} . ∀x⃗^{σ⃗^{1}} P̂_{j_{1}}(y_{m+1}x⃗) → ⋯ →
∀x⃗^{σ⃗^{n}} P̂_{j_{n}}(y_{m+n}x⃗) →
P̂_{j}(constr_{i}^{μ⃗}(y⃗)).

Here y⃗ = y_{1}^{ρ_{1}}, x, y_{m}^{ρ_{m}}, y_{m+1}^{σ⃗_{1}→μ_{j_{1}}} , x, y_{m+n}^{σ⃗_{n}→μ_{jn}} are the components of the object constr_{i}^{μ⃗}(y⃗) of type μ_{j} under consideration, and . ∀xσ⃗_{1} P̂_{j_{1}}(y_{m+1}x⃗), …, ∀xσ⃗_{n} P̂_{j_{n}}(y_{m+n}x⃗) are the hypotheses available when proving the induction step. The induction axiom Ind_{μ_{j}} then proves the formula . Ind_{μ_{j}}: D_{1} → ⋯ → D_{k} → ∀x_{j}^{μ_{j}} P̂_{j}(x_{j}). We will often write Ind_{j} for Ind_{μ_{j}}. An example is

E_{1} → E_{2} → E_{3} → E_{4} → ∀x_{1}^{tree}P̂_{1}(x_{1})

with

E_{1} := P̂_{1}(Leaf),

E_{2} := ∀x^{tlist}.P̂_{2}(x) → P̂_{1}(Branch(x)),

E_{3} := P̂_{2}(Empty),

E_{4} := ∀x_{1}^{tree}, x_{2}^{tlist}.P̂_{1}(x_{1}) → P̂_{2}(x_{2}) → P̂_{2}(Tcons(x_{1}, x_{2})).

Here the fact that we deal with a simultaneous induction (over tree and tlist), and that we prove a formula of the form ∀x^{tree}x, can all be inferred from what is given: the ∀x^{tree}x is right there, and for tlist we can look up the simultaneously defined algebras. – The internal representation is

(aconst Ind E_{1} → E_{2} → E_{3} → E_{4} → ∀x_{1}^{tree}P̂_{1}(x_{1})

(P̂_{1} ↦{ x_{1}^{tree} | A_{1} }, P̂_{2} ↦{ x_{2}^{tlist} | A_{2} }))

A simplified version (without the recursive calls) of the induction axiom is the following cases axiom.

(aconst Cases E_{1} → E_{2} → ∀x_{1}^{tree}P̂_{1}(x_{1}) (P̂_{1} ↦{ x_{1}^{tree} | A_{1} }))

with

E_{1} := P̂_{1}(Leaf),
E_{2} := ∀x^{tlist}P̂_{1}(Branch(x)).

However, rather than using this as an assumption constant we will – parallel to the if-construct for terms – use a cases-construct for proofs. This does not change our notion of proof; it is done to have the if-construct in the extracted programs.

The assumption constants corresponding to these axioms are generated by

        (all-formulas-to-ind-aconst all-formula1 ...)  for Ind
        (all-formula-to-cases-aconst all-formula)  for Cases

For the introduction and elimination axioms Ex-Intro and Ex-Elim for the existential quantifier we provide

      (ex-formula-to-ex-intro-aconst ex-formula)
      (ex-formula-and-concl-to-ex-elim-aconst ex-formula concl)

and similarly for exnc instead of ex.

To deal with inductively defined predicate constants, we need additional axioms with names “Intro” and “Elim”, which can be generated by

                (number-and-idpredconst-to-intro-aconst i idpc)
                (imp-formulas-to-elim-aconst imp-formula1x...);

here an imp-formula is expected to have the form I(x⃗) → A.

8.3. Theorems.

SS:Theorems A theorem is a special assumption constant. Theorems are normally created after successfully completing an interactive proof. One may also create a theorem from an explicitely given (closed) proof. The command is

                      (add-theorem string .xopt-proof)  or save

From a theorem name we can access its aconst, its (original) proof and also its instantiated proof by

(theorem-name-to-aconst string)
(theorem-name-to-proof string)
(theorem-name-to-inst-proof string)

We also provide

     (remove-theorem string1 ...)
     (display-theorems string1 ...)

Initially we provide the following theorems

atom(p) → p = tt  Atom-True
(atom(p) → F) → p = ff  Atom-False
F → atom(p)  Efq-Atom
((atom(p) → F) → F) → atom(p)  Stab-Atom

and for every finitary algebra, e.g.xnat

n = n  =-Refl-nat

n̂_{1} = n̂_{2} → n̂_{2} = n̂_{1}  =-Symm-nat
n̂_{1} = n̂_{2} → n̂_{2} = n̂_{3} → n̂_{1} = n̂_{3}  =-Trans-nat

Proof of Atom-True. By Ind. In case tt use Eq-Compat with tt ≈ =(tt, tt) to infer atom(=(tt, tt)) (i.e.xtt = tt) from atom(tt). In case ff use Eq-Compat with ff ≈ =(ff, tt) to infer atom(=(ff, tt)) (i.e.xff = tt) from atom(ff). x

Proof of Atom-False. Use Ind, and Truth-Axiom in both cases. – Notice that the more general (atom(p̂) → F) → p̂ = ff does not hold with bb for p̂, since =(bb, ff) ≈ bb. x Proof of Efq-Atom. Again by Ind. In case tt use Truth-Axiom, and the case ff is obvious. x

Proof of Stab-Atom. By Ind. In case tt use Truth-Axiom, and the case ff is obvious. x

Remark. Notice that from Efq-Atom one easily obtains F → A for every formula A all whose strictly positions occurrences of prime formulas are of the form atom(r), by induction on A. For all other formulas we shall make use of the global assumption Efq: F → P̂ (cf.xSectionx8.4). Similarly, Notice that from Stab-Atom one again obtains ((A → F) → F) → A for every formula A all whose strictly positions occurrences of prime formulas are of the form atom(r), by induction on A. For all other formulas we shall make use of the global assumption Stab: ((P̂ → F) → F) → P̂ (cf.xSectionx8.4).

Proof of =-Refl-nat. Use Ind, and Truth-Axiom in both cases. – Notice that n̂ = n̂ does not hold, since =(bb, bb) ≈ bb. x

Here are some other examples of theorems; we give the internal representation as assumption constants, which show how the assumed formula is split into an uninstantiated formula and a substitution, in this case a type substitution α ↦ρ, an object substitution f^{α→nat} ↦g^{ρ→nat} and a predicate variable substitution P̂^{(α)} ↦{ ẑ^{ρ} | A }.

  (aconst Cvind-with-measure-11

∀f^{α→nat}. (∀x^{α}.∀y(f(y)<f(x) → P̂(y)) → P̂(x) ) → ∀xP̂(x)

(α ↦ρ, f^{α→nat} ↦g^{ρ→nat}, P̂^{(α)} ↦{ ẑ^{ρ} | A })).

  (aconst Minpr-with-measure-l11

∀f^{α→nat}.∃^{cl}x^{α}P̂(x) → ∃^{cl}x.P̂(x)!∀y.f(y)<f(x) → P̂(y) → ⊥

(α ↦ρ, f^{α→nat} ↦g^{ρ→nat}, P̂^{(α)} ↦{ ẑ^{ρ} | A })).

Here ∃^{cl} is the classical existential quantifier defined by ∃^{cl}xA := ∀x(A → ⊥) → ⊥ with the logical form of falsity ⊥ (as opposed to the arithmetical form (atomxff)). l indicates “logic” (we have used the logical form of falsity), the first 1 that we have one predicate variable P̂, and the second that we quantify over just one variable x. Both theorems can easily be generalized to more such parameters.

When dealing with classical logic it will be useful to have

(P̂ → P̂_{1}) → ((P̂ → ⊥) → P̂_{1}) → P̂_{1}  Cases-Log

The proof uses the global assumption Stab-Log (see below) for P̂_{1}; hence we cannot extract a term from it.

The assumption constants corresponding to these theorems are generated by

                                 (theorem-name-to-aconst name)

8.4. Global assumptions.

SS:GlobalAss A global assumption is a special assumption constant. It provides a proposition whose proof does not concern us presently. Global assumptions are added, removed and displayed by

         (add-global-assumption name formula) (abbreviated aga)

         (remove-global-assumption string1 ...)
         (display-global-assumptions string1 ...)

We initially supply global assumptions for ex-falso-quodlibet and stability, both in logical and arithmetical form (for our two forms of falsity).

⊥ → P̂  Efq-Log

((P̂ → ⊥) → ⊥) → P̂  Stab-Log

F → P̂  Efq

((P̂ → F) → F) → P̂  Stab

The assumption constants corresponding to these global assumptions are generated by

(global-assumption-name-to-aconst name)

9 Proofs

[next] [prev] [prev-tail] [tail] [up]

9. Proofs

Proof Proofs are built from assumption variables and assumption constants (i.e.xaxioms, theorems and global assumption) by the usual rules of natural deduction, i.e.xintroduction and elimination rules for implication, conjunction and universal quantification. From a proof we can read off its context, which is an ordered list of object and assumption variables.

9.1. Constructors and accessors.

We have constructors, accessors and tests for assumption variables

               (make-proof-in-avar-form avar)  constructor
               (proof-in-avar-form-to-avar proof)  accessor,
               (proof-in-avar-form?xproof)  test,

for assumption constants

   (make-proof-in-aconst-form aconst)  constructor
   (proof-in-aconst-form-to-aconst proof)  accessor
   (proof-in-aconst-form?xproof)  test,

for implication introduction

(make-proof-in-imp-intro-form avar proof)  constructor
(proof-in-imp-intro-form-to-avar proof)  accessor
(proof-in-imp-intro-form-to-kernel proof)  accessor
(proof-in-imp-intro-form?xproof)  test,

for implication elimination

(make-proof-in-imp-elim-form proof1 proof2)  constructor
(proof-in-imp-elim-form-to-op proof)  accessor
(proof-in-imp-elim-form-to-arg proof)  accessor
(proof-in-imp-elim-form?xproof)  test,

for and introduction

(make-proof-in-and-intro-form proof1 proof2)  constructor
(proof-in-and-intro-form-to-left proof)  accessor
(proof-in-and-intro-form-to-right proof)  accessor
(proof-in-and-intro-form?xproof)  test,

for and elimination

(make-proof-in-and-elim-left-form proof)  constructor
(make-proof-in-and-elim-right-form proof)  constructor
(proof-in-and-elim-left-form-to-kernel proof)  accessor
(proof-in-and-elim-right-form-to-kernel proof)  accessor
(proof-in-and-elim-left-form?xproof)  test
(proof-in-and-elim-right-form?xproof)  test,

for all introduction

     (make-proof-in-all-intro-form var proof)  constructor
     (proof-in-all-intro-form-to-var proof)  accessor
     (proof-in-all-intro-form-to-kernel proof)  accessor
     (proof-in-all-intro-form?xproof)  test,

for all elimination

(make-proof-in-all-elim-form proof term)  constructor
(proof-in-all-elim-form-to-op proof)  accessor
(proof-in-all-elim-form-to-arg proof)  accessor
(proof-in-all-elim-form?xproof)  test

and for cases-constructs

(make-proof-in-cases-form test alt1 ...)  constructor
(proof-in-cases-form-to-test proof)  accessor
(proof-in-cases-form-to-alts proof)  accessor
(proof-in-cases-form-to-rest proof)  accessor
(proof-in-cases-form?xproof)  test.

It is convenient to have more general introduction and elimination operators that take arbitrary many arguments. The former works for implication-introduction and all-introduction, and the latter for implication-elimination, and-elimination and all-elimination.

                (mk-proof-in-intro-form x1 ...xproof)
                (mk-proof-in-elim-form proof arg1 ...)
                (proof-in-intro-form-to-kernel-and-vars proof)
                (proof-in-elim-form-to-final-op proof)
                (proof-in-elim-form-to-args proof).

(mk-proof-in-intro-form x1 ...xproof) is formed from proof by first

abstracting x1, then x2 and so on. Here x1, x2 … can be assumption or object variables. We also provide

                 (mk-proof-in-and-intro-form proof proof1 ...)

In our setup there are axioms rather than rules for the existential quantifier. However, sometimes it is useful to construct proofs as if an existence introduction rule would be present; internally then an existence introduction axiom is used.

(make-proof-in-ex-intro-form term ex-formula proof-of-inst)
(mk-proof-in-ex-intro-formx.x
terms-and-ex-formula-and-proof-of-inst)

Moreover we need

(proof?xx)
(proof=?xproof1 proof2)
(proofs=?xproofs1 proofs2)
(proof-to-formula proof)
(proof-to-context proof)
(proof-to-free proof)
(proof-to-free-avars proof)
(proof-to-bound-avars proof)
(proof-to-free-and-bound-avars proof)
(proof-to-aconsts-without-rules proof).
(proof-to-aconsts proof).

To work with contexts we need

                                (context-to-varsxcontext)
                                (context-to-avarsxcontext)
                                (context=?xcontext1 context2).

9.2. Normalization.

Normalization of proofs will be done by reduction to normalization of terms. (1) Construct a term from the proof. To do this properly, create for every free avar in the given proof a new variable whose type comes from the formula of the avar; store this information. Note that in this construction one also has to create new variables for the bound avars. Similary to avars we have to treat assumption constants which are not axioms, i.e.xtheorems or global assumptions. (2) Normalize the resulting term. (3) Reconstruct a normal proof from this term, the end formula and the stored information. – The critical variables are carried along for efficiency reasons.

To assign recursion constants to induction constants, we need to associate type variables with predicate variables, in such a way that we can later refer to this assignment. Therefore we carry along a procedure pvar-to-tvar which remembers the assignment done so far (cf.xmake-rename).

Due to our distinction between general variables x^0, x^1, x^2, x and variables x0, x1, x2, x intended to range over existing (i.e.xtotal) objects only, η-conversion of proofs cannot be done via reduction to η-conversion of terms. To see this, consider the proof

.  \begin{matrix}∀x̂P x̂ & x \\ P x \end{matrix} ; ∀xP x ; ∀x̂P x̂ → ∀xP x

The proof term is λuλx.ux. If we η-normalize this to λuu, the proven formula would be all ∀x̂P x̂ → ∀x̂P x̂. Therefore we split nbe-normalize-proof into

nbe-normalize-proof-without-eta and proof-to-eta-nf.

Moreover, for a full normalization of proofs (including permutative conversions) we need a preprocessing step that η-expands each ex-elim axiom such that the conclusion is atomic or existential.

We need the following functions.

     (proof-and-genavar-var-alist-to-pterm pvar-to-tvar proof)
     (npterm-and-var-genavar-alist-and-formula-to-proof
       npterm var-genavar-alist crit formula)
     (elim-npterm-and-var-genavar-alist-to-proof
       npterm var-genavar-alist crit).

Then we can define nbe-normalize-proof, abbreviated np.

9.3. Substitution.

In a proof we can substitute

types for type variables (by a type variable substitution tsubst),

terms for variables (by a substitution subst),

comprehension terms for predicate variables (by a predicate variable substitution psubst), and

proofs for assumption variables (by a assumption variable substitution asubst).

It is assumed that subst only affects those vars whose type is not changed by tsubst, psubst only affects those predicate variables whose arity is not changed by tsubst, and that asubst only affects those assumtion variabless whose formula is not changed by tsubst, subst and psubst.

In the abstraction cases of the recursive definition, the abstracted variable (or assumption variable) may need to be renamed. However, its type (or formula) can be affected by tsubst (or tsubst, subst and psubst). Then the renaming cannot be made part of subst (or asubst), because the condition above would be violated. Therefore we carry along procedures rename renaming variables and arename for assumption variables, which remember the renaming done so far.

All these substitutions can be packed together, as an argument topasubst for

proof-substitute.

                            (proof-substitute proof topasubst)

If we want to substitute for a single variable only (which can be a type-, an object-, a predicate - or an assumption-variable), then we can use

                                   (proof-subst proof arg val)

The procedure expand-theorems expects a proof and a test whether a string denotes a theorem to be replaced by its proof. The result is the (normally quite long) proof obtained by replacing the theorems by their saved proofs.

                            (expand-theorems proof name-test?)

9.4. Display.

There are many ways to display a proof. We normally use display-proof for a linear representation, showing the formulas and the rules used. When we in addition want to check the correctness of the proof, we can use

check-and-display-proof.

However, we also provide a readable type-free lambda expression via

(proof-to-expr proof).

To display proofs we use the following functions. In case the optional proof argument is not present, the current proof of an interactive proof development is taken instead.

(display-proofx.xopt-proof)  abbreviated dp
(check-and-display-proofx.xopt-proof)  abbreviated cdp
(display-ptermx.xopt-proof)  abbreviated dpt
(display-proof-exprx.xopt-proof)  abbreviated dpe

We also provide versions which normalize the proof first:

(display-normalized-proofx.xopt-proof)  abbreviated dnp
(display-normalized-ptermx.xopt-proof)  abbreviated dnpt
(display-normalized-proof-exprx.xopt-proof)  abbreviated dnpe

9.5. Classical logic.

(proof-of-stab-at formula) generates a proof of ((A → F) → F) → A. For F, T one takes the obvious proof, and for other atomic formulas the proof using cases on booleans. For all other prime or existential formulas one takes an instance of the global assumption Stab: ((P̂ → F) → F) → P̂. Here the argument formula must be unfolded. For the logical form of falsity we take (proof-of-stab-log-at formula), and similary for ex-falso-quodlibet we provide

                                 (proof-of-efq-at formula)
                                 (proof-of-efq-log-at formula)

Using these functions we can then define (reduce-efq-and-stab proof), which reduces all instances of stability and ex-falso-quodlibet axioms in a proof to instances of these global assumptions with prime or existential formulas, or (if possible) replaces them by their proofs.

With rm-exc we can transform a proof involving classical existential quantifiers in another one without, i.e.xin minimal logic. The Exc-Intro and Exc-Elim theorems are replaced by their proofs, using expand-theorems.

10 Interactive theorem proving with partial proofs

[next] [prev] [prev-tail] [tail] [up]

10. Interactive theorem proving with partial proofs

Pproof

10.1. Partial proofs.

A partial proof is a proof with holes, i.e.xspecial assumption variables (called goal variables) v, v1, v2 … whose formulas must be closed. We assume that every goal variable v has a single occurrence in the proof. We then select a (not necessarily maximal) subproof vx1...xn with distinct object or assumption variables x1...xn. Such a subproof is called a goal. When interactively developing a partial proof, a goal vx1...xn is replaced by another partial proof, whose context is a subset of x1...xn (i.e.xthe context of the goal with v removed).

To gain some flexibility when working on our goals, we do not at each step of an interactive proof development traverse the partial proof searching for the remaining goals, but rather keep a list of all open goals together with their numbers as we go along. We maintain a global variable PPROOF-STATE containing a list of three elements: (1) num-goals, an alist of entries (number goal

drop-info hypname-info), (2) proof and (3) maxgoal, the maximal goal

number used.

At each stage of an interactive proof development we have access to the current proof and the current goal by executing

                                                (current-proof)
                                                (current-goal)

10.2. Interactive theorem proving.

For interactively building proofs we need

(goal-to-goalvar goal)
(goal-to-context goal)
(goal-to-formula goal)
(goal=?xproof goal)
(goal-subst proof goal proof1)
(pproof-state-to-num-goals)
(pproof-state-to-proof)
(pproof-state-to-formula)
(display-current-goal)
(display-current-goal-with-normalized-formulas)
(display-current-pproof-state)

We list some commands for interactively building proofs.

10.2.1. set-goal. An interactive proof starts with (set-goal formula), i.e.xwith setting a goal. Here formula should be closed; if it is not, universal quantifiers are inserted automatically.

10.2.2. normalize-goal. (normalize-goal goal) (abbreviated ng) replaces every formula in the goal by its normal form.

10.2.3. assume. With (assume x1 ...) we can move universally quantified variables and hypotheses into the context. The variables must be given names (known to the parser as valid variable names for the given type), and the hypotheses should be identified by numbers or strings.

10.2.4. use. In (use x . elab-path-and-terms), x is

a number or string identifying a hypothesis form the context,

the string “Truth-Axiom”,

the name of a theorem or global assumption. If it is a global assumption whose final conclusion is a nullary predicate variable distinct from ⊥ (e.g.xEfq-Log or Stab-Log), this predicate variable is substituted by the goal formula.

a closed proof,

a formula with free variables from the context, generating a new goal.

The optional elab-path-and-terms is a list consisting of symbols left or right, giving directions in case the used formula contains conjunctions, and of terms. The universal quantifiers of the used formula are instantiated (via pattern-unify) with appropriate terms in case a conclusion has the form of the goal. The terms provided are substituted for those variables that cannot be instantiated by pattern unification (e.g.xusing ∀x.P x → ⊥ for the goal ⊥). For the instantiated premises new goals are created.

10.2.5. use-with. This is a more verbose form of use, where the terms are not inferred via unification, but have to be given explicitely. Also, for the instantiated premises one can indicate how they are to come about. So in (use-with x . x-list), x is as in use, and x-list is a list consisting of

a number or string identifying a hypothesis form the context,

the name of a theorem or global assumption,

a closed proof,

the string “?” (value of DEFAULT-GOAL-NAME), generating a new goal,

a symbol left or right, a term, whose free variables are added to the context,

a type, which is substituted for the first type variable,

a comprehension term, which is substituted for the first predicate variable.

Notice that new free variables not in the ordered context can be introduced in use-with. They will be present in the newly generated goals. The reason is that proofs should be allowed to contain free variables. This is necessary to allow logic in ground types where no constant is available (e.gxto prove ∀xP x → ∀x¬P x → ⊥).

Notice also that there are situations where use-with can be applied but use can not. For an example, consider the goal P (S(k + l)) with the hypothesis ∀lP (k + l) in the context. Then use cannot find the term Sl by matching; however, applying use-with to the hyposthesis and the term Sl succeeds (since k + Sl and S(k + l) have the same normal form).

10.2.6. inst-with. inst-with does for forward chaining the same as use-with for backward chaining. It replaces the present goal by a new one, with one additional hypothesis obtained by instantiating a previous one. Notice that this effect could also be obtained by cut. In (inst-with x . x-list), x is

a number or string identifying a hypothesis form the context,

the name of a theorem or global assumption,

a closed proof,

a formula with free variables from the context, generating a new goal.

and x-list is a list consisting of

a number or string identifying a hypothesis form the context,

the name of a theorem or global assumption,

a closed proof,

the string “?” (value of DEFAULT-GOAL-NAME), generating a new goal,

a symbol left or right,

a term, whose free variables are added to the context, a type, which is substituted for the first type variable,

a comprehension term, which is substituted for the first predicate variable.

10.2.7. inst-with-to. inst-with-to expects a string as its last argument, which is used (via name-hyp) to name the newly introduced instantiated hypothesis.

10.2.8. cut. The command (cut A) replaces the goal B by the two new goals A and A → B.

10.2.9. strip. To move (all or n) universally quantified variables and hypotheses of the current goal into the context, we uns the command (strip) or (strip

n).

10.2.10. drop. In (drop .xx-list), x-list is a list of numbers or strings identifying hypotheses from the context. A new goal is created, which differs from the previous one only in display aspects: the listed hypotheses are hidden (but still present). If x-list is empty, all hypotheses are hidden.

10.2.11. name-hyp. The command name-hyp expects an index i and a string. Then a new goal is created, which differs from the previous one only in display aspects: the string is used to label the ith hypothesis.

10.2.12. split. The command (split) expects a conjunction A ∧ B as goal and splits it into the two new goals A and B.

10.2.13. get. To be able to work on a goal different from that on top of the goal stack, we have have to move it up using (get n).

10.2.14. undo. With (undo .xn), the last n steps of an interactive proof can be made undone. (undo) has the same effect as (undo 1).

10.2.15. ind. (ind) expects a goal ∀x^{ρ}A with ρ an algebra. Let c_{1}, x, c_{n} be the constructors of the algebra ρ. Then n new goals ∀x⃗_{i}.A[x:=x_{1i}] → ⋯ → A[x:=x_{ki}] → A[x:=c_{i}x⃗_{i}] are generated.

(ind t) expects a goal A[x:=t]. It computes the algebra ρ as type of the term t. Then again n new goals ∀x⃗_{i}.A[x:=x_{1i}] → ⋯ → A[x:=x_{ki}] → A[x:=c_{i}x⃗_{i}] are generated.

10.2.16. simind. (simind all-formula1 ...) also expects a goal ∀x^{ρ}A with ρ an algebra. Then we have to provide the other all formulas to be proved simultaneously with the given one.

10.2.17. intro. (intro i .xterms) expects as goal an inductively defined predicate. The i-th introduction axiom for this predicate is applied, via use (hence terms may have to be provided).

10.2.18. elim. (elim) expects a goal I(t⃗) → A[x⃗:=t⃗]. Then the (strengthened) clauses are generated as new goals, via use-with.

10.2.19. ex-intro. In (ex-intro term), the user provides a term to be used for the present (existential) goal. (exnc-intro x) works similarly for the exnc-quanhtifier.

10.2.20. ex-elim. In (ex-elim x), x is

a number or string identifying an existential hypothesis from the context,

the name of an existential global assumption or theorem,

a closed proof on an existential formula,

an existential formula with free variables from the context, generating a new goal.

Let ∃yA be the existential formula identified by x. The user is then asked to provide a proof for the present goal, assuming that a y satisfying A is available. (exnc-elim x) works similarly for the exnc-quanhtifier.

10.2.21. by-assume-with. Suppose we are proving a goal G from an existential hypothesis ExHyp: ∃yA. Then the natural way to use this hypothesis is to say “by ExHyp assume we have a y satisfying A”. Correspondingly we provide (by-assume-with x y u). Here x – as in ex-elim – identifies an existential hypothesis, and we assume (i.e.xadd to the context) the variable y and – with label u – the kernel A. (by-assume-with x y u) is implemented by the

sequence (ex-elim x), (assume y u), (drop x). by-exnc-assume-with works

similarly for the exnc-quantifier.

10.2.22. cases. (cases) expects a goal ∀x^{ρ}A with ρ an algebra. Assume that c_{1}, x, c_{n} are the constructors of the algebra ρ. Then n new (simplified) goals ∀x⃗_{i}A[x:=c_{i}x⃗_{i}] are generated.

(cases t) expects a goal A[x:=t]. It computes the algebra ρ as type of the term t. Then again n new goals ∀x⃗_{i}A[x:=c_{i}x⃗_{i}] are generated.

(cases 'auto) expects an atomic goal and checks whether its boolean kernel contains an if-term whose test is neither an if-term nor contains bound variables. With the first such test (cases test) is called.

10.2.23. casedist. (casedist t) replaces the goal A containing a boolean term t by two new goals (atomxt) → A[t:=tt] and ((atomxt) → ff) → A[t:=ff].

10.2.24. simp. In (simp opt-dir x . elab-path-and-terms), the optional

argument opt-dir is either the string “<-” or missing. x is

a number or string identifying a hypothesis form the context,

the name of a theorem or global assumption,

a closed proof,

a formula with free variables from the context, generating a new goal.

The optional elab-path-and-terms is a list consisting of symbols left or right, giving directions in case the used formula contains conjunctions, and of terms. The universal quantifiers of the used formula are instantiated with appropriate terms to match a part of the goal. The terms provided are substituted for those variables that cannot be inferred. For the instantiated premises new goals are created. This generates a used formula, which is to be an atom, a negated atom or t ≈ s. If it as a (negated) atom, it is checked whether the kernel or its normal form is present in the goal. If so, it is replace by T (or F). If it is an equality t = s or t ≈ s with t or its normal form present in the goal, t is replaced by s. In case “<-” exchange t and s.

10.2.25. simp-with. This is a more verbose form of simp, where the terms are not inferred via matching, but have to be given explicitely. Also, for the instantiated premises one can indicate how they are to come about. So in (simp-with opt-dir x . x-list), opt-dir and x are as in simp, and x-list is a list consisting of

a number or string identifying a hypothesis form the context,

the name of a theorem or global assumption,

a closed proof,

the string “?” (value of DEFAULT-GOAL-NAME), generating a new goal,

a symbol left or right,

a term, whose free variables are added to the context,

a type, which is substituted for the first type variable,

a comprehension term, which is substituted for the first predicate variable.

10.2.26. min-pr. In (min-pr x measure), x is

a number or string identifying a classical existential hypothesis from the context,

the name of a classical existential global assumption or theorem,

a closed proof on a classical existential formula,

a classical existential formula with free variables from the context, generating a new goal.

The result is a new implicational goal, whose premise provides the (classical) existence of instances with least measure.

10.2.27. exc-intro. In (exc-intro terms), the user provides terms to be used for the present (classical existential) goal.

10.2.28. exc-elim. In (exc-elim x), x is

a number or string identifying a classical existential hypothesis from the context, the name of a classical existential global assumption or theorem,

a closed proof on a classical existential formula,

a classical existential formula with free variables from the context, generating a new goal.

Let ∃^{ca}y⃗A⃗ or ∃^{cl}y⃗A⃗ be the classical existential formula identified by x. The user is then asked to provide a proof for the present goal, assuming that terms y⃗ satisfying A⃗ are available.

10.2.29. pair-elim. In (pair-elim), a goal ∀pP (p) is replaced by the new goal ∀x_{1}, x_{2}P (⟨x_{1}, x_{2}⟩).

11 Search

[next] [prev] [prev-tail] [tail] [up]

11. Search Following Miller [10] and Berger, we have implemented a proof search algorithm for minimal logic. To enforce termination, every assumption can only be used a fixed number of times.

We begin with a short description of the theory involved.

Q always denotes a ∀∃∀-prefix, say ∀x⃗∃y⃗∀z⃗, with distinct variables. We call x⃗ the signature variables, y⃗ the flexible variables and z⃗ the forbidden variables of Q, and write Q_{∃} for the existential part ∃y⃗ of Q.

Q-terms are inductively defined by the following clauses.

If u is a universally quantified variable in Q or a constant, and r⃗ are Q-terms, then ur⃗ is a Q-term.

For any flexible variable y and distinct forbidden variables z⃗ from Q, yz⃗ is a Q-term.

If r is a Q∀z-term, then λzr is a Q-term.

Explicitely, r is a Q-term iff all its free variables are in Q, and for every subterm yr⃗ of r with y free in r and flexible in Q, the r⃗ are distinct variables either λ-bound in r (such that yr⃗ is in the scope of this λ) or else forbidden in Q.

Q-goals and Q-clauses are simultaneously defined by

If r⃗ are Q-terms, then P r⃗ is a Q-goal as well as a Q-clause.

If D is a Q-clause and G is a Q-goal, then D → G is a Q-goal.

If G is a Q-goal and D is a Q-clause, then G → D is a Q-clause.

If G is a Q∀x-goal, then ∀xG is a Q-goal.

If D[y:=Y z⃗] is a ∀x⃗∃y⃗, Y ∀z⃗-clause, then ∀yD is a ∀x⃗∃y⃗∀z⃗-clause.

Explicitely, a formula A is a Q-goal iff all its free variables are in Q, and for every subterm yr⃗ of A with y either existentially bound in A (with yr⃗ in the scope) or else free in A and flexible in Q, the r⃗ are distinct variables either λ- or universally bound in A (such that yr⃗ is in the scope) or else free in A and forbidden in Q.

A Q-sequent has the form P ⇒ G, where P is a list of Q-clauses and G is a Q-goal.

A Q-substitution is a substitution of Q-terms.

A unification problem U consists of a ∀∃∀-prefix Q and a conjunction C of equations between Q-terms of the same type, i.e.x⋀ ⋀_{i=1}^{n}r_{i} = s_{i}. We may assume that each such equation is of the form λx⃗r = λx⃗s with the same x⃗ (which may be empty) and r, s of ground type.

A solution to such a unification problem U is a Q-substitution φ such that for every i, r_{i}φ = s_{i}φ holds (i.e.xr_{i}φ and s_{i}φ have the same normal form). We sometimes write C as r⃗ = s⃗, and (for obvious reasons) call it a list of unification pairs.

We work with lists of sequents instead of single sequents; they all are Q-sequents for the same prefix Q. One then searches for a Q-substitution φ and proofs of the φ-substituted sequents. intro-search takes the first sequent and extends Q by all universally quantified variables x_{1}x. It then calls select, which selects (using or) a fitting clause. If one is found, a new prefix Q′ (raising the new flexible variables) is formed, and the n (≥ 0) new goals with their clauses (and also all remaining sequents) are substituted with star ∘ ρ, where star is the “raising” substitution and ρ is the mgu. For this constellation intro-search is called again. In case of success, one obtains a Q′-substitution φ′ and proofs of the star ∘ ρ ∘ φ′ -substituted new sequents. Let φ := (ρ ∘ φ′)↾Q_{∃}, and take the first n proofs of these to build a proof of the φ-substituted (first) sequent originally considered by

intro-search.

Compared with Miller [10], we make use of several simplifications, optimizations and extensions, in particular the following.

Instead of arbitrarily mixed prefixes we only use those of the form ∀∃∀. Nipkow in [11] already had presented a version of Miller’s pattern unification algorithm for such prefixes, and Miller in [10, Sectionx9.2] notes that in such a situation any two unifiers can be transformed into each other by a variable renaming substitution. Here we restrict ourselves to ∀∃∀-prefixes throughout, i.e.xin the proof search algorithm as well.

The order of events in the pattern unification algorithm is changed slightly, by postponing the raising step until it is really needed. This avoids unnecessary creation of new higher type variables. – Already Miller noted in [10, p.515] that such optimizations are possible.

The extensions concern the (strong) existential quantifier, which has been left out in Miller’s treatment, and also conjunction. The latter can be avoided in principle, but of course is a useful thing to have.

(search m (name1 m1) ...) expects for m a default value for multiplicity (i.e.xhow often assumptions are to be used), for name1 x

numbers of hypotheses from the present context or

names for theorems or global assumptions,

and for m1 … multiplicities (positive integers for global assumptions or theorems). A search is started for a proof of the goal formula from the given hypotheses with the given multiplicities and in addition from the other hypotheses (but not any other global assumptions or theorems) with m or mult-default. To exclude a hypothesis from being tried, list it with multiplicity 12 Computational content of classical proofs

[next] [prev] [prev-tail] [tail] [up]

12. Computational content of classical proofs

Classical This section is based on [3]. We restrict to formulas in the language {⊥, →, ∀} in this section, and - as in the paper - make use of a special nullary predicate variable X.

A formula is relevant if it ends with (logical) falsity. Definite and goal formulas are defined by a simultaneous recursion, as in [3].

                                     (atr-relevant?xformula)
                                     (atr-definite?xformula)
                                     (atr-goal?xformula)

To implement [3, Lemmax3.1], we need to construct proofs from formulas:

N_{D}: ((D → ⊥) → X) → D^{X}  for D relevant
M_{D}: D → D^{X}
K_{G}: G → G^{X}  for G irrelevant
H_{G}: G^{X} → (G → X) → X

This is done by

                              (atr-rel-definite-proof formula)
                              (atr-arb-definite-proof formula)
                              (atr-irrel-goal-proof formula)
                              (atr-arb-goal-proof formula)

Next we need to implement [3, Lemmax3.2], which says that for goal formulas G⃗ = G_{1}, x, G_{n} we can derive in minimal logic augmented with a special predicate variable X

. (G⃗ → X) → G⃗^{X} → X.

In our implementation this function is called

                              (atr-goals-to-x-proof goal1 ...)

Finally we implement [3, Theoremx3.3], which says the following. Assume that for definite formulas D⃗ and goal formulas G⃗ we can derive in minimal logic

.  D⃗ → (∀y⃗.G⃗ → ⊥) → ⊥.

Then we can also derive in intuitionistic logic augmented with the special predicate variable X

.  D⃗ → (∀y⃗.G⃗ → X) → X.

In particular, substitution of the formula

. ∃y⃗.G⃗ := ∃y⃗.G_{1} ∧ ⋯ ∧ G_{n}

for X yields a derivation in intuitionistic logic of

.  D⃗ → ∃y⃗.G⃗.

This is done by

(atr-min-excl-proof-to-x-proof min-excl-proof)
(atr-min-excl-proof-to-intuit-ex-proof min-excl-proof)

13 Extracted terms

[next] [prev] [prev-tail] [tail] [up]

13. Extracted terms

S:ExtrTerms We assign to every formula A an object τ(A) (a type or the symbol nulltype). τ(A) is intended to be the type of the program to be extracted from a proof of A. This is done by

                                  (formula-to-et-type formula)

In formula-to-et-type we assign type variables to the predicate variables. For to be able to later refer to this assignment, we use a global variable PVAR-TO-TVAR-ALIST, which memorizes the assigment done so far. Later reference is necessary, because such type variables will appear in extracted programs of theorems involving predicate variables, and in a given development there may be many auxiliary lemmata containing the same predicate variable. A

fixed pvar-to-tvar refers to and updates PVAR-TO-TVAR-ALIST.

When we want to execute the program, we have to replace the constant cL corresponding to a lemma L by the extracted program of its proof, and the constant cGA corresponding to a global assumption GA by an assumed extracted term to be provided by the user. This can be achieved by adding computation rules for cL and cGA. We can be rather flexible here and enable/block rewriting by using animate/deanimate as desired. Notice that the type of the extracted term provided for a cGA must be the extracted type of the assumed formula. When predicate variables are present, one must use the type variables assigned to

them in PVAR-TO-TVAR-ALIST.

                          (animate thm-or-ga-namex.xopt-eterm)
                          (deanimate thm-or-ga-name)

We can define, for a given derivation M of a formula A with τ(A) ≠nulltype, its extracted term (or extracted program) et(M) of type τ(A). We also need extracted terms for the axioms. For induction we take recursion, for the proof-by-cases axiom we take the cases-construct for terms; for the other axioms the extracted terms are rather clear. Term extraction is implemented by

                               (proof-to-extracted-term proof)

It is also possible to give an internal proof of soundness. This can be done by

(proof-to-soundness-proof proof)

14 Reading formulas in external form

[next] [prev] [prev-tail] [tail] [up]

14. Reading formulas in external form

Reading A formula can be produced from an external representation, for example a string, using the pt function. It has one argument, a string denoting a formula, that is converted to the internal representation of the formula. For the following syntactical entities parsing functions are provided:

(py string)  for parsing types
(pv string)  for parsing variables
(pt string)  for parsing terms
(pf string)  for parsing formulas

The conversion occurs in two steps: lexical analysis and parsing.

14.1. Lexical analysis.

In this stage the string is brocken into short sequences, called tokens. A token can be one of the following:

An alphabetic symbol: A sequence of letters a–z and A–Z. Upper and lower case letters are considered different.

A number: A sequence of digits 0–9 A punctuation mark: One of the characters: ( ) [ ] . , ;

A special symbol: A sequence of characters, that are neither letters, digits, punctuation marks nor white space.

For example: abc, ABC and A are alphabetic symbols, 123, 0123 and 7 are numbers, ( is a punctuation mark, and <=, +, and #:-^are special symbols.

Tokens are always character sequences of maximal length belonging to one of the above categories. Therefore fx is a single alphabetic symbol not two and likewise <+ is a single special symbol. The sequence alpha<=(-x+z), however, consists of the 8 tokens alpha, <=, (, -, x, +, z, and ). Note that the special symbols <= and - are separated by a punctuation mark, and the alphabetic symbols x and z are separated by the special symbol

+.

If two alphabetic symbols, two special symbols, or two numbers follow each other they need to be separated by white space (spaces, newlines, tabs, formfeeds, etc.). Except for a few situations mentioned below, whitespace has no significance other than separating tokens. It can be inserted and removed between any two tokens without affecting the significance of the string.

Every token has a token type, and a value. The token type is one of the following: number, var-index, var-name, const, pvar-name, predconst, type-symbol, pscheme-symbol, postfix-op, prefix-op, binding-op, add-op, mul-op, rel-op, and-op, or-op, imp-op, pair-op, if-op, postfix-jct, prefix-jct, and-jct, or-jct, tensor-jct, imp-jct, quantor, dot, hat, underscore, comma, semicolon, arrow, lpar, rpar, lbracket, rbracket.

The possible values for a token depend on the token type and are explained below.

New tokens can be added using the function

.  (add-token string token-type value).

The inverse is the function

.  (remove-token string).

A list of all currently defined tokens sorted by token types can be obtained by the function

.  (display-tokens).

14.2. Parsing.

The second stage, parsing, extracts structure form the sequence of tokens.

Types. Type-symbols are types; the value of a type-symbol must be a type. If σ and τ are types, then σ;τ is a type (pair type) and σ=>τ is a type (function type). Parentheses can be used to indicate proper nesting. For example boole is a predefined type-symbol and hence, (boole;boole)=>boole is again a type. The parentheses in this case are not strictly necessary, since ; binds stronger than =>. Both operators associate to the right.

Variables. Var-names are variables; the value of a var-name token must be a pair consisting of the type and the name of the variable (the same name string again! This is not nice and may be later, we find a way to give the parser access to the string that is already implicit in the token). For example to add a new boolean variable called “flag”, you have to invoke the

function (add-token "flag" 'var-name (cons 'boole "flag")). This

will enable the parser to recognize “flag3”, “flag^”, or “flag^14” as well.

Further, types, as defined above, can be used to construct variables.

A variable given by a name or a type can be further modified. If it is followed by a ^, a partial variable is constructed. Instead of the ^a _can be used to specify a total variable.

Total variables are the default and therefore, the _can be omitted.

As another modifier, a number can immediately follow, with no whitespace in between, the ^or the _, specifying a specific variable index.

In the case of indexed total variables given by a variable name or a type symbol, again the _can be omitted. The number must then follow, with no whitespace in between, directly after the variable name or the type.

Note: This is the only place where whitespace is of any significance in the input. If the ^, _, type name or variable name is separated from the following number by whitespace, this number is no longer considered to be an index for that variable but a numeric term in its own right.

For example, assuming that p is declared as a variable of type boole, we have:

p a total variable of type boole with name p and no index.

p_a total variable of type boole with name p and no index.

p^a partial variable of type boole with name p and no index.

p2 a total variable of type boole with name p and index 2. p_2 a total variable of type boole with name p and index 2.

p^2 a partial variable of type boole with name p and index 2.

boole a total anonymous variable of type boole with no index.

boole_a total anonymous variable of type boole with no index.

boole^a partial anonymous variable of type boole with no index.

boole_2 a total anonymous variable of type boole with index 2.

boole2 a total anonymous variable of type boole with index 2.

boole^2 a partial anonymous variable of type boole with index 2.

boolex2 a total anonymous variable of type boole applied to the numeric term 2.

(boole)2 a total anonymous variable of type boole applied to the numeric term 2.

(boole)_2 a total anonymous variable of type boole with index 2.

boole=>boole^2 a partial anonymous variable of type function of boole to boole with index 2.

Terms are built from atomic terms using application and operators.

An atomic term is one of the following: a constant, a variable, a number, a conditional, or any other term enclosed in parentheses.

Constants have const as token type, and the respective term in internal form as value. There are also composed constants, so-called constant schemata. A constant schema has the form of the name of the constant schema (token type constscheme) followed by a list of types, the whole thing enclosed in parentheses. There are a few built in constant schemata: (Recx<typelist>) is the recursion over the types given in the type list; (EQatx<type>) is the equality for the given type; (Eatx<type>) is the existence predicate for the given type. The constant schema EQat can also be written as the relational infix operator =; the constant schemata Eat can also be written as the prefix operator

E.

For a number, the user defined function make-numeric-term is called with the number as argument. The return value of make-numeric-term should be the internal term representation of the number.

To form a conditional term, the if operator if followed by a list of atomic terms is enclosed in square brackets. Depending on the constructor of the first term, the selector, a conditional term can be reduced to one of the remaining terms.

From these atomic terms, compound terms are built not only by application but also using a variety of operators, that differ in binding strength and associativity.

Postfix operators (token type postfix-op) bind strongest, next in binding strength are prefix operators (token type prefix-op), next come binding operators (token type binding-op).

A binding operator is followed by a list of variables and finally a term. There are two more variations of binding operators, that bind much weaker and are discussed later.

Next, after the binding operators, is plain application. Juxtaposition of two terms means applying the first term to the second. Sequences of applications associate to the left. According to the vector notation convention the meaning of application depends on the type of the first term. Two forms of applications are defined by default: if the type of the first term is of arrow-form? then make-term-in-app-form is used; for the type of a free algebra we use the corresponding form of recursion. However, there is one exception: if the first term is of type boole application is read as a short-hand for the “if… then … else” construct (which is a special form) rather than boolean recursion. The user may use the function add-new-application to add new forms of applications. This function takes two arguments, a predicate for the type of the first argument, and a function taking the two terms and returning another term intended to be the result of this form of application. Predicates are tested in the inverse order of their definition, so more general forms of applications should be added first.

By default these new forms of application are not used for output; but the user might declare that certain terms should be output as formal application. When doing so it is the user’s responisbility to make sure that the syntax used for the output can still be parsed correctly by the

parser! To do so the function (add-new-application-syntax pred toarg

toop) can be used, where the first argument has to be a predicate (i.e., a function mapping terms to #t and #f) telling whether this special form of application can be used. If so, the arguments toarg and toop have to be functions mapping the term to operator and argument of this “application” respectively.

After that, we have binary operators written in infix notation. In order of decreasing binding strength these are:

multiplicative operators, leftassociative, token type mul-op;

additive operators, leftassociative, token type add-op;

relational operators, not associative, token type rel-op;

boolean and operators, leftassociative, token type and-op; boolean or operators, leftassociative, token type or-op;

boolean implication operators, rightassociative, token type imp-op;

pairing operators, rightassociative, token type pair-op. On the top level, we have two more forms of binding operators, one using the

dot “.”, the other using square brackets “[x]”. Recall that a binding operator is followed by a list of variables and a term. This notation can be augmented by a period “.” following after the variable list and before the term. In this case the scope of the binding extends as far to the right as possible. Bindings with the lambda operator can also be specified by including the list of variables in square brackets. In this case, again, the scope of the binding extends as far as possible.

Predefined operators are E and = as described above, the binding operator lambda, and the pairing operator @ with two prefix operators left and right for projection.

The value of an operator token is a function that will obtain the internal representation of the component terms as arguments and returns the internal representation of the whole term.

If a term is formed by application, the function make-gen-application is called with two subterms and returns the compound term. The default here (for terms with an arrow type) is to make a term in application form. However other rules of composition might be introduced easily.

Formulas are built from atomic formulas using junctors and quantors.

The simplest atomic formulas are made from terms using the implicit predicate “atom”. The semantics of this predicate is well defined only for terms of type boole. Further, a predicate constant (token type predconst) or a predicate variable (token type pvar) followed by a list of atomic terms is an atomic formula. Lastly, any formula enclosed in parentheses is considered an atomic formula.

The composition of formulas using junctors and quantors is very similar to the composition of terms using operators and binding. So, first postfix junctors, token type postfix-jct, are applied, next prefix junctors, token type prefix-jct, and quantors, token type quantor, in the usual form: quantor, list of variables, formula. Again, we have a notation using a period after the list of variables, making the scope of the quantor as large as possible. Predefined quantors are ex, excl, exca, and all.

The remaining junctors are binary junctors written in infix form. In order of decreasing binding strength we have:

conjunction junctors, leftassociative, token type and-jct;

disjunction junctors, leftassociative, token type or-jct;

tensor junctors, rightassociative, token type tensor-jct;

implication junctors, rightassociative, token type imp-jct.

Predefined junctors are & (and), ! (tensor), and -> (implication).

The value of junctors and quantors is a function that will be called with the appropriate subformulas, respectively variable lists, to produce the compound formula in internal form.

14 References

[next] [prev] [prev-tail] [tail] [up] References

[1] xxxKlaus  Aehlig  and  Helmut  Schwichtenberg,  A

syntactical analysis of non-size-increasing polynomial time computation, Proceedings 15’th Symposium on Logic in Computer Science (LICS 2000), 2000, pp.x84–91.

[2] xxxUlrich Berger, Program extraction from normalization proofs, Typed Lambda Calculi and Applications (M.xBezem and J.F. Groote, eds.), LNCS, vol. 664, Springer Verlag, Berlin, Heidelberg, New York, 1993, pp.x91–106.

[3] xxxUlrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 (2002), 3–25.

[4] xxxUlrich Berger, Matthias Eberl, and Helmut Schwichtenberg, Term rewriting for normalization by evaluation, Information and Computation 183 (2003), 19–42.

[5] xxxUlrich Berger and Helmut Schwichtenberg, An inverse of the evaluation functional for typed λ-calculus, Proceedings 6’th Symposium on Logic in Computer Science (LICS’91) (R.xVemuri, ed.), IEEE Computer Society Press, Los Alamitos, 1991, pp.x203–211.

[6] xxxStefan Berghofer, Proofs, programs and executable specifications in higher order logic, Ph.D. thesis, Institut fxr Informatik, TU Mxnchen, 2003.

[7] xxxMartin Hofmann, Linear types and non-size-increasing polynomial time computation, Proceedings 14’th Symposium on Logic in Computer Science (LICS’99), 1999, pp.x464–473.

[8] xxxFelix Joachimski and Ralph Matthes, Short proofs of normalisation for the simply-typed λ-calculus, permutative conversions and Gxdel’s T, Archive for Mathematical Logic 42 (2003), 59–87.

[9] xxxRalph Matthes, Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types, Ph.D. thesis, Mathematisches Institut der Universitxt Mxnchen, 1998.

[10] xxxDale Miller, A logic programming language with lambda–abstraction, function variables and simple unification, Journal of Logic and Computation 2 (1991), no.x4, 497–536.

[11] xxxTobias Nipkow, Higher-order critical pairs, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (Los Alamitos) (R.xVemuri, ed.), IEEE Computer Society Press, 1991, pp.x342–349.

[12] xxxViggo Stoltenberg-Hansen, Edward Griffor, and Ingrid Lindstrxm, Mathematical theory of domains, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1994.

[13] xxxAnnexS. Troelstra and Helmut Schwichtenberg, Basic proof theory, 2nd ed., Cambridge University Press, 2000.

14 Index

[prev] [prev-tail] [tail] [up] Index

=-to-E-1, 1
=-to-E-2, 2
=-to-Eq, 3
aconst-to-formula, 4
aconst-to-inst-formula, 5
aconst-to-kind, 6
aconst-to-name, 7
aconst-to-repro-formulas, 8
aconst-to-string, 9
aconst-to-tpsubst, 10
aconst-to-uninst-formula, 11
aconst-without-rules?, 12
aconst=?, 13
aconst?, 14, 15
add-alg, 16
add-algebras-with-parameters,

17

add-algs, 18
add-computation-rule, 19
add-global-assumption, 20
add-ids, 21
add-new-application, 22
add-param-alg, 23
add-param-algs, 24
add-predconst-name, 25
add-program-constant, 26
add-pvar-name, 27
add-rewrite-rule, 28
add-theorem, 29
add-tvar-name, 30
add-var-name, 31
aga, 32
alg-form-to-name, 33
alg-form-to-types, 34
alg-form?, 35
alg-name-to-arity, 36
alg-name-to-simalg-names, 37
alg-name-to-token-types, 38
alg-name-to-tvars, 39
alg-name-to-typed-constr-names,

40

alg?, 41
All-AllPartial, 42, 43, 44
all-allpartial-aconst, 45
All-AllPartial-nat, 46
all-form-to-kernel, 47
all-form-to-var, 48

                                          all-form-to-vars-and..., 49
                                          all-form?, 50
                                          all-formula-to-cases-aconst, 51
                                          all-formulas-to-ind-aconst, 52
                                          allnc-form-to-kernel, 53
                                          allnc-form-to-var, 54
                                          allnc-form?, 55
                                          AllPartial-All, 56, 57
                                          allpartial-all-aconst, 58
                                          AllPartial-All-nat,, 59
                                          and-form-to-left, 60
                                          and-form-to-right, 61
                                          and-form?, 62
                                          animate, 63

animation, 64

arity

x of a predicate variable, 65 x of a program constant, 66

                                          arity-to-string, 67
                                          arity-to-types, 68
                                          arrow-form-to-arg-type, 69
                                          arrow-form-to-arg-types, 70
                                          arrow-form-to-final-val-type,

71

                                          arrow-form-to-val-type, 72
                                          arrow-form?, 73
                                          arrow-types-to-rec-const, 74
                                          assume, 75

assumption constant, 76

                                          asubst, 77
                                          Atom-False, 78
                                          atom-form-to-kernel, 79
                                          atom-form?, 80
                                          Atom-True, 81
                                          atr-arb-definite-proof, 82
                                          atr-arb-goal-proof, 83
                                          atr-definite?, 84
                                          atr-goal?, 85
                                          atr-goals-to-x-proof, 86
                                          atr-irrel-goal-proof, 87
                                          atr-min-...-to-intuit-ex-proof,

88

                                          atr-min-excl-proof-to-x-proof,

89

                                          atr-rel-definite-proof, 90
                                          atr-relevant?, 91
                                          avar-proof-equal?, 92
                                          avar-to-formula, 93

avar-to-index, 94
avar-to-name, 95
avar=?, 96
avar=?, 97
avar?, 98

Berger, 99 bottom, 100

by-assume-with, 101
by-exnc-assume-with, 102

Cases, 103, 104

cases, 105

cases-construct, 106

Cases-Log, 107
check-and-display-proof, 108
classical-cterm=?, 109
classical-formula=?, 110, 111

clause, 112

Compatibility, 113
Compose, 114
compose-o-substitutions, 115
compose-substitutions, 116
compose-substitutions-wrt, 117
compose-t-substitutions, 118

composition, 119 comprehension term, 120, 121 computation rule, 122 computation rules, 123

consistent-substitutions-wrt?,

124

const-to-arrow-types-or..., 125
const-to-kind, 126
const-to-name, 127
const-to-object-or-arity, 128
const-to-t-deg, 129
const-to-token-type, 130
const-to-tsubst, 131
const-to-tvars, 132
const-to-type, 133
const-to-uninst-type, 134
const=?, 135
const?, 136

constant scheme, 137

constr-name-and-tsubst..., 138
constr-name-to-constr, 139
constr-name?, 140
Constr-Total, 141
Constr-Total-Args, 142

constructor, 143 constructor pattern, 144 context, 145

context-to-avars, 146
context-to-vars, 147
context=?, 148

conversion relation, 149

Coquand, 150

                                          cterm-subst, 151
                                          cterm-substitute, 152
                                          cterm-to-formula, 153
                                          cterm-to-free, 154
                                          cterm-to-string, 155
                                          cterm-to-vars, 156
                                          cterm=?, 157
                                          cterm?, 158
                                          current-goal, 159
                                          current-proof, 160

cut, 161

                                          Cvind-with-measure-11, 162
                                          deanimate, 163
                                          default-var-name, 164, 165

degree of totality, 166

                                          display-constructors, 167
                                          display-current-goal, 168
                                          display-current-goal-with...,

169

                                          display-current-num-goals...,

170

                                          display-global-assumptions, 171
                                          display-normalized-proof, 172
                                          display-normalized-proof-expr,

173

                                          display-normalized-pterm, 174
                                          display-p-substitution, 175
                                          display-program-constants, 176
                                          display-proof, 177
                                          display-proof-expr, 178
                                          display-pterm, 179
                                          display-substitution, 180
                                          display-t-substitution, 181
                                          display-theorems, 182

dnp, 183

                                          dnpe, 184
                                          dnpt, 185

cdp, 186 dp, 187 dpe, 188 dpt, 189

                                          drop, 190

E, 191

                                          E-to-Total, 192
                                          E-to-Total-nat, 193

Efq, 194

                                          Efq-Atom, 195
                                          Efq-Log, 196

Elim, 197

                                          elim, 198
                                          empty-subst, 199

Eq, 200

Eq-Compat, 201
eq-compat-aconst, 202
Eq-Ext, 203

Eq-Refl, 204, 205

eq-refl-aconst, 206

Eq-Symm, 207, 208

eq-symm-aconst, 209
Eq-to-=-1, 210
Eq-to-=-1-nat, 211
Eq-to-=-2, 212
Eq-to-=-2-nat, 213
Eq-Trans, 214, 215
eq-trans-aconst, 216
equal-pvars?, 217
=-Refl-nat, 218
=-Symm-nat, 219
=-Trans-nat, 220

equality, 221

=-to-E-1-nat, 222
=-to-E-2-nat, 223
=-to-Eq-nat, 224

evaluation, 225 Ex-Elim, 226, 227, 228

Ex-Elim, 229
ex-elim, 230
Ex-ExPartial, 231, 232
ex-expartial-aconst, 233
Ex-ExPartial-nat, 234
ex-form-to-kernel, 235
ex-form-to-var, 236
ex-form-to-vars-and..., 237
ex-form?, 238
ex-for...-to-ex-elim-const, 239,

240

ex-formula-to-ex-intro-aconst,

241

Ex-Intro, 242, 243
Ex-Intro, 244
ex-intro, 245
exc-elim, 246
exc-intro, 247
exca, 248
exca-form-to-kernel, 249
exca-form-to-var, 250
exca-form?, 251
excl, 252
excl-form-to-kernel, 253
excl-form-to-var, 254
excl-form?, 255
exnc-elim, 256
exnc-form-to-kernel, 257
exnc-form-to-var, 258
exnc-form?, 259

                                          exnc-intro, 260
                                          expand-theorems, 261
                                          ExPartial-Ex, 262, 263, 264
                                          expartial-ex-aconst, 265
                                          ExPartial-Ex-nat, 266
                                          ext-aconst, 267
                                          Extensionality, 268

extracted program, 269 extracted term, 270

                                          falsity, 271
                                          falsity-log, 272

Filliatre, 273

                                          finalg-to-=-const, 274
                                          finalg-to-=-to-e-1-aconst, 275
                                          finalg-to-=-to-e-2-aconst, 276
                                          finalg-to-=-to-eq-aconst, 277
                                          finalg-to-all-allpartial-aconst,

278

                                          finalg-to-e-const, 279
                                          finalg-to-e-to-total-aconst, 280
                                          finalg-to-eq-to-=-1-aconst, 281
                                          finalg-to-eq-to-=-2-aconst, 282
                                          finalg-to-expartial-ex-aconst,

283

                                          finalg-to-total-to-e-aconst, 284
                                          finalg?, 285
                                          fold-cterm, 286
                                          fold-formula, 287

formula

x definite, 288 x folded, 289 x goal, 290 x prime, 291 x relevant, 292 x unfolded, 293

                                          formula-subst, 294
                                          formula-substitute, 295
                                          formula-to-et-type, 296
                                          formula-to-free, 297
                                          formula-to-prime-subformulas,

298

                                          formula-to-string, 299
                                          formula=?, 300, 301

get, 302

global assumption, 303

                                          global-assdots-name-to-aconst,

304 goal, 305

                                          goal-subst, 306
                                          goal-to-context, 307
                                          goal-to-formula, 308
                                          goal-to-goalvar, 309
                                          goal=?, 310

ground-type?, 311

Harrop degree, 312 Harrop formula, 313 Huet, 314

if-construct, 315, 316

imp-form-to-conclusion, 317
imp-form-to-final-conclusion,

318

imp-form-to-premise, 319
imp-form-to-premises, 320
imp-form?, 321
imp-formulas-to-elim-aconst, 322

Ind, 323, 324 Ind, 325 ind, 326 induction, 327

inst-with, 328
inst-with-to, 329

Intro, 330

intro, 331
intro-search, 332

Letouzey, 333 lexical analysis, 334

make-=, 335
make-aconst, 336
make-alg, 337
make-all, 338
make-allnc, 339
make-and, 340
make-arity, 341
make-arrow, 342
make-atomic-formula, 343
make-avar, 344
make-const, 345
make-cterm, 346
make-e, 347
make-eq, 348
make-ex, 349
make-exca, 350
make-excl, 351
make-exnc, 352
make-imp, 353
make-inhabited, 354
make-predconst, 355
make-predicate-formula, 356
make-proof-in-aconst-form, 357
make-proof-in-all-elim-form, 358
make-proof-in-all-intro-form,

359

make-proof-in-and-elim-l..., 360
make-proof-in-and-elim-r..., 361

make-proof-in-and-intro-form,

362

make-proof-in-avar-form, 363
make-proof-in-cases-form, 364
make-proof-in-ex-intro-form, 365
make-proof-in-imp-elim-form, 366
make-proof-in-imp-intro-form,

367

make-pvar, 368
make-quant-formula, 369
make-star, 370
make-subst, 371
make-subst-wrt, 372
make-substitution, 373
make-substitution-wrt, 374
make-tensor, 375
make-term-in-abst-form, 376
make-term-in-app-form, 377
make-term-in-const-form, 378
make-term-in-if-form, 379
make-term-in-lcomp-form, 380
make-term-in-pair-form, 381
make-term-in-rcomp-form, 382
make-term-in-var-form, 383
make-total, 384

Miller, 385, 386

min-pr, 387
Minpr-with-measure-l11, 388
mk-all, 389
mk-allnc, 390
mk-and, 391
mk-arrow, 392
mk-ex, 393
mk-exca, 394
mk-excl, 395
mk-exnc, 396
mk-imp, 397
mk-neg, 398
mk-neg-log, 399
mk-proof-in-and-intro-form, 400
mk-proof-in-elim-form, 401
mk-proof-in-ex-intro-form, 402
mk-proof-in-intro-form, 403
mk-quant, 404
mk-tensor, 405
mk-term-in-abst-form, 406
mk-term-in-app-form, 407
mk-var, 408
name-hyp, 409
nbe-constr-value-to-constr, 410
nbe-constr-value-to-name, 411
nbe-constr-value?, 412
nbe-constructor-pattern?, 413

nbe-extract, 414
nbe-fam-value?, 415
nbe-formula-to-type, 416
nbe-genargs, 417
nbe-inst?, 418
nbe-make-constr-value, 419
nbe-make-object, 420
nbe-match, 421
nbe-normalize-proof, 422
nbe-normalize-term, 423
nbe-object-app, 424
nbe-object-apply, 425
nbe-object-compose, 426
nbe-object-to-type, 427
nbe-object-to-value, 428
nbe-object?, 429
nbe-pconst-...-to-object, 430
nbe-reflect, 431
nbe-reify, 432
nbe-term-to-object, 433
new-tvar, 434

nf, 435 ng, 436 Nipkow, 437

normalize-formula, 438
normalize-goal, 439

np, 440 nf, 441 nt, 442

number-and-idpredconst-to-intro-aconst,

443

numerated-var-to-index, 444
numerated-var, 445
object-type?, 446
osubst, 447
p-substitution-to-string, 448
pair-elim, 449

parsing, 450

pattern-unify, 451

Paulin-Mohring, 452 Paulson, 453

pconst-name-to-comprules, 454
pconst-name-to-inst-objs, 455
pconst-name-to-object, 456
pconst-name-to-pconst, 457
pconst-name-to-rewrules, 458

pf, 459

pproof-state-to-formula, 460
pproof-state-to-proof, 461
predconst-name-to-arity, 462
predconst-name?, 463
predconst-to-index, 464
predconst-to-name, 465

                                          predconst-to-string, 466
                                          predconst-to-tsubst, 467
                                          predconst-to-uninst-arity, 468
                                          predconst?, 469

predicate constant, 470

                                          predicate-form-to-args, 471
                                          predicate-form-to-predicate, 472
                                          predicate-form?, 473
                                          prename, 474

Presburger, 475

                                          prime-form?, 476
                                          proof-in-aconst-form-to-aconst,

477

                                          proof-in-aconst-form?, 478
                                          proof-in-all-elim-form-to-arg,

479

                                          proof-in-all-elim-form-to-op,

480

                                          proof-in-all-elim-form?, 481
                                          pr...all-intro-form-to-kernel,

482

                                          pr...all-intro-form-to-var, 483
                                          proof-in-all-intro-form?, 484
                                          proof-in-and-elim..., 485
                                          proof-in-and-elim-left-form?,

486

                                          proof-in-and-elim..., 487
                                          proof-in-and-elim-right-form?,

488

                                          pr...and-intro-form-to-left, 489
                                          pr...and-intro-form-to-right,

490

                                          proof-in-and-intro-form?, 491
                                          proof-in-avar-form-to-avar, 492
                                          proof-in-avar-form?, 493
                                          proof-in-cases-form-to-alts, 494
                                          proof-in-cases-form-to-rest, 495
                                          proof-in-cases-form-to-test, 496
                                          proof-in-cases-form?, 497
                                          proof-in-elim-form-to-args, 498
                                          pr...elim-form-to-final-op, 499
                                          proof-in-imp-elim-form-to-arg,

500

                                          proof-in-imp-elim-form-to-op,

501

                                          proof-in-imp-elim-form?, 502
                                          proof-in-imp-intro-form-to-avar,

503

                                          pr...-imp-intro-form-to-kernel,

504

                                          proof-in-imp-intro-form?, 505
                                          proof-in-intro-form-to..., 506
                                          proof-of-efq-at, 507
                                          proof-of-efq-log-at, 508

proof-of-stab-at, 509
proof-of-stab-log-at, 510
proof-subst, 511
proof-substitute, 512
proof-to-aconsts, 513
proof-to-aconsts-without-rules,

514

proof-to-bound-avars, 515
proof-to-context, 516
proof-to-expr, 517
proof-to-extracted-term, 518
proof-to-formula, 519
proof-to-free, 520
proof-to-free-and-bound-avars,

521

proof-to-free-avars, 522
proof-to-soundness-proof, 523
proof=?, 524
proof?, 525
proofs=?, 526
psubst, 527

pt, 528 pv, 529

pvar-cterm-equal?, 530
pvar-name-to-arity, 531
pvar-name?, 532
pvar-to-arity, 533
pvar-to-h-deg, 534
pvar-to-index, 535
pvar-to-name, 536
pvar?, 537

py, 538

Q-clause, 539 Q-goal, 540, 541 Q-sequent, 542 Q-substitution, 543 Q-term, 544

quant-form-to-kernel, 545
quant-form-to-quant, 546
quant-form-to-vars, 547
quant-form?, 548
quant-free?, 549
quant-prime-form?, 550

Rec, 551 Rec, 552 recursion, 553 recursion operator, 554

reduce-efq-and-stab, 555
remove-alg-name, 556
remove-computation-rules-for,

557

remove-global-assumption, 558
remove-predconst-name, 559

remove-program-constant, 560
remove-pvar-name, 561
remove-rewrite-rules-for, 562
remove-theorem, 563
remove-tvar-name, 564
remove-var-name, 565

rename, 566

restrict-substitution-to-args,

567

restrict-substitution-wrt, 568

rewrite rule, 569

rm-exc, 570
save, 571
search, 572
select, 573

semantical model, 574

set-goal, 575
simind, 576
simp, 577
simp-with, 578

special form, 579

split, 580
Stab, 581
Stab-Atom, 582
Stab-Log, 583
star-form-to-left-type, 584
star-form-to-right-type, 585
star-form?, 586
strip, 587

strong elimination, 588

subst-item-equal-wrt?, 589
substitution-equal-wrt?, 590
substitution-equal?, 591
substitution-to-string, 592
synt-total?, 593
tensor-form-to-left, 594
tensor-form-to-parts, 595
tensor-form-to-right, 596
tensor-form?, 597
term-in-abst-form-to-kernel, 598
term-in-abst-form-to-var, 599
term-in-abst-form?, 600
term-in-app-form-to-arg, 601
term-in-app-form-to-args, 602
term-in-app-form-to-final-op,

603

term-in-app-form-to-op, 604
term-in-app-form?, 605
term-in-const-form-to-const, 606
term-in-const-form?, 607
term-in-if-form-to-alts, 608
term-in-if-form-to-rest, 609
term-in-if-form-to-test, 610

term-in-if-form?, 611
term-in-lcomp-form-to-kernel,

612

term-in-lcomp-form?, 613
term-in-pair-form-to-left, 614
term-in-pair-form-to-right, 615
term-in-pair-form?, 616
term-in-rcomp-form-to-kernel,

617

term-in-rcomp-form?, 618
term-in-var-form-to-var, 619
term-in-var-form?, 620
term-subst, 621
term-substitute, 622
term-to-bound, 623
term-to-free, 624
term-to-string, 625
term-to-t-deg, 626
term-to-type, 627
term=?, 628
term?, 629
terms=?, 630
theorem-name-to-aconst, 631, 632
theorem-name-to-inst-proof, 633
theorem-name-to-proof, 634

token, 635 token type, 636, 637 Total, 638, 639

total-aconst, 640
Total-to-E, 641
Total-to-E-nat, 642
truth, 643
truth-aconst, 644
Truth-Axiom, 645, 646
tsubst, 647
tvar-to-index, 648
tvar-to-name, 649
tvar?, 650

type constant, 651 type substitutions, 652 type variable, 653

type-subst, 654
type-substitute, 655
type-to-new-partial-var, 656
type-to-new-var, 657
type-to-string, 658
type?, 659
undo, 660
unfold-cterm, 661
unfold-formula, 662

use, 663

use-with, 664
var-form?, 665

                                          var-term-equal?, 666
                                          var-to-index, 667
                                          var-to-name, 668
                                          var-to-new-var, 669
                                          var-to-t-deg, 670
                                          var-to-type, 671
                                          var?, 672

vector notation, 673

[prev] [prev-tail] [front] [up]