Definition of closure

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






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

Define the closure of the set s under the function f as the intersection of all sets x that contain s and are closed under f. Thus 
(a kintersection
   (lambda x
     (a eq (pair (pair p1
                       p1)
                 (pair (a subset (pair s x))
                       (a closedunder (pair x f)))))))

is the constant function whose value is the closure of s under f. Note also that s and f are at level -1 in the above term. I can recover the closure itself from this constant function by applying it to any arbitrary term. By doing so, I also bring s and f up to level zero so that they can be abstracted out. I chose the term pair(s, f) as the term to which I applied the above term. So, applying the above term to pair(s, f) and then abstracting out pair(s, f), we get the definition of closure, below.
(lambda (s f)
  (a (a kintersection
        (lambda x
          (a eq (pair (pair p1
                            p1)
                      (pair (a subset (pair s x))
                            (a closedunder (pair x f)))))))
     (pair s f)))

up show outline