Definition of charq

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






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

By definition, f is a characterstic function if for all x, either f x = p1 or f x = p2. One can write a very simple predicate for the set of all characteristic functions by noting that f is a characteristic function iff it is a fixed point for isp1, i. e. if isp1 f = f. This definition is expressed by the following stratified lambda-term:
(lambda f
  (a eq (pair f
              (a isp1 f))))

up show outline