XUMERATIOK MODELS OF A-CALCULUS
by AKIRA KANDA in Vancouver (Canada)')
81. A-ealculns
The A-calculus developed by CHURCH [2] is a formal system designed to study the equivalence of functions composed from other functions in certain primitive ways. In this section, we briefly overview this calculus. Since the synt'ax of A-calculus plays an important role in the construction of numeration models, we present the syntax in quite a detailed manner. \Ve start, with assuming a countable set V of varialiles.
Definition 1.2. We define a binary relation occurs over A-terms as follows:
1 . X occurs in X. 2 . If 9 occurs in Jf or in N : then X occurs in ( M N ) .
3 . If S occurs in iM, t,hen for every variable y. S occurs in (Ay.JI). IYe writ,e S E 1for " X occurs in Y".
Definition 1.3. An occurrence of a variable . r in M is bound if it is inside a part of JI of the form A.z.Y, otherwise it' is free. We say x is free in M if it has a free occurrence in Jf. D e f i n i t i o n 1.4. For any terms M , N and any variable zI the result M [ s := N ] of substituting N for each free occurrence of .P in M (and changing bound variables to avoid clashes) is defined as follows:
2 . z[x :
= N ] = z for all variables z + 2.