Restrictions Imposed by Function Declarations

The definition of a function must satisfy the restrictions imposed by the input and output formats of the function.

Let a function declaration have either of the two forms

$func  Fname Farg = Fres;
$func? Fname Farg = Fres;

where Farg is the input format of the function, i.e. a format expression which specifies the structure of the function's argument, and Fres is the output format of the function, i.e. a format expression which specifies the structure of the function's result. As mentioned previously the variable indices appearing in formats are of no significance, for which reason, without any loss of generality, they will be supposed to have been omitted.

Then, to formulate the restrictions imposed by the input and output formats of the function, we assume the set of format expressions to be equipped with the following partial ordering.

Let F1 and F2 be two formats. Then F2 >> F1 means that the format F1 is an instance of the format F2. The relation >> is defined by the following rules.

F >> F.
If F1' >> F1 and F2' >> F2 , then F1' F2' >> F1 F2 .
If F1 >> F2 , then (F1) >> (F2) .
e >> F .
If F is not of the form e e ... e, then v >> F .
t >> Gs , for all symbols Gs.
t >> s .
t >> (F) .
s >> Gs , for all symbols Gs.

Now consider a program written in Refal Plus and the constructs appearing in the program.

Let Re be a result expression appearing in the program. A format expression F is said to be the format of Re, if F can be produced from Re by the following transformations.

The indices of all variables appearing in Re are discarded.
All function calls appearing in Re are replaced with the output formats of the corresponding functions. In other words, suppose that a function Fname has been declared as either $func Fname Farg = Fres; or $func? Fname Farg = Fres; . Then each call <Fname Re'> is replaced with Fres.

Let P be a pattern appearing in the program. A format expression F is said to be the format of P, if F can be produced from P by the following transformations.

The indices of all variables appearing in P are discarded.
If P has a direction designator, the designator is discarded.

Let He be a hard expression appearing in the program. A format expression F is said to be the format of He, if F can be produced from P by discarding the indices of all variables appearing in He.

Henceforth, the format of a result expression will be denoted by form[Re], the format of a pattern P by form[P], and the format of a hard expression He by form[He].

It should be emphasized that not only does the format of a result expression Re depend on the structure of Re, but it also depends on the output formats of the functions called in Re. Nevertheless, given a particular program, the meaning of form[Re] is unambiguously defined.

Now we can formulate the restrictions that must be met by the function definitions. These restrictions are imposed on the function calls, the input patterns in the function definitions, and the results returned by the paths.

Suppose the declaration of a function Fname contains the input format Farg, the output format Fres, whereas the pattern alternative Palt appearing in the function definition

     Fname Palt

has the form \{P₁ R₁; ... P_n R_n;}.

Then the following conditions must be satisfied.

The function's input patterns P₁, ..., P_n must satisfy the restriction Farg >> form[P_j].

The calls to the function Fname in all function definitions must satisfy the following condition.

Let a call to the function Fname have the form <Fname Re> . Then there must be satisfied the restriction Farg >> form[Re].

To describe the restrictions imposed on the results returned by paths, we use the following notation.

The fact that the results returned by a path Q satisfy a format F will be written as F |- Q.

Rests, sources, and result expressions may be regarded as particular cases of paths, for which reason the above notation is applicable to them as well as to paths.

Similarly, the fact that the results returned by a pattern alternative Palt satisfy a format F will be written as F |- Palt.

Now we can formulate the restrictions imposed on the function definitions by the output formats of the functions.

Let the definition of a function Fname be Fname Palt, and the output format Fres. Then there must be satisfied Fres |- Palt.

The relations F |- Q and F |- Palt are defined by the following inference rules.

     form[] |- S              form[He] |- S
     F |- R                   F |- R
     ------------             ---------------
     F |- S R                 F |- S :: He R


     form[He] |- S''
     form[He] |- S'
     F |- R
     -------------------------
     F |- S'' $iter S' :: He R


                                        form[] |- S
     F |- R              F |- Q         F |- R
     -------------       ---------      ------------
     F |- S : P R        F |- , Q       F |- # S R


     F |- Q              F |- Q
     ----------          ----------     F |- $fail
     F |- \? Q           F |- \! Q


     F |- Q
     ---------           F |- $error Q
     F |- = Q


     F |- Q
     F |- Palt
     ------------------------
     F |- $trap Q $with Palt


     F |- Q_j  for all j=1,...,n
     ---------------------------
     F |- \{Q₁; ... Q_n;}


     F |- Palt           F >> form[Re]
     --------------      --------------
     F |- S : Palt       F |- Re


     F |- R_j  for all j=1,...,n
     ---------------------------
     F |- \{P₁ R₁; ... P_n R_n;}