Lax709149.Types

Types and their string representation

concepts/Lax709149/Types.lean · lax-709149

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 138 of the paper of lax-157538, Transducers

Definition

The types of Section C.5 of Transducers (Definition C.5.1) are the expressions built from the unit type $\mathbb{1}$ , which has the unique element $1$ , by the product $A \times B$ , the co-product $A + B$ and the list type $A^*$ . Every element of a type has a string representation over a fixed alphabet with eight letters

( \quad ) \quad [ \quad ] \quad , \quad 1 \quad L \quad R,

defined by induction on the type: the unique element of $\mathbb{1}$ is $1$ , an element of $A + B$ is $L\,a$ or $R\,b$ , a pair is $(a, b)$ , and a list is $[a_1, \ldots, a_n]$ . Through this representation, type-to-type functions can be computed by string-to-string transducers (Definition C.5.2).

Lean source view on GitHub

1	import Mathlib.Data.Fintype.Basic
2	import Mathlib.Tactic.DeriveFintype
3
4	/-!
5	---
6	title: Types and their string representation
7	type: definition
8	---
9	The types of Section C.5 of Transducers (Definition C.5.1) are the
10	expressions built from the unit type $\mathbb{1}$ , which has the unique element
11	$1$ , by the product $A \times B$ , the co-product $A + B$ and the list type
12	$A^$ . Every element of a type has a string representation* over a fixed
13	alphabet with eight letters
14	$( \quad ) \quad [ \quad ] \quad , \quad 1 \quad L \quad R,$
15	defined by induction on the type: the unique element of $\mathbb{1}$ is $1$ , an
16	element of $A + B$ is $L\,a$ or $R\,b$ , a pair is $(a, b)$ , and a list is
17	$[a_1, \ldots, a_n]$ . Through this representation, type-to-type functions can
18	be computed by string-to-string transducers (Definition C.5.2).
19
20	# Formalization notes
21
22	`Ty.Elt` interprets a type as a Lean type — `Unit`, products, sums and lists —
23	and `Ty.repr` is the representation, a string over the eight-letter alphabet
24	`Sym8`, the same alphabet for all types. Lists are written with the separating
25	commas of the book and no trailing separator.
26	-/
27
28	namespace Lax709149.Types
29
30	/-- A type: built from the unit type by product, co-product and list. -/
31	inductive Ty : Type
32	\| one : Ty
33	\| prod : Ty → Ty → Ty
34	\| sum : Ty → Ty → Ty
35	\| list : Ty → Ty
36	deriving DecidableEq
37
38	/-- The set of elements of a type. -/
39	def Ty.Elt : Ty → Type
40	\| .one => Unit
41	\| .prod A B => A.Elt × B.Elt
42	\| .sum A B => A.Elt ⊕ B.Elt
43	\| .list A => List A.Elt
44
45	/-- The alphabet with eight letters `(`, `)`, `[`, `]`, `,`, `1`, `L`, `R`. -/
46	inductive Sym8 : Type
47	\| lpar \| rpar \| lbrack \| rbrack \| comma \| one \| left \| right
48	deriving DecidableEq, Fintype
49
50	/-- The entries of a list representation, separated by commas. -/
51	def joinSep : List (List Sym8) → List Sym8
52	\| [] => []
53	\| [x] => x
54	\| x :: xs => x ++ Sym8.comma :: joinSep xs
55
56	/-- The string representation of an element: `1` for the unit, `L a` and `R b` for
57	the co-product, `(a,b)` for a pair, `[a₁,…,aₙ]` for a list. -/
58	def Ty.repr : (t : Ty) → t.Elt → List Sym8
59	\| .one, _ => [Sym8.one]
60	\| .prod A B, x => Sym8.lpar :: (A.repr x.1 ++ Sym8.comma :: (B.repr x.2 ++ [Sym8.rpar]))
61	\| .sum A B, x => Sum.elim (fun a => Sym8.left :: A.repr a) (fun b => Sym8.right :: B.repr b) x
62	\| .list A, l => Sym8.lbrack :: (joinSep (l.map A.repr) ++ [Sym8.rbrack])
63
64	end Lax709149.Types
65

Formalization notes

$Ty.Elt$ interprets a type as a Lean type — $Unit$ , products, sums and lists — and $Ty.repr$ is the representation, a string over the eight-letter alphabet $Sym8$ , the same alphabet for all types. Lists are written with the separating commas of the book and no trailing separator.

Builds on

none

Used by

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive