How inputs are given to algorithms

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

definition

Loading review…

Natural Language Statement

Definition

The encodings of all values that algorithms in this submission read or write. Except for lists, functions on $Fin n$ , finite sets, graphs and the values of ℕ∞, they are given by the rule of $Lax185574.Encoding$ . Encodings of further types, such as partial graphs and type trees, are given next to their definitions.

type	value	encoding
$Bool$	$false$ , $true$	$0$ , $1$
$Fin n$	$i$	$i$
$α × β$	$(a, b)$	encoding of $a$ , then of $b$
$α ⊕ β$	$inl a$ , $inr b$	$0$ , encoding of $a$ , and $1$ , encoding of $b$
$Option α$	$none$ , $some a$	$0$ , and $1$ , encoding of $a$
$ℤ$	$m ≥ 0$ , $-(m + 1)$	$0, m$ , and $1, m$
$ℚ$	$p / q$ in lowest terms, $q > 0$	$p$ as an integer, then $q$
$ℕ∞$	$d$ , $∞$	$d + 1$ , and $0$
$Empty$	(no values)
$List α$	$[a₁, …, aₘ]$	$m$ , then the encodings of $a₁$ , …, $aₘ$
$Fin n → α$	$f$	the list $[f 0, …, f (n - 1)]$
$Finset α$	$S$	the list of the encodings of the elements of $S$ , in increasing order

The encodings of the elements of a finite set are lists of numbers, and they are compared lexicographically. As a list of lists, the encoding of a set gives the length of each element's encoding in front of it.

A first-order formula is written in prefix (Polish) notation, with one number per connective.

formula	encoding
xᵢ adjacent to xⱼ	$0, i, j$
xᵢ = xⱼ	$1, i, j$
¬φ	$2$ , encoding of φ
φ ∧ ψ	$3$ , encoding of φ, encoding of ψ
∃xₙ φ	$4$ , encoding of φ
xᵢ has color c	$5$ , encoding of $c$ , $i$

The first-order formulas $Lax3.FirstOrder.FO$ of the archive, which have no colors, are encoded in the same way, $0, i, j$ for adjacency, $1, i, j$ for equality, and $2$ , $3$ , $4$ for negation, conjunction and the quantifier.

A graph with n vertices is encoded by the family of the neighborhoods of its vertices 0, 1, …, n − 1, each a finite set of vertices. So the encoding starts with n, followed for each vertex by its degree and its neighbors in increasing order, each neighbor preceded by $1$ , the length of its encoding. A graph with n vertices and m edges has an encoding of length n + 4m + 1, whose numbers are at most n. A graph of mathlib on the vertices 0, 1, …, n − 1, a $SimpleGraph (Fin n)$ , is encoded in the same way.

Concept map

5 concepts

100%

DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Lean source view on GitHub

Show types on hover

1	import Lax185574.Encoding
2	import Lax185574.FirstOrderLogic
3	import Lax3.FirstOrder
4	import Mathlib.Data.Finset.Sort
5	import Mathlib.Data.List.Lex
6	import Mathlib.Data.Rat.Defs
7	import Mathlib.Data.ENat.Basic
8
9	/-!
10	---
11	title: How inputs are given to algorithms
12	type: definition
13	---
14	The encodings of all values that algorithms in this submission read or
15	write. Except for lists, functions on `Fin n`, finite sets, graphs and
16	the values of ℕ∞, they are given by the rule of `Lax185574.Encoding`.
17	Encodings of further types, such as partial graphs and type trees, are
18	given next to their definitions.
19
20	\| type \| value \| encoding \|
21	\| --- \| --- \| --- \|
22	\| `Bool` \| `false`, `true` \| `0`, `1` \|
23	\| `Fin n` \| `i` \| `i` \|
24	\| `α × β` \| `(a, b)` \| encoding of `a`, then of `b` \|
25	\| `α ⊕ β` \| `inl a`, `inr b` \| `0`, encoding of `a`, and `1`, encoding of `b` \|
26	\| `Option α` \| `none`, `some a` \| `0`, and `1`, encoding of `a` \|
27	\| `ℤ` \| `m ≥ 0`, `-(m + 1)` \| `0, m`, and `1, m` \|
28	\| `ℚ` \| `p / q` in lowest terms, `q > 0` \| `p` as an integer, then `q` \|
29	\| `ℕ∞` \| `d`, `∞` \| `d + 1`, and `0` \|
30	\| `Empty` \| (no values) \| \|
31	\| `List α` \| `[a₁, …, aₘ]` \| `m`, then the encodings of `a₁`, …, `aₘ` \|
32	\| `Fin n → α` \| `f` \| the list `[f 0, …, f (n - 1)]` \|
33	\| `Finset α` \| `S` \| the list of the encodings of the elements of `S`, in increasing order \|
34
35	The encodings of the elements of a finite set are lists of numbers, and
36	they are compared lexicographically. As a list of lists, the encoding
37	of a set gives the length of each element's encoding in front of it.
38
39	A first-order formula is written in prefix (Polish) notation, with one
40	number per connective.
41
42	\| formula \| encoding \|
43	\| --- \| --- \|
44	\| xᵢ adjacent to xⱼ \| `0, i, j` \|
45	\| xᵢ = xⱼ \| `1, i, j` \|
46	\| ¬φ \| `2`, encoding of φ \|
47	\| φ ∧ ψ \| `3`, encoding of φ, encoding of ψ \|
48	\| ∃xₙ φ \| `4`, encoding of φ \|
49	\| xᵢ has color c \| `5`, encoding of `c`, `i` \|
50
51	The first-order formulas `Lax3.FirstOrder.FO` of the archive, which
52	have no colors, are encoded in the same way, `0, i, j` for adjacency,
53	`1, i, j` for equality, and `2`, `3`, `4` for negation, conjunction and
54	the quantifier.
55
56	A graph with n vertices is encoded by the family of the neighborhoods of
57	its vertices 0, 1, …, n − 1, each a finite set of vertices. So the
58	encoding starts with n, followed for each vertex by its degree and its
59	neighbors in increasing order, each neighbor preceded by `1`, the length
60	of its encoding. A graph with n vertices and m edges has an encoding of
61	length n + 4m + 1, whose numbers are at most n. A graph of mathlib on
62	the vertices 0, 1, …, n − 1, a `SimpleGraph (Fin n)`, is encoded in the
63	same way.
64
65	# Formalization notes
66
67	The tables are not part of the definition. They spell out what the
68	instances below and `deriving Encode` write for these declarations.
69
70	The adjacency of a graph is a relation, so the encoding of a graph is not
71	derived. A number or ∞ takes one entry, so that a matrix of distances
72	has entries of constant size. Its derived encoding, as an optional
73	number, would take two entries for a finite value. Every finite set has exactly one encoding, so every graph has
74	exactly one encoding. Its length is at least the number of vertices, so
75	an algorithm whose running time is measured in the number of vertices
76	can read its whole input.
77	-/
78
79	namespace Lax185574.Encodings
80
81	open Lax185574.Encoding Lax185574.Graphs Lax185574.FirstOrderLogic
82
83	universe u
84
85	deriving instance Encode for Bool, Fin, Prod, Sum, Option, Int, Rat, Empty, Formula,
86	Lax3.FirstOrder.FO
87
88	/-- A list is encoded by its length, followed by the encodings of its
89	entries. -/
90	instance {α : Type u} [Encode α] : Encode (List α) where
91	encode l := l.length :: (l.map encode).flatten
92
93	/-- A family indexed by `Fin n` is encoded as the list of its members. -/
94	instance {α : Type u} {n : ℕ} [Encode α] : Encode (Fin n → α) where
95	encode f := encode (List.ofFn f)
96
97	/-- A finite set is encoded by the list of the encodings of its elements,
98	in increasing lexicographic order. -/
99	instance {α : Type u} [Encode α] : Encode (Finset α) where
100	encode S := encode ((S.image encode).sort (· ≤ ·))
101
102	/-- A number `d` or `∞` is encoded as one number, `d + 1` for `d` and
103	`0` for `∞`. -/
104	instance : Encode ℕ∞ where
105	encode d := [if d = ⊤ then 0 else d.toNat + 1]
106
107	open Classical in
108	/-- A graph of mathlib on `Fin n` is encoded by the family of the
109	neighborhoods of its vertices. -/
110	noncomputable instance {n : ℕ} : Encode (SimpleGraph (Fin n)) where
111	encode H := encode fun v : Fin n => Finset.univ.filter (H.Adj v)
112
113	open Classical in
114	/-- A graph is encoded by the family of the neighborhoods of its
115	vertices. -/
116	noncomputable instance : Encode Graph where
117	encode G := encode fun v : Fin G.n => ({u \| G.Adj v u} : Finset (Fin G.n))
118
119	end Lax185574.Encodings
120

Formalization notes

The tables are not part of the definition. They spell out what the instances below and $deriving Encode$ write for these declarations.

The adjacency of a graph is a relation, so the encoding of a graph is not derived. A number or ∞ takes one entry, so that a matrix of distances has entries of constant size. Its derived encoding, as an optional number, would take two entries for a finite value. Every finite set has exactly one encoding, so every graph has exactly one encoding. Its length is at least the number of vertices, so an algorithm whose running time is measured in the number of vertices can read its whole input.

Builds on

Used by

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

How inputs are given to algorithms

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments