[TYPES] A new take on bracket abstraction, and a historical question about the first take

[Oleg]

There have been recently several interesting historical threads on
this list. I also have a question, which came when developing a new
approach to translating lambda-terms to SK combinators. Incidentally,
this new approach may be of interest to this list because of the close
relationship with types: the meaning derivation (i.e., translation)
mirrors the typing derivation. The translation of course works in the
general un(i)typed lambda calculus. One may thus say, types are useful
even when they are absent.

The traditional approach -- bracket abstraction -- is syntactic: a
term-rewriting system. It is formulated as a set of ordered re-writing
rules, with side conditions checking if a particular variable occurs
free within a term.

The new approach is semantic: the SK term for a given possibly open
lambda-expression is _compositionally_ computed as the expression's
denotation. It is described in a paper accepted for FLOPS, whose near
final version is available at
        http://okmij.org/ftp/tagless-final/ski.pdf
There is also a code with many variations and examples:
        http://okmij.org/ftp/tagless-final/skconv.ml

My question is to check my understanding of the origins of the bracket
abstraction. As far as I can see from reading the Stanford
Encyclopedia of Philosophy and Schoenfinkel's original paper,
Schoenfinkel was the first to describe the main idea: converting a
combinator term with variables into a form in which all of its
variables are at the margin. However, Curry should be credited with
showing that lambda-calculus is combinatorially complete (that every
lambda-expression can be represented as a combinator applied to the
series of the expression's free variables). The Curry's bracket
abstraction is essentially Schoenfinkel's. Although Schoenfinkel has
introduced B and C combinators (called differently, though), his
bracket abstraction only deals with S and K. It is David Turner who
has to be credited with optimizations. Is this understanding correct?