blob: 6da264cceb18a73aaf9751974248e066ce4441f3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; 0ℓ; suc)
module Data.System.Core {ℓ : Level} where
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Data.Circuit.Value using (Monoid)
open import Data.Nat using (ℕ)
open import Data.Setoid using (_⇒ₛ_; ∣_∣)
open import Data.Setoid.Unit using (⊤ₛ)
open import Data.Values Monoid using (Values; _≋_; module ≋; <ε>)
open import Function using (Func; _⟨$⟩_)
open import Function.Construct.Constant using () renaming (function to Const)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (_∙_)
open import Relation.Binary using (Setoid; Reflexive; Transitive)
open Func
-- A dynamical system with a set of states,
-- a state update function,
-- and a readout function
record System (n m : ℕ) : Set₁ where
field
S : Setoid 0ℓ 0ℓ
fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
fₒ : ∣ S ⇒ₛ Values m ∣
fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣
fₛ′ i = to (to fₛ i)
fₒ′ : ∣ S ∣ → ∣ Values m ∣
fₒ′ = to fₒ
module S = Setoid S
open System
-- the discrete system from n nodes to m nodes
discrete : (n m : ℕ) → System n m
discrete _ _ .S = ⊤ₛ
discrete n _ .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ)
discrete _ m .fₒ = Const ⊤ₛ (Values m) <ε>
module _ {n m : ℕ} where
-- Simulation of systems: a mapping of internal
-- states which respects i/o behavior
record _≤_ (A B : System n m) : Set ℓ where
private
module A = System A
module B = System B
field
⇒S : ∣ A.S ⇒ₛ B.S ∣
≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) B.S.≈ B.fₛ′ i (⇒S ⟨$⟩ s)
≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s)
infix 4 _≤_
open _≤_
open System
-- ≤ is reflexive: every system simulates itself
≤-refl : Reflexive _≤_
⇒S ≤-refl = Id _
≗-fₛ (≤-refl {x}) _ _ = S.refl x
≗-fₒ ≤-refl _ = ≋.refl
-- ≤ is transitive: if B simulates A, and C simulates B, then C simulates A
≤-trans : Transitive _≤_
⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a
≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin
⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩
⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩
fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values m) in begin
fₒ′ x s ≈⟨ ≗-fₒ a s ⟩
fₒ′ y (⇒S a ⟨$⟩ s) ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩
fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎
|
