Some Properties of Conversion
Author(s): Alonzo Church and J. B. Rosser
Source: Transactions of the American Mathematical Society , May, 1936, Vol. 39, No. 3
(May, 1936), pp. 472-482
Published by: American Mathematical Society
Stable URL: https://www.jstor.org/stable/1989762
JSTOR is a not-for-profit service that helps scholars, researchers, and students discover, use, and build upon a wide
range of content in a trusted digital archive. We use information technology and tools to increase productivity and
facilitate new forms of scholarship. For more information about JSTOR, please contact support@jstor.org.
Your use of the JSTOR archive indicates your acceptance of the Terms & Conditions of Use, available at
https://about.jstor.org/terms
American Mathematical Society is collaborating with JSTOR to digitize, preserve and extend
access to Transactions of the American Mathematical Society
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
SOME PROPERTIES OF CONVERSION*
BY
ALONZO CHURCH AND J. B. ROSSER
Our purpose is to establish the properties of conversion which are expressed
in Theorems 1 and 2 below. We shall consider first conversion defined
by Church's Rules I, II, IIIt and shall then extend our results to several other
kinds of conversion.:
1. Conversion defined by Church's Rules I, II, III. In our study of conversion
we are particularly interested in the effects of Rules II and III and
consider that applications of Rule I, though often necessary to prevent confusion
of free and bound variables, do not essentially change the structure of
a formula. Hence we shall omit mention of applications of Rule I whenever it
seems that no essential ambiguity will result. Thus when we speak of replacing
{ Xx. MI (N) ? by S xMI it shall be understood that any applications of I
are made which are needed to make this substitution an application of II.
Also we may write bound variables as unchanged throughout discussions even
though tacit applications of I in the discussion may have changed them.
A conversion in which III is not used and II is used exactly once will be
called a reduction. If II is not used and III is used exactly once, the conversion
will be called an expansion. "A imr B," read "A is immediately reducible to
B," shall mean that it is possible to go from A to B by a single reduction.
"A red B," read "A is reducible to B," shall mean that it is possible to go
from A to B by one or more reductions. "A conv-I B," read "A conv B by
applications of I only," shall mean just that (including the case of a zero number
of applications). "A conv-I-II B," read "A conv B by applications of I
* Presented to the Society, April 20, 1935; received by the editors June 4, 1935.
t By Church's rules we shall mean the rules of procedure given in A. Church, A set of postulat
for thefoundation of logic, Annals of Mathematics, (2), vol. 33 (1932), pp. 346-366 (see pp. 355-356),
as modified by S. C. Kleene, Proof by cases informal logic, Annals of Mathematics, (2), vol. 35 (1934),
pp. 529-544 (see p. 530). We assume familiarity with the material on pp. 349-355 of Church's paper
and in ??1, 2, 3, 5 of Kleene's paper. We shall refer to the latter paper as "Kleene."
I The authors are indebted to Dr. S. C. Kleene for assistance in the preparation of this paper,
in particular for the detection of an error in the first draft of it and for the suggestion of an improvement
in the proof of Theorem 2.
? Note carefully the convention at the beginning of ?3, Kleene, which we shall constantly use.
|| Our use of "conv" allows us to write "A conv B" even in the case that no applications of J,
II, or III are made in going from A to B and A is the same as B. But we write "A red B" only if
there is at least one reduction in the process of going from A to B by applications of I and II, and
use the notation "A conv-I-II B" if we wish to allow the possibility of no reductions.
472
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
SOME PROPERTIES OF CONVERSION 473
and II only," shall mean just that (including the case of a zero number of
applications).
We shall say that we contract or perform a contraction on { Xx. M } (N) if
we replace it by S 'MI.
It is possible to visualize the process of conversion by drawing a broken
line in which the segments correspond to successive steps of the conversion,
horizontal segments indicating applications of I, segments of negative slope
applications of II, and segments of positive slope applications of III. Thus,
in the figure A1 conv A2 and B1 conv B2 each by a single use of I, A2 conv A3
and B2 conv B3 each by a single use of III, and A7 conv A8 and C1 conv C2
each by a single use of II. The dotted lines represent various alternative conversions
to the conversion given by the solid line.
A-6 At
A A4
B, B2 ,,
C2 C3
A conversion in which no expansions follow any reductions will be called
peak and one in which no reductions follow any expansions will be called a
valley. The central theorem of this paper states that if A conv B, there is a
conversion from A to B which is a valley. We prove it by means of a lemma
which states that a peak in which there is a single reduction can always be
replaced by a valley. Then the theorem becomes obvious. For example, in
the conversion pictured by the solid line in the figure we replace the peak
A1A2... A8 by the valley A1B1B2B3A8, then the peak B2B3A8A9 by the valley
B2A9, then the peak A10All .. A14 by the valley A10C1C2C3A14, getting the
valley A1B1B2A9A1oC1C2C3A14.
Suppose that a formula A has parts { Xx1. M2 } (N1) which may or may not
be parts of each other (cf. Kleene 2VIII (p. 532)). We suppose that, if p-q,
{Ixp. Mp } (Np) is not the same part as {XXq. Mq } (Nq), though it may be th
same formula. The { xxj. M, } (Ni) need not be all of the parts of A which hav
the form { Xy. P } (Q). We shall define the residuals of the { Xx2. Mj } (Ni) aft
a sequence of applications of I and II (these residuals being certain wellformed
parts of the formula which results from the sequence of applications of
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
474 ALONZO CHURCH AND J. B. ROSSER [May
I and II). If no applications of I or II occur, each part { Xxi. Mj } (Nj) is its
own residual. If a series of applications of I occur, then each part { Xx1. Mj I (N
is changed into a part { Xyi. MJ } (NJ) of the resulting formula and this pa
Xyi.MJ } (NJ) is the residual of { Xx1. M1 } (Nj) in the resulting formula.
Clearly the residuals of two parts coincide only if the parts coincide. Next
consider the case where a single reduction occurs. Let { Xx. M } (N) be the part
of A which is contracted in performing the reduction and A' be the formula
resulting from A by the reduction. Let { xp. Mp } (Np) be an arbitrary one
of the { Xx1. Mj } (Nj).
Case 1. Let {Xxp.Mp}(Np) not be part of {Xx.M}(N). Then either (a)
{Xx.M} (N) has no part in common with {Xxp.M,} (Np) or else (b)
{Xx. M} (N) is part of {Xxp. Mp } (Np) (by Kleene 2VIII). If (a) holds,
then under the reduction from A to A', {Xxp. Mp } (Np) goes into a definite
part of A' which we shall call the residual in A' of { xp. Mp } (Np). In this
case the residual of {Axpx. Mp } (Np) is the same formula as { Xxp. Mp } (Np). If
(b) holds then { Xx. M } (N) is part either of Mp or of Np since { Xxp. Mp } (Np)
is not part of {Xx.M} (N) (see Kleene, 2X and 2XII). Hence if we contract
{Xx. M }(N) we perform a reduction on the formula { xp. Mp } (Np) whic
carries it into a formula {IXx' . Mp' } (Np). Then the reduction from A t
can be considered as consisting of the replacement of the part { Xxp. Mp
of A by {Ix<' . Mp' } (Np) and this particular occurrence of { Xx<' . Mp }
in A' is called the residual in A' of {Xxp. Mp } (Np).
Case 2. Let {Xxp.Mp}(Np) be part of {Xx.M}(N). By Kleene 2X this
case breaks up into three subcases.
(a) Let { Xxp. Mp } (Np) be { Xx. M } (N). Then we say that { xpx. Mp } (Np)
has no residual in A'.
(b) Let { Xxp. Mp } (Np) be part of Xx. M and hence part of M (by Kleen
2XII). Let M' be the result of replacing all free x's of M except those occurring
in { Xxp . Mp } (Np) by N. Under these changes the part { Xxp. Mp } (Np) o
Mgoes into a definite part of M' which we shall denote also by {Xxxp. Mp } (Np
since it is the same formula. If now we replace { xp. Mp } (Np) in M' by
XxP . Mp } (Np) |, M' becomes SN MI and we denote by S {x Xxp. M, I (N,) I
the particular occurrence of S {' Xxp. Mp } (Np) I in SzXMI that resulted from replacing
{ Xxp. Mp } (Np) in M' by the formula S {x Xxp. Mp } (Np) . Now the residual
in A' of { xp,. Mp } (Np) in A is defined to be the part SN { IXxp. Mp } (Np)|
in the particular occurrence of S xMI in A' that resulted from replacing
{Xx. M} (N) in A by SNxMI.
(c) Let {Xxp. Mp } (Np) be part of N. And let {XYi. Pi} (Qi) respectively
stand for the particular occurrences of the formula { Xxp. Mp } (Np) in S xNMI
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
1936] SOME PROPERTIES OF CONVERSION 475
which are the part { Xx,. Mp } (Np)
formula N in S1'MI that resulted f
the residuals in A' of {IXx.M,}
the particular occurrence of the f
placing {Xx.M}(N)inAbyS xMI
This completes the definition o
in A in the case that A' is obtained from A by a single reduction. Clearly the
residuals in A' of {Xxp. Mp } (Np) in A (if any) have the form {Xx. M} (N). Call
them {XY i. Pi } (Q ). Then if A' imr A ", the residuals in A " of {Xxp .Mp } (Np)
in A are defined to be the residuals in A" of the {Xyi%. pi } (Qi) in A'. We continue
in this way, defining the residuals after each successive reduction as
the residuals of the formulas that were residuals before the reduction, and
noting that the residuals always have the form { Xx. MI (N). We also no
that a residual in B of the part { Xx. MI (N) in A cannot coincide with
residual in B of the part {Xx'. M' } (N') in A unless I Xx. M} (N) coincide
with {Xx'.M'}(N').
We say that a sequence of reductions on A, say A imr A1 imr A2 imr
imr A,+,, is a sequence of contractions on the parts { Xxi. Mj I (Nj) of A if the
reduction from Ai to Ai+, (i=O, , n; Ao the same as A) is a contraction
on one of the residuals in Ai of the {xxj. Mj 1 (Nj). Moreover, if no residuals
of the { Xx1. Mj } (Nj) occur in A,+, we say that the sequence of contractions
on the {IXx. M1 1(Nj) terminates and that A,+, is the result.
In some cases we wish to speak of a sequence of contractions on the parts
{Xxj. M } (Nj) of A where the set {Xx. Mj} (Nj) may be vacuous. To handle
this we shall agree that if the set {Xx. Mj (Nj) is vacuous, the sequence of
contractions shall be a vacuous sequence of reductions.
LEMMA 1. If { Xx . Mj 1 (Nj) are parts of A, then a number m can be fo
such that any sequence of contractions on the { Xx1. Mj } (Nj) will terminate aft
at most m contractions, and if A' and A" are two results of terminating sequen
of contractions on the {xjx. Mj } (Nj), then A' conv-I A".
Proof by induction on the number of proper symbols of A.
The lemma is true if A is a proper symbol, the number m being 0.
Assume the lemma true for formulas with n or less proper symbols. Let A
have n+ 1 proper symbols.
Case 1. A is Xx. M. Then all the parts {IXx. Mj } (Nj) of A must be parts
of M. However M has only n proper symbols and so we use the hypothesis
of the induction.
Case 2. A is {F } (X).
(a) {F} (X) is not one of the {IXx.M1} (Nj). Then any sequence of co
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
476 ALONZO CHURCH AND J. B. ROSSER [May
tractions on the parts { Xx1. Mj } (Nj) of A can be replaced* by two sequences
of contractions performed successively, one on those of the { Xx1. M, } (Nj)
which are parts of F and one on those of the { Xxi. Mj } (Nj) which are parts
of X, in such a way that if the original sequence of contractions carried
IF I (X) into { F' } (X') then the two sequences of contractions by
is replaced carry F into F' and X into X' respectively and the total number
of contractions on residuals of parts of F or on residuals of parts of X is the
same as before.t Then we use the hypothesis of the induction, since F and X
each have n or less proper symbols.
(b) { F } (X) is one of the { Xx1. Mj I (Nj), say { Xx,. Mp } (Np). As long as
the residual of { Xx,. Mp } (Np) has not been contracted, the argument of (a)
applies. Hence if any sequence of contr'actions on the { Xx1. M1 } (Nj) of A
is continued long enough, the residual of {Xxp . Mp } (Np) must be contracted
(since we prove readily that one and only one residual of {Ixp. Mp } (Np
occurs, until a contraction on the residual of {Ixp . Mp } (Np)). Let a sequence
of contractions, A, on the { Xx1. Mj } (Nj) consist of a sequence, 4, of contractions
on the { Xx1. M, 1(Nj) which are different from { xpx. Mp } (Np), a contraction,
3, on the residual of { xp. Mp } (Np), and a sequence, 0, consisting
of the remaining contractions of ,. Now, as in (a), we can replace 0 by a sequence,
a, of contractions on the { Xx3. M, } (Nj) which are parts of Xxp.Mp
(and therefore parts of Mp), followed by a sequence, -q, of contractions on the
IXx. M1 } (Nj) which are parts of Np, and this without changing the total
number of contractions on residuals of parts of Mp or on residuals of parts of
Np. Then -q followed by 3 can be replaced by 3', a contraction on the residual,
{Xy. P} (Np), of {Xxp.Mp} (Np), followed by a set of applications of -7 onl
each of the occurrences of Np in SNY P that arose by substituting Np for y in
P. Our sequence of contractions now has a special form, namely a sequence of
contractions, a, on parts of Mp, followed by a contraction, 3', on the resid
of {Ixp. Mp } (Np), followed by other contractions. We will now indicat
process whereby this sequence of contractions can be replaced by another
having the same special form but having the property that after the contraction
on the residual of { xp. Mp } (Np) one less contraction on the residuals
of parts of Mp occurs. This process can then be successively applied
* We say that a sequence, ,u, of reductions on A can be replaced by a sequence, v', of reductions
on A, if both ,u and v give the same end formula B and residuals in B of any part { Xxj.Mj I (Nj) are
the same under both A and v.
t The reader will easily understand the convention which we use when we say that the same
sequence of contractions which carries F into F' will carry IF| (X) into {F'| (X) and that the same
sequence of contractions which carries X into X' will carry { F' |(X) into { F' | (X'). This convention
will also be used in (b).
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
1936] SOME PROPERTIES OF CONVERSION 477
until no contraction on a residual o
tion on the residual of Xx,. M, }
one the number of contractions which precede the contraction on the residual
of {IXx. M, } (Np), so that the total number of contractions on residuals of
parts of M, is the same after the process as before, and hence the same as in
Let us consider that sequence of reductions v which is composed of d'
and the contractions that follow it, up to and including the first contraction
on a residual of a part of M,. Denoting the formula on which ? acts by
I Xy. P } (Np), we see that ? can be considered as the act of first replacing the
free y's of P by various formulas, Npk, got from N, by sets of reductions, and
then contracting on a residual, { Xz. R } (S), of one of the { Xx3. M, } (Nj) which
are parts of Mp, say { xq Mq } (Nq). From this point of view, we see that
none of the free z's of R are parts of any Npk, and hence k can be replaced by
a contraction on the residual in Xy. P of { XXq . Mq } (Nq) of which { Xz .R } (S)
is a residual, followed by a contraction on the residual of { Xxp. Mp } (Np), followed
by contractions on residuals of parts of Np. This completes the indication
of what the process is.
Hence A can be replaced by a sequence of contractions, a, on the
Xx,. Mi } (Nj) which are parts of Mp (such that a contains as many contractions
as there are contractions in ,u on residuals of parts of Mr), followed by
a contraction, /, on the residual of {Xxp . M. } (Np), followed by a sequence of
contractions, y, on residuals of parts of Np. Moreover, after a and 3,
{Xxxp. Mp } (Np) has become a formula containing several occurrences of N,
and y is a sequence of contractions on parts of these occurrences of N,
Hence, since xpx. Mp and Np each contain n or less proper symbols, we can
use the hypothesis of the induction in connection with a and y to show that
if a followed by ,B followed by -y terminates the result is unique to within applications
of I. But if u terminates, so does a followed by / followed by y.
Hence the results of any two terminating sequences are unique to within applications
of I.
It remains to be shown that a number m can be found such that each sequence
of contractions terminates after at most m contractions.
By the hypothesis of induction, a number a can be found such that any
sequence of contractions on those { Xx1. M2 } (Nj) which are parts of M
terminates after at most a contractions, and a number b can be found such
that any sequence of contractions on those { Xx3. M3 } (Nj) which are parts of
Np terminates after at most b contractions. Then any sequence of contractions
on the Xx1. M1 } (Nj) of A must, if continued, include a contraction
on the residual of {Xxp.Mp} (Np), after at most a+b+l contractions.
Hence we may confine our attention to sequences of contractions A on
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
478 ALONZO CHURCH AND J. B. ROSSER [May
the {IXx. M2 I (N1) of A which inclu
Xxv. Mp (Nr) and which can therefore be replaced by a sequence of contractions
of the form, a followed by / followed by y. Moreover it will be
clear, on examination of our preceding argument, that, when the sequence 4
is replaced by the sequence, a followed by / followed by y, the total number
of contractions in the sequence is either increased or left unchanged (because
each step in the process of transforming A into a followed by : followed by y
has the property that it cannot decrease the total number of contractions).
Therefore it is sufficient to find a number m such that any sequence of contractions
on the {IXx1. M1 I (Nj) of A which has the form, a followed by A followed
by y, must terminate after at most m contractions.
If we start with the formula M, and perform a terminating sequence of
contractions on those {\Xx. M2 1(Nj) which are parts of Mp, the result is a
formula M,, which is unique to within applications of I, and which contains
a certain number, c, > 1, of occurrences of xp as a free symbol. And in the
case of any sequence of contractions on those { Xx1. M1 1 (Nj) which are parts
of M,, whether terminating or not, the result (that is, the formula into which
Mp is transformed) contains at most c occurrences of x, as a free symbol.
Hence the required number m is a+ 1 +cb.
LEMMA 2. If A imr B by a contraction on the part {Xx. MI (N) of A, and
A is A1, and A, imr A2, A2 imr A3, , and, for all k, Bk is the result of a
terminating sequence of contractions on the residuals in Ak of { Xx. MI (N), then:
I. B1 is B.
II. For all k, Bk conv-I-II Bk+l.
III. Even if the sequence A1, A2, -can be continued to infinity, there is
a number 0m, depending on the formula A, the part { Xx. MI (N) of A, and the
number m, such that, starting with B,n, at most q$in consecutive Bk's occur for which
it is not true that Bk red Bk+1.
Part I is obvious.
We prove Part II readily as follows. Let {xyi. Pi I (Qi) be the residuals in
Ak of {Xx.MI (N) and let Ak imr Ak+l be a contraction on the part
{Xz.R I(S) of Ak. Then Bk+1 is the result of a terminating sequence of contractions
on {IXz.R } (S) and the parts {xyi. Pi I (Qi) of Ak. Now if {IXz.R I (S)
is one of the {xyi. Pi (Qi), then no residuals of {Xz.RI (S) occur in Bk, and
Bk conv-I Bk+l. If however {Xz.RI (S) is not one of the {xyi. Pi4 (Qi), then
a set of residuals of Xz.R I (S) does occur in Bk and a terminating sequence
of contractions on these residuals in Bk gives Bk+j by Lemma 1.
In order to prove Part III we note that Bk red Bk+1 unless the reduction
from Ak to Ak+1 consists of a contraction on a residual in Ak of { Xx. M I (N)
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
1936] SOME PROPERTIES OF CONVERSION 479
(see preceding paragraph). But if we start with any particular Ak this can
only be the case a finite number of successive times, by Lemma 1. Hence we
define 0)m as follows. Perform m successive reductions on A in all possib
ways. This gives a finite set of formulas (except for applications of I). In
each formula find the largest number of reductions that can occur in a terminating
sequence of contractions on the residuals of {Xx . M} (N). Then let 'Im
be the largest of these.
THEOREM 1. If A conv B, there is a conversion from A to B in which no
expansion precedes any reduction.
That is, any conversion can be replaced by a conversion which is a valley.
This follows from Lemma 2 by the process already indicated.
COROLLARY 1. If B is a normal form* of A, then A conv-I-II B.
For no reductions are possible on a normal form.
COROLLARY 2. If A has a normal form, its normal form is unique (to within
applications of Rule I).
For if B and B' are both normal forms of A, then B' is a normal form of B.
Hence B conv-I-II B'. Hence B conv-I B', since no reductions are possible
on the normal form B.
Note that only parts I and II of Lemma 2 are needed for Theorem 1 and
its corollaries.
THEOREM 2. If B is a normal form of A, then there is a number m such
that any sequence of reductions starting from A will lead to B (to within applications
of Rule I) after at most m reductions.
We prove by induction on n that, if a formula B is a normal form of some
formula A, and there is a sequence of n reductions leading from A to B, then
there is a number VA,n depending on the formula A and the number n such
that any sequence of reductions starting from A will lead to a normal form of A
(which will be B to within applications of I by Theorem 1, Corollary 2) in
at most VIA,n reductions.
If n=O, we take 41A,O to be 0.
Assume our statement for n =k. Let A imr C, C imr C1, C1 imr C2, ,
Ck-l imr B. Let A be the same as A1, A1 imr A2, A2 imr A3, ... . By Lemma 2
there is a sequence (D1 the same as C) D1 conv-I-II D2, D2 conv-I-II D3,
such that Ai conv-I-II Di for all j's for which Ai exists, and also, if the reduction
from A to D1 (or C) is a contraction on Xx. M} (N), such that, starting
with Dmn at most Om consecutive D2's occur for which it is not true that
* Kleene ?5, p. 535.
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
480 ALONZO CHURCH AND J. B. ROSSER [May
Di red Di+,. The sequence C imr C
and so by the hypothesis of the in
any sequence of reductions on C leads to a normal form (i.e., terminates)
after at most 4'C,k reductions. Hence there are at most 4tC,k reductions in t
sequence D1 conv-I-II D2, D2 conv-I-II D3, - * * , and hence this terminates
after at most f(41c, k) steps where f(p) is defined as follows:
f(0) = 41,
f(p + 1) = f(P) + M + 1,
where M is the greatest of the numbers c1,02, . , f(p)+I.*
Then, since the sequence of Di's continues as long as there are Ai's on
which reductions can be performed, it follows that after at mostf(Vtc,k) reductions
we come to an Ai on which no reductions are possible. But this is
equivalent to saying that this Aj is a normal form. Hence any sequence of
k+1 reductions from A to B determines an upper bound which holds for all
sequences of reductions starting from A. We then take all sequences of k +1
reductions starting from A (this is a finite set of sequences, since we reckon
two sequences as the same if they differ only by applications of I) and find
the upper bounds determined by each one of them that leads to a normal
form. Then we define VIA,k+1 to be the least of these upper bounds.
This completes our induction. But, by Theorem 1, Corollary 1, if B is a
normal form of A, there is a sequence of some finite number of reductions
leading from A to B. Hence Theorem 2 follows.
COROLLARY. If a formula has a normal form, every well-formed part of it
has a normal form.
2. Other kinds of conversion. There are also other systems of operations
on formulas, similar to the system which we have been discussing and in
which there can be distinguished reductions and expansions and possibly neutral
operations (such as applications of Rule I). For convenience, we speak
of the operations of any such system as conversions, and we define a normal
form to be a formula on which no reductions are possible.
A kind of conversion which appears to be useful in certain connections is
obtained by taking a new undefined term a (restricting ourselves by never
using a as a bound symbol) and adding to Church's Rules I, II, III the following
rules:
IV. Suppose that M and N contain no free symbols other than 3, that there
* f(p) depends, of course, on the formula A and the part { Xx.M} (N) of A, as well as on p,
because 'km depends on A and I Xx.M} (N).
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
1936] SOME PROPERTIES OF CONVERSION 481
is no part {Xz . P } (Q) of either M or
M or N in which R and S contain no free symbols other than a. Then we may
pass from a formula J to a formula K obtained from J by substituting for a particular
occurrence of 5 (M, N) in J either Xfx.f(f(x)) or Xfx.f(x) according to
whether it is or is not true that M conv-I N.
V. The inverse operation of that described in Rule IV is allowable. That is,
we may pass from K to J under the same circumstances.
We call an application of Rule II together with applications of Rule I,
or an application of Rule IV together with applications of Rule I, a reduction,
and the reverse operations (involving Rule III or Rule V) expansions. We
call any sequence of applications of various ones of the five rules a conversion.
Also we say that we contract { Xx. MI (N) if we replace it by S'MI, and that
we contract a(M, N) if we replace it by Xfx.f(f(x)) or Xfx.f(x) in accordance
with Rule IV.
We define the residuals of { Xx. MI (N) after an application of I or II in
the same way as before, and after an application of IV as what {Xx. MI (N
becomes (the restrictions in IV ensure that it becomes something of the form
Xy. P 1(Q)). The residuals of a (M, N) after an application of I, II, or IV
are defined only in the case that M and N are in normal form and contain no
free symbols other than a. In that case the residuals of a(M, N) are whatever
part or parts of the entire resulting formula a(M, N) becomes, except that
after an application of IV which is a contraction of a (M, N) itself, a (M, N)
has no residual. Thus residuals of a (M, N) are always of the form a (P, Q),
where P and Q are in normal form and contain no free symbols other than a.
We define a sequence of contractions on the parts { Xxj. Mj 1 (Nj) and
b(Pi,Qi) of A, where Pi and Qi are in normal form and contain no free
symbols other than a, by analogy with our former definition. Similarly for a
terminating sequence of such contractions. Then we prove Lemma 1 by an
obvious extension of our former argument. Lemma 2 and Theorems 1 and 2
then follow as before. Of course we replace "conv-I-II" by "conv-I-II-IV"
in Lemma 2 and in general throughout the proofs of Theorems 1 and 2. In
Lemma 1 we allow that the set of parts of A on which a sequence of contractions
is taken should include not only parts of the form { Xx1. M, 1 (Nj) but
also parts of the form a(Pk,Qk) in which Pk and Qk are in normal form and
contain no free symbols other than a. And in Lemma 2 we consider also the
case that A imr B by a contraction on the part a(P,Q) of A.
We may also consider a third kind of conversion, namely the conversion
that results if we modify Kleene's definitions of well-formed, free, and bound
by omitting the requirement that x be a free symbol of R from (3) of the defiThis
content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms
482 ALONZO CHURCH AND J. B. ROSSER
nition (see Kleene, top of p. 530) and then modify Church's rules I, II, III
by using the new meanings of well-formed,free and bound and by omitting "if
the proper symbol x occurs in M" from both II and IIJ.* Then we call an
application of the modified II together with applications of the modified I
a reduction, and the reverse operation an expansion, and applications of all
three rules conversion. Also we say that we contract {Xx. M} (N) if we replace
it by S1'M . If A has the form {Xx. M} (N1 I N2, ... ,Nr), then {'Xx. M} (N1)
is said to be of order one in A and a contraction of {Xx.M} (N1) is said to be
a reduction of order one of A. Then Lemma 1 and parts I and II of Lemma
2 hold (although some modification is required in the proofs). Hence Theorem
1 and its corollaries hold. But Theorem 2 is false. Instead a weaker form of
Theorem 2 can be proved, namely:
THEOREM 3. If A has a normal form, then there is a number m such that at
most m reductions of order one can occur in a sequence of reductions on A.
* The first kind of conversion which we have considered is essentially equivalent to a certain
portion of the combinatory axioms and rules of H. B. Curry (American Journal of Mathematics,
vol. 52 (1930), pp. 509-536, 789-834), as has been proved by J. B. Rosser (see Annals of Mathematics,
(2), vol. 36 (1935), p. 127). In terms of Curry's notation, our third kind of conversion can be
thought of as differing from the first kind by the addition of the constancy function K.
In dealing with properties of conversion, use of the Schonfinkel-Curry combinatory analysis
appears in certain connections to be an important, even indispensable, device. But to recast the present
discussion and results entirely into a combinatory notation would, it is thought, be awkward
or impossible, because of the difficulty in finding a satisfactory equivalent, for combinations, of the
notions of reduction and normalform as employed in this parer.
PRINCETON UNIVERSITY,
PRINCETON, N. J.
This content downloaded from
147.251.47.166 on Tue, 12 Mar 2024 10:47:06 +00:00
All use subject to https://about.jstor.org/terms