[TYPES/announce] A Combinatory Account of Internal Structure

[Barry Jay]

A draft of the paper "A Combinatory Account of Internal Structure"  is 
available at
http://www-staff.it.uts.edu.au/~cbj/Publications/factorisation.pdf
This work may be of interest to the many readers of this list that are 
interested in foundational issues.
It has been accepted for publication by J Symbolic Logic.

The paper exposes some of the limitations of SK-combinatory logic (and 
so, by implication of lambda-calculus) by developing new combinatory 
calculi which cannot be represented in SK-calculus. The work has been 
controversial since each person has their own notion of representation. 
For us, this is not merely an encoding of one calculus within another, 
but refers to the ability to represent a symbolic function by a combinator.

The simplest of these new calculi has two operators, S and F which 
satisfy the rules

SMNX      --> MX(NX)
FOMN      --> M               if O is S or F
F(PQ)MN --> NPQ           if PQ is a factorable form

where the factorable forms are those combinators of the form 
S,SM,SMN,F,FM,FMN. These turn out to be the partially applied operators, 
which ensures confluence. SF-calculus is able to represent static 
pattern matching, in the sense of pattern calculus.

All comments welcome.

Barry Jay
Thomas Given-Wilson