Types

Lax149335.Types · concepts/Lax149335/Types.lean · lax-149335

definition

Loading review…

Natural Language Statement

Definition

Types are the expressions generated by the grammar

A \;::=\; 1 \;\mid\; A \times A \;\mid\; A + A \;\mid\; A^* .

A type denotes a set: $1$ is a one-element set, $A \times B$ is the Cartesian product, $A + B$ is the disjoint union, and $A^*$ is the set of finite lists over $A$ .

Elements of types are represented as strings over the eight-letter alphabet

\mathbb{8} = \{\, (\,,\ )\,,\ [\,,\ ]\,,\ \texttt{,}\,,\ 1,\ \mathsf{Left},\ \mathsf{Right} \,\}:

the element of $1$ is written $1$ , an element of $A + B$ is written $\mathsf{Left}\,a$ or $\mathsf{Right}\,b$ , a pair is written $(a,b)$ and a list is written $[a_1,\ldots,a_n]$ .

A type is a finite alphabet if it has the form $1 + \cdots + 1$ . We write $\overline{n+1}$ for the finite alphabet with $n+1$ letters, bracketed to the right.

Concept map

1 concept

100%

DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Nat.Notation
2
3	/-!
4	---
5	title: Types
6	type: definition
7	---
8	Types are the expressions generated by the grammar
9
10	$A \;::=\; 1 \;\mid\; A \times A \;\mid\; A + A \;\mid\; A^* .$
11
12	A type denotes a set: $1$ is a one-element set, $A \times B$ is the Cartesian product,
13	$A + B$ is the disjoint union, and $A^*$ is the set of finite lists over $A$ .
14
15	Elements of types are represented as strings over the eight-letter alphabet
16
17	$\mathbb{8} = \{\, (\,,\ )\,,\ [\,,\ ]\,,\ \texttt{,}\,,\ 1,\ \mathsf{Left},\ \mathsf{Right} \,\}:$
18
19	the element of $1$ is written $1$ , an element of $A + B$ is written $\mathsf{Left}\,a$ or
20	$\mathsf{Right}\,b$ , a pair is written $(a,b)$ and a list is written $[a_1,\ldots,a_n]$ .
21
22	A type is a finite alphabet if it has the form $1 + \cdots + 1$ . We write
23	$\overline{n+1}$ for the finite alphabet with $n+1$ letters, bracketed to the right.
24
25	# Formalization notes
26
27	The finite alphabet with $n+1$ letters is `Ty.finAlph n`, defined as `1` for $n = 0$ and
28	as `1 + finAlph n` otherwise. A type is a finite alphabet (`Ty.IsFinAlph`) if it is equal
29	to one of these; the paper does not fix a bracketing of the sum, and any bracketing is
30	isomorphic to the right-bracketed one.
31
32	`Ty.someElem` picks a canonical element of every type; it shows that every type is
33	nonempty and is used to state the decision procedure of Corollary 2.8.
34	-/
35
36	namespace Lax149335.Types
37
38	/-- Types: the unit type `1`, products `A × B`, co-products `A + B` and lists `A*`. -/
39	inductive Ty : Type
40	\| unit : Ty
41	\| prod : Ty → Ty → Ty
42	\| sum : Ty → Ty → Ty
43	\| list : Ty → Ty
44	deriving DecidableEq, Repr
45
46	namespace Ty
47
48	/-- Notation `A ⊗ B` for the product type. -/
49	infixl:70 " ⊗ " => Ty.prod
50	/-- Notation `A ⊕' B` for the co-product type. -/
51	infixl:65 " ⊕' " => Ty.sum
52	/-- Notation `A⋆` for the list type. -/
53	postfix:max "⋆" => Ty.list
54
55	/-- The set denoted by a type. -/
56	def den : Ty → Type
57	\| .unit => Unit
58	\| .prod A B => den A × den B
59	\| .sum A B => den A ⊕ den B
60	\| .list A => List (den A)
61
62	/-- Notation `⟦A⟧` for the set denoted by a type. -/
63	notation "⟦" A "⟧" => Ty.den A
64
65	/-- The eight-letter alphabet used to represent elements of types as strings. -/
66	inductive Sym : Type
67	\| lpar \| rpar \| lbrack \| rbrack \| comma \| one \| left \| right
68	deriving DecidableEq, Repr
69
70	/-- The string representing an element of a type: `1`, `Left a`, `Right b`, `(a,b)` and
71	`[a₁,…,aₙ]`. -/
72	def repr : (A : Ty) → ⟦A⟧ → List Sym
73	\| .unit, _ => [Sym.one]
74	\| .prod A B, (a, b) => Sym.lpar :: (repr A a ++ Sym.comma :: repr B b ++ [Sym.rpar])
75	\| .sum A _, .inl a => Sym.left :: repr A a
76	\| .sum _ B, .inr b => Sym.right :: repr B b
77	\| .list A, l =>
78	Sym.lbrack :: ((l.map (repr A)).intersperse [Sym.comma]).flatten ++ [Sym.rbrack]
79
80	/-- A canonical element of every type. -/
81	def someElem : (A : Ty) → ⟦A⟧
82	\| .unit => ()
83	\| .prod A B => (someElem A, someElem B)
84	\| .sum A _ => .inl (someElem A)
85	\| .list _ => []
86
87	/-- The finite alphabet `1 + (1 + ⋯ + 1)` with `n + 1` letters. -/
88	def finAlph : ℕ → Ty
89	\| 0 => Ty.unit
90	\| (n + 1) => Ty.sum Ty.unit (finAlph n)
91
92	/-- A type is a finite alphabet if it has the form `1 + ⋯ + 1`. -/
93	def IsFinAlph (A : Ty) : Prop := ∃ n : ℕ, A = finAlph n
94
95	end Ty
96
97	end Lax149335.Types
98

Formalization notes

The finite alphabet with $n+1$ letters is $Ty.finAlph n$ , defined as $1$ for $n = 0$ and as $1 + finAlph n$ otherwise. A type is a finite alphabet ( $Ty.IsFinAlph$ ) if it is equal to one of these; the paper does not fix a bracketing of the sum, and any bracketing is isomorphic to the right-bracketed one.

$Ty.someElem$ picks a canonical element of every type; it shows that every type is nonempty and is used to state the decision procedure of Corollary 2.8.

Builds on

none

Used by

From Mathlib

Mathlib.Data.Nat.Notation

Discussion

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

Loading discussion…

Lax Lean Archive

Types

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments