[ The Types Forum (announcements only),
    http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


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



Reply via email to