Lax Lean Archive

Encoding data as lists of numbers

Lax185574.Encoding · concepts/Lax185574/Encoding.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A random access machine reads its input as a list of natural numbers and writes its output as one. An object is handed to an algorithm through an encoding, a map from its type to lists of numbers. The encodings in this submission follow one rule, with a few exceptions.

    • A natural number is the one-element list containing it.
    • A value of an inductive type is a constructor applied to some arguments. Its encoding is the number of the constructor (counting from 0 in the order of declaration), followed by the encodings of the arguments in order. If the type has only one constructor, the number is left out.

    Arguments that are proofs carry no information and are left out. So are the implicit arguments that the type of the value determines, such as the number of free variables of a formula.

    For example, the pair (3,true)(3, true) is encoded as 3,13, 1, since truetrue is the second constructor of BoolBool. An element ii of FinnFin n is a natural number together with a proof that it is less than nn, so it is encoded as ii.

    The exceptions are listed in Lax185574.EncodingsLax185574.Encodings. The main ones are lists and finite sets. A list is encoded by its length, followed by the encodings of its entries, so the list [7,8][7, 8] is encoded as 2,7,82, 7, 8. A finite set is encoded by the list of the encodings of its elements, in increasing order.

    Each such encoding is a prefix code. An algorithm that knows the type can read the encoding from the front, one constructor or one length at a time, without knowing where it ends. The encoding has length linear in the size of the value, and every number in it is a number of the value, the number of a constructor or the length of a list. Some of the other exceptions write further numbers, such as d + 1 for a finite value d of ℕ∞.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lean.Elab.Deriving.Basic
    2import Lean.Elab.Deriving.Util
    3import Mathlib.Data.Nat.Notation
    4
    5/-!
    6---
    7title: Encoding data as lists of numbers
    8type: definition
    9---
    10A random access machine reads its input as a list of natural numbers and
    11writes its output as one. An object is handed to an algorithm through an
    12*encoding*, a map from its type to lists of numbers. The encodings in
    13this submission follow one rule, with a few exceptions.
    14
    15* A natural number is the one-element list containing it.
    16* A value of an inductive type is a constructor applied to some
    17 arguments. Its encoding is the number of the constructor (counting
    18 from 0 in the order of declaration), followed by the encodings of the
    19 arguments in order. If the type has only one constructor, the number is
    20 left out.
    21
    22Arguments that are proofs carry no information and are left out. So are
    23the implicit arguments that the type of the value determines, such as
    24the number of free variables of a formula.
    25
    26For example, the pair `(3, true)` is encoded as `3, 1`, since `true` is
    27the second constructor of `Bool`. An element `i` of `Fin n` is a natural
    28number together with a proof that it is less than `n`, so it is encoded
    29as `i`.
    30
    31The exceptions are listed in `Lax185574.Encodings`. The main ones are
    32lists and finite sets. A list is encoded by its length, followed by the
    33encodings of its entries, so the list `[7, 8]` is encoded as `2, 7, 8`.
    34A finite set is encoded by the list of the encodings of its elements, in
    35increasing order.
    36
    37Each such encoding is a prefix code. An algorithm that knows the type
    38can read the encoding from the front, one constructor or one length at a
    39time, without knowing where it ends. The encoding has length linear in
    40the size of the value, and every number in it is a number of the value,
    41the number of a constructor or the length of a list. Some of the other
    42exceptions write further numbers, such as d + 1 for a finite value d of
    43ℕ∞.
    44
    45# Formalization notes
    46
    47The rule is the class `Encode` together with `deriving Encode`, a
    48deriving handler that writes the encoding function of an inductive type
    49from its declaration, by structural recursion. The handler is the
    50counterpart of Lean's own `deriving Hashable`, with the constructor number
    51and the encodings of the arguments in place of hashes. It supports
    52recursive types and indexed families. It rejects mutual and nested
    53inductive types, and it rejects an implicit argument that the type of the
    54constructor does not determine, since leaving such an argument out could
    55lose information. Natural numbers are the only base case. They are an
    56inductive type too, but their derived encoding would be unary, so their
    57instance is written by hand.
    58
    59Lists are an inductive type as well. Their derived encoding would mark
    60every entry with the number of `cons`. The length in front is the usual
    61convention, and it lets an algorithm skip a list, or find its end,
    62without reading its entries.
    63
    64Types whose values are not built from constructors, such as graphs given
    65by an adjacency relation, are encoded through an explicit representation
    66by an encodable type, as the graphs of `Lax185574.Encodings`.
    67
    68The size of a value, in bounds on running times and on outputs, is the
    69length of its encoding, `wordLength`.
    70
    71No decoding function is part of the definition. A statement about an
    72algorithm only fixes what it reads and what it must write, and these are
    73determined by the encoding alone.
    74-/
    75
    76namespace Lax185574.Encoding
    77
    78universe u
    79
    80/-- An encoding of the values of `α` as lists of natural numbers. -/
    81class Encode (α : Type u) where
    82 /-- The list of numbers encoding a value. -/
    83 encode : α → List ℕ
    84
    85export Encode (encode)
    86
    87/-- The size `‖a‖` of a value, as used in running-time bounds: the
    88length of its encoding. -/
    89def wordLength {α : Type u} [Encode α] (a : α) : ℕ := (encode a).length
    90
    91/-- A natural number is encoded as itself. -/
    92instance : Encode ℕ where
    93 encode n := [n]
    94
    95section Deriving
    96
    97open Lean Elab Command Meta Term Deriving
    98open Lean.Parser.Term
    99
    100/-- The match expression of the derived encoding function: one
    101alternative per constructor, whose right-hand side is the constructor
    102number (if there are several constructors) followed by the encodings of
    103the explicit arguments that are not proofs. Recursive arguments are
    104encoded by a recursive call. -/
    105def mkEncodeMatch (ctx : Deriving.Context) (header : Header) (indVal : InductiveVal) :
    106 TermElabM Term := do
    107 let discrs ← mkDiscrs header indVal
    108 if indVal.ctors.isEmpty then
    109 return ← `(nomatch $(mkIdent header.targetNames[0]!):ident)
    110 let mut alts : Array (TSyntax ``matchAlt) := #[]
    111 for ctorName in indVal.ctors, ctorIdx in [0:indVal.ctors.length] do
    112 let ctorInfo ← getConstInfoCtor ctorName
    113 let alt : TSyntax ``matchAlt ← forallTelescopeReducing ctorInfo.type fun xs resultType => do
    114 let mut patterns : Array Term := #[]
    115 for _ in [0:indVal.numIndices] do
    116 patterns := patterns.push (← `(_))
    117 let mut ctorArgs : Array Term := #[]
    118 for _ in [0:indVal.numParams] do
    119 ctorArgs := ctorArgs.push (← `(_))
    120 let mut parts : Array Term := #[]
    121 if indVal.ctors.length > 1 then
    122 parts := parts.push (← `([$(quote ctorIdx)]))
    123 for i in [0:ctorInfo.numFields] do
    124 let x := xs[indVal.numParams + i]!
    125 let a := mkIdent (← mkFreshUserName `a)
    126 ctorArgs := ctorArgs.push a
    127 let decl ← x.fvarId!.getDecl
    128 let xTy ← whnf decl.type
    129 if ← isProp decl.type then
    130 continue
    131 unless decl.binderInfo.isExplicit do
    132 unless resultType.containsFVar x.fvarId! do
    133 throwError "deriving Encode: the implicit argument {decl.userName} of \
    134 {ctorName} is not determined by the type of the constructor"
    135 continue
    136 match xTy.getAppFn with
    137 | .const declName .. =>
    138 if declName == indVal.name then
    139 parts := parts.push (← `($(mkIdent ctx.auxFunNames[0]!) $a:ident))
    140 else
    141 parts := parts.push (← `(Encode.encode $a:ident))
    142 | _ => parts := parts.push (← `(Encode.encode $a:ident))
    143 patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
    144 let rhs : Term ← if parts.isEmpty then `(([] : List Nat))
    145 else parts[1:].foldlM (fun acc p => `($acc ++ $p)) parts[0]!
    146 `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
    147 alts := alts.push alt
    148 `(match $[$discrs],* with $alts:matchAlt*)
    149
    150/-- The commands defining the encoding function of the inductive type
    151`declName` and its `Encode` instance. -/
    152def mkEncodeInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
    153 let ctx ← mkContext ``Encode "encode" declName
    154 if ctx.usePartial then
    155 throwError "deriving Encode: mutual and nested inductive types are not supported"
    156 let indVal := ctx.typeInfos[0]!
    157 let header ← mkHeader ``Encode 1 indVal
    158 let body ← mkEncodeMatch ctx header indVal
    159 let fn ← `(def $(mkIdent ctx.auxFunNames[0]!):ident $(header.binders):bracketedBinder* :
    160 List Nat := $body:term)
    161 return #[fn] ++ (← mkInstanceCmds ctx ``Encode #[declName])
    162
    163/-- The deriving handler for `Encode`. -/
    164def mkEncodeHandler (declNames : Array Name) : CommandElabM Bool := do
    165 unless ← declNames.allM isInductive do
    166 return false
    167 for declName in declNames do
    168 let cmds ← liftTermElabM <| mkEncodeInstanceCmds declName
    169 cmds.forM elabCommand
    170 return true
    171
    172initialize registerDerivingHandler ``Encode mkEncodeHandler
    173
    174end Deriving
    175
    176end Lax185574.Encoding
    177
    Formalization notes

    The rule is the class EncodeEncode together with derivingEncodederiving Encode, a deriving handler that writes the encoding function of an inductive type from its declaration, by structural recursion. The handler is the counterpart of Lean's own derivingHashablederiving Hashable, with the constructor number and the encodings of the arguments in place of hashes. It supports recursive types and indexed families. It rejects mutual and nested inductive types, and it rejects an implicit argument that the type of the constructor does not determine, since leaving such an argument out could lose information. Natural numbers are the only base case. They are an inductive type too, but their derived encoding would be unary, so their instance is written by hand.

    Lists are an inductive type as well. Their derived encoding would mark every entry with the number of conscons. The length in front is the usual convention, and it lets an algorithm skip a list, or find its end, without reading its entries.

    Types whose values are not built from constructors, such as graphs given by an adjacency relation, are encoded through an explicit representation by an encodable type, as the graphs of Lax185574.EncodingsLax185574.Encodings.

    The size of a value, in bounds on running times and on outputs, is the length of its encoding, wordLengthwordLength.

    No decoding function is part of the definition. A statement about an algorithm only fixes what it reads and what it must write, and these are determined by the encoding alone.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…