up | previous | next | detailed contents | brief contents

Definition of kintersection

list(demodulators).
kintersection = a(a(abst,a(a(abst,k(abst)),a(a(abst,k(a(abst,k(abst)))),a(a(abst,a(a(abst,k(abst)),a(a(abst,k(a(abst,k(abst)))),a(a(abst,k(a(abst,k(a(abst,k(eq)))))),pair(k(k(k(k(p2)))),a(a(abst,k(a(abst,k(a(abst,k(a(abst,k(eq)))))))),pair(k(k(k(k(pair(p1,k(p2)))))),pair(pair(p1,p2),k(k(a(abst,a(a(abst,k(abst)),a(abst,k(isp1)))))))))))))),k(k(k(pair(p1,p2)))))))),k(k(k(pair(p1,p2))))).
end_of_list.






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

Any combinator f can be thought of as representing a set, whose characteristic function is isp1 f. (Of course, many combinators could represent the same set in this way.) Since every combinator represents a set, it follows that every combinator represents a set of sets. It is natural to ask for a combinator intersection such that intersection f x = p1 if and only if for every z, if f z = p1 then z x = p1. In fact intersection cannot exist in TRC. ***JUSTIFY We can still talk about intersections using the combinator kintersection. Instead of outputting the intersection of a collection, kintersection outputs the constant function that sends everything to the intersection of that collection. We need to perform special manipulations of types at two points in the definition.


Let us see how to express kintersection as a stratified lambda-term. Given f and x, we want to know whether or not x is in the intersection of f. This will be true if there is no z such that f z = p1 and z x != p1, that is, there is no z such that pair(f z, isp1 z x) = pair(p1, p2). In order to say that there is no such z, we would like to abstract out the z, but z occurs at level zero and at level one in this statement. We can fix this using the fact that the operation of forming constant functions is one-to-one. Thus x belongs to the intersection of f if there is no z such that pair(f z, k(isp1 z x)) = pair(p1, k(p2)). Now z occurs only at level zero and we can say that x is in the intersection of f if the following term is equal to k(p2), i. e. if the equality expressed by its eq is always false:

(lambda z
  (a eq (pair (pair p1
                    (k p2))
              (pair (a f z)
                    (k (a (a isp1 z) x))))))))

It is easy to say in the language of TRC that the above term is equal to k(p2).
(a eq (pair (k p2)
            (lambda z
              (a eq (pair (pair p1
                                (k p2))
                          (pair (a f z)
                                (k (a (a isp1 z) x))))))))

The above term now expresses the statement that x is in the intersection of f. If we could abstract out the x and the f, then we would have the sought-after combinator intersection, but x is at level -2. (It is at level 0 in the expression (a (a isp1 z) x). It is inside one constant-function expression and one lambda-expression, each of which reduces its type by 1.) Since the entire term is always equal either to p1 or to p2, we can get an equivalent term by applying the whole thing to pair(p1, p2). If we do this twice, we bring x up to level zero and can then abstract it out:
(lambda x
  (a (a (a eq (pair (k p2)
                    (lambda z
                      (a eq (pair (pair p1
                                        (k p2))
                                  (pair (a f z)
                                        (k (a (a isp1 z) x))))))))
        (pair p1 p2))
     (pair p1 p2)))

The above term exactly represents the intersection of f. But we can't abstract out the f now, because it is at level one. At this point we wrap the whole thing in a constant function and settle for the term kintersection, defined below, instead of intersection, which can't exist in TRC. ***JUSTIFY
(lambda f
  (k (lambda x
       (a (a (a eq (pair (k p2)
                         (lambda z
                           (a eq (pair (pair p1
                                             (k p2))
                                       (pair (a f z)
                                             (k (a (a isp1 z) x))))))))
             (pair p1 p2))
          (pair p1 p2)))))

up | previous | next | detailed contents | brief contents