TY - JOUR
T1 - The Better Bubbling Lemma
AU - Meyer, Robert K.
PY - 2007/6/14
Y1 - 2007/6/14
N2 - BCD [Barendregt, Henk, Mario Coppo and Mariangiola Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment, JSL 48 (1983), 931-940] relies for its modeling of λ calculus in intersection type filters on a key theorem which I call BL (for the Bubbling Lemma, following someone). This lemma has been extended in [Castagna, Giuseppe, and Alain Frisch. A gentle introduction to semantic subtyping. In PPDP05, ACM Press (full version) and ICALP05, LNCS volume 3580, Springer-Verlag (summary), 2005. Joint ICALP-PPDP keynote talk; Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp] to encompass Boolean structure, including specifically union types; this extended lemma I call BBL (the Better Bubbling Lemma). There are resonances, explored in [Dezani-Ciancaglini, M., R.K. Meyer and Y. Motohama, The semantics of entailment omega, NDJFL 43 (2002), 129-145] and [Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp], between intersection and union type theories and the already existing minimal positive relevant logic B+ of [Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192-208]. (Indeed [Pal, Koushik, and Robert K. Meyer. 2005. Basic relevant theories for combinators at levels I and II, AJL 3, http://www.philosophy.unimelb.edu.au/2005/2003_2.pdf, 19 pages] applies BL and BBL to get further results linking combinators to relevant theories and propositions.) On these resonances the filters of algebra become the theories of logic. The semantics of [Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., "Truth and Probability: Essays in Honour of Hugues Leblanc," pages 59-84, College Publications, King's College, London, 2005] yields here a new and short proof of BBL, which takes account of full Boolean structure by encompassing not only B+ but also its conservative Boolean extension CB [Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192-208; Meyer, Robert K., 1995. Types and the Boolean system CB+, cslab.anu.edu.au/ftp/techreports/SRS/1995/TR-SRS-5-95/meyer.ps.gz; Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., "Truth and Probability: Essays in Honour of Hugues Leblanc," pages 59-84, College Publications, King's College, London, 2005.].
AB - BCD [Barendregt, Henk, Mario Coppo and Mariangiola Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment, JSL 48 (1983), 931-940] relies for its modeling of λ calculus in intersection type filters on a key theorem which I call BL (for the Bubbling Lemma, following someone). This lemma has been extended in [Castagna, Giuseppe, and Alain Frisch. A gentle introduction to semantic subtyping. In PPDP05, ACM Press (full version) and ICALP05, LNCS volume 3580, Springer-Verlag (summary), 2005. Joint ICALP-PPDP keynote talk; Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp] to encompass Boolean structure, including specifically union types; this extended lemma I call BBL (the Better Bubbling Lemma). There are resonances, explored in [Dezani-Ciancaglini, M., R.K. Meyer and Y. Motohama, The semantics of entailment omega, NDJFL 43 (2002), 129-145] and [Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp], between intersection and union type theories and the already existing minimal positive relevant logic B+ of [Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192-208]. (Indeed [Pal, Koushik, and Robert K. Meyer. 2005. Basic relevant theories for combinators at levels I and II, AJL 3, http://www.philosophy.unimelb.edu.au/2005/2003_2.pdf, 19 pages] applies BL and BBL to get further results linking combinators to relevant theories and propositions.) On these resonances the filters of algebra become the theories of logic. The semantics of [Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., "Truth and Probability: Essays in Honour of Hugues Leblanc," pages 59-84, College Publications, King's College, London, 2005] yields here a new and short proof of BBL, which takes account of full Boolean structure by encompassing not only B+ but also its conservative Boolean extension CB [Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192-208; Meyer, Robert K., 1995. Types and the Boolean system CB+, cslab.anu.edu.au/ftp/techreports/SRS/1995/TR-SRS-5-95/meyer.ps.gz; Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., "Truth and Probability: Essays in Honour of Hugues Leblanc," pages 59-84, College Publications, King's College, London, 2005.].
KW - B+
KW - CB
KW - bubbling
KW - classical relevant logic
KW - minimal relevant logic
KW - semantics
KW - subtyping
KW - type theory
UR - http://www.scopus.com/inward/record.url?scp=34249825171&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2006.12.038
DO - 10.1016/j.entcs.2006.12.038
M3 - Article
SN - 1571-0661
VL - 171
SP - 77
EP - 84
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 3
ER -