Commits

ppavel  committed bc0a2f7

Формулировка аксиоматики

  • Participants

Comments (0)

Files changed (5)

File EventAlgebra.agda

+open import Level
+open import Algebra
+module EventAlgebra (algebra : BooleanAlgebra zero zero) where
+  open import Relation.Binary
+  module BA = BooleanAlgebra algebra  renaming (
+       Carrier to Event ;
+       ⊤ to Ω ;
+       ⊥ to ∅ ;
+       _∧_ to _∩_ ; 
+       _∨_ to _∪_ ; 
+       ¬_ to ∁_)
+  open BA public
+  import Algebra.Props.BooleanAlgebra as B
+  import Algebra.FunctionProperties as FP
+  open import Algebra.Structures
+  open FP _≈_
+  abstract
+    _∖_ : Op₂ Event
+    a ∖ b = a ∩ ∁ b
+    
+--    _⊆_ : Rel Event zero
+--    e₁ ⊆ e₂ = {!!}
+
+  _disj_ : Rel Event zero
+  e₁ disj e₂ = e₁ ∩ e₂ ≈ ∅
+
+  ∪-monoid : Monoid zero zero
+  ∪-monoid = record { -- TODO заиспользовать имеющийся моноид
+      Carrier = Event; _≈_ = _≈_; _∙_ = _∪_; ε = ∅; 
+      isMonoid = IsCommutativeSemiring.+-isMonoid (B.∨-∧-isCommutativeSemiring algebra) }
+
+ 

File FinAdditives.agda

+open import Algebra
+module FinAdditives {ℓ₁ ℓ₂} (m : Monoid ℓ₁ ℓ₂)  where
+open import Data.List hiding (sum)
+open Monoid m
+abstract
+  sum : List Carrier → Carrier
+  sum = foldl _∙_  ε

File Numbers.agda

+open import Algebra
+module Numbers  where
+open import Level
+open import Relation.Binary
+record Nums  : Set₁ where
+  field
+    commRing : CommutativeRing zero zero
+  module CR = CommutativeRing commRing hiding (zero) renaming (Carrier to Num)
+  open CR
+  field
+    _≤_ : Rel Num _
+    partialOrder : IsTotalOrder _≈_ _≤_
+  module TO = IsTotalOrder partialOrder hiding (isEquivalence ; refl ; reflexive ; trans) 
+  open TO
+  0≤_ : Num → Set 
+  0≤_ n = 0# ≤ n
+  field
+    0≤b→a≤a+b : ∀ a → ∀{b} → 0≤ b → a ≤ (a + b)
+    0≤1 : 0≤ 1#
+
+  open TO public
+  open CR public

File OrderedBooleanAlgebra.agda

+open import Level
+open import Algebra
+module OrderedBooleanAlgebra (algebra : BooleanAlgebra zero zero) where
+  open import Relation.Binary
+  open BooleanAlgebra algebra public renaming (
+       Carrier to Event ;
+       ⊤ to Ω ;
+       ⊥ to ∅ ;
+       _∧_ to _∩_ ; 
+       _∨_ to _∪_)
+  import Algebra.Props.BooleanAlgebra as B
+  open B algebra 
+  open Poset poset public hiding (_≈_ ; isEquivalence ; refl ; reflexive ; trans) renaming (_≤_ to _⊆_) 
+ 

File Probability.agda

+import EventAlgebra
+open import Numbers 
+module Probability (nums : Nums) (ba : _) where
+open module EA = EventAlgebra ba hiding (_≈_)
+open Nums nums hiding (_≈_)
+import FinAdditives as FA
+open FA +-monoid renaming (sum to Σ_)
+open FA ∪-monoid renaming (sum to ∪_)
+import Algebra.Structures
+
+open import Relation.Binary
+open Setoid {{...}} public
+
+open import Data.List
+open import Algebra
+
+data Disjoint : List Event → Set where
+  [] : Disjoint []
+  _∷_ : ∀ {e l} → e disj (∪ l) → Disjoint l → Disjoint (e ∷ l)
+
+record Axioms : Set where
+  field
+    P : Event → Num
+    a₁ : ∀ e → 0≤ P e
+    a₂ : P Ω ≈ 1#
+    a₃ : ∀{l} → Disjoint l → P (∪ l) ≈ Σ (map P l)
+     
+-- e₁⊆e₂→Pe₁≤Pe₂ : ∀ {e₁ e₂ } → e₁ ⊆ e₂ → P e₁ ≤ P e₂
+-- e₁⊆e₂→Pe₁≤Pe₂ = {!-m!}