Abstract
The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. This paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in reasoning about type classes.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Lu, L., King, A.: Determinacy Inference for Logic Programs. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 108–123. Springer, Heidelberg (2005)
Kriener, J., King, A.: RedAlert: Determinacy Inference for Prolog. TPLP 11, 537–553 (2011)
Bossi, A., Cocco, N., Fabris, M.: Norms on Terms and their use in Proving Universal Termination of a Logic Program. TCS 124, 297–328 (1994)
Martin, J.C., King, A., Soper, P.: Typed Norms for Typed Logic Programs. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 224–238. Springer, Heidelberg (1997)
Weispfenning, V.: The Complexity of Linear Problems in Fields. Journal of Symbolic Computation 5, 3–27 (1988)
Craig, W.: Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. J. Symb. Log. 22, 269–285 (1957)
Weissenbacher, G.: Program Analysis with Interpolants. PhD thesis, Magdalen College (2010), http://ora.ouls.ox.ac.uk/objects/uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6
Krajíček, J.: Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. J. Symb. Log. 62, 457–486 (1997)
Farkas, J.: Theorie der einfachen Ungleichungen. Journal für die Reine und Angewandte Mathematik 124, 1–27 (1902)
Avis, D.: lrs: A Revised Implementation of the Reverse Search Vertex Enumeration Algorithm. In: Kalai, G., Ziegler, G.M. (eds.) Polytopes - Combinatorics and Computation, pp. 177–198. Birkhauser-Verlag (2000)
Goodman, J.E., O’Rourke, J. (eds.): Handbook of Discrete and Computational Geometry. CRC Press (2004)
Read, R.C.: Everyone a Winner. Annals of Discrete Mathematics 2, 107–120 (1978)
Peyton-Jones, S., Jones, M., Meijer, E.: Type Classes: an exploration of the design space. In: ACM SIGPLAN Haskell Workshop (1997)
Morris, J.G., Jones, M.P.: Instance Chains: Type Class Programming Without Overlapping Instances. In: Hudak, P., Weirich, S. (eds.) ICFP, pp. 375–386. ACM (2010)
The GHC Team: The Glorious Glasgow Haskell Compilation System User’s Guide, Version 7.2.1 (2011), http://www.haskell.org/ghc/docs/latest/html/users_guide
O’Keefe, R.A.: The Craft of Prolog. MIT Press (1990)
King, A., Lu, L.: Forward versus Backward Verification of Logic Programs. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 315–330. Springer, Heidelberg (2003)
Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 199–213. Springer, Heidelberg (2009)
Ziegler, G.M.: Lectures on Polytopes. Springer, New York (1995)
Bertsimas, D., Tsitsiklis, J.: Introduction to Linear Optimization, 1st edn. Athena Scientific (1997)
Avis, D., Fukuda, K.: Reverse search for enumeration. Discrete Applied Mathematics 65, 21–46 (1996)
Benoy, F., King, A.: Inferring Argument Size Relationships with CLP(R). In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 204–223. Springer, Heidelberg (1997)
Miné, A.: The Octagon Abstract Domain. HOSC 19, 31–100 (2006)
Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning 2, 41–62 (2009)
Sahlin, D.: Determinacy Analysis for Full Prolog. In: Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 23–30. ACM (1991)
Mogensen, T.Æ.: A Semantics-Based Determinacy Analysis for Prolog with Cut. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) PSI 1996. LNCS, vol. 1181, pp. 374–385. Springer, Heidelberg (1996)
Dawson, S., Ramakrishnan, C.R., Ramakrishnan, I.V., Sekar, R.C.: Extracting Determinacy in Logic Programs. In: Proceedings of the Tenth International Conference on Logic Programming, pp. 424–438. MIT Press (1993)
López-García, P., Bueno, F., Hermenegildo, M.V.: Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Analyses. New Generation Computing 28, 177–206 (2010)
McMillan, K.L.: Applications of Craig Interpolants in Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005)
Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. Journal of Symbolic Computation 45, 1212–1233 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kriener, J., King, A. (2012). Mutual Exclusion by Interpolation. In: Schrijvers, T., Thiemann, P. (eds) Functional and Logic Programming. FLOPS 2012. Lecture Notes in Computer Science, vol 7294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29822-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-29822-6_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29821-9
Online ISBN: 978-3-642-29822-6
eBook Packages: Computer ScienceComputer Science (R0)