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

[Gabriel Scherer]

Dear Oleg (and list),

Thanks for the reference to your work, which I didn't know about. Below is
a question.

You highlight that your translation to a the combinator calculus is
compositional.
This is also a property of the Categorical Abstract Machine of Guy
Cousineau, Pierre-Louis Curien and Michel Mauny (1987). They used a
combinator calculus extended with tuples and projections, which corresponds
to a syntax for morphisms in cartesian-closed categories, and makes it easy
to represent the environmnet as nested tuples and variables as
de-bruijn-index accessors. Can your compositional translation be understood
as a curryfication/de-tuplification of the CAM compilation strategy (you
remark that your semantics has a currified environment)?

(Your De Bruijn presentation is more general than the one used in the CAM,
as you represent the "successor" operation S as a general term combinator
corresponding to weakening, which suffices to express some of Turner's
optimisations. I suppose that the question makes precise sense only when
you restrict your system to use S on "variable" terms of the form (S^n z),
and don't use your rule Abs0. But any scope-related typing rules could
easily be taken into account by an optimized CAM translation, so you could
also compare your system with such an optimized CAM.)

Best


On Mon, Feb 26, 2018 at 12:24 PM, Oleg <oleg at okmij.org> wrote:

> [ 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?
>
>
>