Definition of closedunder

Definition of `closedunder`

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





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

The term closedunder pair(s, f) can be interpreted as saying that the set represented by s is closed under the function represented by f. The combinator closedunder has the following defining properties:

closedunder pair(f, s) = p1 if for every z, if s z = p1 then s (f z) = p1.
closedunder pair(f, s) = p2 if for some z, both s z = p1 and s (f z) != p1.

To translate this into a stratified lambda-term, let z be a counterexample to the statement that s is closed under f. Then s z = p1 and isp1 s (f z) = p2. That is, pair(s z, isp1 s (f z)) = pair(p1, p2). Equivalently, the term

(a eq (pair (pair (a s z)
                  (a (a isp1 s) (a f z)))
            (pair p1
                  p2)))

is equal to p1. Now we want to say that there is no such counterexample z. Since the above lambda-term is an application of eq, it must be equal to p1 or p2. If there is no value for z which makes the above term equal to p1 then when we abstract z from the above term, we must get k(p2). These observations lead us to the following lambda-term which we take as the definition of closedunder:

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

Note how this definition takes advantage of TRC's ability to rewrite any sentence with stratified quantifiers as a simple equation between two terms: we can translate `there is no z such that blah1 = blah2' as (lambda z (a eq (pair blah1 blah2))) = (k p2).

As usual, our first order of business will be to prove the basic defining properties listed above.
up show outline