Definition of push

list(demodulators).
push = a(a(abst,a(a(abst,k(eq)),pair(k(k(p1)),a(abst,k(a(closure,pair(a(notp1,charq),setof))))))),pair(setof,pair(p1,p2))).
end_of_list.






 Click button to load the definition of push into TRC applet.

We know that setof is a one-to-one function from the universe into the characteristic functions. A Schroeder-Bernstein construction then yields push, a bijection from the universe onto the characteristic functions.


The term push is defined so that push x = setof x if x is in the closure of the noncharacteristic functions under setof. Otherwise, push x = x. Holmes writes pushset for the closure of the noncharacteristic functions under setof. The following figure shows the standard visualization of the Schroeder-Bernstein construction. The largest square represents the universe; the largest circle represents the characteristic functions. The shaded part represents the closure of the noncharacteristic functions under setof, which is a bijection from the shaded part to the shaded part minus the outermost shaded area. Then push is defined piecewise to agree with the identity function on the white areas and with setof on the shaded areas:



The usal way to define a piecewise or if function in combinatory logic is test pair(then-part, else-part) where test is equal to p1 or p2. Then the idea of the definition of push is simply

(lambda x
  (a (a pushset x)
     (pair (a setof x)
           x)))                          (1)

The first occurence of x in the body of the above lambda-term is at level 1, while the other two are at level 0. Since pushset x is always equal to p1 or p2, the following term, in which x is at level -1, is equivalent to pushset x:


(a eq (pair (k p1)
            (k (a pushset
                  x))))                  (2)

Finally for pushset write
(a closure (pair (a notp1 charq)
                 setof)).                (3)

Substituting (3) into (2) and (2) into (1), the term push is defined by the following stratified lambda-term: 
 
(lambda x
  (a (a eq (pair (k p1)
                 (k (a (a closure (pair (a notp1 charq)
                                        setof))
                       x))))
     (pair (a setof x)
           x)))

up show outline