Investigating iconic combinators

Various properties of two bracket abstraction algorithms are discussed and some of those properties are proved in "Investigations into Iconic Representations of Combinators". Algorithm (L) is uni-variate and uses yes-no representations, whereas algorithm (M) is multi-variate and uses array representations. It is shown that

1. both algorithms are structure-preserving;
2. there is a straightforward connection between [x]P and [x]Q, produced by algorithm (L), if the primal components of Q, except the first, are a permutation of the primal components of P, except the first;
3. there is a simple connection between the two abstracts produced when algorithm (L) is used repeatedly on the same input term, but the abstractions are performed in a different order in each case;
4. there is a straightforward connection between the array representations produced by algorithm (M) and the yes-no representations produced when algorithm (L) is used to abstract the same variables individually from the same input term and
5. using algorithm (M) multi-variate abstraction can be "partitioned".

Since writing this paper about 15 years ago, I have continued to study bracket abstraction algorithms.

Reference

© Antoni Diller (27 March 2014)