The Law and the complexity of recursively defined data structures.

As Carl Woolf has pointed out and as we did during the design of the Law
there are two ways to represent the Law: the type-based version and the
object-based version. The object-based version is formulated as:

A method may send messages only to the following OBJECTS: 
    'self', 
    the objects passed by the method's parameters, 
    objects created by the method, 
    children (if self is a repetition object), and 
    parts of self (if self is a construction object).

How do we distinguish between the two versions? One important distinguishing
feature is the complexity of checking the Law. The type-based version of
the Law is checkable in polynomial time and the object-based version
I conjecture is NP-hard to check.

Consider the following example:
; Grammar ~ {Rule}.
(defmethod (Grammar :m) ()
  (send (send self ':m1) ':m2))

We assume that the return type of :m1 is Rule. It can be difficult to
verify that :m1 really returns a member of THIS list of rules and not
some other instance of Rule.

My NP-hard-ness conjecture is based on the following paper:

@ARTICLE{oppen:rec-data-80,
  AUTHOR = "Derek C. Oppen",
    TITLE = "Reasoning about recursively defined data structures",
      JOURNAL = jacm,
	YEAR = 1980,   
	  PAGES = "403-411",
	    MONTH = "July",    
	      VOLUME = 27,  
		NUMBER = 3 
		  }

which shows that the quantifier-free theory of recursively defined data
structures is NP-complete.

I suggest that Ian studies this complexity question in detail and that
we put the result (not necessarily the proof) into the OOPSLA Law
paper. 

I consider it of utmost importance that we motivate our formulation of the
Law as much as we can. We again found a very useful application of complexity
theory to the science of programming.

Does Ian agree to taking on this task?

-- Karl