×

The semantics of entailment omega. (English) Zbl 1042.03019

Summary: This paper discusses the relation between the minimal positive relevant logic \({\mathbf B}_+\) and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking \({\mathbf B}\wedge {\mathbf T}\) of \({\mathbf B}_+\), which saves implication \(\to\) and conjunction \(\wedge\) but drops disjunction \(\vee\). The filter models of the \(\lambda\)-calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models of these calculi. (The logician’s “theory” is the algebraist’s “filter”.) The coincidence extends to a dual interpretation of key particles – the subtype \(\leq\) translates to provable \(\to\), type intersection \(\cap\) to conjunction \(\wedge\), function space \(\to\) to implication, and whole domain \(\omega\) to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union \(\cup\) should correspond to the logical disjunction \(\vee\) of \({\mathbf B}_+\). But the simulation of functional application by a fusion (or modus ponens product) operation \(\circ\) on theories leaves the key Bubbling lemma of work on ITD unprovable for the \(\vee\)-prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of \(\lambda\) and CL.

MSC:

03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Anderson, A. R., and N. D. Belnap, Jr., Entailment. Vol. I. The Logic of Relevance and Necessity. , Princeton University Press, Princeton, 1975. · Zbl 0323.02030
[2] Anderson, A. R., N. D. Belnap, Jr., and J. M. Dunn, Entailment. The Logic of Relevance and Necessity. Vol. II , Princeton University Press, Princeton, 1992. · Zbl 0921.03025
[3] Barbanera, F., M. Dezani-Ciancaglini, and U. de’Liguoro, ”Intersection and union types: Syntax and semantics”, Information and Computation , vol. 119 (1995), pp. 202–30. · Zbl 0832.68065 · doi:10.1006/inco.1995.1086
[4] Barendregt, H. P., The Lambda Calculus. Its Syntax and Semantics , revised edition, vol. 103 of Studies in Logic and the Foundations of Mathematics , North-Holland Publishing Co., Amsterdam, 1984. · Zbl 0551.03007
[5] Barendregt, H., M. Coppo, and M. Dezani-Ciancaglini, ”A filter lambda model and the completeness of type assignment”, The Journal of Symbolic Logic , vol. 48 (1983), pp. 931–40. JSTOR: · Zbl 0545.03004 · doi:10.2307/2273659
[6] Curry, H. B., Foundations of Mathematical Logic , McGraw-Hill Book Co., New York, 1963. · Zbl 0163.24209
[7] Curry, H. B., and R. Feys, Combinatory Logic. Vol. I , Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam, 1958. · Zbl 0081.24104
[8] Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti, and Y. Motohama, ”The relevance of semantic subtyping”, in ITRS 2002 , vol. 70 (1) of Electric Notes in Theoretical Computer Science , edited by S. van Bakel, 2002. \hrefhttp://www.elsevier.nl/locate/entcs/volume70.htmlhttp://www.elsevier.nl/locate/entcs/volume70.html · Zbl 1270.03043
[9] Dezani-Ciancaglini, M., and J. R. Hindley, ”Intersection types for combinatory logic”, Theoretical Computer Science , vol. 100 (1992), pp. 303–24. · Zbl 0771.03004 · doi:10.1016/0304-3975(92)90306-Z
[10] Dunn, J. M., The Algebra of Intensional Logics , Ph.D. thesis, University of Pittsburgh, 1966. · Zbl 0145.45104
[11] Frisch, A., G. Castagna, and V. Benzaken, ”Semantic subtyping”, pp. 137–46 in Seventeenth IEEE Symposium on Logic in Computer Science , edited by G. Plotkin, IEEE Computer Society Press, 2002. · Zbl 1082.68581 · doi:10.1007/11523468
[12] Harrop, R., ”Concerning formulas of the types \(A\rightarrow B\bigvee C,\,A\rightarrow (Ex)B(x)\)” in intuitionistic formal systems, The Journal of Symbolic Logic , vol. 25 (1960), pp. 27–32. JSTOR: · Zbl 0098.24201 · doi:10.2307/2964334
[13] Hindley, J. R., and G. Longo, ”Lambda-calculus models and extensionality”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik , vol. 26 (1980), pp. 289–310. · Zbl 0453.03015 · doi:10.1002/malq.19800261902
[14] Hindley, J. R., and J. P. Seldin, Introduction to Combinators and \(\lambda\) -Calculus, vol. 1 of London Mathematical Society Student Texts , Cambridge University Press, Cambridge, 1986. · Zbl 0614.03014
[15] Kripke, S. A., ”Semantical analysis of modal logic. I. Normal modal propositional calculi”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik , vol. 9 (1963), pp. 67–96. · Zbl 0118.01305 · doi:10.1002/malq.19630090502
[16] Leblanc, H., ”On dispensing with things and worlds”, pp. 103–19 in Existence, Truth, and Provability , edited by H. Leblanc, State University of New York Press, Albany, 1982. Originally published in Logic and Ontology, pp. 241–59, edited by M. K. Munitz, New York University Press, New York, 1973. · Zbl 0502.03003
[17] Meyer, R. K., and R. Routley, ”Algebraic analysis of entailment. I”, Logique et Analyse, Nouvelle Série , vol. 15 (1972), pp. 407–28. · Zbl 0336.02020
[18] Routley, R., and R. K. Meyer, ”The semantics of entailment. III”, Journal of Philosophical Logic , vol. 1 (1972), pp. 192–208. · Zbl 0317.02019 · doi:10.1007/BF00650498
[19] Routley, R., V. Plumwood, R. K. Meyer, and R. T. Brady, Relevant Logics and Their Rivals. Part I , Ridgeview Publishing Co., Atascadero, 1982. · Zbl 0579.03011
[20] van Bakel, S., M. Dezani-Ciancaglini, U. de’Liguoro, and Y. Motohama, ”The minimal relevant logic and the call-by-value lambda calculus”, Technical Report TR-ARP-05-2000, Australian National University, 2000.
[21] Venneri, B., ”Intersection types as logical formulae”, Journal of Logic and Computation , vol. 4 (1994), pp. 109–24. · Zbl 0798.03013 · doi:10.1093/logcom/4.2.109
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.