[ The Types Forum (announcements only),
A draft of the paper "A Combinatory Account of Internal Structure" is
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.