3 Variables

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. n,m for variables of type nat. Then also n0,n1,n2,…,m0,… can be used for the same purpose.

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

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

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

The ﬁrst 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 speciﬁc 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? x)		incomplete test
	(var? x).		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? var)
	(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 inﬁnitely many variables of every type”. Giving a constructive proof for this statement would require to give inﬁnitely 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 speciﬁcation ﬁnite we require the examples to be given in a uniform way, i.e. by a function of two arguments. To make sure that all these examples are in fact different, we would have to require make-var to be injective. Instead, we require (classically equivalent) make-var to be a bijection on its image, as again, this can be turned into a computational statement by requiring that a witness (i.e. an inverse function) is given.

Finally, as often the exact knowledge of inﬁnitely many variables of every type is not needed we require that, either by using the above functions or by some other form of deﬁnition, functions

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

are deﬁned that return a (total or partial) variable of the requested type, different from all variables that have ever been returned by any of the speciﬁed 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. for bound renaming. Therefore we supply

(var-to-new-var var).

Implementation. Variables are implemented as lists:

(var type index t-deg name ).

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