Boxes

Up: Corpus of Examples
Previous: Dynamics
Next: Rings

Solid Boxes

Definition Box.D1

A box is a bounded, connnected region whose complement consists of at least two connected components. Any bounded thickly connected component of the complement is a cavity; the union of the cavities is the inside.

Formalism:
box(R : region) -- Predicate.
inside(R : region) : point-set -- Function.
cavity(R1,R2 : region) -- Predicate

Definitions:
inside(R) = closure(complement(R) -- outside(R))

box(R) < = > inside(R) != empty.

cavity(RC,R) <=> thickly_connected_component(RC,inside(R)).

Comment: The statements of the facts and definitions involving closed boxes require more care to get right than one might suppose, because there are ``everywhere thick'' boxes with internal cavities that are separated from the outside (figure 1.A); there are boxes with ``thin'' points where an internal cavity meets the outside (figure 1.B); there are boxes with both cavities separated from the outside and cavities that meet the outside (figure 1.C); and there are boxes with chains of cavities that meet along thin points, that either meet the outside (figure 1.D) or do not meet the outside (figure 1.E).) The definition above includes all these cases.

Fact Box.F1

If R2 is a box and R1 is inside R2 then R2 is outside R1, and the outside of R2 is outside R1.

Characteristics: Topology.

Formalism:
box(R2) ^ P(R1 : region, inside(R2)) => P(R2,outside(R1)) ^ P(outside(R2), outside(R1)).

Fact Box.F2

If regions RB1 and RB2 are closed boxes, and R is inside RB1 and inside RB2, and RB1 and RB2 are disjoint, then either RB1 is inside RB2 or RB2 is inside RB1.

Characteristics: Topology

Formalism:
box(RB1) ^ box(RB2) ^ P(R : region,inside(RB1)) ^ P(R,inside(RB2)) ^ rcc_DS(RB1,RB2) => [PP(RB1,inside(RB2)) V PP(RB2,inside(RB2))]

Fact Box.F3

(Inside/outside compositional rules). If box R1 is inside box R2, then the inside of R1 is inside R2.

Characteristics: Topology.

Formalism:
box(R1) ^ box(R2) ^ P(R1,inside(R2)) => PP(inside(R1),inside(R2)).

Fact Box.F4

(Inside/outside compositional rules). If object R1 is outside box R2, then R2 and its inside are outside R1.

Characteristics: Topology.

Formalism:
box(R2) ^ P(R1 : region,outside(R2)) => PP(R2,outside(R1)) ^ PP(inside(R2),outside(R1)).

Definition Box.D2

A thin point in a box is a point that is in both the closure of the inside and the closure of the outside of the box. (Figure). A box with no thin points is a thick box.

Declaration:
thin_box_pt(P : point, R : region) -- Predicate.
thick_box(R : region) -- Predicate.

Formalism:
thin_box_pt(P,R) < = > box(R) ^ P in outside(R) intersect inside(R).

thick_box(R) < = > box(R) ^ not exists(P) thin_box_pt(P,R).

Fact Box.F5

The outside and inside of a thick box are disconnected.

Characteristics: Topology.

Formalism:
thick_box(R) < = > box(R) ^ DC(outside(R),inside(R))

Fact Box.F6

You can turn any region into a thick box by carving out an internal cavity. Formally, let R be a connected region, and let R1 be a region that is NTPP to R. Then R--R1 is a closed box.

Characteristics: Topology.

Formalism:
rcc_NTTP(R1,R2 : region) => thick_box(R1--R2)

Fact Box.F7

You can turn any region into a thick box by adding a blister.

Characteristics: Topology.

Formalism:
forall(R1: region) exists (R2) blob(R2) ^ thick_box(R1 union R2).

Fact Box.F8

If two externally connected blobs meet in an surface ring, then their union is a box.

Characteristics: Topology.

Formalism:
blob(R1) ^ blob(R2) ^ rcc_EC(R1,R2) ^ SU = boundary(R1) intersect boundary(R2) ^ SU=SU1--SU2 ^ surface_NTPP(SU2,SU1) =>
box(R1 union R2).

Fact Box.F9

If RB is a box and region R is disjoint from RB, then either R is inside RB or R is outside RB.

Characteristics: Topology.

Formalism:
box(RB) ^ rcc_DS(R : region,RB) => P(R,outside(RB)) V P(R,inside(RB))

Fact Box.F10

Let R be a region and let P1 and P2 be two points not in R. If there does not exist a connected point-set PS1 that contains P1 and P2 and is disjoint from R, then R is a thick box. If there does not exist a region R1 that contains P1 and P2 and is disjoint from R, then R is a box. In either case, either P1 is on the outside and P2 is on the inside, or P1 and P2 are in different cavities.

Characteristics: Topology.

Formalism:
forall(P1, P2 : point; R : region) ~(P1 in R) ^ ~(P2 in R) ^
[~exists(PS1 : point-set) connected(PS1) ^ in(P1,PS1) ^ in(P2,PS1) ^ DC(PS1,interior(R))] =>
thick_box(R) ^
exists (RC1,RC2) [RC1 = outside(R) V cavity(RC1,R)] ^ [RC2 = outside(R) V cavity(RC2,R)] ^
RC1 != RC2 ^ in(P1,RC1) ^ in(P2,RC2)

forall(P1, P2 : point; R : region) ~(P1 in R) ^ ~(P2 in R) ^
[~exists(R1 :region) P1 in R1 ^ P2 in R1 ^ rcc_DS(R1,R)] =>
box(R) ^
exists (RC1,RC2) [RC1 = outside(R) V cavity(RC1,R)] ^ [RC2 = outside(R) V cavity(RC2,R)] ^
RC1 != RC2 ^ in(P1,RC1) ^ in(P2,RC2)

Fact Box.F11

If region RB is a box and region RC is a superset of RB that does not contain all the inside of RB, then RC is a box.

Characteristics: Topology.

Formalism:
box(RB) ^ P(RB,RC) ^ ~P(inside(RB),RC) => box(RC) ^ P(inside(RB)--RC, inside(RC)).

Fact Box.F12

If RA and RB are boxes and RA fits inside RB then RB does not fit inside RA.

Characteristics: Geometry.

Formalism:
box(RA) ^ box(RB) ^ fits_in(RA,inside(RB)) => ~fits_in(RB,inside(RA)).

Fact Box.F13

If RB and RC are boxes, RA fits inside RB and RB fits inside RC, then RA fits inside RC.

Characteristics: Geometry.

Formalism:
fits_in(RA,inside(RB)) ^ fits_in(RB,inside(RC)) => fits_in(RA,inside(RC))

Fact Box.F14

Let OB be a solid box. If object O1 is inside OB in situation S, then it has always been inside OB and will always be inside OB. If O1 is outside OB, then it has always been outside OB and will always be outside OB.

Characteristics: Kinematics

Formalism:
box(OB) ^ kinematic(H) ^ S in H ^ S1 in H =>
[holds(S,P^*(O1,inside⁺(OB))) => holds(S1,P^*(O1,inside⁺(OB)))] ^
[holds(S,P^*(O1,outside⁺(OB))) => holds(S1,P^*(O1,outside⁺(OB)))].

Fact Box.F15

If box OB goes through hole RH, then the inside of OB goes through RH. (Hence, by fact Holes.F2, any object inside OB goes through RH.)

Characteristics: Topology.

Formalism: box(OB) ^ occurs(H,goes_through(OB,OH,OU1,OSU2)) => exists(H1) subhistory(H1,H) ^ occurs(H1,goes_through(inside*(OB),OH,OSU1,OSU2)).

Boxes with holes

Definition Box.D3

Let RC be a box and let RH be a hole that extends through RC. SU is an outer / inner outlet of RH from RC if it is an outlet of RH through RC and is part of the outside / inside surface of RC.

Declaration:
outer_outlet(SU : surface; RH, RC : region) -- Predicate.
inner_outlet(SU : surface; RH, RC : region) -- Predicate.

Formalism
outer_outlet(SU,RH,RC) < = > outlet(SU,RH,RC) ^ P(SU,outside(RC))
inner_outlet(SU,RH,RC) < = > outlet(SU,RH,RC) ^ P(SU,inside(RC))

Definition Box.D4:

Let RB (the box with holes) and RC be regions and let RHS (the set of holes) be a set of regions. RB is said to be a geometric box with holes RHS and completion RC if the following conditions are met:

RC is a box and a subset of convex_hull(RB).
RHS is the set of holes through RB relative to filling-in RC.
Each hole RH has at least one inner outlet and one outer outlet from PB.

Declaration: g_box_with_holes(RB : region; RHS : set[region]; RC : region) -- Predicate.

Formalism:
g_box_with_holes(RB,RHS,RC) < = >
holes(PHS,RB,RC) ^ box(RC) ^ P(RC,convex_hull(RB)) ^
forall(RH in RHS) exist(SU1,SU2 : surface) inner_outlet(SU1,RH,RC) ^ outer_outlet(SU2,RH,RC)

Definition Box.D5:

Let OB be an object, let PHS be a set of pseudo-objects associated with OB, and let PC be a pseudo-object associated with OB. OB is a box with holes PHS and completion PC if the shapes of these g_objects constitutes a geometrical box with holes.

Declaration: box_with_holes(OB: object; PHS : set[pseudo-object]; PC : pseudo-object) -- Predicate

Formalism:
box_with_holes(OB,PHS,PC) < = >
g_box_with_holes(OB,PHS,PC) ^ source(PC) = OB ^ forall(PH in PHS) source(PH) = OB.

Fact Box.F16

Let OB be a box with holes PHS and completion PC. If object O1 is at one time inside PC and at another time outside PC, then then O1 goes through some hole PH in PHS in between.

Characteristics: Kinematics

Formalism:
forall(O1, OB : object; PHS : set[pseudo-object]; PC : pseudo-object; S1,S2 : situation ; H : history);
[box_with_holes(OB,PHS,PC) ^ S1 in H ^ S2 in H ^ kinematic(H) ^ holds(S1,P^*(O1,inside⁺(PC))) ^ holds(S2,P^*(O1,outside⁺(PC))) =>
exists(PH in PHS,PSUI,PSUO,H1) source(PSUI) = source(PSUO) = OB ^ inner_outlet(PSUI,PH,PC) ^ outer_outlet(PSUO,PH,PC) ^ subhistory(H1,H) ^
[ time(S1) < time(S2) => occurs(H1,goes_through(O1,PH,PSUI,PSUO))] ^
[ time(S2) < time(S1) => occurs(H1,goes_through(O1,PH,PSUO,PSUI))].

Fact Box.F16a

Corollary: It follows, therefore that, if O goes from inside OB to outside OB, then it fits through some hole in OB. If O does not fit through any hole in OB, then it cannot go from the inside to the outside, or vice versa. (We include this here separately, because it was easier to explain in the conference paper than the more general fact Box.F16.)

Characteristics: Kinematics.

Formalism:
[box_with_holes(OB,PHS,PC) ^
holds(S1,PP^*(O1 : object; inside⁺(PC)) ^ holds(S2,PP^*(O1 : object; outside⁺(PC)) ^
kinematic(H) ^ S1 in H ^ S2 in H] => \\ exists(PH in PHS,PSO,PSI) inner_outlet(PSI,PH,PC) ^ outer_outlet(PSI,PH,PC) ^
fits_through(O,PH,PSI,PSO)

Definition Box.D6:

can_exit(O,OB : object; POC : pseudo-object; S : situation).
OB is a box with completion POC. Object O can go from situation S, where it is inside POC, to outside POC.

Formalism: can_exit(O,OB,POC,S) < = >
exists(POHS) box_with_holes(OB,POHS,POC) ^
exists(H) kinematic(H) ^ S = start(H) ^ holds(S,P^*(O,inside⁺(POC))) holds(end(H),P^*(O,outside⁺(PB)))

Fact Box.F17

If O can exit OB then it fits through one of the holes in OB.

Characteristics: Kinematics.

Formalism:
box_with_holes(OB,POHS,POC) ^ can_exit(O,OB,POC,S) =>
exists(POH in POHS, POSUI, POSUO)
inner_outlet(POSUI,POH,POC) ^ outer_outlet(POSUO,POH,POC) ^ source(POSUI) = source(POSUO) = OB ^ fits_through(O,POH,POSUI,POSUO).

Fact Box.F18

It is possible to construct a box with holes OB and an object O such that O cannot exit OB from any situation even though O fits through one of the holes of OB. (because other parts of OB, other than the sides of the hole, interfere with it.)

Characteristics: Kinematics.

Formalism:
exists(O,OB,PC,PHS,PH,POSUI,POSUO)
box_with_holes(OB,PHS,PC) ^ PH in PHS ^ inner_outlet(POSUI,POH,POC) ^ outer_outlet(POSUO,POH,POC) ^
source(POSUI) = source(POSUO) = POB ^ fits_through(O,POH,POSUI,POSUO) ^ ~exists(S) can_exit(O,OB,PC,S)

Fact Box.F19

(Monotonicity of "can_exit" with respect to additional objects). Let OB be a box with completion PC. Suppose that object O can exit OB in situation S. Let S1 be a situation identical to S except that some of the objects other than O and OB are removed. Then O1 can exit OB1 in S1.

Characteristics: Kinematics; collection of objects.

Formalism:
forall(O,OB,O1,OB1 : object; PC, PC : pseudo-object; S,S1 : situation) can_exit(O,OB,PC,S) ^ subset(objects(S1),objects(S)) ^ subset({O,OB},objects(S1)) ^ forall(O in objects(S1)) place(O,S1) = place(O,S) ^ =>
can_exit(O1,OB1,PC,S1).

Fact Box.F20

(Monotonicity of "can_exit" with respect to shape inclusion). Let OB be a box with completion PC, and let OB1 be a smaller box with the same completion. Suppose that object O can exit OB in situation S. Let S1 be a situation where O is replaced by a smaller object O1 and OB is replaced by a smaller box with holes OB1, all other objects remaining the same. Then O1 can exit OB1 in S1.

Characteristics: Kinematics; collection of objects.

Formalism:
forall(O,OB,O1,OB1 : object; PC, PC : pseudo-object; S,S1 : situation)
can_exit(O,OB,PC,S) ^ objects(S1) = (objects(S) -- {O,OB}) union {O1,OB1} ^
P(place(O1,S1),place(O,S)) ^ P(place(OB1,S1),place(OB,S)) ^
forall(O2 in objects(S) -- {O,OB}) place(O,S1) = place(O,S2) ^ exists(PHS1) box_with_holes(OB1,PHS1,PC) =>
can_exit(O1,OB1,PC,S1).

Open Box

Definition Box.D7

Let RB be a region and SU be a connected planar surface. RB is an geometric open box with outlet SU if there exist regions RH and RC such that

RB is a box with the single hole RH and completion RC.
SU is the outer outlet of RH.

We say that the open box RB,SU opens in direction D where D is the normal to SU pointing outward from RH. A point P is in the inside of open box OB,SU if it is in SU or it is in the inside of RC for some such RC.

Declaration:
g_open_box1(RB,RH,RC : region; SU : surface) -- Predicate.
g_open_box(RB : region; SU : surface) -- Predicate.
g_open_box_out(RB : region; SU : surface) : direction -- Function.
g_open_box_inside(RB : region; SU : surface) : region --- Function.

Formalism:
g_open_box1(RB,RH,RC,SU) < = > g_box_with_holes(RB,{RH},RC) ^ planar(SU) ^ outer_outlet(SU,RH,RC)

g_open_box(RB,SU) < = >
exists(RH,RC) g_open_box1(RB,RH,RC,SU).

g_open_box_out(RB,SU) = D < = >
exists(RH,RC,P) g_open_box1(RB,RH,RC,SU) ^ P in SU ^ D=out_normal(RC,P).

forall (P : point) P in g_open_box_inside(RB,SU) < = >
P in SU V exists(RH,RC) g_open_box(RB,RH,RC,SU) ^ P in inside(RC).

Diagram

Definition Box.D8

Object OB is a (physical) open box with opening PSU if PSU is a pseudo-object associated with OB such that OB, PSU form a geometric open box. The outward direction and the inside are corresponding pseudo-objects.

Declaration:
open_box(OB : object; PSU : pseudo-object[surface]) -- Predicate.
open_box_out(OB : object; PSU : pseudo-object[surface]) : pseudo-object[direction] --- Function.
open_box_inside(OB : object; PSU : pseudo-object[surface]) : pseudo-object[region]

Formalism:

open_box(OB,PSU) < = > OB = source(PSU) ^ g_open_box(OB,PSU).

open_box_out(OB,PSU) = PD < = > OB = source(PSU) = source(PD) ^ D = open_box⁺(OB,PSU).

open_box_inside(OB,PSU) = PI < = > OB = source(PSU) = source(PI) ^ PI = open_box_inside⁺(OB,PSU).

Fact Box.F21

One can form a geometric open box by slicing a closed box through an interior point.

Characteristics: Geometry.

Formalism: closed_box(RB1) ^ PT in interior(inside(RB1)) ^ plane(PL) ^ PT in PL =>
exists(RB2) connected_component(RB2,RB1 -- PL) ^ PP(SU,PL) ^ open_box(RB2,SU) ^ PT in SU.

Fact Box.F22

If open box OB is held motionless with its opening upward throughout history H, and if, at the start of H, object O1 is inside OB and its velocity is zero, and if O1 is isolated from all objects and forces other than OB throughout H, then O1 will probably remain at least partly in OB throughout H. (Since initially the center of mass of O1 is below the horizontal plane SU and O1 has zero velocity, and since there is no source of energy, it follows by conservation of enerty that the center of mass of O1 can never be higher than SU. It is conceivable that a semi-circular O1 could bounce off the bottom of OB and do a Fosbury flop out of OB, keeping its center of mass below SU.)

Characteristics: Dynamics, probabilistic.

forall(OB,PSU,O1) open_box(OB,PSU) =>  

Prob(forall(S in H) holds(S,O^*(O1,open_box_inside(OB,PSU)) | 
     dynamic(H) ^ motionless(OB,H) ^ isolated({O1},{OB},H) ^ 
     holds(start(H),open_box_out(OB,SU) =^* up) ^ holds(start(H),still(O1)))
> 1 -- small_prob.

Comment: If O1 is required to be convex, then the conclusion can be proven deterministically (Davis, 1988). However, this distinction is presumably not part of a commonsense understanding.

Fact Box.F23

If OB is an open box with outlet SU, and O1 is resting stably in OB at the start of history H, and OB is moved sufficiently smoothly during H with SU facing up, and O1 is isolated in H, then O1 will remain in OB. The more rough the motion of O1, and the shallower the height of the inside of OB,SU, the more likely that O1 will come out of OB.

Characteristics: Dynamics, probabilistic tendency.

Formalism:

open_box(OB,PSU) =>
Prob_Tendency
 (conclusion: forall(S in H) holds(S,O^*(O1,open_box_inside(OB,PSU)).
  givens: isolated({O1},{OB},H) ^ 
     holds(start(H),open_box_out(OB,PSU) =^* up) ^ holds(S,still(O1)))
  influences: [roughness_motion(O1,H),small], 
              [height(SU) -- height(bottom(open_box_inside(OB,PSU)), big]
)

Fact Box.F24

If the following conditions hold:

OB is an open box with outlet SU.
The inside of OB is convex.
SU is the widest part of the inside of OB. Formally, SU is equal to the projection of the inside of OB onto SU.
Object O1 is inside OB.
OB is held upside down long enough in history H.
O1 is isolated in history H.

Then O1 will fall out of OB.

Characteristics: Dynamics.

Formalism:
[open_box(OB,SU) ^ convex(open_box_inside(OB,SU)) ^ SU=projection(open_box_inside(OB,SU),SU) ^
holds(S,PP^*(O1,open_box_inside(OB,SU))] =>
exists(D : duration) forall(H : history)
[[duration(H) > D ^ forall(S in H) value(S,open_box_out(OB,SU)) = --up ^ isolated({O1},{OB},H)} =>
holds(end(H), DC*(O1,open_box_inside(OB,SU)))]

A Box with a Lid

Definition Box.D9:

In situation S, OB is a box with lid OL and cavity PI and

place(PI,S) is an internal cavity of place(OB,S) union place(OL,S) but not an internal cavity of either OB or OL separately.
PI is associated with the box OB.

Declaration:
box_with_lid(OB,OL : object; PI : pseudo-object[region]) : fluent[boolean] --- Function.

Formalism:
holds(S,box_with_lid(OB,OL,PI)) < = >
source(PI)=OB ^ holds(S,cavity^*(PI, OB union^* OL)) ^
~holds(S,cavity^*(PI, OB)) ^ ~holds(S,cavity^*(PI, OL)) ^

Fact Box.F25

If OB,OL is a box with a lid with cavity PI, and O1 is inside PI at the start of history H and OB,OL form a box with a lid with essentially the same cavity throughout H, then O1 remains inside the box at the end of H. (Note that OB,OL can form a box-lid pair with more than one cavity, which is why the fact has to state that the same cavity is preserved throughout H.)

Characteristics: Kinematics.

Formalism:
[kinematic(H) ^ holds(start(H), box_with_lid(OB,OL,PI)) ^ holds(start(H), P^*(O1,PI)) ^
[forall (S in H) exists(PI1) holds(S,box_with_lid(OB,OL,PI1)) ^ holds(S,rcc_O^*(PI1,PI))]] => [forall (S in H) exists(PI1) holds(S,box_with_lid(OB,OL,PI1)) ^ holds(S, P^*(O1,PI1))].