type: definition
verification: machine_ready
dependencies: ["D1-1-formal.md"]
verification_points:
- encoding_injectivity
- prefix_freedom
- self_embedding
- encoding_closure
BinaryRepresentation(S : System) : Prop ≡
∃Encode : Function[System → {0,1}*] .
Injective(Encode) ∧
PrefixFree(Encode) ∧
SelfEmbedding(Encode) ∧
Closed(Encode)
Injective(Encode : Function[System → {0,1}*]) : Prop ≡
∀s₁, s₂ : Element . s₁ ∈ S ∧ s₂ ∈ S ∧ s₁ ≠ s₂ →
Encode(s₁) ≠ Encode(s₂)
PrefixFree(Encode : Function[System → {0,1}*]) : Prop ≡
∀s₁, s₂ : Element . s₁ ∈ S ∧ s₂ ∈ S ∧ s₁ ≠ s₂ →
¬IsPrefix(Encode(s₁), Encode(s₂))
SelfEmbedding(Encode : Function[System → {0,1}*]) : Prop ≡
Encode ∈ Domain(Encode) ∧
Encode(Encode) ∈ Range(Encode)
Closed(Encode : Function[System → {0,1}*]) : Prop ≡
∀s : Element . s ∈ S →
Encode(s) ∈ {0,1}* ∧
Encode(s) ⊆ S
Type BinaryString := List[Bit]
Type Bit := {0, 1}
Type Encoding := System → BinaryString
IsPrefix(x : BinaryString, y : BinaryString) : Bool ≡
∃z : BinaryString . y = x ++ z
DecodingExists(Encode : Encoding) : Prop ≡
∃Decode : Function[BinaryString → System] .
∀s ∈ S . Decode(Encode(s)) = s
Notation: BinRep(S) := BinaryRepresentation(S)
Notation: {0,1}* := Set of all finite binary strings
Notation: |s| := length of string s
Notation: ε := empty string
def verify_injectivity(encode_func, system):
return all_encodings_unique(encode_func, system)
def verify_prefix_freedom(encode_func, system):
return no_encoding_is_prefix_of_another(encode_func, system)
def verify_self_embedding(encode_func):
return can_encode_itself(encode_func)
def verify_closure(encode_func, system):
return all_encodings_are_binary_strings(encode_func, system)