Definition of remove_singleton

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






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

The first idea for the definition of remove_singleton would be that remove_singleton set single should be the characteristic function of set - { single }. A natural way to implement this would be to start with a general set-difference combinator. I tried that approach, but it seemed that the number of layers of auxilliary definitions to the definition of push was getting large and OTTER was beginning to bog down.


If we return to the equation remove_singleton set single = set - {single}, we run into a difficulty with types because the function remove_singleton set is sending single to something one type higher than single. I solve this problem by working in terms of k(single) which is now at the same level as set.


Thus we abandon the above definition and instead define remove_singleton pair(set, k(single)) = set - { single }, that is, remove_singleton pair(set, k(single)) x = p1 iff set x = p1 and single != x, otherwise remove_singleton pair(set, k(single)) x = p2.


The term below embodies this definition of remove_singleton and should by now be self-explanatory except perhaps for one point: to recover single from ksingle = k(single) we apply ksingle to any arbitrarily chosen term. I chose x because this makes the whole term remove_singleton look a bit simpler when written in TRC using bracket abstraction. Thus, when reading the definition of remove_singleton below, read ksingle as k(single) and (a ksingle x) as single.

(lambda (set ksingle)
  (lambda x
    (a eq (pair (pair p1
                      p2)
                (pair (a set x)
                      (a eq (pair (a ksingle x)
                                  x)))))))

up show outline