Subject: jumbo connectives - comments please!
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-12-18 17:20:57 GMT (2 years, 20 weeks, 4 days, 21 hours and 49 minutes ago)
Dear froggists, I would welcome comments on the manuscript "Jumbo Connectives in Type Theory and Logic", which is available here: http://www.cs.bham.ac.uk/~pbl/papers/jumboshort.pdf It's not about deep inference, but I think it might be interesting to you guys, because it's about systems where things that have traditionally been done in several steps are done in one step. And it addresses issues like associativity of connectives that have been discussed on this list. regards Paul Abstract: We make an argument that, for any study involving computational effects such as divergence or continuations, the traditional syntax of simply typed lambda-calculus cannot be regarded as canonical, because standard arguments for canonicity rely on isomorphisms that may not exist in an effectful setting. To remedy this, we define a "jumbo lambda-calculus" that fuses the traditional connectives together into more general ones, so-called "jumbo connectives". We provide two pieces of evidence for our thesis that the jumbo formulation is advantageous. Firstly, we show that the jumbo lambda-calculus provides a "complete" range of connectives, in the sense of including every possible connective that, within the beta-eta theory, possesses a reversible rule. Secondly, in the presence of effects, we explore plausible decompositions of these jumbo connectives, in both call-by-name and call-by-value. We see that hardly any are universally valid, and so the jumbo connectives really are necessary. Finally, we look at Gentzen's LK (propositional), in order to illustrate how the form of sequents within a system determines the range of connectives. We see that, because a sequent in LK has multiple conclusions, its range of jumbo connectives is larger than that of simply typed lambda-calculus.