Abstract
We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Reduction then becomes identified with logical entailment.
Thus, the models suggest a new way to identify logic and computation. Both have elementary and concrete representations in our models; where these representations overlap, they coincide.
In a concluding speculation, we note a certain subclass of the models which seems to play a role analogous to that played by the cumulative hierarchy models in axiomatic set theory and the natural numbers in formal arithmetic — there are many models of the respective theories, but only some, characterised by a fully second order interpretation, are the ‘intended’ ones.
The authors are grateful to the anonymous referees for their comments.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. Journal of Symbolic Logic 69, 1027–1088 (2004)
Dekkers, W., Bunder, M., Barendregt, H.: Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic. Journal of Symbolic Logic 3, 869–890 (1998)
Dekkers, W., Bunder, M., Barendregt, H.: Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus. Archive für Mathematische Logik 37, 327–341 (1998)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)
Michael Dunn, J., Restall, G.: Relevance logic. In: Gabbay, D.M. (ed.) Handbook of Philosophical Logic, 2nd edn., vol. 6, pp. 1–136. Kluwer Academic Publishers, Dordrecht (2002)
Gabbay, M., Gabbay, M.J.: Term sequent logic. In: Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008). Electronic Notes in Theoretical Computer Science, vol. 246, pp. 87–106 (August 2009)
Werner, B., Dowek, G.: Arithmetic as a theory modulo. In: Proceedings of RTA, pp. 423–437 (2005)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Girard, J.-Y.: Linear logic: its syntax and semantics. In: Proceedings of the Workshop on Advances in Linear Logic, pp. 1–42. Cambridge University Press, New York (1995)
Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and types. Cambridge University Press, Cambridge (1989)
Goldblatt, R.: Logics of Time and Computation, 2nd edn., Center for the Study of Language and Information. CSLI Lecture Notes, vol. 7 (1992)
Henkin, L.: Completeness in the theory of types. Journal of Symbolic Logic 15, 81–91 (1950)
Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge, New York (1996)
Jay, C.B., Ghani, N.: The virtues of eta-expansion. Journal of Functional Programming 5(2), 135–154 (1995)
Kleene, S.C., Rosser, J.B.: The inconsistency of certain formal logics. Annals of Mathematics 36(3) (1935)
Meyer, R.K., Bunder, M.W., Powers, L.: Implementing the ‘fool’s model’ of combinatory logic. Journal of Automated Reasoning 7(4), 597–630 (1991)
O’Hearn, P., Pym, D.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
Plotkin, G.D.: The lambda-calculus is omega-incomplete. Journal of Symbolic Logic 39(2), 313–317 (1974)
Selinger, P.: Order-incompleteness and finite lambda reduction models. Theoretical Computer Science 309(1), 43–63 (2003)
Shapiro, S.: Foundations without foundationalism: a case for second-order logic. Oxford logic guides, vol. 17. Oxford University Press, Oxford (2000)
van Benthem, J.: Higher-order logic. In: Handbook of Philosophical Logic, 2nd edn., vol. 1, pp. 189–244. Kluwer, Dordrecht (2001)
Visser, A.: An overview of interpretability logic. In: Proceedings of the 1988 Heyting Conference on Mathematical Logic, pp. 307–359. Plenum Press, New York (1997)
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gabbay, M., Gabbay, M.J. (2010). A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing. In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-17511-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17510-7
Online ISBN: 978-3-642-17511-4
eBook Packages: Computer ScienceComputer Science (R0)