Encodings of fixed finite types

A finite type is encoded by unary ranks in one fixed enumeration. The enumeration and its size are independent of the runtime input; this does not give a uniform algorithm for growing types. Concrete finite types with a FinEnum instance use Turing.MultiTapeTM.encFinEnum, which is computable; generic [Finite α] parameters use Turing.MultiTapeTM.encFinite.

Main definitions

• Turing.MultiTapeTM.encFinEnum: computable unary ranks for a constructively enumerated finite type.
• Turing.MultiTapeTM.encFinite: unary ranks for a fixed finite type.

Main results

• Turing.MultiTapeTM.length_encFinEnum_lt: the cardinality bounds every constructively encoded rank.
• Turing.MultiTapeTM.length_encFinite_lt: the cardinality bounds every encoded rank.

References

Adapts Computability/Probabilistic/Finite.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing unary encoding.

@[instance_reducible]

instance Turing.MultiTapeTM.instFinEnumBool : FinEnum Bool

Concrete bit enumeration.

def Turing.MultiTapeTM.encFinEnum (α : Type) [FinEnum α] : α ↪ List Bool

Encode a constructively enumerated finite type by unary ranks.

theorem Turing.MultiTapeTM.length_encFinEnum_lt {α : Type} [FinEnum α] (a : α) : ((encFinEnum α) a).length < Nat.card α

Every constructively encoded finite tag has length less than the fixed domain's cardinality.

noncomputable def Turing.MultiTapeTM.encFinite (α : Type) [Finite α] : α ↪ List Bool

Encode a fixed finite type by unary ranks in an enumeration chosen once.

theorem Turing.MultiTapeTM.length_encFinite_lt {α : Type} [Finite α] (a : α) : ((encFinite α) a).length < Nat.card α

Every encoded finite tag has length less than the fixed domain's cardinality.