[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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?