Frantisek SILVÁŠI, Martin TOMÁŠEK
Extending lean cellular automata framework – boundary conditions and properties of canonical forms
Číslo: 1/2020
Periodikum: Acta Electrotechnica et Informatica
DOI: 10.15546/aeei-2020-0005
Klíčová slova: Cellular Automata, Formalization, Lean, Mechanization
Pro získání musíte mít účet v Citace PRO.
Anotace:
We present several extensions to our Lean–based formal mechanized framework for computing with cellular automata (CA). First we extend the definition of CAs to allow for specification of arbitrary boundary conditions. We use this addition to represent constant and periodic boundaries. We then formulate and prove numerous missing properties pertaining to canonical forms of cellular automata, culminating in a theorem stating that canonical forms preserve counts of nonempty cell states.