Heaps and Towers

Any definition of a heap and of the dividing line between two heaps is necessarily somewhat arbitrary.

Definition Heap.D1

A set of objects OS is stable in situation S if every object in OS remains motionless for a time in every history H following OS, assuming that no external forces are applied.

Declaration: stable(OS : set[object]; S : situation) -- Predicate.

Formalism:
stable(OS,S) < = >
[forall(H) dynamic(H) ^ start(H)=S ^ ~exists(F : force ; S1 in H, O in OS) external_force(F,O,S1)] => exists(H1) start(H1,H) ^ forall(O in OS) motionless(O,H1).

Definition Heap.D2

Situation S1 is the restriction of situation S2 to the objects in OS.

Declaration: restriction(S : situation; OS : set[objects]) : situation --- Function.

Formalism:
restriction(S,OS)=S1 =>
P(OS,objects(S)) ^
[forall(O in OS) value_in(S1,placement(O)) = value_in(S,placement(O)) ^
value_in(S1,velocity(O)) = value_in(S,velocity(O))

Definition Heap.D3:

A set of objects OS is a support structure for object O1 in situation S iff OS union { O1 } is stable in S. An object O2 (indirectly) supports O1 in situation S if O2 is an element of some minimal support structure for O1 in S. An object O2 directly supports O1 if O2 supports O1 and O2 abuts O1.

Declaration:
support(O2,O1 : object; S : situation) --- Predicate. direct_support(O2,O1 : object; S : situation) --- Predicate.

Formalism
support(O2,O1,S) < = >
exists(OS1) O1 in OS1 ^ O2 in OS1 ^ stable(OS1,restriction(S,OS1)) ^
~exists(OS2) PP(OS2,OS1) ^ O1 in OS2 ^ stable(OS2,restriction(S,OS2)).

direct_support(O2,O1,S) < = > support(O2,O1,S) ^ holds(S,rcc_EC^*(O2,O1)). \noindent

Definition Heap.D4

The relation ``same_heap(O1,O2,S)'' over two mobile objects O1,O2 is the transitive closure of the support relation and its inverse restricted to mobile objects. A heap is an equivalence class over same_heap.

Declaration:
same_heap(O1,O2 : object: S : situation) --- Predicate.
heap(OS: set[object]: S : situation) --- Predicate.

Formalism:
same_heap(O1,O2,S) < = > [~fixed(O1) ^ ~fixed(O2) ^ [O1=O2 V supports(O1,O2,S) V supports(O2,O1,S)]] V
[exists(O3) same_heap(O1,O3,S) ^ same_heap(O3,O2,S)].

heap(OS,S) < = >
forall(O1,O2 in OS) same_heap(O1,O2,S) ^ forall(O1 in OS ,O2 not in OS) ~same_heap(O1,O2,S).

Fact Heap.F1:

In any stable configuration, each mobile object is in exactly one heap.

Characteristics: Statics, set of objects.

Formalism:
[stable(OS,S) ^ O in OS ^ ~fixed(O,S)] => exists(OH) heap(OH,S) ^ O in OH.

Fact Heap.F2

If O1 and O2 are in heap OH and O1 adjoins O2 and O1 meets O2 only at points where O1 has a normal with an upward component, then probably O1 supports O2.

Characteristics: Statics, probabilistic, set of objects.

Formalism:

Prob_S 
   (supports(O1,O2,S) |
    same_heap(O1,O2,S) ^ holds(S,rcc_EC^*(O1,O2)) ^
    forall(P) holds(S,P in^* O1 intersect^* O2) =>
              dot_prod(value(S,out_normal^*(O1,P)),up) > 0)
   )
> 0.9

Fact Heap.F3

If an object is in the middle of a heap and does not support any other object, then it is probably substantially smaller than most of the other objects in the heap.

Characteristics: Statics, probabilistic, set of objects.

Formalism:

Prob_OH,S,O1,O2(
   diameter(O1) < diameter(O2) / 4 
   |
   heap(OH,S) ^ O1 in OS ^ O2 in OS ^ O1 != O2 ^
   holds(S,middle_heap(O1,OS)) ^ ~exists(OA) support(O1,OA,S)
   )
> 0.9.

Fact Heap.F4

If the only fixed object supporting a heap is a flat table, and no objects in the heap are jammed together and it is kinematically possible to disassemble the heap, then it is likely that a sufficiently hard blow to the bottom of the heap will break up the heap.

Characteristics: Dynamics, probabilistic, set of objects, external forces.

Formalism:

Prob_OS,S( 
  exists(M : momentum)
     forall(S1,B : impact) [momentum(B) > M ^ strikes(B,OB) ^ OB in OS ^ occurs(B,S,S2)] => 
        exists(O1,O2 in OS) ~same_heap(O1,O2,S1)
   |
  heap(OS,S) ^ 
  [forall(O in OS,O1) support(O1,O,S) ^ fixed(O1,S) < = > O1 = OTABLE]  ^
  [forall(P,O in OS) holds(S,P in^* OTABLE intersect O) =>
        [P in upper_surface(OTABLE,S) ^ value(S,out_tangent^*(O1,P) = up)] ^
  [forall (OX subset OS) ~jammed(OX,S)] 
  [exists(H) kinematic(H) ^ start(H)=S ^ 
      forall(O1,O2 in OS) holds(end(H),DC^*(O1,O2))]
  )
> 0.5

Fact Heap.F5

Indirect support is the transitive closure of direct support.

Characteristics: Statics.

Formalism:
support(O1,O2,S) < =>
O1=O2 V direct_support(O1,O2,S) V
exists(O3) support(O1,O3,S) ^ direct_support(O3,O2,S)