On the Computational Interpretation of CK_n for Contextual Information Processing

• Autorzy: Mendler M. , Scheele S.

Identyfikatory

DOI

10.3233/FI-2014-984

• Języki publikacji: EN

Abstrakty

EN

We aim to establish the multi-modal logic CK_n as a baseline for a constructive correspondence theory of constructive modal logics. Just like many classical multi-modal logics may be studied as theories of the basic system K obtained by model-theoretic specialisation, we envisage constructive modal logics to be derived as proof-theoretic enrichments of CK_n. The system CK_n would then act as a core system for constructive contextual reasoning with controlled information flow. In this paper, as a first step towards this goal, we study CK_n as a type theory and introduce its computational λ-calculus, λCK_n. Extending previous work on CK_n, we present a cut-free contextual sequent system in the spirit of Masini’s two-dimensional generalisation of natural deduction and Brünnler’s nested sequents and give a computational interpretation for CK_n following the Curry- Howard Correspondence. The associated modal type theory λCK_n permits an interpretation for both the modalities □ and ⋄ of CK_n as type operators with simple and independent constructors and destructors, which has been missing in the literature. It is shown that the calculus satisfies subject reduction, strong normalisation and confluence. Since normal forms can be characterised by way of a Gentzen-style typing system with sub-formula property, CK_n is suitable for proof search in CK_n. At the same time, λCK_n enjoys natural deduction style typing which is important for programming applications. In contrast to most existing modal type theories, which are obtained as theories of the constructive modal logic S4, CK_n is not bound to a particular contextual interpretation. Thus, λCK_n constitutes the core of a functional language which provides static type checking of information processing to support safe contextual navigation in relational structures like those treated by description logics. We review some existing work on modal type theories and discuss their relation to λCK_n.

Słowa kluczowe

EN

information processing; contextual analysis; mathematical proofs; information resources management; calculus; generalization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 130, nr 1
• Strony: 125--162
• Opis fizyczny: Bibliogr. 48 poz.

Twórcy

autor

Mendler M.

• Faculty of Information Systems and Applied Computer Sciences The Otto-Friedrich-University of Bamberg, Germany

autor

Scheele S.

• Faculty of Information Systems and Applied Computer Sciences The Otto-Friedrich-University of Bamberg, Germany

Bibliografia

• [1] Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and Kripke Semantics for Constructive S4 Modal Logic, in: Proc. of Computer Science Logic 2001 (CSL 2001) (L. Fribourg, Ed.), vol. LNCS 2142, Springer Verlag, 2001, 292–307.
• [2] Appel, A. W.: Compiling with Continuations, Cambridge University Press, 1992.
• [3] Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., Patel-Schneider, P. F., Eds.: The Description Logic Handbook: Theory, Implementations and Applications, 2nd edition, Cambridge University Press, 2007.
• [4] Barber, A., Plotkin, G.: Dual Intuitionisic Linear Logic, Technical Report ECS-LFCS-96-347, University of Edinburgh, 1996.
• [5] Bellin, G., de Paiva, V., Ritter, E.: Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic, Methods for Modalities II, Amsterdam, November 2001.
• [6] Benton, N., Bierman, G., de Paiva, V.: Computational Types From a Logical Perspective, Journal of Functional Programming, 8(2), 1998.
• [7] Borghuis, V. A. J.: Coming to Terms with Modal Logic, Ph.D. Thesis, Technical University of Eindhoven, 1994.
• [8] Botazzo, L., Ferrari, M., Fiorentini, C., Fiorino, G.: A constructive semantics for ALC, Int’l Workshop on Description Logics (DL 2007) (D. Calvanese, E. Franconi, V. H. D. Lembo, B. Motik, S. Tessaris, A.-Y. Turhan, Eds.), Bolzano University Press, June 2007.
• [9] Brünnler, K.: Deep sequent systems for modal logic, Archive for Mathematical Logic, 48(6), 2009, 551–577.
• [10] Calvanese, D., Giacomo, G. D., Lenzerini, M., Nardi, D., Rosati, R.: Information Integration: Conceptual Modeling and Reasoning Support, 3rd IFCIS Conference on Cooperative Information Systems, IEEE Computer Society, 1998.
• [11] van Dalen, D.: Intuitionistic Logic, in: Handbook of Philosophical Logic (D. Gabbay, F. Guenthner, Eds.), vol. III, chapter 4, Reidel, 1986, 225–339.
• [12] Fairtlough, M., Mendler, M.: Propositional Lax Logic, Information and Computation, 137(1), August 1997, 1–33.
• [13] Fischer-Servi, G.: Semantics for a class of intuitionistic modal calculi, in: Italian Studies in the Philosophy of Science (M. L. D. Chiara, Ed.), Reidel, 1980, 59–72.
• [14] Fitch, F. B.: Intuitionistic Modal Logic with Quantifiers, Portugaliae Mathematica, 1948, 113–118.
• [15] Gabbay, D. M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics, Elsevier, 2003.
• [16] Ghani, N., de Paiva, V., Ritter, E.: Explicit Substitutions for Constructive Necessity, Automata, Languages and Programming (ICALP’98) (K. Larsen, S. Skyum, G. Winskel, Eds.), LNCS 1443, Springer, 1998.
• [17] Girard, J. Y., Lafont, Y., Taylor, P.: Proofs and Types, Cambridge University Press, 1989.
• [18] Goubault-Larrecq, J.: On Computational Interpretations of the Modal Logic S4 I. Cut Elimination, Technical report, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, 1996.
• [19] Goubault-Larrecq, J.: On Computational Interpretations of the Modal Logic S4 II. The lambda-evQ calculus, Technical report, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, 1996.
• [20] Goubault-Larrecq, J., Goubault, E.: On the geometry of intuitionistic S4 proofs, Homology, Homotopy and Applications, 5(2), 2003, 137–209.
• [21] de Groote, P.: On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Information and Computation, 178(2), 2002, 441–464.
• [22] Kobayashi, S.: Monad as Modality, Theoretical Computer Science, 175, 1997, 29–74.
• [23] Luettgen, G., Mendler, M.: The Intuitionism behind Statecharts step, ACM Transactions on Computational Logic, 3(1), January 2002, 1–41.
• [24] Martini, S., Masini, A.: A Computational Interpretation of Modal Proofs, Proof Theory of Modal Logics (H. Wansig, Ed.), Kluwer, 1996.
• [25] Masini, A.: 2-sequent calculus: Intuitionism and natural deduction, Journal of Logic and Computation, 3(4), 1993, 533–562.
• [26] Mendler, M.: Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification, Workshop on Designing Correct Circuits (G. Jones, M. Sheeran, Eds.), Springer, 1991.
• [27] Mendler, M., de Paiva, V.: Constructive CK for Contexts, Context Representation and Reasoning (CRR-2005) (L. Serafini, P. Bouquet, Eds.), CEUR Proceedings, Paris, July 2005.
• [28] Mendler, M., Scheele, M.: On the Computational Interpretation of _CKn for Contextual Information Processing, Bamberger Beiträge zurWirtschaftsinformatik und Angewandten Informatik 91, The Otto-Friedrich-University of Bamberg, May 2013.
• [29] Mendler, M., Scheele, S.: Towards constructive description logics for abstraction and refinement, 21st Int’l Workshop on Description Logics (DL2008), CEUR Workshop proceedings 353, May 2008.
• [30] Mendler, M., Scheele, S.: Towards a Simply Typed CALculus for Semantic Knowledge, Logics for Agents and Mobility (LAM 2010), Edinburgh, July 2010.
• [31] Mendler, M., Scheele, S.: Towards Constructive DL for Abstraction and Refinement, Journal of Automated Reasoning, 44(3), 2010, 207–243.
• [32] Mendler, M., Scheele, S.: Cut-free Gentzen Calculus for Multimodal CK, Information and Computation, 209, 2011, 1465–1490.
• [33] Moggi, E.: Notions of Computation and Monads, Information and Computation, 93, 1991, 55–92.
• [34] Möller, R.: A functional layer for description logics: knowledge representation meets object-oriented programming, 11th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA’96) (L. Anderson, J. Coplien, Eds.), ACM, 1996.
• [35] Nanevski, A., Pfenning, F., Pientka, B.: Contextual Modal Type Theory, ACM Transactions on Computational Logic, 9(3), June 2008, 1–49.
• [36] Nanevski, A., Pientka, B., Pfenning, F.: A Modal Foundation for Meta-Variables, Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2003), Upsaala, August 2003.
• [37] de Paiva, V.: Constructive Description Logics: What, Why and How, Context Representation and Reasoning, Riva del Garda, Italy, August 2006.
• [38] de Paiva, V., Bierman, G.: Intuitionistic Necessity Revisited, Technical Report CSRP-96-10, School of Computer Science, University of Birmingham, June 1996.
• [39] Paschke, A.: Typed Hybrid Description Logic Programs with Order-sorted semantic web type systems on OWL and RDFS, Technical report, TU Munich, December 2005.
• [40] Pfenning, F., Davies, R.: A Judgemental Reconstruction of Modal Logic, Mathematical Structures in Computer Science, 11(4), August 2001, 511–540.
• [41] Pfenning, F., Wong, H.-C.: On a modal _-calculus for S4, Proc. 11th Conf. on Mathematical Foundations of Programming Semantics (S. Brookes, M. Main, Eds.), 1, 1995.
• [42] Schacht, S., Hahn, U.: A denotational semantics for joining description logics and object-oriented programming, SCAI’97: Proceedings of the sixth Scandinavian Conference on Artificial Intelligence, IOS Press, Amsterdam, 1997.
• [43] Schürmann, C., Despeyroux, J., Pfenning, F.: Primitive recursion for higher-order abstract syntax, Theoretical Computer Science, 266(1-2), 2001, 1–57.
• [44] Simmons, H.: Derivation and Computation, Cambridge University Press, 2000.
• [45] Simpson, A. K.: The Proof Theory and Semantics of Intuitionistic Modal Logic, Ph.D. Thesis, University of Edinburgh, 1994.
• [46] Strassburger, L.: Nested sequents for intuitionistic and modal logics, Intuitionistic Modal Logics and Applications (IMLA 2011), Nancy, July 2011.
• [47] Troelstra, A. S., van Dalen, D.: Constructivism in Mathematics, vol. II, North-Holland, 1988.
• [48] Wijesekera, D.: Constructive Modal Logic I, Annals of Pure and Applied Logic, 50, 1990, 271–301