------------------------------------------------------------------------ -- Some algebraic properties ------------------------------------------------------------------------ module AlgebraicProperties where open import Syntax open import Semantics.BigStep open import Equivalence open import StatusLemmas open import Totality open import Relation.Nullary open import Data.Product open import Algebra import Algebra.FunctionProperties as AlgProp private open module AP (t : Totality) = AlgProp (≈-setoid t) open import Relation.Binary.PropositionalEquality open import Data.Nat open import Data.Nat.Properties as ℕ open import Data.Empty ------------------------------------------------------------------------ -- A lemma cast : ∀ {n₁ n₂ i t} {x : Expr t} → n₁ ≡ n₂ → x ⇓[ i ] nat n₁ → x ⇓[ i ] nat n₂ cast ≡-refl x = x ------------------------------------------------------------------------ -- Associativity -- These properties show that the fixity declarations make sense. -- _⊕_ is associative. ⊕-assoc : ∀ {t} → Associative t _⊕_ ⊕-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑ where assoc = CommutativeSemiring.+-assoc ℕ.commutativeSemiring ⟶⇓ : (x ⊕ y) ⊕ z ⊑⇓ x ⊕ (y ⊕ z) ⟶⇓ Int = Int ⟶⇓ (Add₃ (Add₁ x y) z) = Add₃ x (Add₃ y z) ⟶⇓ (Add₂ Int) = Int ⟶⇓ (Add₂ (Add₃ x y)) = Add₃ x (Add₂ y) ⟶⇓ (Add₂ (Add₂ x)) = Add₂ x ⟶⇓ {i = i} (Add₁ {n = n₃} (Add₁ {m = n₁} {n = n₂} x⇓ y⇓) z⇓) = cast (≡-sym (assoc n₁ n₂ n₃)) (Add₁ x⇓ (Add₁ y⇓ z⇓)) ⟵⇓ : x ⊕ (y ⊕ z) ⊑⇓ (x ⊕ y) ⊕ z ⟵⇓ Int = Int ⟵⇓ (Add₃ x Int) = Int ⟵⇓ (Add₃ x (Add₂ y)) = Add₂ (Add₃ x y) ⟵⇓ (Add₃ x (Add₃ y z)) = Add₃ (Add₁ x y) z ⟵⇓ (Add₂ x) = Add₂ (Add₂ x) ⟵⇓ {i = i} (Add₁ {m = n₁} x⇓ (Add₁ {m = n₂} {n = n₃} y⇓ z⇓)) = cast (assoc n₁ n₂ n₃) (Add₁ (Add₁ x⇓ y⇓) z⇓) ⟶⇑ : (x ⊕ y) ⊕ z ⊑⇑ x ⊕ (y ⊕ z) ⟶⇑ (Add₁ (Add₁ x⇑)) = Add₁ x⇑ ⟶⇑ (Add₁ (Add₂ x↡ y⇑)) = Add₂ x↡ (Add₁ y⇑) ⟶⇑ (Add₂ (._ , Add₁ x↡ y↡) z⇑) = Add₂ (_ , x↡) (Add₂ (_ , y↡) z⇑) ⟵⇑ : x ⊕ (y ⊕ z) ⊑⇑ (x ⊕ y) ⊕ z ⟵⇑ (Add₁ x⇑) = Add₁ (Add₁ x⇑) ⟵⇑ (Add₂ x↡ (Add₁ y⇑)) = Add₁ (Add₂ x↡ y⇑) ⟵⇑ (Add₂ x↡ (Add₂ y↡ z⇑)) = Add₂ (zip-Σ _+_ Add₁ x↡ y↡) z⇑ -- _catch_ is "left associative". catch-assocˡ : ∀ {t} (x y z : Expr t) → x catch (y catch z) ⊑ (x catch y) catch z catch-assocˡ x y z = record { ⇓ = ⇓; ⇑ = ⇑ } where ⇓ : x catch (y catch z) ⊑⇓ (x catch y) catch z ⇓ (Catch₁ x⇓) = Catch₁ (Catch₁ x⇓) ⇓ (Catch₂ x↯ (Catch₁ y⇓)) = Catch₁ (Catch₂ x↯ y⇓) ⇓ (Catch₂ x↯ (Catch₂ y↯ z)) = Catch₂ (Catch₂ x↯ y↯) z ⇓ Int = Int ⇑ : x catch (y catch z) ⊑⇑ (x catch y) catch z ⇑ (Catch₁ x⇑) = Catch₁ (Catch₁ x⇑) ⇑ (Catch₂ x↯ (Catch₁ y⇑)) = Catch₁ (Catch₂ x↯ y⇑) ⇑ (Catch₂ x↯ (Catch₂ y↯ z⇑)) = Catch₂ (Catch₂ x↯ y↯) z⇑ -- _catch_ is not associative. ¬catch-assoc : ∀ {t} → ¬ Associative t _catch_ ¬catch-assoc assoc with _⊑_.⇓ (_≈_.⊑ (assoc ⌜ throw ⌝ ⌜ nat 0 ⌝ ⌜ nat 1 ⌝)) {i = U} (Catch₂ Int Val) ¬catch-assoc assoc | Catch₁ () ¬catch-assoc assoc | Catch₂ x↯ (Catch₁ ()) ¬catch-assoc assoc | Catch₂ x↯ (Catch₂ () y⇓) -- _>>_ is associative. >>-assoc : ∀ {t} → Associative t _>>_ >>-assoc x y z = is-≈ ⟶⇓ ⟵⇓ ⟶⇑ ⟵⇑ where ⟶⇓ : (x >> y) >> z ⊑⇓ x >> (y >> z) ⟶⇓ (Seqn₁ (Seqn₁ x⇓ y⇓) z) = Seqn₁ x⇓ (Seqn₁ y⇓ z) ⟶⇓ (Seqn₂ (Seqn₁ x⇓ y↯)) = Seqn₁ x⇓ (Seqn₂ y↯) ⟶⇓ (Seqn₂ (Seqn₂ x↯)) = Seqn₂ x↯ ⟶⇓ (Seqn₂ Int) = Int ⟶⇓ Int = Int ⟵⇓ : x >> (y >> z) ⊑⇓ (x >> y) >> z ⟵⇓ (Seqn₁ x⇓ (Seqn₁ y⇓ z)) = Seqn₁ (Seqn₁ x⇓ y⇓) z ⟵⇓ (Seqn₁ x⇓ (Seqn₂ y↯)) = Seqn₂ (Seqn₁ x⇓ y↯) ⟵⇓ (Seqn₁ x↯ Int) = Int ⟵⇓ (Seqn₂ x↯) = Seqn₂ (Seqn₂ x↯) ⟵⇓ Int = Int ⟶⇑ : (x >> y) >> z ⊑⇑ x >> (y >> z) ⟶⇑ (Seqn₁ (Seqn₁ x⇑)) = Seqn₁ x⇑ ⟶⇑ (Seqn₁ (Seqn₂ x↡ y⇑)) = Seqn₂ x↡ (Seqn₁ y⇑) ⟶⇑ (Seqn₂ (_ , Seqn₁ x↡ y↡) z⇑) = Seqn₂ (_ , x↡) (Seqn₂ (_ , y↡) z⇑) ⟵⇑ : x >> (y >> z) ⊑⇑ (x >> y) >> z ⟵⇑ (Seqn₁ x⇑) = Seqn₁ (Seqn₁ x⇑) ⟵⇑ (Seqn₂ x↡ (Seqn₁ y⇑)) = Seqn₁ (Seqn₂ x↡ y⇑) ⟵⇑ (Seqn₂ x↡ (Seqn₂ y↡ z⇑)) = Seqn₂ (zip-Σ (λ u v → v) Seqn₁ x↡ y↡) z⇑ -- _finally_ is "right associative". finally-assocʳ : ∀ {t} (x y z : Expr t) → (x finally y) finally z ⊑ x finally (y finally z) finally-assocʳ x y z = record { ⇓ = ⇓; ⇑ = ⇑ } where ⇓ : (x finally y) finally z ⊑⇓ x finally (y finally z) ⇓ Int = Int ⇓ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↡)))) z⇒)) = Block (Seqn₁ (Catch₁ x↡) (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇓ y↡))) z⇒))) ⇓ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _)) ⇓ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)) ⇓ (Block (Seqn₂ (Catch₂ _ z↯))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ (Block (Seqn₂ (Catch₂ (Unblock Int) z↯)))))) ⇑ : (x finally y) finally z ⊑⇑ x finally (y finally z) ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x⇑))))))) = Block (Seqn₁ (Catch₁ x⇑)) ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ x↯ (Seqn₁ y⇑)))))))) = Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇑ y⇑)))))))) ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ())))))))) ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₂ (_ , Catch₁ x↡) y⇑)))))) = Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₁ (Catch₁ (Unblock (Bto·⇑ y⇑)))))) ⇑ (Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₂ (_ , Catch₂ _ (Seqn₁ _ ())) _)))))) ⇑ (Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ z⇑)))) = Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ (Block (Seqn₁ (Catch₂ (Unblock Int) (Seqn₁ z⇑))))))) ⇑ (Block (Seqn₁ (Catch₂ _ (Seqn₂ _ ())))) ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↯))) (Seqn₁ z⇑)))) = Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₁ (Catch₂ (Unblock (Bto·⇓ y↯)) (Seqn₁ z⇑))))) ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _))) _))) ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₂ (Catch₂ x↯ (Seqn₁ y↡ _))))) (Seqn₁ z⇑)))) = Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₂ (_ , Catch₁ (Unblock (Bto·⇓ y↡))) z⇑))))) ⇑ (Block (Seqn₁ (Catch₂ (Unblock (Block (Seqn₂ (Catch₂ x↯ (Seqn₂ y↯))))) (Seqn₁ z⇑)))) = Block (Seqn₁ (Catch₂ x↯ (Seqn₁ (Block (Seqn₁ (Catch₂ (Unblock (Bto·⇓ y↯)) (Seqn₁ z⇑))))))) ⇑ (Block (Seqn₂ (_ , Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x↡) y↡)))) z⇑)) = Block (Seqn₂ (_ , Catch₁ x↡) (Block (Seqn₂ (_ , Catch₁ (Unblock (Bto·⇓ y↡))) z⇑))) ⇑ (Block (Seqn₂ (_ , Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _)) ⇑ (Block (Seqn₂ (_ , Catch₂ _ (Seqn₁ _ ())) _)) -- In a partial setting _finally_ is not associative (c.f. -- StatusLemmas.¬UtoB'). ¬finally-assoc : ¬ Associative partial _finally_ ¬finally-assoc assoc with _⊑_.⇓ (_≈_.⊒ (assoc ⌜ nat 0 ⌝ (loop ⌜ nat 0 ⌝ catch ⌜ nat 0 ⌝) ⌜ nat 0 ⌝)) {i = U} (Block (Seqn₁ (Catch₁ (Unblock Val)) (Block (Seqn₁ (Catch₁ (Unblock (Catch₂ Int Val))) Val)))) ... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₁ ↡))))) Val) = loop-¬⇓ nat-¬↯ (, ↡) ... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₂ ↯ _))))) Val) = loop-¬⇓ nat-¬↯ (, ↯) ... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) _) ... | Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _) -- In a total setting _finally_ is associative. finally-assoc : Associative total _finally_ finally-assoc x y z = record { ⊑ = finally-assocʳ x y z ; ⊒ = record { ⇓ = ⟵⇓; ⇑ = ⟵⇑ } } where ⟵⇓ : x finally (y finally z) ⊑⇓ (x finally y) finally z ⟵⇓ Int = Int ⟵⇓ (Block (Seqn₁ (Catch₁ x) (Block (Seqn₁ (Catch₁ (Unblock y)) z)))) = Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ x) y')))) z) where y' = proj₂ (Uto·' (_ , y)) ⟵⇓ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)))) ⟵⇓ (Block (Seqn₁ (Catch₁ _) (Block (Seqn₂ (Catch₂ _ z↯))))) = Block (Seqn₂ (Catch₂ (Unblock Int) z↯)) ⟵⇓ (Block (Seqn₁ (Catch₂ _ (Seqn₁ _ ())) _)) ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₁ (Block (Seqn₁ _ z)) _)))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₁ z Val))) ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₁ _ z)))))) = Block (Seqn₂ (Catch₂ (Unblock Int) (Seqn₂ z))) ⟵⇓ (Block (Seqn₂ (Catch₂ _ (Seqn₂ (Block (Seqn₂ (Catch₂ _ z↯))))))) = Block (Seqn₂ (Catch₂ (Unblock Int) z↯)) ⟵⇑ : x finally (y finally z) ⊑⇑ (x finally y) finally z ⟵⇑ ⇑ = ⊥-elim (¬undefined _ ⇑) ------------------------------------------------------------------------ -- Commutativity -- _⊕_ is commutative if the language is total. ⊕-comm : Commutative total _⊕_ ⊕-comm x y = is-≈ (⟶⇓ _) (⟶⇓ _) ⟶⇑ ⟶⇑ where comm = CommutativeSemiring.+-comm ℕ.commutativeSemiring ⟶⇓ : ∀ {x} y → x ⊕ y ⊑⇓ y ⊕ x ⟶⇓ _ Int = Int ⟶⇓ _ (Add₃ x⇓ y↯) = Add₂ y↯ ⟶⇓ y {i = i} (Add₂ x↯) with defined y i ⟶⇓ _ (Add₂ x↯) | (nat _ , y⇓) = Add₃ y⇓ x↯ ⟶⇓ _ (Add₂ x↯) | (throw , y↯) = Add₂ y↯ ⟶⇓ _ (Add₁ {m = m} {n = n} x⇓ y⇓) = cast (≡-sym (comm m n)) (Add₁ y⇓ x⇓) ⟶⇑ : {x y : Expr total} → x ⊕ y ⊑⇑ y ⊕ x ⟶⇑ ⇑ = ⊥-elim (¬undefined _ ⇑) -- _⊕_ is not commutative if the language is partial. ¬⊕-comm : ¬ Commutative partial _⊕_ ¬⊕-comm ⊕-comm with _⊑_.⇓ (_≈_.⊑ (⊕-comm ⌜ throw ⌝ (loop ⌜ nat 0 ⌝))) {i = B} (Add₂ Val) ... | Add₂ ↡ = loop-¬⇓ nat-¬↯ (, ↡) ... | Add₃ ↯ _ = loop-¬⇓ nat-¬↯ (, ↯)