Entailment with Conditional Equality Constraints

  • Zhendong Su
  • Alexander Aiken
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


Equality constraints (unification constraints) have widespread use in program analysis, most notably in static polymorphic type systems. Conditional equality constraints extend equality constraints with a weak form of subtyping to allow for more accurate analyses. We give a complete complexity characterization of the various entailment problems for conditional equality constraints. Additionally, for comparison, we study a natural extension of conditional equality constraints.


  1. 1.
    A. Aiken, E. Wimmers, and T.K. Lakshman. Soft Typing with Conditional Types. In Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 163–173, January 1994.Google Scholar
  2. 2.
    L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen, May 1994. DIKU report 94/19.Google Scholar
  3. 3.
    A. Colmerauer. Prolog and Infinite Trees. In K. L. Clark and S.-A. Tärnlund, editors, Logic Programming, pages 231–251. Academic Press, London, 1982.Google Scholar
  4. 4.
    A. Colmerauer. Equations and Inequations on Finite and Infinite Trees. In 2nd International Conference on Fifth Generation Computer Systems, pages 85–99, 1984.Google Scholar
  5. 5.
    M. Fähndrich and A. Aiken. Making Set-Constraint Based Program Analyses Scale. In First Workshop on Set Constraints at CP’96, Cambridge, MA, August 1996. Available as Technical Report CSD-TR-96-917, University of California at Berkeley.Google Scholar
  6. 6.
    M. Fähndrich, J. Foster, Z. Su, and A. Aiken. Partial Online Cycle Elimination in Inclusion Constraint Graphs. In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 85–96, Montreal, CA, June 1998.Google Scholar
  7. 7.
    C. Flanagan and M. Felleisen. Componential Set-Based Analysis. In Proceedings of the 1997 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 235–248, June 1997.Google Scholar
  8. 8.
    C. Flanagan, M. Flatt, S. Krishnamurthi, S. Weirich, and M. Felleisen. Catching Bugs in the Web of Program Invariants. In Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 23–32, May 1996.Google Scholar
  9. 9.
    J. Foster, M. Fähndrich, and A. Aiken. Monomorphic versus Polymorphic Flow-insensitive Points-to Analysis for C. In Proceedings of the 7th International Static Analysis Symposium, pages 175–198, 2000.Google Scholar
  10. 10.
    James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison Wesley, 1996.Google Scholar
  11. 11.
    N. Heintze. Set Based Analysis of ML Programs. In Proceedings of the 1994 ACM Conference on LISP and Functional Programming, pages 306–317, June 1994.Google Scholar
  12. 12.
    F. Henglein and J. Rehof. The Complexity of Subtype Entailment for Simple Types. In Symposium on Logic in Computer Science, pages 352–361, 1997.Google Scholar
  13. 13.
    F. Henglein and J. Rehof. Constraint Automata and the Complexity of Recursive Subtype Entailment. In ICALP98, pages 616–627, 1998.Google Scholar
  14. 14.
    Fritz Henglein. Global Tagging Optimization by Type Inference. In 1992 ACM Conference on Lisp and Functional Programming, pages 205–215, June 1992.Google Scholar
  15. 15.
    Joxan Jaffar and Michael J. Maher. Constraint Logic Programming: A Survey. The Journal of Logic Programming, 19 & 20:503–582, May 1994.CrossRefMathSciNetGoogle Scholar
  16. 16.
    N. D. Jones and S. S. Muchnick. Flow Analysis and Optimization of LISP-like Structures. In Sixth Annual ACM Symposium on Principles of Programming Languages, pages 244–256, January 1979.Google Scholar
  17. 17.
    S. Marlow and P. Wadler. A Practical Subtyping System For Erlang. In Proceedings of the International Conference on Functional Programming (ICFP’ 97), pages 136–149, June 1997.Google Scholar
  18. 18.
    R Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, 17(3):348–375, December 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    J. Palsberg. Equality-based Flow Analysis versus Recursive Types. ACM Transactions on Programming Languages and Systems, 20(6):1251–1264, 1998.CrossRefGoogle Scholar
  20. 20.
    J. Palsberg and M. I. Schwartzbach. Object-Oriented Type Inference. In Proceedings of the ACM Conference on Object-Oriented programming: Systems, Languages, and Applications, pages 146–161, October 1991.Google Scholar
  21. 21.
    M.S. Paterson and M.N. Wegman. Linear Unification. Journal of Computer and Systems Sciences, 16(2):158–167, 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    J. C. Reynolds. Automatic Computation of Data Set Definitions, pages 456–461. Information Processing 68. North-Holland, 1969.Google Scholar
  23. 23.
    O. Shivers. Control Flow Analysis in Scheme. In Proceedings of the ACM SIGPLAN’ 88 Conference on Programming Language Design and Implementation, pages 164–174, June 1988.Google Scholar
  24. 24.
    G. Smolka and R. Treinen. Records for Logic Programming. Journal of Logic Programming, 18(3):229–258, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    B. Steensgaard. Points-to Analysis in Almost Linear Time. In Proceedings of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 32–41, January 1996.Google Scholar
  26. 26.
    Z. Su and A. Aiken. Entailment with Conditional Equality Constraints. Technical Report UCB//CSD-00-1113, University of California, Berkeley, October 2000.Google Scholar
  27. 27.
    Z. Su, M. Fähndrich, and A. Aiken. Projection Merging: Reducing Redundancies in Inclusion Constraint Graphs. In Proceedings of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 81–95, 2000.Google Scholar
  28. 28.
    R.E. Tarjan. Efficiency of a Good but Not Linear Set Union Algorithm. JACM, pages 215–225, 1975.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Zhendong Su
    • 1
  • Alexander Aiken
    • 1
  1. 1.EECS DepartmentUniversity of CaliforniaBerkeley

Personalised recommendations