Investigations into iconic representations of 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, "Investigations into Iconic Representations of Combinators", in Javier Blanco (editor), Argentine Workshop on Theoretical Computer Science (WAIT2000) Proceedings: Tandil, September 4-9, 2000, [Buenos Aires, Sociedad Argentina de Informática e Investigación Operativa (SADIO), 2000], pp. 52–62; a PDF version of this paper is available on this website.

© Antoni Diller (27 March 2014)