4. Constants

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

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

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

4.1. Rewrite and computation rules for program constants.

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

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

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

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

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

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

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

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

4.2. Recursion over simultaneous free algebras.

,

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

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

the step type

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

,

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

A simple example for simultaneous free algebras is

The constructors are

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

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

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

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

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

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

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

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

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

,

,

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

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

Constructor, accessors and tests for all kinds of constants:

From these we can define

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

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

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

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

To add and remove program constants we use

To add and remove computation and rewrite rules we have

To generate our constants with fixed rules we use

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

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