4 CHAPTER 1.AN OVERVIEW laws,the fact that emp is a neutral element,and various distributive and semidistributive laws: p1*P2台P2*P (P1*p2)*内台P1*(P2*P3) p*emp台p (P1 V p2)*(p q)v (p2 q) (p1Ap2）*9÷(P1*q)A(P2*q (目z.p)*P2÷3r.(p1*p2)when x not free in p2 (.ph)*p2→z.(p1*h)when x not free in p2 There is also an inference rule showing that separating conjunction is mono- tone with respect to implication: pm→24→2 (monotonicity） P1*91→P2*92 and two further rules capturing the adjunctive relationship between separat- ing conjunction and separating implication: P1*P2→P内 p1→(p2*) (currying) (decurrying) p1→(P2*p) D1*2→p3· On the other hand,there are two rules that one might expect to hold for an operation called "conjunction"that in fact fail: (Contraction-unsound) p*q→p (Weakening-unsound) A counterexample to both of thes to be x1 and g to be y→2；then p holds for a certain single-field heap while p *p holds for no heap,and p *q holds for a certain two-field heap while p holds for no two-field heap.(Thus separation logic is a substructural logic.) 14 CHAPTER 1. AN OVERVIEW laws, the fact that emp is a neutral element, and various distributive and semidistributive laws: p1 ∗ p2 ⇔ p2 ∗ p1 (p1 ∗ p2) ∗ p3 ⇔ p1 ∗ (p2 ∗ p3) p ∗ emp ⇔ p (p1 ∨ p2) ∗ q ⇔ (p1 ∗ q) ∨ (p2 ∗ q) (p1 ∧ p2) ∗ q ⇒ (p1 ∗ q) ∧ (p2 ∗ q) (∃x. p1) ∗ p2 ⇔ ∃x. (p1 ∗ p2) when x not free in p2 (∀x. p1) ∗ p2 ⇒ ∀x. (p1 ∗ p2) when x not free in p2 There is also an inference rule showing that separating conjunction is mono￾tone with respect to implication: p1 ⇒ p2 q1 ⇒ q2 p1 ∗ q1 ⇒ p2 ∗ q2 (monotonicity) and two further rules capturing the adjunctive relationship between separat￾ing conjunction and separating implication: p1 ∗ p2 ⇒ p3 p1 ⇒ (p2 −∗ p3) (currying) p1 ⇒ (p2 −∗ p3) p1 ∗ p2 ⇒ p3. (decurrying) On the other hand, there are two rules that one might expect to hold for an operation called “conjunction” that in fact fail: p ⇒ p ∗ p (Contraction — unsound) p ∗ q ⇒ p (Weakening — unsound) A counterexample to both of these axiom schemata is provided by taking p to be x 7→ 1 and q to be y 7→ 2; then p holds for a certain single-field heap while p ∗ p holds for no heap, and p ∗ q holds for a certain two-field heap while p holds for no two-field heap. (Thus separation logic is a substructural logic.)