zbMATH — the first resource for mathematics

Kripke semantics for higher-order type theory applied to constraint logic programming languages. (English) Zbl 1387.68059
Summary: We define a Kripke semantics for Intuitionistic Higher-Order Logic with constraints formulated within Church’s Theory of Types via the addition of a new constraint base type. We then define an executable fragment, \({hoHH}(\mathcal{C})\), of the logic: a higher-order logic programming language with typed \(\lambda\)-abstraction, implication and universal quantification in goals and constraints, and give a modified model theory for this fragment. Both formal systems are shown sound and complete for their respective semantics.
We also solve the impredicativity problem in \(\lambda\)Prolog semantics, namely how to give a definition of truth without appealing to induction on subformula structure. In the last section we give a simple semantics-based conservative extension proof that the language \(hoHH(\mathcal{C})\) satisfies a uniformity property along the lines of [D. Miller et al., Ann. Pure Appl. Logic 51, No. 1–2, 125–157 (1991; Zbl 0721.03037)].
68N17 Logic programming
03B15 Higher-order logic; type theory (MSC2010)
HiLog; CiaoPP; Hiord; Ciao; CoALP
Full Text: DOI
[1] Abadi, M.; Blanchet, B., Analyzing security protocols with secrecy types and logic programs, J. ACM, 52, 1, 102-146, (Jan. 2005)
[2] Aczel, P., Saturated intuitionistic theories, (Schmidt, H. Arnold; Schütte, K.; Thiele, H.-J., Contributions to Mathematical Logic. Proceedings of the Logic Colloquium, (1968), North-Holland Amsterdam), 1-11 · Zbl 0198.32205
[3] Albert, E.; Puebla, G.; Hermenegildo, M. V., Abstraction-carrying code: a model for mobile code safety, New Gener. Comput., 26, 2, 171-204, (2008) · Zbl 1169.68356
[4] Amato, G.; Lipton, J.; McGrail, R., On the algebraic structure of declarative programming languages, Theoret. Comput. Sci., 410, 46, 4626-4671, (2009) · Zbl 1187.68121
[5] Andreoli, J.-M., Logic programming with focusing proofs in linear logic, J. Logic Comput., 2, 297-347, (1992) · Zbl 0764.03020
[6] Andrews, P., Resolution in type theory, J. Symbolic Logic, 36, 3, (1971) · Zbl 0231.02038
[7] Appel, A. W.; Felty, A. P., Lightweight lemmas in λprolog, (International Conference on Logic Programming, (November 1999), MIT Press)
[8] Aranda-López, G.; Nieva, S.; Sáenz-Pérez, F.; Sánchez-Hernández, J., Implementing a fixed point semantics for a constraint deductive database based on hereditary harrop formulas, (Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’09, (2009), ACM), 117-128
[9] Awodey, S.; Rabe, F., Kripke semantics for martin-Löf’s extensional type theory, Log. Methods Comput. Sci., 7, 3, (2011) · Zbl 1237.03007
[10] Baelde, D., A linear approach to the proof-theory of least and greatest fixed points, (2008), École Polytechnique, PhD thesis
[11] Bai, M.; Blair, H., General model theoretic semantics for higher-order Horn logic programming, (Logic Programming and Automated Reasoning, International Conference LPAR’92, Lecture Notes in Comput. Sci., vol. 624, (1992), Springer) · Zbl 0925.68100
[12] Benzmüller, C.; Brown, C. E.; Kohlhase, M., Higher order semantics and extensionality, J. Symbolic Logic, 69, 1027-1088, (2004) · Zbl 1071.03024
[13] Cabeza, D.; Hermenegildo, M. V.; Lipton, J., Hiord: a type-free higher-order logic programming language with predicate abstraction, (9th Asian Computing Science Conference, ASIAN 2004, Lecture Notes in Comput. Sci., vol. 3321, (2004), Springer), 93-108 · Zbl 1115.68370
[14] Capretta, V., Coalgebras in functional programming and type theory, Theoret. Comput. Sci., 412, 38, 5006-5024, (2011) · Zbl 1225.68057
[15] Chen, W.; Kifer, M.; Warren, D. S., Hilog: a foundation for higher-order logic programming, J. Log. Program., 15, 3, 187-230, (1993) · Zbl 0787.68017
[16] Church, A., A formulation of the simple theory of types, J. Symbolic Logic, 5, 56-68, (1940) · JFM 66.1192.06
[17] Comini, M.; Meo, C.; Levi, G., A theory of observables in logic programming, Inform. and Comput., 169, 1, 23-80, (2000)
[18] DeMarco, M.; Lipton, J., Completeness and cut elimination in the intuitionistic theory of types, J. Logic Comput., 15, 6, 821-854, (December 2005)
[19] Komendantskaya, E.; Power, J.; Schmidt, M., Coalgebraic logic programming: implicit versus explicit resource handling, (ICLP 12, Budapest, (September 2012))
[20] Enderton, H. B., A mathematical introduction to logic, (1972), Academic Press · Zbl 0298.02002
[21] Gabbay, D. M.; Reyle, U., N-prolog: an extension of prolog with hypothetical implications I, J. Log. Program., 1, 4, 319-355, (1984) · Zbl 0576.68001
[22] Girard, J.; Lafont, Y.; Taylor, P., Proofs and types, (1998), Cambridge University Press
[23] Henkin, L., Completeness in the first-order function calculus, J. Symbolic Logic, 14, 159-166, (1949) · Zbl 0034.00602
[24] Henkin, L., Completeness in the theory of types, J. Symbolic Logic, 15, 81-91, (June 1950)
[25] Hermenegildo, M. V.; Puebla, G.; Bueno, F.; López-García, P., Integrated program debugging, verification, and optimization using abstract interpretation (and the ciao system preprocessor), Sci. Comput. Program., 58, 1-2, 115-140, (2005) · Zbl 1076.68540
[26] Hindley, J. R., Basic simple type theory, (1997), Cambridge University Press New York, NY, USA · Zbl 0906.03012
[27] Jaffar, J.; Maher, M., Constraint logic programming: a survey, J. Log. Program., 19/20, 503-581, (1994)
[28] Jagadeesan, R.; Nadathur, G.; Saraswat, V. A., Testing concurrent systems: an interpretation of intuitionistic logic, (Proc. 25th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2005, Lecture Notes in Comput. Sci., vol. 3821, (2005), Springer), 517-528 · Zbl 1172.68555
[29] Komendantskaya, E.; Power, J., Coalgebraic derivations in logic programming, (Computer Science Logic, CSL’11, (2011), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), 352-366 · Zbl 1247.68044
[30] Kripke, S. A., Semantical analysis of intuitionistic logic I, (Crossley, J.; Dummett, M., Formal Systems and Recursive Functions, (1965), North-Holland Amsterdam), 92-130 · Zbl 0137.00702
[31] Lastres, E., A semantics for logic programs based on HH formulas, (2002), Università di Pisa, PhD thesis
[32] Leach, J.; Nieva, S., A higher-order logic programming language with constraints, (FLOPS’01, Lecture Notes in Comput. Sci., vol. 2024, (2001), Springer), 108-122 · Zbl 0977.68012
[33] Leach, J.; Nieva, S.; Rodríguez-Artalejo, M., Constraint logic programming with hereditary harrop formulas, Theory Pract. Log. Program., 1, 4, 409-445, (2001) · Zbl 1091.68522
[34] Liang, C.; Miller, D., Focusing and polarization in linear, classical and intuitionistic logic, Theoret. Comput. Sci., 410, 46, 4747-4768, (2009) · Zbl 1187.68528
[35] Lipton, J.; Nieva, S., Higher-order logic programming languages with constraints: a semantics, (8th International Conference Typed Lambda Calculi and Applications, TLCA 2007, Lecture Notes in Comput. Sci., vol. 4583, (June 2007), Springer-Verlag), 272-289 · Zbl 1215.68058
[36] Lloyd, J. W., Foundations of logic programming, (1987), Springer Verlag New York · Zbl 0547.68005
[37] Miller, D., A logical analysis of modules in logic programming, J. Log. Program., 79-108, (1989) · Zbl 0681.68022
[38] Miller, D.; Nadathur, G., Programming with higher-order logic, (2012), Cambridge University Press · Zbl 0900.68129
[39] Miller, D.; Nadathur, G.; Pfenning, F.; Scedrov, A., Uniform proofs as a foundation for logic programming, Ann. Pure Appl. Logic, 51, 1-2, 125-157, (1991) · Zbl 0721.03037
[40] Mitchell, J., Foundations for programming languages, (1996), MIT Press Cambridge, Massachusetts
[41] Mitchell, J.; Moggi, E., Kripke-style models for typed lambda calculus, Ann. Pure Appl. Logic, 51, 99-124, (1991) · Zbl 0728.03011
[42] Necula, G., Proof carrying code, (Proc. 24th Annual Symp. on Principles of Programming Languages, POPL ’97, (1997))
[43] Nieva, S.; Sáenz-Pérez, F.; Sánchez, J., Formalizing a constraint deductive database language based on hereditary harrop formulas with negation, (Proc. 9th International Symposium on Functional and Logic Programming, FLOPS’08, Lecture Notes in Comput. Sci., vol. 4989, (2008), Springer), 289-304 · Zbl 1137.68339
[44] Saeedloei, N.; Gupta, G., Coinductive constraint logic programming, (FLOPS, (2012)), 243-259 · Zbl 1354.68040
[45] Saraswat, V., The category of constraints is Cartesian closed, (Proc. of the 7th Symposium on Logic in Computer Science, LICS ’92, (1992), IEEE Press), 341-345
[46] Simon, L. E., Extending logic programming with coinduction, (2006), University of Texas at Dallas, AAI3224400
[47] Takahashi, M., A proof of cut-elimination in simple type theory, J. Math. Soc. Japan, 19, 4, 399-410, (1967) · Zbl 0206.27503
[48] Tarski, A., A decision method for elementary algebra and geometry, (1951), University of California Press · Zbl 0044.25102
[49] Tiu, A., A logical framework for reasoning about logical specifications, (2004), The Pennsylvania State University, PhD thesis
[50] van Dalen, D., Logic and structure, (2004), Springer · Zbl 1048.03001
[51] van Dalen, D.; Troelstra, A. S., Constructivism in mathematics: an introduction, (1988), North-Holland · Zbl 0653.03040
[52] Wolfram, D. A., A semantics for λprolog, Theoret. Comput. Sci., 136, 277-289, (1994) · Zbl 0874.68181
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.