Documentation

Complexitylib.Models.RoseTreeMachine.DataEncode

Encodings into Data #

This file defines the class that is used to encode arbitrary data structures into Data, so that RTMs (rose tree machines) can operate on them.

Instances are provided for convenience for Data itself, Bool, List α, Option α, α × β, and ℕ (binary encoding via List Bool)

source
class Complexity.RoseTreeMachine.DataEncode (α : Type) :
Type

Encoding of types into Data.

  • encode : α → Data

    Encode a value of α as Data.

  • h_inj : Function.Injective encode

    The encoding is injective, so distinct values never collide.

Instances
    source
    @[implicit_reducible]
    instance Complexity.RoseTreeMachine.instDataEncodeData :
    DataEncode Data
    Equations
    source
    @[simp]
    theorem Complexity.RoseTreeMachine.DataEncode_encode_data (d : Data) :
    DataEncode.encode d = d
    source
    @[implicit_reducible]
    instance Complexity.RoseTreeMachine.instDataEncodeBool :
    DataEncode Bool
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implicit_reducible]
    instance Complexity.RoseTreeMachine.instDataEncodeList (α : Type) [DataEncode α] :
    DataEncode (List α)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[simp]
    theorem Complexity.RoseTreeMachine.DataEncode_list_nil {α : Type} [DataEncode α] :
    DataEncode.encode [] = Data.l []
    source
    @[simp]
    theorem Complexity.RoseTreeMachine.DataEncode_list_eq_nil_iff_nil {α : Type} [DataEncode α] (xs : List α) :
    DataEncode.encode xs = Data.empty ↔ xs = []
    source
    @[simp]
    theorem Complexity.RoseTreeMachine.DataEncode_list_tail {α : Type} [DataEncode α] (xs : List α) :
    (DataEncode.encode xs).asList.tail = (DataEncode.encode xs.tail).asList
    source
    @[implicit_reducible]
    instance Complexity.RoseTreeMachine.instDataEncodeOption (α : Type) [DataEncode α] :
    DataEncode (Option α)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[simp]
    theorem Complexity.RoseTreeMachine.DataEncode_Option_empty {α : Type} [DataEncode α] (x : Option α) :
    (DataEncode.encode x == Data.empty) = x.isNone
    source
    @[implicit_reducible]
    instance Complexity.RoseTreeMachine.instDataEncodeProd (α β : Type) [DataEncode α] [DataEncode β] :
    DataEncode (α × β)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem Complexity.RoseTreeMachine.DataEncode_pair {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) :
    DataEncode.encode (a, b) = Data.l [DataEncode.encode a, DataEncode.encode b]
    source
    @[implicit_reducible]
    instance Complexity.RoseTreeMachine.instDataEncodeNat :
    DataEncode ℕ
    Equations