up | previous | next | detailed contents | brief contents

Notations and Definitions

For technical reasons, three different notations are used for terms of TRC in this document. The reader will quickly get used to switching between them.

OTTER's default input notation, in which the basic operations of pairing, application and constant-function formation are written in the usual mathematical notation for functions. An example is a(a(a(abst,x),y),z) = a(a(x,k(z)),a(y,z)). This notation is used only in the direct listings of the OTTER input.
OTTER's bird_print output notation (so named presumably because combinators are described as "birds" in Ramond Smullyan's book To Mock a Mockingbird [7]). The bird_print notation is just the standard notation for combinatory logic, where the application operation is written simply as a blank space, and parentheses are dropped when possible using the convention of association to the left. An example is abst x y z = x k(z) (y z).
A LISP-like notation which uses the language of TRC together with syntax for two forms of lambda-expression. An example is (a (a (a abst x) y) z) = (a (a x (k z)) (a y z)). I format this notation using the LISP pretty-printing convention of aligning all the operands of a given operation at the same column. I use this notation for readability in long, complex terms and as input to my programs which use Holmes's abstraction-algorithm to eliminate the lambda syntax. This lambda-syntax is not part of the formal language I use in this document. It is always systematically eliminated using my implementation of Holmes's abstraction algorithm before an OTTER input file is generated.

An example of the third notation with the lambda syntax follows:

(lambda x
  (lambda y
    (lambda z
      (a (a x (k z))
	 (a y z)))))

Note that the two operands of the top-level a operator are aligned at the same column, making it easier to discern the structure of the term. The above lambda-term would be converted by my program to the atomic term abst.

We can think of abst as a function of three arguments x, y, and z at three different levels, level 2, level 1, and level 0 respectively. A level-2 object is thought of as a function from level-1 objects to level-1 objects, and a level-1 object is thought of as a function from level-0 objects to level-0 objects.

More formally, if x is a variable and S and T are terms, then

x occurs at level 0 in the atomic term x
if x occurs at level n in S then x occurs at level n + 1 in S T.
if x occurs at level n in T then x occurs at level n in S T.
if x occurs at level n in S then x occurs at level n - 1 in k(S).
if x occurs at level n in S or in T then x occurs at level n in pair(S,T).

Note that a variable may occur at more than one level in a term. In this case we say that the term is unstratified. The basic abstraction property [2] of TRC is that if x does not occur in T at any level other than zero, then there is a term (lambda x T) which when applied to S yields a term provably equal to the term T' obtained from T by substituting S for all occurrences of x.

We can use TRC's pairing facility to represent functions of multiple arguments where all arguments are at the same level. My programs allow a special lambda-notation for a function of two level-0 arguments. An example follows:

(lambda f
  (lambda (x y)
    (a eq (pair (a f x)
		(a f y)))))

Note that a single argument (like f in the above term) is not enclosed in parentheses, but a pair of arguments at the same level (like (x y) in the above term) is enclosed in parentheses. Every object in TRC can also be regarded as a pair of objects. The above lambda-term is actually just a shorthand for the one below, where the argument pair (x y) is replaced by u, while x is replaced by (a p1 u), and y is replaced by (a p2 u).

(lambda f
  (lambda u
    (a eq (pair (a f (a p1 u))
		(a f (a p2 u))))))

My program will eliminate the bound variables f, x, y, and u in the above terms, and both terms will be transformed into the following term built using only the four constants mentioned in the axioms of TRC:

(a (a abst (k (a abst (k eq))))
   (pair (a (a abst abst) 
	    (k p1)) 
	 (a (a abst abst) 
	    (k p2))))

In the online version of this thesis, you can click the button above to bring up an applet that I wrote in Java. The applet translates between the three notations described above. Any change you make in the input term is immediately reflected in the output. The applet follows the OTTER convention of treating atomic terms as variables if their names begin with u, v, w, x, y, or z. The text box on the right-hand side of the applet window lists the free variables beginning with u, v, w, x, y, or z and the levels at which they occur. Check both the reduce and factor checkboxes to simplify the answers using axioms of TRC. The pop-up menu and command button let you insert the definition of push, or of other terms used in the definition of push, into the input.

Try pasting the following examples into the applet, then try your own variations. Notice the levels of the variables, listed on the right-hand side of the applet window.

In LISP input mode:
- (k (a x y))
- (lambda x (k (a x y)))
- (lambda y (k (a x y)))
- (lambda x z)
- (lambda (f g) (lambda x (a eq (pair (a f x) (a g x)))))
- (lambda x (lambda y (lambda z (a (a x (k z)) (a y z)))))
- (lambda (x y) (pair (pair y x) (pair y x)))
- (lambda (x y) (a eq (pair x y)))
In Bird input mode:
- abst abst x y z (check the "Reduce" checkbox)
- x y z (x y z)
- eq (pair(p1,p2) x)

up | previous | next | detailed contents | brief contents