~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Languages.v -rw-r--r-- 1.7 KiB View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
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
Require Import Unicode.Utf8_core.
Require Import Symbolic_Dynamics.Pattern_Sets.
Require Import Powerset.

Section Languages.

  Variable 𝕄 : Type.  (* the "time" domain, e.g. N^d or Z^d (d: nat) *)
  Variable 𝔸 : Set.  (* the alphabet, the space of the symbols,
                        the equality of symbols is proof-irrelevant *)

  Variable 𝛸 : Ensemble (pattern_structure 𝕄 𝔸).

  Import Patterns.

  Definition restriction'
             (U: Symbolic_Dynamics.Families.Family _)
             (x: pattern_structure 𝕄 𝔸):
    U  support 𝕄 𝔸 x -> pattern_structure 𝕄 𝔸.
  Proof.
    intro H. exact (Build_pattern_structure 𝕄 𝔸
                      _ (restriction _ _ H (pattern _ _ x))).
  Defined.

  Inductive language: Ensemble (pattern_structure 𝕄 𝔸) :=
    language_intro (𝑈 : Ensemble (Ensemble _)) :
       x, 𝛸 x ->  U, 𝑈 U ->  H: U  support _ _ x,
            language (restriction' U x H).

  Definition language_ := language_intro (Power_set _ (Full_set _)).

  (* TODO: definition of factorial closure; needed where? *)

  Variable 𝓕 : Ensemble (pattern_structure 𝕄 𝔸).
  Inductive language_avoid
            (𝑈 : Symbolic_Dynamics.Families.Family 𝕄):
    Ensemble (pattern_structure 𝕄 𝔸) :=
    language_avoid_intro (u: anchored_pattern 𝕄 𝔸 𝑈):
      ¬ subpattern' 𝕄 𝔸 𝓕 (Singleton_pattern_structure 𝕄 𝔸
                         (Build_pattern_structure 𝕄 𝔸 _ u))
      -> language_avoid 𝑈 (Build_pattern_structure 𝕄 𝔸 _ u).
  Definition language_avoid_: Ensemble _ :=
    fun x => exists U, Power_set _ (Full_set _) U /\ language_avoid U x.

End Languages.