Definition of setof

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






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

The combinator setof sends each function to the characteristic function of its graph, i. e. setof f pair(x, y) = p1 if f x = y, and otherwise setof f pair(x, y) = p2. This definition is expressed by the following stratified lambda-term:
(lambda f
  (lambda (x y)
    (a eq (pair y
                (a f x)))))

up show outline