Inductive structures

Documentation and user's manual

Table of contents

OCaml programs

Inductive structures

An inductive definition of a set S gives a way to construct any element of S.

This is useful when defining a function whose application returns results in S (or results that are tuples at least one component of which is in S).

But this is not immediately useful when recursively defining a function whose arguments are in S (or are tuples at least one component of which is in S).

While the inductive definition of S gives a way to synthesize any element of S, what is required here is a way to analyze any element of S.

What is required is called from now on an inductive structure over S, that is, a set of functions: Constructors: a 0-ary basic constructor (function) for each rule in the basis, a n-ary inductive constructor (function) for each n-ary inductive rule and if necessary predicate functions that check whether inductive constructors can be applied. Accessors: functions that give access to the components of the non-atomic elements of S (i.e., not in the basis of S) and predicate functions that check whether these functions can be applied. At least one such predicate function is required in order to check whether an element of S is atomic. Moreover if there is more than one atomic element then other predicate functions are required in order to identify each atomic element.

In the sequel several inductive structures over types (i.e., sets of values) are given. An inductive structure over a type makes it of practical use because its values can then be synthesized or analyzed. Yet this is true only if the internal representation of values is accessible. However as most of the types given in the sequel will be made abstract, the functions in their inductive structures will not be sufficient for practical use (internal representations will be hidden). Functions that return string representations of values will be necessary. Thus each type will be equipped with a set of functions: those in its inductive structure and one or several functions that return string representations of its values.

Inductive structures

Documentation and user's manual

Table of contents

OCaml programs