Title: Theory / Unimportant / CS / Fundamental / Lambda calculus / Its syntax and semantics+9

Question: Original goals of lambda calculus
Answer: To develop a general theory of functions (dealing, for example, with
formula manipulations).
Page: 3
Section: I
Answer2: To extend that theory with logical notions providing a foundation for
logic and (parts of ) mathematics.

Question: Difference between lambda calculus and category theory
Answer: Function in lambda calculus are used for their applications behavior and not for their composition
Page: 6
Chapter: 1
Section: I

Name: The set of \(\lambda\)-term
Definition: variables \(v_1,v_1,\dots\)
Page: 6, 22
Chapter: 1, 2.2
Section: 1, 1
Notation: \(\Lambda\)
Definition2: \(MN\) for \(M,N\) two elemets of this set
Definition3: \((\lambda xM)\) for \(x\) a variable and \(M\) an element of this set
Denoted by: \(M, N, L\)
DefType: The smallest set containing

Question: Principal question of lambda calculus
Answer: What kind of functions (on terms) are definable (as term)?
Page: 7
Chapter: 1
Section: I
Answer2: Let Af, Ν be non-convertible terms. Is it reasonable to identify M and TV (taking a less intensional view)?
Answer3: What is the correspondence between the applicative behaviour and
the syntactic form of terms?

Name: after page 8
Page: 7
Chapter: 1
Section: I
Notation: todo

Name: The alphabet of lambda term
Definition: \(v_0,\dots,v_1\) variables
Page: 2
Section: 1.1
Definition2: \(\lambda\)
Definition3: ( and )

Name: abstractor
Page: 2
Section: 1.1
Context: Lambda calculus
Notation: \(\lambda\)

Name: \(t_1\) and \(t_2\) are syntactically equal
Definition: all syntactic sugar is removed are exactly the same
Page: 2
Section: 1.1
Notation: \(t_1\equiv t_2\)
Definition2: \(\alpha\)-congruence
Conjdef: \(t_1\) and \(t_2\), up to

Definition: \(\lambda x_1(\lamdba x_2(\dots(\lambda x_n(M))\dots))\)
Page: 22
Chapter: 2
Section: 1.1
Variables: \(M\in\Lamdba\)
\(\vec x = x_1,\dots,x_n\) variables
Notation: \(\lambda \vec x. M\)
Notation2: \(\lambda x_1,\dots, x_n.M\)

Definition: \((\dots ((MN_1)N_2)\dots N_n)\)
Page: 22
Chapter: 2
Section: 1.1
Variables: \(M\in\Lambda\),
\(\vec N=N_1,\dots, N_n\in\Lambda\)
Notation: \(M\vec N\)
Notation2: \(MN_1\dots N_n\)

Name: The length of \(M\)
Definition: The number of symbols in \(M\)
Page: 22
Chapter: 2
Section: 1.1
Variables: \(M\in\Lambda\)
Notation: \(\norm{M}\)

Name: Substitution
Definition: The result of subsitutig \(N\) for \(x\) in \(M\)
Page: 23, 27
Chapter: 2
Section: 1.1
Variables: \(M,N\in\Lambda\)
\(x\) a variable
Notation: \(M[x:=N]\)

Name: \(\beta\)-conversion
Definition: The axiom \((\lambda x.M)N=M[x:=N]\)
Page: 23
Chapter: 2
Section: 1.1
Variables: \(M,N\in\Lambda\)
\(x\) a variable

Page: 23
Section: 1.1
Chapter: 2
Axiom: \(\beta\)-conversion
Name: Theory of \(\lambda\)-calculus
Vocabulary: \(=\) and \(\Lambda\)
Extends: \(=\) is an equivalence relation
Axiom2: \(M=M\)
Axiom3: \(M=N\implies ML=NL\)
Variables: \(M,N\in\Lambda\)
\(x\) a variable
Axiom4: \(M=N\implies LM=LN\)
Axiom5: rule \(\xi\)
Notation: \(\mathbf\lambda\)

Name: weak extensionality
Definition: \(M=N\implies \lambda x.M=\lambda x.N\)
Page: 23
Chapter: 2
Section: 1.1
Variables: \(M,N\in\Lambda\)
\(x\) a variable
Notation: rule \(\xi\)

Name: \(M\) and \(N\) are convertilbe
Definition: The equality of \(M\) and \(N\) are equals according to \(\mathbf\lambda\)-axioms
Page: 23
Chapter: 2
Section: 1.1
Variables: \(M,N\in\Lambda\)
\(x\) a variable
Notation: \(M=N\)

Smaller0: \(M\equiv N\)
Greater0: \(M=N\)
Page: 23
Chapter: 2
Section: 1.1
Variables: \(M,N\in\Lambda\)
\(x\) a variable

Name: Fixed point theorem
Definition: For each \(F\) there exists \(X\) such that \(FX=X\)
Page: 24
Chapter: 2
Section: 1.1
Index: 5
Construction: Let \(W=\lambda x.F(xx)\)  and \(X=WW\)
Then \(X\equiv WW\equiv (\lambda x.F(xx))W=F(WW)=F(X)\)

Name: \(x\) occurs free in \(M\)
Definition: \(x\) appears in \(M\) not in the scope of a \(\lambda\)-term
Page: 24
Chapter: 2
Section: 1
Variables: \(M\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Name: \(x\) occurs bounds in \(M\)
Definition: \(x\) appears in \(M\) in the scope of a \(\lambda\)-term
Page: 24
Chapter: 2
Section: 1
Variables: \(M\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Question: \(FV(x)\)
Answer: \(\{x\}\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Question: The set of bound variable in \(x\)
Answer: \(\{\}\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Question: The set of bound variable in \(\lambda x. M\)
Answer: Union of \(\{x\}\) and the set of bound variable in \(M\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Question: \(FV(\lambda x. M)\)
Answer: \(FV(M)\setminux \{x\}\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Question: \(FV(MN)\)
Answer: \(FV(M)\cup FV(N)\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M,N\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Question: The set of bound variables in \(MN\)
Answer: The union of the set of bound variables of \(M\) and \(N\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M,N\) a \(\lambda\)-term
\(x\) a variable
Index: 6

Name: The set of free variables in \(M\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M,N\) a \(\lambda\)-term
\(x\) a variable
Notation: \(FV(M)\)
Index: 6

Name: A closed term
Definition: A term without free variables
Page: 24
Chapter: 2
Section: 1
Index: 6
Name2: A combinator

Name: The set of closed terms
Page: 24
Chapter: 2
Section: 1
Notation: \(\Lambda^0\)
Index: 7

Definition: The set of terms whose free variables are in \(\vec x\)
Page: 24
Chapter: 2
Section: 1
Variables: \(\vec x=x_1,\dots,x_n\)
Notation: \(\Lambda^0(\vec x)\)
Index: 7

Name: The closure of \(M\)
Definition: \(\lambda FV(M). M\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\)
Index: 7

Name: The set of subterm of \(M\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\)
Index: 7
Abbreviation: \(\mathtt{Sub}(M)\)

Question: \(\mathtt{Sub}(x)\)
Answer: \(\{x\}\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\),
\(x\) a variable
Index: 7

Question: \(\mathtt{Sub}(\lambda x. M)\)
Answer: \(\{\lambda x. M\}\cup\mathtt{Sub}(M)\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\),
\(x\) a variable
Index: 7

Question: \(\mathtt{Sub}(N_1N_2)\)
Answer: \(\{N_1N_2\}\cup\mathtt{Sub}(N_1)\cup\mathtt{Sub}(N_2)\)
Page: 24
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\),
\(x\) a variable
Index: 7

Name: Disjoint subterms of \(M\)
Definition: Subterms of \(M\) that have no common symbol occurrences
Page: 25
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\),
\(x\) a variable
Index: 7(ii)

Name: An active subterm of \(M\)
Definition: Some subterm \(N\) for \(NZ\) a subterm of \(M\)
Page: 25
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\),
\(x\) a variable
Index: 7(ii)

Definition: \(M\dots MN\)
Page: 25
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Notation: \(M^nN\)
Index: 9(i)

Definition: \(MN\dots N\)
Page: 25
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Notation: \(MN^{~n}\)
Index: 9(ii)

Name: A change of free variable in \(M\)
Definition: Replacing some subterm \(\lambda x.N\) by \(\lambda y.N[x:=Y]\) with \(y\) being a fresh variable
Page: 25
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 10

Name: A fresh variable for \(M\)
Definition: A variable which is not a subterm of \(M\)
Page: 25
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 10

Name: \(\alpha\)-congruent terms
Definition: Terms that are equivalent after change of bound variables
Page: 25
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Notation: \(\equiv_\alpha\)
Index: 10

Name: \(\alpha\)-conversion
Definition: Replacing \(\lambda x.M\) by \(\lambda y. M[x:=y]\) where free is fresh in \(M\)
Page: 25
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 11

Question: \(x[x:=N]\)
Answer: \(N\)
Page: 27
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 11

Question: \(y[x:=N]\) with \(x\ne y\)
Answer: \(y\)
Page: 27
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 11

Question: \((\lambda y.M_1)[x:=N]\) for \(y\ne x\)
Answer: \(\lambda y.(M_1)[x:=N]\)
Page: 27
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 11

Question: \((M_1M_2)[x:=N]\) for \(y\ne x\)
Answer: \((M_1[x:=N])(M_2[x:=N])\)
Page: 27
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 11

Question: \(M[x:=N][y:=L]\) equals
Answer: \(M[y:=L][x:N[y:=L]]\)
Page: 27
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 11
Name: Substitution lemma

Name: A context
Definition: containing variables
Page: 29
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\),
\(x\) a variable,
\(n\in\mathbb N\)
Index: 18
Definition2: containing \([\ ]\), a hole
Definition3: closed under composition
Intuition: A term with some holes in it
Definition4: closed under abstraction
Denoted by: \(C[\ ]\)
DefType: The smallest set

Definition: The result of placing \(M\) in the holes of \(C[\ ]\) (literally, without replacing captured variables)
Page: 29
Chapter: 2
Section: 1
Variables: \(C[\ ]\) a context
\(M\in\Lambda\)
Notation: \(C[M]\)
Index: 18

Name: A hole
Page: 29
Chapter: 2
Section: 1
Context: lambda term and context
Notation: v
Index: 18

Question: Difference between placing a term \(M\) in a context \(C[\ ]\) and in a lambda abstraction \(\lambda x. N\)?
Answer: With lambda abstractions, no variable is captured, \(M\)'s \(x\) are renamed. With context, \(M\)'s \(x\) remain \(x\)
Page: 29
Chapter: 2
Section: 1
Context: lambda term and context
Index: 18

Question: \(C[M]\) can be rewritten as
Answer: \(F(\lambda \vec x. M)\) for some \(\vec x\) and \(F\)
Page: 29
Chapter: 2
Section: 1
Index: 20
Kind: (ii)

Question: \(C[\ ]\), with some free variables \(\vec x\)
Answer: \(F(\lambda \vec x. M)\) for some \(F\) and all \(M\in\Lambda^0(\vec x)\)
Page: 29
Chapter: 2
Section: 1
Index: 20
Kind: (ii)

Name: \(\vec N\) fits in \(\vec x\)
Definition: \(m=n\) and \(\vec x\) do not occur in \(FV(\vec N)\)
Page: 29
Chapter: 2
Section: 1
Variables: \(\vec x = x_1,\dots, x_n\)
\(\vec N=N_1,\dots,N_m\)
Index: 21
Kind: (ii)

Name: \(\vec N=\vec M\)
Definition: \(m=n\) and for each \(i\) \(M_i=N_i\)
Page: 29
Chapter: 2
Section: 1
Variables: \(\vec M = M_1,\dots, M_n\)
\(\vec N=N_1,\dots,N_m\)
Index: 21
Kind: (ii)

Definition: \(M[x_1:=N_1]\dots [x_n:=N_n]\)
Page: 29
Chapter: 2
Section: 1
Variables: \(\vec x = x_1,\dots, x_n\)
\(\vec N=N_1,\dots,N_n\) fitting in \(\vec x\)
\(M\in\Lambda\)
Notation: \(M[\vec x:=\vec N]\)
Index: (iii)
Kind: 21

Definition: \(M[\vec x:=\vec N]\)
Page: 31
Chapter: 2
Section: 1
Variables: \(\vec x = x_1,\dots, x_n\)
\(M(\vec x)\)
\(\vec N\) fitting in \(\vec x\)
Notation: \(M(\vec N)\)
Index: (iv)
Kind: 21

Question: \(M(\vec x)\) can be rewritten as
Answer: \(F\vec x\) for some \(F\)
Page: 31
Chapter: 2
Section: 1
Variables: \(\vec x = x_1,\dots, x_n\)
\(M(\vec x)\)
\(\vec N\) fitting in \(\vec x\)
Answer2: \(((\lambda\vec x). M(\vec x))(\vec x)\)
Index: (i)
Kind: 24

Definition: \(\lambda xyz.xz(yz)\)
Page: 31
Chapter: 2
Section: 1
Notation: S
Kind: 25

Question: SKK
Answer: I
Page: 31
Chapter: 2
Section: 1
Kind: 25

Name: Extensionality
Definition: \(Mx=Nx\) implies \(M=N\)
Page: 31
Chapter: 2
Section: 1
Notation: \(\mathbb ext\)
Kind: 27

Name: \(\eta\)-conversion
Definition: \(\lambda x. Mx=M\) provided that \(x\not\in FV(M)\)
Page: 32
Chapter: 2
Section: 1
Kind: 27

Smaller0: \(\mathbf{\lambda+ext}\)
Greater0: \(\lambda\eta\)
Page: 32
Chapter: 2
Section: 1
Kind: 27
Smaller to greater: is equivalent to
Name: Curry

Name: An equation
Definition: \(M=N\) with \(M,N\in\Lambda\)
Page: 32
Chapter: 2
Section: 1
Context: Lambda calculus
Kind: 30

Name: A closed equation
Definition: \(M=N\) with \(M,N\in\Lambda^0\)
Page: 32
Chapter: 2
Section: 1
Context: Lambda calculus
Kind: 30

Name: A set of closed equations
Page: 76
Chapter: 4
Section: 1
Context: Lambda calculus
Denoted by: \(\mathcal T\)

Name: \(\mathcal T\) is consistent
Definition: \(\mathcal T\) does not prove every closed equation
Page: 32, 63
Chapter: 2, 3
Section: 1, 2
Variables: A theory \(\mathcal T\)
Context: Lambda calculus
Notation: \(\mathtt{Cont}(\mathcal T)\)
Kind: 30, 10
Example: \(\lambda\)

Name: \(\mathcal T\) is inconsistent
Definition: \(\mathcal T\) is not consistent
Page: 32
Chapter: 2
Section: 1
Variables: A theory \(\mathcal T\)
Context: Lambda calculus
Kind: 30

Name: \(M,N\) are incompatible
Definition: \(\neg\mathtt{Con}(M=N)\)
Page: 33
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\)
Context: Lambda calculus
Notation: \(M\# N\)
Kind: 30
Example: \(K\#S\)

Name: A term in \(\beta\)-normal form
Definition: A term with no subterm of the form \((\lambda x.R)S\)
Page: 34
Chapter: 2
Section: 1
Context: Lambda calculus
Kind: 30
Example: I
Abbreviation: \(\beta\)-nf or nf

Name: A \(\beta\)-nf of \(M\)
Definition: A \(\beta\)-nf term \(N\) with \(M=N\)
Page: 34
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\)
Context: Lambda calculus
Kind: 30
Example: \(\lambda y.\mathbf I\)
Applied to: \(\mathbf{KI}\)
Counterexample: \(\mathbf{Omega}\)

Definition: \((\lambda x. xx)(\lambda x.xx)\)
Page: 34
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\)
Context: Lambda calculus
Notation: \(\mathbf\Omega\)
Kind: 30
Intuition: A function such that each application is equal to itself

Name: A term in \(\eta\)-normal form
Definition: A term with no \((\lambda x.Rx)\) subterm with \(x\not\in \mathtt{FV}(R)\)
Page: 34
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\)
Context: Lambda calculus
Kind: 35

Smaller0: \(M\) has a \(\beta\)-nf
Greater0: \(M\) has a \(\beta\eta\)-nf
Page: 34
Chapter: 2
Section: 1
Variables: \(M\in\Lambda\)
Kind: 35
Smaller to greater: iff
Context: Lambda calculus

Smaller0: \(M,N\) are different \(\beta\)-nf's
Greater0: \(M\#N\)
Page: 39
Chapter: 2
Section: 1
Variables: \(M,N\in\Lambda\)
Kind: 35

Name: A \(\lambda\mathbf I\)-term
Definition: A term where all subterms \(\lambda x. M\) have \(x\in FV(M)\)
Page: 35
Chapter: 2
Section: 2.2
Index: i

Name: \(M\) is a subterm of \(N\)
Page: 38
Chapter: 2
Section: 2.2
Variables: \(M,N\in\Lambda\)
Notation: \(N\subset N\)
Index: i
Kind: 35

Name: \(\lambda\mathbf I\)-calculus
Definition: The restriction of \(\lambda\mathbf I\) whose axioms are restricted to \(\Lambda_I\)-terms
Page: 38
Chapter: 2
Section: 2.2
Variables: \(M,N\in\Lambda\)
Index: i
Kind: 35

Name: The encoding of \(n\) in lambda calculus
Definition: \(\lambda fz. f^nz\)
Page: 38
Chapter: 2
Section: 2.2
Variables: \(n\in\mathbb N\)
Notation: \(\mathbf c_n\)
Index: (3)
Kind: 35
Name2: A numeral
Notation2: \(\textopencorner n\textcorner\)

Question: Assuming all terms without NF are equal
Answer: is inconsistent
Page: 39
Chapter: 2
Section: 2.2
Index: (3)
Kind: 35

Name: A \(\lambda\)-definable integral function
Definition: A function \(f:\mathbb N^n\to\mathbb N\) such that there exists \(F\in\Lambda\) such that \(F\(\textopencorner c_1\textcorner\)\dots\(\textopencorner c_nn\textcorner\)=\(\textopencorner f(c_1,\dots, c_n)\textcorner\)\)
Page: 39
Chapter: 2
Section: 2.2
Index: 5

Smaller0: \(f\) is definalbe
Greater0: \(f\) is recursive
Page: 39
Chapter: 2
Section: 2.2
Variables: \(f:\mathbb N^n\to\mathbb N\)
Index: 5
Smaller to greater: iff

Question: other formalism
Answer: todo after page 39
Page: 39
Chapter: 2
Section: 2.2
Index: 5

Name: A binary relation compatible with the operations
Definition: A binary relation \(\mathbf{R}\subseteq\Lambda^I\) such that if \((M,M')\in \mathbf R\) then \((ZM,ZM')\in\mathbf R\), \((MZ,M'Z)\in \mathbf R\) and \((\lambda x.M,\lambda x.M')\in \mathbf R\)
Page: 50
Chapter: 3
Section: 1.1
Index: (i)

Name: An equality relation on \(\Lambda\)
Definition: A compatible equivalence relation on \(\Lambda\)
Page: 50
Chapter: 3
Section: 1.1
Index: (ii)
Name2: A congruence relation on \(\Lambda\)

Name: An reduction relation on \(\Lambda\)
Definition: A compatible, reflexive and transitive relation on \(\Lambda\)
Page: 50
Chapter: 3
Section: 1.1
Index: (iii)

Name: A notion of reduction on \(\Lambda\)
Definition: A binary relation on \(\Lambda\)
Page: 50
Chapter: 3
Section: 1.2
Index: (i)
Example: The \(\beta\) reduction
Denoted by: boldface letters

Definition: \(\mathbf{R_1}\cup\mathbf{R_2}\)
Page: 50
Chapter: 3
Section: 1.2
Variables: Notion of reduction on \(\Lambda\) \(\mathbf{R_1,R_2}\)
Notation: \(\mathbf{R_1R_2}\)
Index: (i)

Name: The reflexive closure of \(>-\)
Definition: the least relation extending \(>-\) that is
reflexive
Page: 51
Chapter: 3
Section: 1.2
Variables: \(X\) a set
\(>-\) a binary relation on \(X\)
Index: (i)

Name: The transitive closure of \(>-\)
Definition: the least relation extending \(>-\) that is
transitive
Page: 51
Chapter: 3
Section: 1.2
Variables: \(X\) a set
\(>-\) a binary relation on \(X\)
Notation: \(>-^\circ\)
Index: (i)

Name: One step \(R\)-reduction
Definition: containing \(R\)
Page: 51, 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Notation: \(\to_R\)
Index: (i)
Definition2: if it contains \((M,N)\) it contains \((ZM,ZN)\)
Definition3: if it contains \((M,N)\) it contains \((MZ,NZ)\)
Intuition: \((C[P], C[Q]\) for \((P,Q)\in\mathbf R\)
Definition4: if it contains \((M,N)\) it contains \((\lambda x. M,\lambda x. N)\)
Typ: compatible
DefType: The binary function

Name: \(R\)-reduction
Definition: containing \(\to_R\)
Page: 51
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Notation: \(\twoheadrightarrow_R\)
Index: (i)
Definition2: containing identity
Definition3: transitive
Typ: compatible
DefType: The binary function

Name: \(R\)-equality
Definition: containing \(\twoheadrightarrow_R\)
Page: 51
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Notation: \(=_R\)
Index: (i)
Definition2: closed under transitivity and reflexivity
Name2: \(R\)-convertibility
Typ: compatible
DefType: The binary function

Smaller0: \(N\twoheadrightarrow_RN'\)
Greater0: \(M[N]\twoheadrightarrow_RM[N']\)
Page: 51
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)
Counterexample: \(M=(\lambda x.y)\), and arbitrary \(N,N'\)

Name: An \(\mathbf R\)-contractum of \(M\)
Definition: A term \(N\) such that \((M,N)\in \mathbf R\)
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)

Name: A term in \(\mathbf R\)-normal form
Definition: A term without \(\mathbf R\)-redex
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)

Name: An \(\mathbf R\)-normal form of \(M\)
Definition: A term in \(\mathbf R\)-nf such that \(M=_RN\)
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)

Name: Contraction
Definition: Stepiing from a redex to a contractum
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)

Name: A redex of \(M\)
Definition: A term \(N\) such that \((N,M)\in\mathbf R\)
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)

Name: A \(\mathbf R\)-redex
Definition: A term which has a \(\mathbf R\)-contractum
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)

Name: A \(\mathbf R\)-contractum
Definition: A term which has a \(\mathbf R\)-redex
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Index: (i)

Question: \(M\twoheadrightarrow_RN\) and \(M\) is a \(\mathbb R\)-nf
Answer: \(M\equiv N\)
Page: 53
Chapter: 3
Section: 1.5
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
\(M,N\in\Lambda\)
Index: (i)

Name: \(->\) has the diamond property
Definition: If \(M>-M_1\) and \(M>-M_2\) then there exists \(N\) such that \(M_1>-N\) and \(M_2>-N\)
Page: 53
Chapter: 3
Section: 1.5
Variables: \(>-\) a binary relation on \(\Lambda\)
Index: 11 (1)
Etymology: .

Name: R is said to be Church-Rosser
Definition: \(\twoheadrightarrow_R\) satisfies the diamond property
Page: 53
Chapter: 3
Section: 1.5
Variables: R a notion of reduction
Index: 11 (1)
Example: \(\beta\)
Abbreviation: CR

Smaller0: R is Church-Rosser
Greater0: there exists \(Z\) such that \(M\twoheadrightarrow_RZ\) and \(N\twoheadrightarrow_RZ\)
Page: 54
Chapter: 3
Section: 1.5
Variables: R a notion of reduction
Index: 11 (1)
Smaller1: \(M=_RN\)

Smaller0: R is Church-Rosser
Greater0: \(M\twoheadrightarrow_RN\)
Page: 54
Chapter: 3
Section: 1.5
Variables: R a notion of reduction
Index: 11 (1)
Smaller1: \(N\) is an \(R\)-nf of \(M\)

Smaller0: R is Church-Rosser
Greater0: at most one
Page: 54
Chapter: 3
Section: 1.5
Variables: R a notion of reduction
Index: 11 (1)
Prefix Greater: the number of \(R\)-nf of a term is

Name: A substitutive relation
Definition: A binary relation over \(\Lambda\) such that \((M,N)\in\mathbb R\) implies \((M[x:=L], N[x:=L])\in\mathbb R\)
Page: 54
Chapter: 3
Section: 1.5
Context: lamda calculus
Index: 11 (1)
Example: \(\beta\)

Name: A substitutive relation \(\mathbf R\)
Page: 54
Section: 1.5
Chapter: 3
Index: 11 (1)
Under: \(\to_R\)
Under2: \(\twoheadrightarrow_R\)
Under3: \(=_R\)

Definition: there exists \(C[\ ]\) and \(\Delta,\Delta'\) such that \(M\equiv C[\Delta]\), \(N=C[\Delta']\)
Page: 55
Chapter: 3
Section: 1.5
Notation: \(M\overset{\mbox{\Delta}}{\longrightarrow}_RN\)
Index: 11 (1)
Intuition: The step is done in the subterm \(\Delta\) of \(M\)

Definition: there exists \(C[\ ]\), \(\Delta\) is an \(R\)-redex with contractum \(\Delta'\), and that \(M\equiv C[\Delta]\), \(N=C[\Delta']\)
Page: 55
Chapter: 3
Section: 1.5
Notation: \(M\overset{\mbox{\Delta}}{\longrightarrow}_RN\)
Index: 11 (1)

Name: An \(R\)-reduction (path)
Definition: \(M_0\overset{\mbox{\Delta}}{\longrightarrow}_RM_1\overset{\mbox{\Delta}}{\longrightarrow}_R\dots\) finite or infinite
Page: 55
Chapter: 3
Section: 1.5
Index: 11 (ii)
Denoted by: \(\sigma, \ta\)

Name: An \(R\)-reduction (path) from \(M_0\) to \(M_n\)
Definition: \(M_0\overset{\mbox{\Delta}}{\longrightarrow}_RM_1\overset{\mbox{\Delta}}{\longrightarrow}_R\dots\overset{\mbox{\Delta}}{\longrightarrow}_R M_n\)
Page: 55
Chapter: 3
Section: 1.5
Index: 18 (ii)

Name: An empty reduction
Definition: \(M_0\overset{\mbox{\Delta}}{\longrightarrow}_RM_0\)
Page: 55
Chapter: 3
Section: 1.5
Index: 18 (ii)
Denoted by: \(\emptyset\)

Name: A proper \(R\)-reduction
Definition: \(M_0\underset{\overset{\mbox{\Delta}}{\longrightarrow}}{\mbox{\ne\emptyset}}_RM_n\)
Page: 55
Chapter: 3
Section: 1.5
Index: 18 (ii)

Definition: \(\sigma:M_0\overset{\mbox{\Delta}}{\longrightarrow}_RM_1\overset{\mbox{\Delta}}{\longrightarrow}_R\dots\overset{\mbox{\Delta}}{\longrightarrow}_RM_{n'}\)
Page: 55
Chapter: 3
Section: 1.5
Variables: \(\sigma:M_0\overset{\mbox{\Delta}}{\longrightarrow}_RM_1\overset{\mbox{\Delta}}{\longrightarrow}_R\dots\overset{\mbox{\Delta}}{\longrightarrow}_RM_n\)
 \(\tau:M_n\overset{\mbox{\Delta}}{\longrightarrow}_RM_1\overset{\mbox{\Delta}}{\longrightarrow}_R\dots\overset{\mbox{\Delta}}{\longrightarrow}_RM_{n'}\)
Notation: \(\sigma+\tau\)
Index: 18 (ii)

Name: The length of \(\sigma\)
Definition: \(n\)
Page: 56
Chapter: 3
Section: 1.5
Variables: \(\sigma:M_0\overset{\mbox{\Delta}}{\longrightarrow}_RM_1\overset{\mbox{\Delta}}{\longrightarrow}_R\dots\overset{\mbox{\Delta}}{\longrightarrow}_RM_n\)
Notation: \(||\sigma||\)
Index: 18 (ii)

Name: The \(R\)(reduction) graph of \(M\)
Definition: edges \(\{N\in\Lambda\mid M\overset{\mbox{\Delta}}{\longrightarrow}_RN\}\)
Page: 56
Chapter: 3
Section: 1.5
Variables: \(R\)
\(M\in\Lambda\)
Notation: \(G_R(M)\)
Index: 20
Definition2: edges \(M_0\to_RM_1\) for each potential reduction \(R\)
Example3: \(\dot\to\dot\to\dot\to\dots\)
DefType: The multi-edge digraph with
Applied to: \(G_{\beta}(\Omega)\)
Applied to3: \(G_\beta(\omega_3\omega_3)\) with \(\omega_3=\lambda x.xxx\)
Applied to2: \(G_{\beta}(\mathbf I(\mathbf Ix))\)

Name: \(M\) \(R\)-strongly normalize
Definition: there is no infinite \(R\)-reduction starting with \(M\)
Page: 57
Chapter: 3
Section: 1.5
Variables: \(R\)
\(M\in\Lambda\)
Notation: \(R\)-SN\((M)\)
Index: 22

Name: \(M\) is \(R\)-infinite
Definition: there exists an infinite \(R\)-reduction starting with \(M\)
Page: 57
Chapter: 3
Section: 1.5
Variables: \(R\)
\(M\in\Lambda\)
Notation: \(R-\infty(M)\)
Index: 22

Name: \(R\) is strongly normalizing
Definition: For each \(M\in\Lambda\), \(R\)-SN\((M)\)
Page: 57
Chapter: 3
Section: 1.5
Variables: \(R\)
\(M\in\Lambda\)
Index: 22 (iii)
Abbreviation: SN

Question: Example of \(M\in\Lambda\) with a \(\beta\)-nf, and infinite \(G_\beta(M)\)
Answer: \((\lambda x.y)((\lambda x.xxx)(\lambda x.xxx))\) because the first part delete the second one, which is infinite
Page: 57
Chapter: 3
Section: 1.5
Index: 23

Question: Example of \(M\in\Lambda\) without a \(\beta\)-nf, and finite \(G_\beta(M)\)
Answer: \(\Omega\)
Page: 57
Chapter: 3
Section: 1.5
Index: 23

Smaller0: \(\beta\)-SN(M)
Greater0: \(G_{\beta}(M)\) is finite
Page: 57
Chapter: 3
Section: 1.5
Index: 23(ii)
Greater1: \(M\) has a \(\beta\)-nf
Counterexample: \((\lambda x.\mathbf I)\Omega\) has a \(\beta\)-f, the term \(\mathbf I\) and a finite \(\beta\)-graph . But \(M\) has also an infinite \(\beta\)-reduction (loop around)

Name: \(>-\) satisfies the weak diamond property
Definition: for each \(x>-x_1\), \(x>-x_2\) there exists \(x_3\) such that
Page: 57
Chapter: 3
Section: 1.5
Variables: \(X\) a set
\(>-\in X^2\)
Index: 24

Name: A weakly Church-Rosser reduction
Definition: A reduction that satisfies the weak diamond property
Page: 58
Chapter: 3
Section: 1.5
Index: 24
Abbreviation: WCR

Smaller0: SN
Greater0: CR
Page: 58
Chapter: 3
Section: 1.5
Index: 24
Smaller1: WCR

Definition: The set of lambda terms in R-nf
Page: 58
Chapter: 3
Section: 1
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Notation: R-NF
Index: 26

Definition: The set of \(\Lambda^0\) terms in R-nf
Page: 58
Chapter: 3
Section: 1
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
Notation: R-NF^0
Index: 26

Definition: \(M'=_RM\) for some \(M'\in\mathcal X\)
Page: 58
Chapter: 3
Section: 1
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
\(\mathcal X\subseteq\Lambda\)
\(M\in\Lambda\)
Notation: \(M\in_R\mathcal X\)
Index: 26
Example: \(M\) has a \(\beta\)-nf
Applied to: \(M\in_\beta\beta-NF\)

Name: \(M\) is R-solvable
Definition: There exists \(\vec P\in\Lambda\) such that \(M\vec P=_RI\)
Page: 58
Chapter: 3
Section: 1
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
\(M\in\Lambda^0\)
Index: 27

Name: \(M\) is R-solvable
Definition: Some closed substitution instance of \(M\) is \(R\)-solvable
Page: 58
Chapter: 3
Section: 1
Variables: \(\mathbf R\) a notion of reduction on \(\Lambda\)
\(M\in\Lambda\)
Index: 27

Smaller0: \(M=_\beta N\)
Greater0: \(\lambda\vdash M=N\)
Page: 58
Chapter: 3
Section: 2
Variables: \(M,N\in\Lambda\)
Index: 1
Smaller to greater: iff

Name: Binary relation with the diamond property
Page: 58, 64
Section: 2
Chapter: 3
Under: transitive closure
Under2: union then transitive closure
Condition2: both relation comutes

Definition: containing identity
Page: 60
Chapter: 3
Section: 2
Context: lambda calculus
Definition2: if it contains \(M,M'\) it contains \(\lambda x.M, \lambda x.M'\)
Definition3: if it contains \(M,M'\) and \(N,N?\) it contains \(MN, M'N'\)
Intuition: Executing zero or one step of computation everywhere simultaneously. One step of \(\twoheadrightarrow_\beta\)
Definition4: if it contains \(M,M'\) and \(N,N?\) it contains \((\lambda x.M)N, M'[x:=N']\)
DefType: The binary relation

Question: The transitive closure fo is
Answer: \(\twoheadrightarrow_\beta\)
Page: 60
Chapter: 3
Section: 2
Context: lambda calculus

Definition: The binary relation containing \(((\lambda x. Mx), M)\) for each \(x\not\in\mathtt{FV}(M)\)
Page: 60
Chapter: 3
Section: 2
Context: lambda calculus
Notation: \(\eta\)
Typ: CR, substitutive

Name: CR relation
Page: 64
Section: 2
Chapter: 3
Under: union
Condition: Their \(\twoheadrightarrow\) commutes

Name: A development related to \(\mathcal F\) of \(M\)
Definition: A reduction starting with \(M\) in which only redexes in \(\mathcal F\) and their residuals are contracted
Page: 68
Chapter: 3
Section: 2
Variables: \(M\) a term
\(\mathcal F\) a set of redexes in \(M\)

Question: Properties of developments related to \(\mathcal F\) of \(M\)
Answer: They are all finite
Page: 68
Chapter: 3
Section: 2
Variables: \(M\) a term
\(\mathcal F\) a set of redexes in \(M\)
Answer2: they all end in the same term

Name: An I-redex
Definition: A term \((\lambda x.M)N\) with \(x\in\mathtt{FV}(M)\)
Page: 68
Chapter: 3
Section: 2

Smaller0: \(\Delta\) is an I-redex
Greater0: \(\infty(M)\implies \infty(N)\)
Page: 68
Chapter: 3
Section: 2
Variables: \(M,N\in\Lambda\)

Name: A standard reduction
Definition: A reduction where all contractions proceed from left to right.
Page: 68
Chapter: 3
Section: 11.4
Name2: Call by name (in programming language)

Smaller0: \(M\twoheadrightarrow N\)
Greater0: there exists a standard reduction from \(M\) to \(N\)
Page: 68
Chapter: 3
Section: 11.4
Variables: \(M,N\in\Lambda\)
Smaller to greater: iff

Smaller0: chapter 12 and forward as section of chapter 3
Greater0: todo
Page: 68
Chapter: 3
Section: 11.4
Variables: \(M,N\in\Lambda\)
Smaller to greater: iff

Name: A theory
Definition: Consistent extensions of the \(\lambda\)-calculus that are closed under derivations. I.e. \(\mathcal T^+=\mathcal T\)
Page: 76
Chapter: 4
Section: 1
Index: 3
Denoted by: \(\mathcal T\)

Definition: The set of closed equations provable in \(\lambda+\mathcal T\)
Page: 76
Chapter: 4
Section: 1
Variables: \(\mathcal T\) a set of closed equations
Notation: \(\mathcal T^+\)
Index: 3