[W/K] :: bracket abstraction

  bracket abstraction
       
           An algorithm which turns a term into a function
          of some variable.  The result of using bracket abstraction on
          T with respect to variable v, written as [v]T, is a term
          containing no occurrences of v and denoting a function f such
          that f v = T.  This defines the function f = (\ v . T).  Using
          bracket abstraction and currying we can define a language
          without bound variables in which the only operation is
          monadic function application.
       
          See combinator.
       
          (1995-03-07)