Title: Theory / Unimportant / CS / Fundamental / Lambda calculus / With types

Definition: \(\lambda x.x\)
Page: 31
Chapter: 2
Section: 1
Context: Lambda
Notation: I
Kind: 25

Name: The set atomic types
Page: 1
Context: Typed lambda calculus
Notation: \(\mathbb A\)

Definition: The infinite set of atomic types \(\alpha_i\)
Page: 1
Notation: \(\lambda^\infty_{\to}\)

Definition: The infinite with a single type \(0\)
Page: 1
Notation: \(\lambda^0_{\to}\)

Name: The set of simple types over \(\mathbb A\)
Definition: including \(\mathbb A\)
Page: 1, 8
Chapter: 1
Variables: \(\mathbb A\) a set of atomic types
Notation: \(\mathbb{T^A}\)
Definition2: closed under \((A\to B)\) with \(A,B\) in the set
Conjdef: The smallest set

Name: The set of variables
Page: 2
Chapter: 1
Variables: \(\mathbb A\) a set of atomic types
Context: Lambda calculus with type
Notation: \(V\)

Definition: \(\{x:A\}\vdash M:B\)
Page: 2
Chapter: 1
Variables: \(\mathbb A\) a set of atomic types
Notation: \(x:A\vdash M:B\)

Definition: \(\Gamma\cup\{x:A\}\vdash M:B\)
Page: 2
Chapter: 1
Variables: \(\mathbb A\) a set of atomic types
Notation: \(\Gamma, x:A\vdash M:B\)

Smaller0: \((x:A)\in \Gamma\)
Greater0: \(\Gamma\vdash x:A\)
Page: 2
Chapter: 1
Variables: \(\mathbb A\) a set of atomic types
\(\Gamma\) a type assignment

Smaller0: \(\Gamma\vdash M:(A\to B)\)
Greater0: \(\Gamma\vdash (MN):B\)
Page: 2, 10
Chapter: 1
Variables: \(\mathbb A\) a set of atomic types
\(\Gamma\) a type assignment
Smaller1: \(\Gamma\vdash N:A\)
Name: \(\to\)-elimination

Smaller0: \(\Gamma, x:A\vdash M: B\)
Greater0: \(\Gamma\vdash (\lambda x.M):(A\to B)\)
Page: 2, 10
Chapter: 1
Variables: \(\mathbb A\) a set of atomic types
\(\Gamma\) a type assignment
Name: \(\to\)-introduction

Definition: \((A_1\to (\dots(A_{n-1}\to A_n)\dots)\)
Page: 8
Chapter: 1. 1
Section: 12
Variables: \(A_i\) types
Notation: \(A_1\to\dots\to A_n\)

Name: A statement
Definition: A pair with a lambda-term and a type
Page: 9
Chapter: 1. 1
Section: 12
Intuition: Axiom stating that the type of M is A
Denoted by: \(M:A\)

Name: A type assignment
Definition: A set of type assignment statement
Page: 9
Chapter: 1. 1
Section: 12
Denoted by: \(\Gamma\)

Name: A declaration
Definition: A statement whose subject is a term variable
Page: 9
Chapter: 1. 1
Section: 12

Name: \(M\) in \(A\)
Page: 9
Chapter: 1. 1
Section: 12
Variables: \(M\in\Lambda\)
\(A\in\mathbb T\)
Notation: \((M:A)\)

Name: The predicate of \(M:A\)
Definition: \(A\)
Page: 9
Chapter: 1. 1
Section: 12
Variables: \(M\in\Lambda\)
\(A\in\mathbb T\)
Context: \((M:A)\)

Name: The subject of \(M:A\)
Definition: \(M\)
Page: 9
Chapter: 1. 1
Section: 12
Variables: \(M\in\Lambda\)
\(A\in\mathbb T\)
Context: \((M:A)\)

Name: A basis
Definition: A set of declarations with distinct variables as subject
Page: 9
Chapter: 1. 1
Section: 12
Context: Typed lambda calculus

Name: The domain of \(\Gamma\)
Definition: \(\{x_1,\dots,x_n\}\)
Page: 9
Chapter: 1. 1
Section: 12
Variables: \(\Gamma=\{x_1:A_1,\dots,x_n:A_n\}\)
Notation: \(\texttt{dom}(\Gamma)\)
Index: 15

Definition: \(\emptyset\vdash M:A\)
Page: 9
Chapter: 1. 1
Section: 12
Notation: \(\vdash M:A\)
Index: 15

Definition: \(x_1:A, \dots, x_n:A\)
Page: 9
Chapter: 1. 1
Section: 12
Notation: \(x_1\dots, x_n:A\)
Index: 15

Definition: The set of \(M\in\Lambda\) such that \(\Gamma\to_{\lambda^\alpha_\to}M:A\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(A\) a type
Notation: \(\Lambda^\Gamma_\to(A)\)
Index: 19

Name: The set of typed term
Definition: The union of \(\Lambda^\Gamma_\to(A)\) for all types \(A\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(A\) a type
Notation: \(\Lambda^\Gamma_\to\)
Index: 19

Definition: \(\Lambda^\emptyset_\to(A)\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(A\) a type
Notation: \(\Lambda_\to(A)\)
Index: 19

Definition: \(\Lambda^\emptyset_\to\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(A\) a type
Notation: \(\Lambda_\to\)
Index: 19

Name: A term of type \(A\)
Definition: An element of \(\Lambda_\to(A)\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(A\) a type
Index: 20
Name2: An inhabitant of \(A\)

Name: A typable term
Definition: An element of \(\Lambda_\to\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
Index: 20

Name: A typable term relative to \(\Gamma\)
Definition: An element of \(\Lambda^\Gamma_\to\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(\Gamma\) an assignment
Index: 20

Name: A typable term relative to \(\Gamma\)
Definition: An element of \(\Lambda^\Gamma_\to(A)\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(\Gamma\) an assignment
\(A\in\mathbb {T^A}\)
Index: 20

Name: A type inhabited relative to \(\Gamma\)
Definition: A type \(A\) such that \(\Lambda^A_\to(A)\ne\emptyset\)
Page: 12
Chapter: 1. 1
Variables: \(\mathbb A\) a set of atomic types
\(\Gamma\) an assignment
Index: 20

Name: The depth of \(A\)
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A\in\mathbb T\)
Index: 22
Abbreviation: dpt(\(A\))

Question: The depth of \(\alpha\)
Answer: 1
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22

Question: The depth of \(A\to B\)
Answer: \(1+\max(\mathtt{dpt}(A)),\mathtt{dpt}(B)\)
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22

Question: The rank of \(A\to B\)
Answer: \(\max(1+\mathtt{rk}(A)),\mathtt{rk}(B)\)
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22

Question: The rank of \(\alpha\)
Answer: \(0\)
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22

Name: The rank of \(A\)
Page: 13, 14
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22
Name2: Type level
Abbreviation: rk(\(A\))

Name: The order of \(A\)
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22
Abbreviation: ord(\(A\))
Etymology: o-order logic  is logic manipulating elmenets whose order is o-1

Question: ord (\(A\to B\))
Answer: \(\max(\mathtt{ord}(A)+1, \mathtt{ord}(B))\)
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22

Question: ord (\(\alpha\))
Answer: 1
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
Index: 22

Name: The depth/rank/ord of \(\Gamma\)
Definition: The maximal depth/rank/ord of types in \(\Gamma\)
Page: 13
Chapter: 1. 1
Section: 12
Variables: \(A,B\in\mathbb T\)
\(\alpha\in\mathbb A\)
\(\Gamma\) an environment
Index: 22

Definition: \((k-1)\to 0\)
Page: 14
Chapter: 1. 1
Section: 12
Variables: \(k\in\mathbb N^+\)
Context: simple type
Notation: \(k\)
Index: 25
Example: \(((0\to 0)\to0)\to0\)
Applied to3: 3

Definition: \(0\)
Page: 14
Chapter: 1. 1
Section: 12
Variables: \(k\in\mathbb N^+\)
Context: simple type
Notation: \(0_k\)
Index: 25

Definition: \((n-1)^k\to 0\)
Page: 14
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
Context: simple type
Notation: \((n)_k\)
Index: 25

Definition: \(A\to \dots \to A\to B\)
Page: 14
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
\(A, B\in\mathbb T\)
Context: simple type
Notation: \(A^k\to B\)
Index: 25

Question: A type of \(\lambda_\to^\infty\) is of the form
Answer: \(A_1\to\dots\to A_a\to\alpha\) for \(\alpha\in\mathbb A\)
Page: 14
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
\(A, B\in\mathbb T\)
Index: 26

Question: A type of \(\lambda_\to^0\) is of the form
Answer: \(A_1\to\dots\to A_a\to0\)
Page: 14
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
\(A, B\in\mathbb T\)
Index: 26

Question: The rank of \(A_1\to\dots\to A_a\to\alpha\) is
Answer: \(\max\{\mathtt{rk}(A_i)+1\}\)
Page: 14
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
\(A, B\in\mathbb T\)
Index: 26

Name: A component of \(A_1\to\dots\to A_a\to\alpha\)
Definition: some \(A_i\)
Page: 15
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
\(A, B\in\mathbb T\)
Index: 27

Name: The arity of \(A_1\to\dots\to A_a\to\alpha\)
Definition: \(a\)
Page: 15
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
\(A, B\in\mathbb T\)
Index: 27
Abbreviation: arity(\(A\))

Name: The target of \(A_1\to\dots\to A_a\to\alpha\)
Definition: \(\alpha\)
Page: 15
Chapter: 1. 1
Section: 12
Variables: \(k, n\in\mathbb N^+\)
\(A, B\in\mathbb T\)
Index: 27

Definition: \(A_i\)
Page: 15
Chapter: 1. 1
Section: 12
Variables: \(A=(A_1\to\dots\to A_a\to\alpha)\)
Notation: \(A(i)\)
Index: 27

Name: Curry
Page: 15
Chapter: 1. 1
Section: 12
Variables: \(A=(A_1\to\dots\to A_a\to\alpha)\)
Index: 29
Abbreviation: Cu

Name: Ch
Definition: variation of lambda calculus where type is assigned to each variable
Page: 15
Chapter: 1. 1
Section: 12
Variables: \(A=(A_1\to\dots\to A_a\to\alpha)\)
Index: 29

Name: de Bruijn
Definition: Lambda calculus where bound variables are ornamented with types
Page: 18
Chapter: 1. 1
Section: 12
Abbreviation: dB